Documentation

Mathlib.Data.Real.Archimedean

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

instance Real.instArchimedean :

Archimedean ℝ

@[implicit_reducible]

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), 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 :

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)

@[implicit_reducible]

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.isGLB_sInf {s : Set ℝ} (h₁ : s.Nonempty) (h₂ : BddBelow s) :

IsGLB s (sInf s)

@[implicit_reducible]

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 ℝ} {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 :

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 :

@[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) :

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) :

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) :

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) :

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) :

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) :

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) :

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) :

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) :

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