Documentation

Mathlib.Data.Real.Archimedean

The real numbers are an Archimedean floor ring, and a conditionally complete linear order. #

instance Real.instArchimedean :

Archimedean ℝ

Equations

Real.instArchimedean = ⋯

noncomputable instance Real.instFloorRing :

Equations

Real.instFloorRing = Archimedean.floorRing ℝ

theorem Real.isCauSeq_iff_lift {f : ℕ → ℚ} :

IsCauSeq abs f ↔ IsCauSeq abs fun (i : ℕ) => ↑(f i)

theorem Real.of_near (f : ℕ → ℚ) (x : ℝ) (h : ∀ ε > 0, ∃ (i : ℕ), ∀ j ≥ i, |↑(f j) - x| < ε) :

∃ (h' : IsCauSeq abs f), Real.mk ⟨f, h'⟩ = x

theorem Real.exists_floor (x : ℝ) :

∃ (ub : ℤ), ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub

theorem Real.exists_isLUB {S : Set ℝ} (hne : S.Nonempty) (hbdd : BddAbove S) :

∃ (x : ℝ), IsLUB S x

theorem Real.exists_isGLB {S : Set ℝ} (hne : S.Nonempty) (hbdd : BddBelow S) :

∃ (x : ℝ), IsGLB S x

A nonempty, bounded below set of real numbers has a greatest lower bound.

noncomputable instance Real.instSupSet :

Equations

Real.instSupSet = { sSup := fun (S : Set ℝ) => if h : S.Nonempty ∧ BddAbove S then Classical.choose ⋯ else 0 }

theorem Real.sSup_def (S : Set ℝ) :

sSup S = if h : S.Nonempty ∧ BddAbove S then Classical.choose ⋯ else 0

theorem Real.isLUB_sSup (S : Set ℝ) (h₁ : S.Nonempty) (h₂ : BddAbove S) :

IsLUB S (sSup S)

noncomputable instance Real.instInfSet :

Equations

Real.instInfSet = { sInf := fun (S : Set ℝ) => -sSup (-S) }

theorem Real.sInf_def (S : Set ℝ) :

sInf S = -sSup (-S)

theorem Real.is_glb_sInf (S : Set ℝ) (h₁ : S.Nonempty) (h₂ : BddBelow S) :

IsGLB S (sInf S)

noncomputable instance Real.instConditionallyCompleteLinearOrder :

ConditionallyCompleteLinearOrder ℝ

Equations

One or more equations did not get rendered due to their size.

theorem Real.lt_sInf_add_pos {s : Set ℝ} (h : s.Nonempty) {ε : ℝ} (hε : 0 < ε) :

∃ a ∈ s, a < sInf s + ε

theorem Real.add_neg_lt_sSup {s : Set ℝ} (h : s.Nonempty) {ε : ℝ} (hε : ε < 0) :

∃ a ∈ s, sSup s + ε < a

theorem Real.sInf_le_iff {s : Set ℝ} (h : BddBelow s) (h' : s.Nonempty) {a : ℝ} :

sInf s ≤ a ↔ ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε

theorem Real.le_sSup_iff {s : Set ℝ} (h : BddAbove s) (h' : s.Nonempty) {a : ℝ} :

a ≤ sSup s ↔ ∀ ε < 0, ∃ x ∈ s, a + ε < x

@[simp]

theorem Real.sSup_empty :

@[simp]

theorem Real.iSup_of_isEmpty {α : Sort u_1} [IsEmpty α] (f : α → ℝ) :

⨆ (i : α), f i = 0

@[simp]

theorem Real.ciSup_const_zero {α : Sort u_1} :

⨆ (x : α), 0 = 0

theorem Real.sSup_of_not_bddAbove {s : Set ℝ} (hs : ¬BddAbove s) :

sSup s = 0

theorem Real.iSup_of_not_bddAbove {α : Sort u_1} {f : α → ℝ} (hf : ¬BddAbove (Set.range f)) :

⨆ (i : α), f i = 0

theorem Real.sSup_univ :

sSup Set.univ = 0

@[simp]

theorem Real.sInf_empty :

@[simp]

theorem Real.iInf_of_isEmpty {α : Sort u_1} [IsEmpty α] (f : α → ℝ) :

⨅ (i : α), f i = 0

@[simp]

theorem Real.ciInf_const_zero {α : Sort u_1} :

⨅ (x : α), 0 = 0

theorem Real.sInf_of_not_bddBelow {s : Set ℝ} (hs : ¬BddBelow s) :

sInf s = 0

theorem Real.iInf_of_not_bddBelow {α : Sort u_1} {f : α → ℝ} (hf : ¬BddBelow (Set.range f)) :

⨅ (i : α), f i = 0

theorem Real.sSup_nonneg (S : Set ℝ) (hS : ∀ x ∈ S, 0 ≤ x) :

As 0 is the default value for Real.sSup of the empty set or sets which are not bounded above, it suffices to show that S is bounded below by 0 to show that 0 ≤ sSup S.

theorem Real.iSup_nonneg {ι : Sort u_1} {f : ι → ℝ} (hf : ∀ (i : ι), 0 ≤ f i) :

0 ≤ ⨆ (i : ι), f i

As 0 is the default value for Real.sSup of the empty set or sets which are not bounded above, it suffices to show that f i is nonnegative to show that 0 ≤ ⨆ i, f i.

theorem Real.sSup_le {S : Set ℝ} {a : ℝ} (hS : ∀ x ∈ S, x ≤ a) (ha : 0 ≤ a) :

As 0 is the default value for Real.sSup of the empty set or sets which are not bounded above, it suffices to show that all elements of S are bounded by a nonnegative number to show that sSup S is bounded by this number.

theorem Real.iSup_le {ι : Sort u_1} {f : ι → ℝ} {a : ℝ} (hS : ∀ (i : ι), f i ≤ a) (ha : 0 ≤ a) :

⨆ (i : ι), f i ≤ a

theorem Real.sSup_nonpos (S : Set ℝ) (hS : ∀ x ∈ S, x ≤ 0) :

As 0 is the default value for Real.sSup of the empty set, it suffices to show that S is bounded above by 0 to show that sSup S ≤ 0.

theorem Real.sInf_nonneg (S : Set ℝ) (hS : ∀ x ∈ S, 0 ≤ x) :

As 0 is the default value for Real.sInf of the empty set, it suffices to show that S is bounded below by 0 to show that 0 ≤ sInf S.

theorem Real.iInf_nonneg {ι : Sort u_1} {f : ι → ℝ} (hf : ∀ (i : ι), 0 ≤ f i) :

As 0 is the default value for Real.sInf of the empty set, it suffices to show that f i is bounded below by 0 to show that 0 ≤ iInf f.

theorem Real.sInf_nonpos (S : Set ℝ) (hS : ∀ x ∈ S, x ≤ 0) :

As 0 is the default value for Real.sInf of the empty set or sets which are not bounded below, it suffices to show that S is bounded above by 0 to show that sInf S ≤ 0.

theorem Real.sInf_le_sSup (s : Set ℝ) (h₁ : BddBelow s) (h₂ : BddAbove s) :

sInf s ≤ sSup s

theorem Real.cauSeq_converges (f : CauSeq ℝ abs) :

∃ (x : ℝ), f ≈ CauSeq.const abs x

instance Real.instIsCompleteAbs :

CauSeq.IsComplete ℝ abs

Equations

Real.instIsCompleteAbs = ⋯

theorem Real.iInf_Ioi_eq_iInf_rat_gt {f : ℝ → ℝ} (x : ℝ) (hf : BddBelow (f '' Set.Ioi x)) (hf_mono : Monotone f) :

⨅ (r : ↑(Set.Ioi x)), f ↑r = ⨅ (q : { q' : ℚ // x < ↑q' }), f ↑↑q

theorem Real.not_bddAbove_coe :

¬BddAbove (Set.range fun (x : ℚ) => ↑x)

theorem Real.not_bddBelow_coe :

¬BddBelow (Set.range fun (x : ℚ) => ↑x)

theorem Real.iUnion_Iic_rat :

⋃ (r : ℚ), Set.Iic ↑r = Set.univ

theorem Real.iInter_Iic_rat :

⋂ (r : ℚ), Set.Iic ↑r = ∅