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 ℚ.

ink

structure Real : Type

• ofCauchy :: (

• The underlying Cauchy completion

  cauchy : CauSeq.Completion.Cauchy abs
• )

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

ink

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 "ℝ")

ink

@[simp]

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

ink

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

ink

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

ink

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 }

ink

theorem Real.zero_def : Real.zero = { cauchy := 0 }

ink

theorem Real.one_def : Real.one = { cauchy := 1 }

ink

theorem Real.add_def : ∀ (x x_1 : ℝ), Real.add x x_1 = match x, x_1 with | { cauchy := a }, { cauchy := b } => { cauchy := a + b }

ink

theorem Real.neg_def : ∀ (x : ℝ), Real.neg x = match x with | { cauchy := a } => { cauchy := -a }

ink

theorem Real.mul_def : ∀ (x x_1 : ℝ), Real.mul x x_1 = match x, x_1 with | { cauchy := a }, { cauchy := b } => { cauchy := a * b }

ink

instance Real.instZeroReal : Zero ℝ

Equations

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

ink

instance Real.instOneReal : One ℝ

Equations

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

ink

instance Real.instAddReal : Add ℝ

Equations

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

ink

instance Real.instNegReal : Neg ℝ

Equations

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

ink

instance Real.instMulReal : Mul ℝ

Equations

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

ink

instance Real.instSubReal : Sub ℝ

Equations

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

ink

noncomputable instance Real.instInvReal : Inv ℝ

Equations

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

theorem Real.cauchy_zero : 0.cauchy = 0

ink

theorem Real.cauchy_one : 1.cauchy = 1

ink

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

ink

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

ink

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

ink

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

ink

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

ink

instance Real.natCast : NatCast ℝ

Equations

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

ink

instance Real.intCast : IntCast ℝ

Equations

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

ink

instance Real.ratCast : RatCast ℝ

Equations

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

instance Real.commRing : CommRing ℝ

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

real.equiv_Cauchy 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.

ink

instance Real.instRingReal : Ring ℝ

Equations

• Real.instRingReal = inferInstance

ink

instance Real.instCommSemiringReal : CommSemiring ℝ

Equations

• Real.instCommSemiringReal = inferInstance

ink

instance Real.semiring : Semiring ℝ

Equations

• Real.semiring = inferInstance

ink

instance Real.instCommMonoidWithZeroReal : CommMonoidWithZero ℝ

Equations

• Real.instCommMonoidWithZeroReal = inferInstance

ink

instance Real.instMonoidWithZeroReal : MonoidWithZero ℝ

Equations

• Real.instMonoidWithZeroReal = inferInstance

ink

instance Real.instAddCommGroupReal : AddCommGroup ℝ

Equations

• Real.instAddCommGroupReal = inferInstance

ink

instance Real.instAddGroupReal : AddGroup ℝ

Equations

• Real.instAddGroupReal = inferInstance

ink

instance Real.instAddCommMonoidReal : AddCommMonoid ℝ

Equations

• Real.instAddCommMonoidReal = inferInstance

ink

instance Real.instAddMonoidReal : AddMonoid ℝ

Equations

• Real.instAddMonoidReal = inferInstance

ink

instance Real.instAddLeftCancelSemigroupReal : AddLeftCancelSemigroup ℝ

Equations

• Real.instAddLeftCancelSemigroupReal = inferInstance

ink

instance Real.instAddRightCancelSemigroupReal : AddRightCancelSemigroup ℝ

Equations

• Real.instAddRightCancelSemigroupReal = inferInstance

ink

instance Real.instAddCommSemigroupReal : AddCommSemigroup ℝ

Equations

• Real.instAddCommSemigroupReal = inferInstance

ink

instance Real.instAddSemigroupReal : AddSemigroup ℝ

Equations

• Real.instAddSemigroupReal = inferInstance

ink

instance Real.instCommMonoidReal : CommMonoid ℝ

Equations

• Real.instCommMonoidReal = inferInstance

ink

instance Real.instMonoidReal : Monoid ℝ

Equations

• Real.instMonoidReal = inferInstance

ink

instance Real.instCommSemigroupReal : CommSemigroup ℝ

Equations

• Real.instCommSemigroupReal = inferInstance

ink

instance Real.instSemigroupReal : Semigroup ℝ

Equations

• Real.instSemigroupReal = inferInstance

ink

instance Real.instInhabitedReal : Inhabited ℝ

Equations

• Real.instInhabitedReal = { default := 0 }

ink

instance Real.instStarRingRealToNonUnitalSemiringToNonUnitalRingToNonUnitalCommRingCommRing : StarRing ℝ

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

Equations

• Real.instStarRingRealToNonUnitalSemiringToNonUnitalRingToNonUnitalCommRingCommRing = starRingOfComm

ink

instance Real.instTrivialStarRealToStarToInvolutiveStarInstAddMonoidRealToStarAddMonoidToNonUnitalSemiringToNonUnitalRingToNonUnitalCommRingCommRingInstStarRingRealToNonUnitalSemiringToNonUnitalRingToNonUnitalCommRingCommRing : TrivialStar ℝ

Equations

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

ink

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 }

ink

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

ink

theorem Real.lt_def : ∀ (x x_1 : ℝ), Real.lt x x_1 = match x, x_1 with | { cauchy := x }, { cauchy := y } => Quotient.liftOn₂ x y (fun x x_2 => x < x_2) Real.definition.proof_1✝

ink

instance Real.instLTReal : LT ℝ

Equations

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

ink

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

ink

@[simp]

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

ink

theorem Real.mk_zero : Real.mk 0 = 0

ink

theorem Real.mk_one : Real.mk 1 = 1

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

theorem Real.le_def (x : ℝ) (y : ℝ) : Real.le x y = (x < y ∨ x = y)

ink

instance Real.instLEReal : LE ℝ

Equations

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

ink

@[simp]

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

ink

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

ink

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

ink

instance Real.partialOrder : PartialOrder ℝ

Equations

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

ink

instance Real.instPreorderReal : Preorder ℝ

Equations

• Real.instPreorderReal = inferInstance

ink

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

ink

theorem Real.zero_lt_one : 0 < 1

ink

theorem Real.fact_zero_lt_one : Fact (0 < 1)

ink

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

ink

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)

ink

instance Real.strictOrderedRing : StrictOrderedRing ℝ

Equations

• Real.strictOrderedRing = inferInstance

ink

instance Real.strictOrderedCommSemiring : StrictOrderedCommSemiring ℝ

Equations

• Real.strictOrderedCommSemiring = inferInstance

ink

instance Real.strictOrderedSemiring : StrictOrderedSemiring ℝ

Equations

• Real.strictOrderedSemiring = inferInstance

ink

instance Real.orderedRing : OrderedRing ℝ

Equations

• Real.orderedRing = inferInstance

ink

instance Real.orderedSemiring : OrderedSemiring ℝ

Equations

• Real.orderedSemiring = inferInstance

ink

instance Real.orderedAddCommGroup : OrderedAddCommGroup ℝ

Equations

• Real.orderedAddCommGroup = inferInstance

ink

instance Real.orderedCancelAddCommMonoid : OrderedCancelAddCommMonoid ℝ

Equations

• Real.orderedCancelAddCommMonoid = inferInstance

ink

instance Real.orderedAddCommMonoid : OrderedAddCommMonoid ℝ

Equations

• Real.orderedAddCommMonoid = inferInstance

ink

instance Real.nontrivial : Nontrivial ℝ

Equations

• Real.nontrivial = Real.nontrivial.proof_1

ink

theorem Real.sup_def : ∀ (x x_1 : ℝ), Real.sup x x_1 = match x, x_1 with | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun x x_2 => x ⊔ x_2) Real.definition.proof_2✝ x y }

ink

instance Real.instSupReal : Sup ℝ

Equations

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

ink

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 }

ink

@[simp]

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

ink

theorem Real.inf_def : ∀ (x x_1 : ℝ), Real.inf x x_1 = match x, x_1 with | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun x x_2 => x ⊓ x_2) Real.definition.proof_2✝ x y }

ink

instance Real.instInfReal : Inf ℝ

Equations

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

ink

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 }

ink

@[simp]

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

ink

instance Real.instDistribLatticeReal : DistribLattice ℝ

Equations

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

ink

instance Real.lattice : Lattice ℝ

Equations

• Real.lattice = inferInstance

ink

instance Real.instSemilatticeInfReal : SemilatticeInf ℝ

Equations

• Real.instSemilatticeInfReal = inferInstance

ink

instance Real.instSemilatticeSupReal : SemilatticeSup ℝ

Equations

• Real.instSemilatticeSupReal = inferInstance

ink

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

Equations

• Real.instIsTotalRealLeInstLEReal = Real.instIsTotalRealLeInstLEReal.proof_1

ink

noncomputable instance Real.linearOrder : LinearOrder ℝ

Equations

• Real.linearOrder = Lattice.toLinearOrder ℝ

ink

noncomputable instance Real.linearOrderedCommRing : LinearOrderedCommRing ℝ

Equations

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

ink

noncomputable instance Real.instLinearOrderedRingReal : LinearOrderedRing ℝ

Equations

• Real.instLinearOrderedRingReal = inferInstance

ink

noncomputable instance Real.instLinearOrderedSemiringReal : LinearOrderedSemiring ℝ

Equations

• Real.instLinearOrderedSemiringReal = inferInstance

ink

instance Real.instIsDomainRealSemiring : IsDomain ℝ

Equations

• Real.instIsDomainRealSemiring = Real.instIsDomainRealSemiring.proof_1

ink

noncomputable instance Real.instLinearOrderedFieldReal : LinearOrderedField ℝ

Equations

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

ink

noncomputable instance Real.instLinearOrderedAddCommGroupReal : LinearOrderedAddCommGroup ℝ

Equations

• Real.instLinearOrderedAddCommGroupReal = inferInstance

ink

noncomputable instance Real.field : Field ℝ

Equations

• Real.field = inferInstance

ink

noncomputable instance Real.instDivisionRingReal : DivisionRing ℝ

Equations

• Real.instDivisionRingReal = inferInstance

ink

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

Equations

• Real.decidableLT a b = inferInstance

ink

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

Equations

• Real.decidableLE a b = inferInstance

ink

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

Equations

• Real.decidableEq a b = inferInstance

ink

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 }

ink

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

ink

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

ink

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

ink

instance Real.instArchimedeanRealOrderedAddCommMonoid : Archimedean ℝ

Equations

• Real.instArchimedeanRealOrderedAddCommMonoid = Real.instArchimedeanRealOrderedAddCommMonoid.proof_1

ink

noncomputable instance Real.instFloorRingRealInstLinearOrderedRingReal : FloorRing ℝ

Equations

• Real.instFloorRingRealInstLinearOrderedRingReal = Archimedean.floorRing ℝ

ink

theorem Real.isCauSeq_iff_lift {f : ℕ → ℚ} : IsCauSeq abs f ↔ IsCauSeq abs fun i => ↑(f i)

ink

theorem Real.of_near (f : ℕ → ℚ) (x : ℝ) (h : ∀ (ε : ℝ), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abs (↑(f j) - x) < ε) : ∃ h', Real.mk { val := f, property := h' } = x

ink

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

ink

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

ink

noncomputable instance Real.instSupSetReal : SupSet ℝ

Equations

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

ink

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

ink

theorem Real.isLUB_supₛ (S : Set ℝ) (h₁ : Set.Nonempty S) (h₂ : BddAbove S) : IsLUB S (supₛ S)

ink

noncomputable instance Real.instInfSetReal : InfSet ℝ

Equations

• Real.instInfSetReal = { infₛ := fun S => -supₛ (-S) }

ink

theorem Real.infₛ_def (S : Set ℝ) : infₛ S = -supₛ (-S)

ink

theorem Real.is_glb_infₛ (S : Set ℝ) (h₁ : Set.Nonempty S) (h₂ : BddBelow S) : IsGLB S (infₛ S)

ink

noncomputable instance Real.instConditionallyCompleteLinearOrderReal : ConditionallyCompleteLinearOrder ℝ

Equations

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

ink

theorem Real.lt_infₛ_add_pos {s : Set ℝ} (h : Set.Nonempty s) {ε : ℝ} (hε : 0 < ε) : ∃ a, a ∈ s ∧ a < infₛ s + ε

ink

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

ink

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

ink

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

ink

@[simp]

theorem Real.supₛ_empty : supₛ ∅ = 0

ink

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

ink

@[simp]

theorem Real.csupᵢ_const_zero {α : Sort u_1} : (⨆ _i, 0) = 0

ink

theorem Real.supₛ_of_not_bddAbove {s : Set ℝ} (hs : ¬BddAbove s) : supₛ s = 0

ink

theorem Real.supᵢ_of_not_bddAbove {α : Sort u_1} {f : α → ℝ} (hf : ¬BddAbove (Set.range f)) : (⨆ i, f i) = 0

ink

theorem Real.supₛ_univ : supₛ Set.univ = 0

ink

@[simp]

theorem Real.infₛ_empty : infₛ ∅ = 0

ink

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

ink

@[simp]

theorem Real.cinfᵢ_const_zero {α : Sort u_1} : (⨅ _i, 0) = 0

ink

theorem Real.infₛ_of_not_bddBelow {s : Set ℝ} (hs : ¬BddBelow s) : infₛ s = 0

ink

theorem Real.infᵢ_of_not_bddBelow {α : Sort u_1} {f : α → ℝ} (hf : ¬BddBelow (Set.range f)) : (⨅ i, f i) = 0

ink

theorem Real.supₛ_nonneg (S : Set ℝ) (hS : ∀ (x : ℝ), x ∈ S → 0 ≤ x) : 0 ≤ supₛ S

As 0 is the default value for Real.supₛ 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 ≤ infₛ S.

ink

theorem Real.supₛ_nonpos (S : Set ℝ) (hS : ∀ (x : ℝ), x ∈ S → x ≤ 0) : supₛ S ≤ 0

As 0 is the default value for Real.supₛ of the empty set, it suffices to show that S is bounded above by 0 to show that supₛ S ≤ 0.

ink

theorem Real.infₛ_nonneg (S : Set ℝ) (hS : ∀ (x : ℝ), x ∈ S → 0 ≤ x) : 0 ≤ infₛ S

As 0 is the default value for Real.infₛ of the empty set, it suffices to show that S is bounded below by 0 to show that 0 ≤ infₛ S.

ink

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

As 0 is the default value for Real.infₛ of the empty set, it suffices to show that f i is bounded below by 0 to show that 0 ≤ infᵢ f.

ink

theorem Real.infₛ_nonpos (S : Set ℝ) (hS : ∀ (x : ℝ), x ∈ S → x ≤ 0) : infₛ S ≤ 0

As 0 is the default value for Real.infₛ 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 infₛ S ≤ 0.

ink

theorem Real.infₛ_le_supₛ (s : Set ℝ) (h₁ : BddBelow s) (h₂ : BddAbove s) : infₛ s ≤ supₛ s

ink

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

ink

instance Real.instIsCompleteRealInstLinearOrderedFieldRealInstRingRealAbsToHasAbsInstNegRealInstSupRealAbs_isAbsoluteValueInstLinearOrderedRingReal : CauSeq.IsComplete ℝ abs

Equations

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