Documentation

Mathlib.Data.Real.Archimedean

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

theorem Real.isCauSeq_iff_lift {f : } :
IsCauSeq abs f IsCauSeq abs fun (i : ) => (f i)
theorem Real.of_near (f : ) (x : ) (h : ε > 0, ∃ (i : ), ji, |(f j) - x| < ε) :
∃ (h' : IsCauSeq abs f), Real.mk f, h' = x
theorem Real.exists_floor (x : ) :
∃ (ub : ), ub x ∀ (z : ), z xz 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
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
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)
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 < ε) :
as, a < sInf s + ε
theorem Real.add_neg_lt_sSup {s : Set } (h : s.Nonempty) {ε : } (hε : ε < 0) :
as, sSup s + ε < a
theorem Real.sInf_le_iff {s : Set } (h : BddBelow s) (h' : s.Nonempty) {a : } :
sInf s a ∀ (ε : ), 0 < εxs, x < a + ε
theorem Real.le_sSup_iff {s : Set } (h : BddAbove s) (h' : s.Nonempty) {a : } :
a sSup s ε < 0, xs, a + ε < x
@[simp]
@[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.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]
@[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.iInf_of_not_bddBelow {α : Sort u_1} {f : α} (hf : ¬BddBelow (Set.range f)) :
⨅ (i : α), f i = 0
theorem Real.sSup_nonneg (S : Set ) (hS : xS, 0 x) :
0 sSup S

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 : xS, x a) (ha : 0 a) :
sSup S 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 : xS, x 0) :
sSup S 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 : xS, 0 x) :
0 sInf S

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) :
0 iInf f

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 : xS, x 0) :
sInf S 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) :
theorem Real.cauSeq_converges (f : CauSeq abs) :
∃ (x : ), f CauSeq.const abs x
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.iUnion_Iic_rat :
⋃ (r : ), Set.Iic r = Set.univ
theorem Real.iInter_Iic_rat :
⋂ (r : ), Set.Iic r =