Documentation

Mathlib.Data.Real.Archimedean

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

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), 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.isGLB_sInf {s : Set } (h₁ : s.Nonempty) (h₂ : BddBelow s) :
        IsGLB s (sInf s)
        theorem Real.lt_sInf_add_pos {s : Set } (h : s.Nonempty) {ε : } ( : 0 < ε) :
        as, a < sInf s + ε
        theorem Real.add_neg_lt_sSup {s : Set } (h : s.Nonempty) {ε : } ( : ε < 0) :
        as, sSup s + ε < a
        theorem Real.sInf_le_iff {s : Set } {a : } (h : BddBelow s) (h' : s.Nonempty) :
        sInf s a ∀ (ε : ), 0 < εxs, x < a + ε
        theorem Real.le_sSup_iff {s : Set } {a : } (h : BddAbove s) (h' : s.Nonempty) :
        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.iSup_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
        @[simp]
        @[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.iInf_of_not_bddBelow {ι : Sort u_1} {f : ι} (hf : ¬BddBelow (Set.range f)) :
        ⨅ (i : ι), f i = 0
        theorem Real.sSup_le {s : Set } {a : } (hs : xs, 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 : xs, 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 : xs, 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 : xs, 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 : xs, 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 : xs, 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 : xs, 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.sInf_nonpos {s : Set } (hs : xs, 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) :
        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.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