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

instance Real.instArchimedean : Archimedean ℝ

@[implicit_reducible]

noncomputable instance Real.instFloorRing : 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), mk ⟨f, h'⟩ = x

@[deprecated exists_floor (since := "2026-01-29")]

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.

@[implicit_reducible]

noncomputable instance Real.instSupSet : SupSet ℝ

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)

@[implicit_reducible]

noncomputable instance Real.instInfSet : InfSet ℝ

theorem Real.sInf_def (s : Set ℝ) : sInf s = -sSup (-s)

theorem Real.isGLB_sInf {s : Set ℝ} (h₁ : s.Nonempty) (h₂ : BddBelow s) : IsGLB s (sInf s)

@[implicit_reducible]

noncomputable instance Real.instConditionallyCompleteLinearOrder : ConditionallyCompleteLinearOrder ℝ

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 ℝ} {a : ℝ} (h : BddBelow s) (h' : s.Nonempty) : sInf s ≤ a ↔ ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε

theorem Real.le_sSup_iff {s : Set ℝ} {a : ℝ} (h : BddAbove s) (h' : s.Nonempty) : a ≤ sSup s ↔ ∀ ε < 0, ∃ x ∈ s, a + ε < x

@[simp]

theorem Real.sSup_empty : sSup ∅ = 0

theorem Real.sInf_univ : sInf Set.univ = 0

@[simp]

theorem Real.iSup_of_isEmpty {ι : Sort u_1} [IsEmpty ι] (f : ι → ℝ) : ⨆ (i : ι), f i = 0

@[simp]

theorem Real.iSup_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 : sInf ∅ = 0

@[simp]

theorem Real.iInf_of_isEmpty {ι : Sort u_1} [IsEmpty ι] (f : ι → ℝ) : ⨅ (i : ι), f i = 0

@[simp]

theorem Real.iInf_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

@[simp]

theorem Real.sSup_neg (s : Set ℝ) : sSup (-s) = -sInf s

@[simp]

theorem Real.sInf_neg (s : Set ℝ) : sInf (-s) = -sSup s

theorem Real.sSup_le {s : Set ℝ} {a : ℝ} (hs : ∀ x ∈ s, x ≤ a) (ha : 0 ≤ a) : sSup s ≤ a

As sSup s = 0 when s is an empty set of reals, it suffices to show that all elements of s are at most some nonnegative number a to show that sSup s ≤ a.

See also csSup_le.

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

As ⨆ i, f i = 0 when the domain of the real-valued function f is empty, it suffices to show that all values of f are at most some nonnegative number a to show that ⨆ i, f i ≤ a.

See also ciSup_le.

theorem Real.le_sInf {s : Set ℝ} {a : ℝ} (hs : ∀ x ∈ s, a ≤ x) (ha : a ≤ 0) : a ≤ sInf s

As sInf s = 0 when s is an empty set of reals, it suffices to show that all elements of s are at least some nonpositive number a to show that a ≤ sInf s.

See also le_csInf.

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

As ⨅ i, f i = 0 when the domain of the real-valued function f is empty, it suffices to show that all values of f are at least some nonpositive number a to show that a ≤ ⨅ i, f i.

See also le_ciInf.

theorem Real.sSup_nonpos {s : Set ℝ} (hs : ∀ x ∈ s, x ≤ 0) : sSup s ≤ 0

As sSup s = 0 when s is an empty set of reals, it suffices to show that all elements of s are nonpositive to show that sSup s ≤ 0.

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

As ⨆ i, f i = 0 when the domain of the real-valued function f is empty, it suffices to show that all values of f are nonpositive to show that ⨆ i, f i ≤ 0.

theorem Real.sInf_nonneg {s : Set ℝ} (hs : ∀ x ∈ s, 0 ≤ x) : 0 ≤ sInf s

As sInf s = 0 when s is an empty set of reals, it suffices to show that all elements of s are nonnegative to show that 0 ≤ sInf s.

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

As ⨅ i, f i = 0 when the domain of the real-valued function f is empty, it suffices to show that all values of f are nonnegative to show that 0 ≤ ⨅ i, f i.

theorem Real.sSup_nonneg' {s : Set ℝ} (hs : ∃ x ∈ s, 0 ≤ x) : 0 ≤ sSup s

As sSup s = 0 when s is a set of reals that's unbounded above, it suffices to show that s contains a nonnegative element to show that 0 ≤ sSup s.

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

As ⨆ i, f i = 0 when the real-valued function f is unbounded above, it suffices to show that f takes a nonnegative value to show that 0 ≤ ⨆ i, f i.

theorem Real.sInf_nonpos' {s : Set ℝ} (hs : ∃ x ∈ s, x ≤ 0) : sInf s ≤ 0

As sInf s = 0 when s is a set of reals that's unbounded below, it suffices to show that s contains a nonpositive element to show that sInf s ≤ 0.

theorem Real.iInf_nonpos' {ι : Sort u_1} {f : ι → ℝ} (hf : ∃ (i : ι), f i ≤ 0) : ⨅ (i : ι), f i ≤ 0

As ⨅ i, f i = 0 when the real-valued function f is unbounded below, it suffices to show that f takes a nonpositive value to show that 0 ≤ ⨅ i, f i.

theorem Real.sSup_nonneg {s : Set ℝ} (hs : ∀ x ∈ s, 0 ≤ x) : 0 ≤ sSup s

As sSup s = 0 when s is a set of reals that's either empty or unbounded above, it suffices to show that all elements of s are nonnegative to show that 0 ≤ sSup s.

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

As ⨆ i, f i = 0 when the domain of the real-valued function f is empty or unbounded above, it suffices to show that all values of f are nonnegative to show that 0 ≤ ⨆ i, f i.

theorem Real.iSup_nonneg_of_nonnegHomClass {ι : Type u_2} {F : Type u_3} {α : Type u_4} [FunLike F α ℝ] [NonnegHomClass F α ℝ] (f : F) (g : ι → α) : 0 ≤ ⨆ (i : ι), f (g i)

theorem Real.sInf_nonpos {s : Set ℝ} (hs : ∀ x ∈ s, x ≤ 0) : sInf s ≤ 0

As sInf s = 0 when s is a set of reals that's either empty or unbounded below, it suffices to show that all elements of s are nonpositive to show that sInf s ≤ 0.

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

As ⨅ i, f i = 0 when the domain of the real-valued function f is empty or unbounded below, it suffices to show that all values of f are nonpositive to show that 0 ≤ ⨅ i, f i.

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

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 = ∅

theorem Real.exists_natCast_add_one_lt_pow_of_one_lt {a : ℝ} (ha : 1 < a) : ∃ (m : ℕ), ↑m + 1 < a ^ m

Exponentiation is eventually larger than linear growth.

theorem Real.exists_nat_pos_inv_lt {b : ℝ} (hb : 0 < b) : ∃ (n : ℕ), 0 < n ∧ (↑n)⁻¹ < b