Real numbers from Cauchy sequences

This file defines ℝ as the type of equivalence classes of Cauchy sequences of rational numbers. This choice is motivated by how easy it is to prove that ℝ is a commutative ring, by simply lifting everything to ℚ.

structure Real : Type

• ofCauchy :: (
• cauchy : CauSeq.Completion.Cauchy abs

  The underlying Cauchy completion

• )

The type ℝ of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.

def termℝ : Lean.ParserDescr

The type ℝ of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.

Equations

• termℝ = Lean.ParserDescr.node `termℝ 1024 (Lean.ParserDescr.symbol "ℝ")

@[simp]

theorem CauSeq.Completion.ofRat_rat {abv : ℚ → ℚ} [IsAbsoluteValue abv] (q : ℚ) : CauSeq.Completion.ofRat q = ↑q

theorem Real.ext_cauchy_iff {x : ℝ} {y : ℝ} : x = y ↔ x.cauchy = y.cauchy

theorem Real.ext_cauchy {x : ℝ} {y : ℝ} : x.cauchy = y.cauchy → x = y

def Real.equivCauchy : ℝ ≃ CauSeq.Completion.Cauchy abs

The real numbers are isomorphic to the quotient of Cauchy sequences on the rationals.

Equations

• Real.equivCauchy = { toFun := Real.cauchy, invFun := Real.ofCauchy, left_inv := Real.equivCauchy.proof_1, right_inv := Real.equivCauchy.proof_2 }

instance Real.instZeroReal : Zero ℝ

Equations

• Real.instZeroReal = { zero := Real.zero }

instance Real.instOneReal : One ℝ

Equations

• Real.instOneReal = { one := Real.one }

instance Real.instAddReal : Add ℝ

Equations

• Real.instAddReal = { add := Real.add }

instance Real.instNegReal : Neg ℝ

Equations

• Real.instNegReal = { neg := Real.neg }

instance Real.instMulReal : Mul ℝ

Equations

• Real.instMulReal = { mul := Real.mul }

instance Real.instSubReal : Sub ℝ

Equations

• Real.instSubReal = { sub := fun a b => a + -b }

noncomputable instance Real.instInvReal : Inv ℝ

Equations

• Real.instInvReal = { inv := Real.inv' }

theorem Real.ofCauchy_zero : { cauchy := 0 } = 0

theorem Real.ofCauchy_one : { cauchy := 1 } = 1

theorem Real.ofCauchy_add (a : CauSeq.Completion.Cauchy abs) (b : CauSeq.Completion.Cauchy abs) : { cauchy := a + b } = { cauchy := a } + { cauchy := b }

theorem Real.ofCauchy_neg (a : CauSeq.Completion.Cauchy abs) : { cauchy := -a } = -{ cauchy := a }

theorem Real.ofCauchy_sub (a : CauSeq.Completion.Cauchy abs) (b : CauSeq.Completion.Cauchy abs) : { cauchy := a - b } = { cauchy := a } - { cauchy := b }

theorem Real.ofCauchy_mul (a : CauSeq.Completion.Cauchy abs) (b : CauSeq.Completion.Cauchy abs) : { cauchy := a * b } = { cauchy := a } * { cauchy := b }

theorem Real.ofCauchy_inv {f : CauSeq.Completion.Cauchy abs} : { cauchy := f⁻¹ } = { cauchy := f }⁻¹

theorem Real.cauchy_zero : 0.cauchy = 0

theorem Real.cauchy_one : 1.cauchy = 1

theorem Real.cauchy_add (a : ℝ) (b : ℝ) : (a + b).cauchy = a.cauchy + b.cauchy

theorem Real.cauchy_neg (a : ℝ) : (-a).cauchy = -a.cauchy

theorem Real.cauchy_mul (a : ℝ) (b : ℝ) : (a * b).cauchy = a.cauchy * b.cauchy

theorem Real.cauchy_sub (a : ℝ) (b : ℝ) : (a - b).cauchy = a.cauchy - b.cauchy

theorem Real.cauchy_inv (f : ℝ) : f⁻¹.cauchy = f.cauchy⁻¹

instance Real.natCast : NatCast ℝ

Equations

• Real.natCast = { natCast := fun n => { cauchy := ↑n } }

instance Real.intCast : IntCast ℝ

Equations

• Real.intCast = { intCast := fun z => { cauchy := ↑z } }

instance Real.ratCast : RatCast ℝ

Equations

• Real.ratCast = { ratCast := fun q => { cauchy := ↑q } }

theorem Real.ofCauchy_natCast (n : ℕ) : { cauchy := ↑n } = ↑n

theorem Real.ofCauchy_intCast (z : ℤ) : { cauchy := ↑z } = ↑z

theorem Real.ofCauchy_ratCast (q : ℚ) : { cauchy := ↑q } = ↑q

theorem Real.cauchy_natCast (n : ℕ) : (↑n).cauchy = ↑n

theorem Real.cauchy_intCast (z : ℤ) : (↑z).cauchy = ↑z

theorem Real.cauchy_ratCast (q : ℚ) : (↑q).cauchy = ↑q

instance Real.commRing : CommRing ℝ

Equations

• Real.commRing = CommRing.mk Real.commRing.proof_25

@[simp]

theorem Real.ringEquivCauchy_symm_apply_cauchy (cauchy : CauSeq.Completion.Cauchy abs) : (↑(RingEquiv.symm Real.ringEquivCauchy) cauchy).cauchy = cauchy

@[simp]

theorem Real.ringEquivCauchy_apply (self : ℝ) : ↑Real.ringEquivCauchy self = self.cauchy

def Real.ringEquivCauchy : ℝ ≃+* CauSeq.Completion.Cauchy abs

Real.equivCauchy as a ring equivalence.

Equations

• One or more equations did not get rendered due to their size.

Extra instances to short-circuit type class resolution.

These short-circuits have an additional property of ensuring that a computable path is found; if Field ℝ is found first, then decaying it to these typeclasses would result in a noncomputable version of them.

instance Real.instRingReal : Ring ℝ

Equations

• Real.instRingReal = inferInstance

instance Real.instCommSemiringReal : CommSemiring ℝ

Equations

• Real.instCommSemiringReal = inferInstance

instance Real.semiring : Semiring ℝ

Equations

• Real.semiring = inferInstance

instance Real.instCommMonoidWithZeroReal : CommMonoidWithZero ℝ

Equations

• Real.instCommMonoidWithZeroReal = inferInstance

instance Real.instMonoidWithZeroReal : MonoidWithZero ℝ

Equations

• Real.instMonoidWithZeroReal = inferInstance

instance Real.instAddCommGroupReal : AddCommGroup ℝ

Equations

• Real.instAddCommGroupReal = inferInstance

instance Real.instAddGroupReal : AddGroup ℝ

Equations

• Real.instAddGroupReal = inferInstance

instance Real.instAddCommMonoidReal : AddCommMonoid ℝ

Equations

• Real.instAddCommMonoidReal = inferInstance

instance Real.instAddMonoidReal : AddMonoid ℝ

Equations

• Real.instAddMonoidReal = inferInstance

instance Real.instAddLeftCancelSemigroupReal : AddLeftCancelSemigroup ℝ

Equations

• Real.instAddLeftCancelSemigroupReal = inferInstance

instance Real.instAddRightCancelSemigroupReal : AddRightCancelSemigroup ℝ

Equations

• Real.instAddRightCancelSemigroupReal = inferInstance

instance Real.instAddCommSemigroupReal : AddCommSemigroup ℝ

Equations

• Real.instAddCommSemigroupReal = inferInstance

instance Real.instAddSemigroupReal : AddSemigroup ℝ

Equations

• Real.instAddSemigroupReal = inferInstance

instance Real.instCommMonoidReal : CommMonoid ℝ

Equations

• Real.instCommMonoidReal = inferInstance

instance Real.instMonoidReal : Monoid ℝ

Equations

• Real.instMonoidReal = inferInstance

instance Real.instCommSemigroupReal : CommSemigroup ℝ

Equations

• Real.instCommSemigroupReal = inferInstance

instance Real.instSemigroupReal : Semigroup ℝ

Equations

• Real.instSemigroupReal = inferInstance

instance Real.instInhabitedReal : Inhabited ℝ

Equations

• Real.instInhabitedReal = { default := 0 }

instance Real.instStarRingRealToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingInstRingReal : StarRing ℝ

The real numbers are a *-ring, with the trivial *-structure.

Equations

• Real.instStarRingRealToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingInstRingReal = starRingOfComm

instance Real.instTrivialStarRealToStarToInvolutiveStarInstAddMonoidRealToStarAddMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingInstRingRealInstStarRingRealToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingInstRingReal : TrivialStar ℝ

Equations

• One or more equations did not get rendered due to their size.

def Real.mk (x : CauSeq ℚ abs) : ℝ

Make a real number from a Cauchy sequence of rationals (by taking the equivalence class).

Equations

• Real.mk x = { cauchy := CauSeq.Completion.mk x }

theorem Real.mk_eq {f : CauSeq ℚ abs} {g : CauSeq ℚ abs} : Real.mk f = Real.mk g ↔ f ≈ g

instance Real.instLTReal : LT ℝ

Equations

• Real.instLTReal = { lt := Real.lt }

theorem Real.lt_cauchy {f : CauSeq ℚ abs} {g : CauSeq ℚ abs} : { cauchy := Quotient.mk CauSeq.equiv f } < { cauchy := Quotient.mk CauSeq.equiv g } ↔ f < g

@[simp]

theorem Real.mk_lt {f : CauSeq ℚ abs} {g : CauSeq ℚ abs} : Real.mk f < Real.mk g ↔ f < g

theorem Real.mk_zero : Real.mk 0 = 0

theorem Real.mk_one : Real.mk 1 = 1

theorem Real.mk_add {f : CauSeq ℚ abs} {g : CauSeq ℚ abs} : Real.mk (f + g) = Real.mk f + Real.mk g

theorem Real.mk_mul {f : CauSeq ℚ abs} {g : CauSeq ℚ abs} : Real.mk (f * g) = Real.mk f * Real.mk g

theorem Real.mk_neg {f : CauSeq ℚ abs} : Real.mk (-f) = -Real.mk f

@[simp]

theorem Real.mk_pos {f : CauSeq ℚ abs} : 0 < Real.mk f ↔ CauSeq.Pos f

instance Real.instLEReal : LE ℝ

Equations

• Real.instLEReal = { le := Real.le }

@[simp]

theorem Real.mk_le {f : CauSeq ℚ abs} {g : CauSeq ℚ abs} : Real.mk f ≤ Real.mk g ↔ f ≤ g

theorem Real.ind_mk {C : ℝ → Prop} (x : ℝ) (h : ∀ (y : CauSeq ℚ abs), C (Real.mk y)) : C x

theorem Real.add_lt_add_iff_left {a : ℝ} {b : ℝ} (c : ℝ) : c + a < c + b ↔ a < b

instance Real.partialOrder : PartialOrder ℝ

Equations

• Real.partialOrder = PartialOrder.mk Real.partialOrder.proof_4

instance Real.instPreorderReal : Preorder ℝ

Equations

• Real.instPreorderReal = inferInstance

theorem Real.ratCast_lt {x : ℚ} {y : ℚ} : ↑x < ↑y ↔ x < y

theorem Real.zero_lt_one : 0 < 1

theorem Real.fact_zero_lt_one : Fact (0 < 1)

theorem Real.mul_pos {a : ℝ} {b : ℝ} : 0 < a → 0 < b → 0 < a * b

instance Real.instStrictOrderedCommRingReal : StrictOrderedCommRing ℝ

Equations

• Real.instStrictOrderedCommRingReal = let src := Real.commRing; let src_1 := Real.partialOrder; let src_2 := Real.semiring; StrictOrderedCommRing.mk (_ : ∀ (a b : ℝ), a * b = b * a)

instance Real.strictOrderedRing : StrictOrderedRing ℝ

Equations

• Real.strictOrderedRing = inferInstance

instance Real.strictOrderedCommSemiring : StrictOrderedCommSemiring ℝ

Equations

• Real.strictOrderedCommSemiring = inferInstance

instance Real.strictOrderedSemiring : StrictOrderedSemiring ℝ

Equations

• Real.strictOrderedSemiring = inferInstance

instance Real.orderedRing : OrderedRing ℝ

Equations

• Real.orderedRing = inferInstance

instance Real.orderedSemiring : OrderedSemiring ℝ

Equations

• Real.orderedSemiring = inferInstance

instance Real.orderedAddCommGroup : OrderedAddCommGroup ℝ

Equations

• Real.orderedAddCommGroup = inferInstance

instance Real.orderedCancelAddCommMonoid : OrderedCancelAddCommMonoid ℝ

Equations

• Real.orderedCancelAddCommMonoid = inferInstance

instance Real.orderedAddCommMonoid : OrderedAddCommMonoid ℝ

Equations

• Real.orderedAddCommMonoid = inferInstance

instance Real.nontrivial : Nontrivial ℝ

Equations

• Real.nontrivial = Real.nontrivial.proof_1

instance Real.instSupReal : Sup ℝ

Equations

• Real.instSupReal = { sup := Real.sup }

theorem Real.ofCauchy_sup (a : CauSeq ℚ abs) (b : CauSeq ℚ abs) : { cauchy := Quotient.mk CauSeq.equiv (a ⊔ b) } = { cauchy := Quotient.mk CauSeq.equiv a } ⊔ { cauchy := Quotient.mk CauSeq.equiv b }

@[simp]

theorem Real.mk_sup (a : CauSeq ℚ abs) (b : CauSeq ℚ abs) : Real.mk (a ⊔ b) = Real.mk a ⊔ Real.mk b

instance Real.instInfReal : Inf ℝ

Equations

• Real.instInfReal = { inf := Real.inf }

theorem Real.ofCauchy_inf (a : CauSeq ℚ abs) (b : CauSeq ℚ abs) : { cauchy := Quotient.mk CauSeq.equiv (a ⊓ b) } = { cauchy := Quotient.mk CauSeq.equiv a } ⊓ { cauchy := Quotient.mk CauSeq.equiv b }

@[simp]

theorem Real.mk_inf (a : CauSeq ℚ abs) (b : CauSeq ℚ abs) : Real.mk (a ⊓ b) = Real.mk a ⊓ Real.mk b

instance Real.instDistribLatticeReal : DistribLattice ℝ

Equations

• Real.instDistribLatticeReal = let src := Real.partialOrder; DistribLattice.mk Real.instDistribLatticeReal.proof_10

instance Real.lattice : Lattice ℝ

Equations

• Real.lattice = inferInstance

instance Real.instSemilatticeInfReal : SemilatticeInf ℝ

Equations

• Real.instSemilatticeInfReal = inferInstance

instance Real.instSemilatticeSupReal : SemilatticeSup ℝ

Equations

• Real.instSemilatticeSupReal = inferInstance

instance Real.instIsTotalRealLeInstLEReal : IsTotal ℝ fun x x_1 => x ≤ x_1

Equations

• Real.instIsTotalRealLeInstLEReal = Real.instIsTotalRealLeInstLEReal.proof_1

noncomputable instance Real.linearOrder : LinearOrder ℝ

Equations

• Real.linearOrder = Lattice.toLinearOrder ℝ

noncomputable instance Real.linearOrderedCommRing : LinearOrderedCommRing ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Real.instLinearOrderedRingReal : LinearOrderedRing ℝ

Equations

• Real.instLinearOrderedRingReal = inferInstance

noncomputable instance Real.instLinearOrderedSemiringReal : LinearOrderedSemiring ℝ

Equations

• Real.instLinearOrderedSemiringReal = inferInstance

instance Real.instIsDomainRealSemiring : IsDomain ℝ

Equations

• Real.instIsDomainRealSemiring = Real.instIsDomainRealSemiring.proof_1

noncomputable instance Real.instLinearOrderedFieldReal : LinearOrderedField ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Real.instLinearOrderedAddCommGroupReal : LinearOrderedAddCommGroup ℝ

Equations

• Real.instLinearOrderedAddCommGroupReal = inferInstance

noncomputable instance Real.field : Field ℝ

Equations

• Real.field = inferInstance

noncomputable instance Real.instDivisionRingReal : DivisionRing ℝ

Equations

• Real.instDivisionRingReal = inferInstance

noncomputable instance Real.decidableLT (a : ℝ) (b : ℝ) : Decidable (a < b)

Equations

• Real.decidableLT a b = inferInstance

noncomputable instance Real.decidableLE (a : ℝ) (b : ℝ) : Decidable (a ≤ b)

Equations

• Real.decidableLE a b = inferInstance

noncomputable instance Real.decidableEq (a : ℝ) (b : ℝ) : Decidable (a = b)

Equations

• Real.decidableEq a b = inferInstance

unsafe instance Real.instReprReal : Repr ℝ

Show an underlying cauchy sequence for real numbers.

The representative chosen is the one passed in the VM to Quot.mk, so two cauchy sequences converging to the same number may be printed differently.

Equations

• Real.instReprReal = { reprPrec := fun r x => Std.Format.text "Real.ofCauchy " ++ repr r.cauchy }

theorem Real.le_mk_of_forall_le {x : ℝ} {f : CauSeq ℚ abs} : (∃ i, ∀ (j : ℕ), j ≥ i → x ≤ ↑(↑f j)) → x ≤ Real.mk f

theorem Real.mk_le_of_forall_le {f : CauSeq ℚ abs} {x : ℝ} (h : ∃ i, ∀ (j : ℕ), j ≥ i → ↑(↑f j) ≤ x) : Real.mk f ≤ x

theorem Real.mk_near_of_forall_near {f : CauSeq ℚ abs} {x : ℝ} {ε : ℝ} (H : ∃ i, ∀ (j : ℕ), j ≥ i → |↑(↑f j) - x| ≤ ε) : |Real.mk f - x| ≤ ε

instance Real.instArchimedean : Archimedean ℝ

Equations

• Real.instArchimedean = Real.instArchimedean.proof_1

noncomputable instance Real.instFloorRingRealInstLinearOrderedRingReal : FloorRing ℝ

Equations

• Real.instFloorRingRealInstLinearOrderedRingReal = 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 : ℕ), j ≥ i → |↑(f j) - x| < ε) : ∃ h', Real.mk { val := f, property := h' } = x

theorem Real.exists_floor (x : ℝ) : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub

theorem Real.exists_isLUB (S : Set ℝ) (hne : Set.Nonempty S) (hbdd : BddAbove S) : ∃ x, IsLUB S x

noncomputable instance Real.instSupSetReal : SupSet ℝ

Equations

• Real.instSupSetReal = { sSup := fun S => if h : Set.Nonempty S ∧ BddAbove S then Classical.choose (_ : ∃ x, IsLUB S x) else 0 }

theorem Real.sSup_def (S : Set ℝ) : sSup S = if h : Set.Nonempty S ∧ BddAbove S then Classical.choose (_ : ∃ x, IsLUB S x) else 0

theorem Real.isLUB_sSup (S : Set ℝ) (h₁ : Set.Nonempty S) (h₂ : BddAbove S) : IsLUB S (sSup S)

noncomputable instance Real.instInfSetReal : InfSet ℝ

Equations

• Real.instInfSetReal = { sInf := fun S => -sSup (-S) }

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

theorem Real.is_glb_sInf (S : Set ℝ) (h₁ : Set.Nonempty S) (h₂ : BddBelow S) : IsGLB S (sInf S)

noncomputable instance Real.instConditionallyCompleteLinearOrderReal : ConditionallyCompleteLinearOrder ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem Real.lt_sInf_add_pos {s : Set ℝ} (h : Set.Nonempty s) {ε : ℝ} (hε : 0 < ε) : ∃ a, a ∈ s ∧ a < sInf s + ε

theorem Real.add_neg_lt_sSup {s : Set ℝ} (h : Set.Nonempty s) {ε : ℝ} (hε : ε < 0) : ∃ a, a ∈ s ∧ sSup s + ε < a

theorem Real.sInf_le_iff {s : Set ℝ} (h : BddBelow s) (h' : Set.Nonempty s) {a : ℝ} : sInf s ≤ a ↔ ∀ (ε : ℝ), 0 < ε → ∃ x, x ∈ s ∧ x < a + ε

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

@[simp]

theorem Real.sSup_empty : sSup ∅ = 0

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

@[simp]

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

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

@[simp]

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

theorem Real.sSup_nonneg (S : Set ℝ) (hS : ∀ (x : ℝ), x ∈ S → 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 : ∀ (x : ℝ), x ∈ S → 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 : ∀ (x : ℝ), x ∈ S → 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 : ∀ (x : ℝ), x ∈ S → 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 : ∀ (x : ℝ), x ∈ S → 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) : sInf s ≤ sSup s

theorem Real.cauSeq_converges (f : CauSeq ℝ abs) : ∃ x, f ≈ CauSeq.const abs x

instance Real.instIsCompleteRealInstLinearOrderedFieldRealInstRingRealAbsToHasAbsInstNegRealInstSupRealAbs_isAbsoluteValueInstLinearOrderedRingReal : CauSeq.IsComplete ℝ abs

Equations

• One or more equations did not get rendered due to their size.

theorem Real.iInf_Ioi_eq_iInf_rat_gt {f : ℝ → ℝ} (x : ℝ) (hf : BddBelow (f '' Set.Ioi x)) (hf_mono : Monotone f) : ⨅ r, f ↑r = ⨅ q, f ↑↑q