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

Equations
noncomputable instance Real.instFloorRing :
Equations
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 : } (hne : S.Nonempty) (hbdd : ) :
∃ (x : ), IsLUB S x
theorem Real.exists_isGLB {S : } (hne : S.Nonempty) (hbdd : ) :
∃ (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 : ) :
sSup S = if h : S.Nonempty then else 0
theorem Real.isLUB_sSup (S : ) (h₁ : S.Nonempty) (h₂ : ) :
IsLUB S (sSup S)
noncomputable instance Real.instInfSet :
Equations
theorem Real.sInf_def (S : ) :
sInf S = -sSup (-S)
theorem Real.is_glb_sInf (S : ) (h₁ : S.Nonempty) (h₂ : ) :
IsGLB S (sInf S)
Equations
• One or more equations did not get rendered due to their size.
theorem Real.lt_sInf_add_pos {s : } (h : s.Nonempty) {ε : } (hε : 0 < ε) :
as, a < sInf s + ε
theorem Real.add_neg_lt_sSup {s : } (h : s.Nonempty) {ε : } (hε : ε < 0) :
as, sSup s + ε < a
theorem Real.sInf_le_iff {s : } (h : ) (h' : s.Nonempty) {a : } :
sInf s a ∀ (ε : ), 0 < εxs, x < a + ε
theorem Real.le_sSup_iff {s : } (h : ) (h' : s.Nonempty) {a : } :
a sSup s ε < 0, xs, a + ε < x
@[simp]
theorem Real.sSup_empty :
= 0
@[simp]
theorem Real.iSup_of_isEmpty {α : Sort u_1} [] (f : α) :
⨆ (i : α), f i = 0
@[simp]
theorem Real.ciSup_const_zero {α : Sort u_1} :
⨆ (x : α), 0 = 0
theorem Real.sSup_of_not_bddAbove {s : } (hs : ) :
sSup s = 0
theorem Real.iSup_of_not_bddAbove {α : Sort u_1} {f : α} (hf : ¬) :
⨆ (i : α), f i = 0
theorem Real.sSup_univ :
sSup Set.univ = 0
@[simp]
theorem Real.sInf_empty :
= 0
@[simp]
theorem Real.iInf_of_isEmpty {α : Sort u_1} [] (f : α) :
⨅ (i : α), f i = 0
@[simp]
theorem Real.ciInf_const_zero {α : Sort u_1} :
⨅ (x : α), 0 = 0
theorem Real.sInf_of_not_bddBelow {s : } (hs : ) :
sInf s = 0
theorem Real.iInf_of_not_bddBelow {α : Sort u_1} {f : α} (hf : ¬) :
⨅ (i : α), f i = 0
theorem Real.sSup_nonneg (S : ) (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 : } {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 : ) (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 : ) (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 : ) (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 : ) (h₁ : ) (h₂ : ) :
theorem Real.cauSeq_converges (f : CauSeq abs) :
∃ (x : ), f CauSeq.const abs x
Equations
theorem Real.iInf_Ioi_eq_iInf_rat_gt {f : } (x : ) (hf : BddBelow (f '' )) (hf_mono : ) :
⨅ (r : ()), 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 =