1. Analysis
  2. 5.3. The construction of the real numbers
Imports
import Mathlib.Tactic import Analysis.Section_5_2 import Mathlib.Algebra.Group.MinimalAxioms

Analysis I, Section 5.3: The construction of the real numbers

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

  • Notion of a formal limit of a Cauchy sequence.

  • Construction of a real number type Chapter5.Real.

  • Basic arithmetic operations and properties.

Tips from past users

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

  • (Add tip here)

namespace Chapter5

A class of Cauchy sequences that start at zero.

@[ext] class CauchySequence extends Sequence where zero : n₀ = 0 cauchy : toSequence.IsCauchy
theorem CauchySequence.ext' {a b: CauchySequence} (h: a.seq = b.seq) : a = b := a:CauchySequenceb:CauchySequenceh:a.seq = b.seq⊢ a = b a:CauchySequenceb:CauchySequenceh:a.seq = b.seq⊢ a.n₀ = b.n₀ All goals completed! 🐙

A sequence starting at zero that is Cauchy, can be viewed as a CauchySequence.

abbrev CauchySequence.mk' {a:ℕ → ℚ} (ha: (a:Sequence).IsCauchy) : CauchySequence where n₀ := 0 seq := (a:Sequence).seq vanish := a:ℕ → ℚha:(↑a).IsCauchy⊢ ∀ n < 0, (↑a).seq n = 0 All goals completed! 🐙 zero := rfl cauchy := ha
@[simp] theorem CauchySequence.coe_eq {a:ℕ → ℚ} (ha: (a:Sequence).IsCauchy) : (mk' ha).toSequence = (a:Sequence) := rflinstance CauchySequence.instCoeFun : CoeFun CauchySequence (fun _ ↦ ℕ → ℚ) where coe a n := a.toSequence (n:ℤ)@[simp] theorem CauchySequence.coe_to_sequence (a: CauchySequence) : ((a:ℕ → ℚ):Sequence) = a.toSequence := a:CauchySequence⊢ (↑fun n ↦ a.seq ↑n) = a.toSequence apply Sequence.ext (a:CauchySequence⊢ (↑fun n ↦ a.seq ↑n).n₀ = a.n₀ All goals completed! 🐙) a:CauchySequencen:ℤ⊢ (↑fun n ↦ a.seq ↑n).seq n = a.seq n; a:CauchySequencen:ℤh:n ≥ 0⊢ (↑fun n ↦ a.seq ↑n).seq n = a.seq na:CauchySequencen:ℤh:¬n ≥ 0⊢ (↑fun n ↦ a.seq ↑n).seq n = a.seq n a:CauchySequencen:ℤh:n ≥ 0⊢ (↑fun n ↦ a.seq ↑n).seq n = a.seq na:CauchySequencen:ℤh:¬n ≥ 0⊢ (↑fun n ↦ a.seq ↑n).seq n = a.seq n a:CauchySequencen:ℤh:n < 0⊢ 0 = a.seq n a:CauchySequencen:ℤh:n < 0⊢ n < a.n₀; rwa [a.zeroa:CauchySequencen:ℤh:n < 0⊢ n < 0@[simp] theorem CauchySequence.coe_coe {a:ℕ → ℚ} (ha: (a:Sequence).IsCauchy) : mk' ha = a := a:ℕ → ℚha:(↑a).IsCauchy⊢ (fun n ↦ (mk' ha).seq ↑n) = a All goals completed! 🐙

Proposition 5.3.3 / Exercise 5.3.1

theorem declaration uses `sorry`Sequence.equiv_trans {a b c:ℕ → ℚ} (hab: Equiv a b) (hbc: Equiv b c) : Equiv a c := a:ℕ → ℚb:ℕ → ℚc:ℕ → ℚhab:Equiv a bhbc:Equiv b c⊢ Equiv a c All goals completed! 🐙

Proposition 5.3.3 / Exercise 5.3.1

instance declaration uses `sorry`CauchySequence.instSetoid : Setoid CauchySequence where r := fun a b ↦ Sequence.Equiv a b iseqv := { refl := sorry symm := sorry trans := sorry }
theorem CauchySequence.equiv_iff (a b: CauchySequence) : a ≈ b ↔ Sequence.Equiv a b := a:CauchySequenceb:CauchySequence⊢ a ≈ b ↔ Sequence.Equiv (fun n ↦ a.seq ↑n) fun n ↦ b.seq ↑n All goals completed! 🐙

Every constant sequence is Cauchy.

theorem declaration uses `sorry`Sequence.IsCauchy.const (a:ℚ) : ((fun _:ℕ ↦ a):Sequence).IsCauchy := a:ℚ⊢ (↑fun x ↦ a).IsCauchy All goals completed! 🐙
instance CauchySequence.instZero : Zero CauchySequence where zero := CauchySequence.mk' (a := fun _: ℕ ↦ 0) (Sequence.IsCauchy.const (0:ℚ))abbrev Real := Quotient CauchySequence.instSetoid

It is convenient in Lean to assign the "dummy" value of 0 to LIM a when a is not Cauchy. This requires classical logic, because the property of being Cauchy is not computable or decidable.

open Classical innoncomputable abbrev LIM (a:ℕ → ℚ) : Real := Quotient.mk _ (if h : (a:Sequence).IsCauchy then CauchySequence.mk' h else (0:CauchySequence))
theorem LIM_def {a:ℕ → ℚ} (ha: (a:Sequence).IsCauchy) : LIM a = Quotient.mk _ (CauchySequence.mk' ha) := a:ℕ → ℚha:(↑a).IsCauchy⊢ LIM a = ⟦CauchySequence.mk' ha⟧ All goals completed! 🐙

Definition 5.3.1 (Real numbers)

theorem Real.eq_lim (x:Real) : ∃ (a:ℕ → ℚ), (a:Sequence).IsCauchy ∧ x = LIM a := x:Real⊢ ∃ a, (↑a).IsCauchy ∧ x = LIM a x:Real⊢ ∀ (a : CauchySequence), ∃ a_1, (↑a_1).IsCauchy ∧ ⟦a⟧ = LIM a_1; x:Reala:CauchySequence⊢ ∃ a_1, (↑a_1).IsCauchy ∧ ⟦a⟧ = LIM a_1; x:Reala:CauchySequence⊢ (↑fun n ↦ a.seq ↑n).IsCauchy ∧ ⟦a⟧ = LIM fun n ↦ a.seq ↑n x:Reala:CauchySequencethis:(↑fun n ↦ a.seq ↑n) = a.toSequence⊢ (↑fun n ↦ a.seq ↑n).IsCauchy ∧ ⟦a⟧ = LIM fun n ↦ a.seq ↑n x:Reala:CauchySequencethis:(↑fun n ↦ a.seq ↑n) = a.toSequence⊢ a.IsCauchy ∧ ⟦a⟧ = ⟦CauchySequence.mk' ⋯⟧ x:Reala:CauchySequencethis:(↑fun n ↦ a.seq ↑n) = a.toSequence⊢ ⟦a⟧ = ⟦CauchySequence.mk' ⋯⟧ x:Reala:CauchySequencethis:(↑fun n ↦ a.seq ↑n) = a.toSequence⊢ a = CauchySequence.mk' ⋯; x:Reala:CauchySequencethis:(↑fun n ↦ a.seq ↑n) = a.toSequence⊢ a.n₀ = (CauchySequence.mk' ⋯).n₀x:Reala:CauchySequencethis:(↑fun n ↦ a.seq ↑n) = a.toSequencen:ℤ⊢ a.seq n = (CauchySequence.mk' ⋯).seq n; x:Reala:CauchySequencethis:(↑fun n ↦ a.seq ↑n) = a.toSequencen:ℤ⊢ a.seq n = (CauchySequence.mk' ⋯).seq n; x:Reala:CauchySequencethis✝:(↑fun n ↦ a.seq ↑n) = a.toSequencen:ℤthis:(↑fun n ↦ a.seq ↑n).seq n = a.seq n⊢ a.seq n = (CauchySequence.mk' ⋯).seq n; All goals completed! 🐙

Definition 5.3.1 (Real numbers)

theorem Real.LIM_eq_LIM {a b:ℕ → ℚ} (ha: (a:Sequence).IsCauchy) (hb: (b:Sequence).IsCauchy) : LIM a = LIM b ↔ Sequence.Equiv a b := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ LIM a = LIM b ↔ Sequence.Equiv a b a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ LIM a = LIM b → Sequence.Equiv a ba:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ Sequence.Equiv a b → LIM a = LIM b a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ LIM a = LIM b → Sequence.Equiv a b a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyh:LIM a = LIM b⊢ Sequence.Equiv a b; a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyh:(if h : (↑a).IsCauchy then CauchySequence.mk' h else 0) ≈ if h : (↑b).IsCauchy then CauchySequence.mk' h else 0⊢ Sequence.Equiv a b rwa [dif_pos ha, dif_pos hb, CauchySequence.equiv_iffa:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyh:Sequence.Equiv (fun n ↦ (CauchySequence.mk' ha).seq ↑n) fun n ↦ (CauchySequence.mk' hb).seq ↑n⊢ Sequence.Equiv a b at h a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyh:Sequence.Equiv a b⊢ LIM a = LIM b; a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyh:Sequence.Equiv a b⊢ (if h : (↑a).IsCauchy then CauchySequence.mk' h else 0) ≈ if h : (↑b).IsCauchy then CauchySequence.mk' h else 0 rwa [dif_pos ha, dif_pos hb, CauchySequence.equiv_iffa:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyh:Sequence.Equiv a b⊢ Sequence.Equiv (fun n ↦ (CauchySequence.mk' ha).seq ↑n) fun n ↦ (CauchySequence.mk' hb).seq ↑n

Lemma 5.3.6 (Sum of Cauchy sequences is Cauchy)

theorem Sequence.IsCauchy.add {a b:ℕ → ℚ} (ha: (a:Sequence).IsCauchy) (hb: (b:Sequence).IsCauchy) : (a + b:Sequence).IsCauchy := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ (↑(a + b)).IsCauchy -- This proof is written to follow the structure of the original text. a:ℕ → ℚb:ℕ → ℚha:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ ε⊢ ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((a + b) j) ((a + b) k) ≤ ε intro ε a:ℕ → ℚb:ℕ → ℚha:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ εε:ℚhε:ε > 0⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((a + b) j) ((a + b) k) ≤ ε a:ℕ → ℚb:ℕ → ℚha✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ εε:ℚhε:ε > 0N1:ℕha:∀ j ≥ N1, ∀ k ≥ N1, Section_4_3.dist (a j) (a k) ≤ ε / 2⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((a + b) j) ((a + b) k) ≤ ε a:ℕ → ℚb:ℕ → ℚha✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ εε:ℚhε:ε > 0N1:ℕha:∀ j ≥ N1, ∀ k ≥ N1, Section_4_3.dist (a j) (a k) ≤ ε / 2N2:ℕhb:∀ j ≥ N2, ∀ k ≥ N2, Section_4_3.dist (b j) (b k) ≤ ε / 2⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((a + b) j) ((a + b) k) ≤ ε a:ℕ → ℚb:ℕ → ℚha✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ εε:ℚhε:ε > 0N1:ℕha:∀ j ≥ N1, ∀ k ≥ N1, Section_4_3.dist (a j) (a k) ≤ ε / 2N2:ℕhb:∀ j ≥ N2, ∀ k ≥ N2, Section_4_3.dist (b j) (b k) ≤ ε / 2⊢ ∀ j ≥ max N1 N2, ∀ k ≥ max N1 N2, Section_4_3.dist ((a + b) j) ((a + b) k) ≤ ε intro j a:ℕ → ℚb:ℕ → ℚha✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ εε:ℚhε:ε > 0N1:ℕha:∀ j ≥ N1, ∀ k ≥ N1, Section_4_3.dist (a j) (a k) ≤ ε / 2N2:ℕhb:∀ j ≥ N2, ∀ k ≥ N2, Section_4_3.dist (b j) (b k) ≤ ε / 2j:ℕhj:j ≥ max N1 N2⊢ ∀ k ≥ max N1 N2, Section_4_3.dist ((a + b) j) ((a + b) k) ≤ ε a:ℕ → ℚb:ℕ → ℚha✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ εε:ℚhε:ε > 0N1:ℕha:∀ j ≥ N1, ∀ k ≥ N1, Section_4_3.dist (a j) (a k) ≤ ε / 2N2:ℕhb:∀ j ≥ N2, ∀ k ≥ N2, Section_4_3.dist (b j) (b k) ≤ ε / 2j:ℕhj:j ≥ max N1 N2k:ℕ⊢ k ≥ max N1 N2 → Section_4_3.dist ((a + b) j) ((a + b) k) ≤ ε a:ℕ → ℚb:ℕ → ℚha✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ εε:ℚhε:ε > 0N1:ℕha:∀ j ≥ N1, ∀ k ≥ N1, Section_4_3.dist (a j) (a k) ≤ ε / 2N2:ℕhb:∀ j ≥ N2, ∀ k ≥ N2, Section_4_3.dist (b j) (b k) ≤ ε / 2j:ℕhj:j ≥ max N1 N2k:ℕhk:k ≥ max N1 N2⊢ Section_4_3.dist ((a + b) j) ((a + b) k) ≤ ε a:ℕ → ℚb:ℕ → ℚha✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ εε:ℚhε:ε > 0N1:ℕha:∀ j ≥ N1, ∀ k ≥ N1, Section_4_3.dist (a j) (a k) ≤ ε / 2N2:ℕhb:∀ j ≥ N2, ∀ k ≥ N2, Section_4_3.dist (b j) (b k) ≤ ε / 2j:ℕhj:j ≥ max N1 N2k:ℕhk:k ≥ max N1 N2h1:Section_4_3.dist (a j) (a k) ≤ ε / 2⊢ Section_4_3.dist ((a + b) j) ((a + b) k) ≤ εa:ℕ → ℚb:ℕ → ℚha✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ εε:ℚhε:ε > 0N1:ℕha:∀ j ≥ N1, ∀ k ≥ N1, Section_4_3.dist (a j) (a k) ≤ ε / 2N2:ℕhb:∀ j ≥ N2, ∀ k ≥ N2, Section_4_3.dist (b j) (b k) ≤ ε / 2j:ℕhj:j ≥ max N1 N2k:ℕhk:k ≥ max N1 N2⊢ j ≥ N1a:ℕ → ℚb:ℕ → ℚha✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ εε:ℚhε:ε > 0N1:ℕha:∀ j ≥ N1, ∀ k ≥ N1, Section_4_3.dist (a j) (a k) ≤ ε / 2N2:ℕhb:∀ j ≥ N2, ∀ k ≥ N2, Section_4_3.dist (b j) (b k) ≤ ε / 2j:ℕhj:j ≥ max N1 N2k:ℕhk:k ≥ max N1 N2⊢ k ≥ N1 a:ℕ → ℚb:ℕ → ℚha✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ εε:ℚhε:ε > 0N1:ℕha:∀ j ≥ N1, ∀ k ≥ N1, Section_4_3.dist (a j) (a k) ≤ ε / 2N2:ℕhb:∀ j ≥ N2, ∀ k ≥ N2, Section_4_3.dist (b j) (b k) ≤ ε / 2j:ℕhj:j ≥ max N1 N2k:ℕhk:k ≥ max N1 N2h1:Section_4_3.dist (a j) (a k) ≤ ε / 2⊢ Section_4_3.dist ((a + b) j) ((a + b) k) ≤ εa:ℕ → ℚb:ℕ → ℚha✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ εε:ℚhε:ε > 0N1:ℕha:∀ j ≥ N1, ∀ k ≥ N1, Section_4_3.dist (a j) (a k) ≤ ε / 2N2:ℕhb:∀ j ≥ N2, ∀ k ≥ N2, Section_4_3.dist (b j) (b k) ≤ ε / 2j:ℕhj:j ≥ max N1 N2k:ℕhk:k ≥ max N1 N2⊢ j ≥ N1a:ℕ → ℚb:ℕ → ℚha✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ εε:ℚhε:ε > 0N1:ℕha:∀ j ≥ N1, ∀ k ≥ N1, Section_4_3.dist (a j) (a k) ≤ ε / 2N2:ℕhb:∀ j ≥ N2, ∀ k ≥ N2, Section_4_3.dist (b j) (b k) ≤ ε / 2j:ℕhj:j ≥ max N1 N2k:ℕhk:k ≥ max N1 N2⊢ k ≥ N1 try All goals completed! 🐙 a:ℕ → ℚb:ℕ → ℚha✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ εε:ℚhε:ε > 0N1:ℕha:∀ j ≥ N1, ∀ k ≥ N1, Section_4_3.dist (a j) (a k) ≤ ε / 2N2:ℕhb:∀ j ≥ N2, ∀ k ≥ N2, Section_4_3.dist (b j) (b k) ≤ ε / 2j:ℕhj:j ≥ max N1 N2k:ℕhk:k ≥ max N1 N2h1:Section_4_3.dist (a j) (a k) ≤ ε / 2h2:Section_4_3.dist (b j) (b k) ≤ ε / 2⊢ Section_4_3.dist ((a + b) j) ((a + b) k) ≤ εa:ℕ → ℚb:ℕ → ℚha✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ εε:ℚhε:ε > 0N1:ℕha:∀ j ≥ N1, ∀ k ≥ N1, Section_4_3.dist (a j) (a k) ≤ ε / 2N2:ℕhb:∀ j ≥ N2, ∀ k ≥ N2, Section_4_3.dist (b j) (b k) ≤ ε / 2j:ℕhj:j ≥ max N1 N2k:ℕhk:k ≥ max N1 N2h1:Section_4_3.dist (a j) (a k) ≤ ε / 2⊢ j ≥ N2a:ℕ → ℚb:ℕ → ℚha✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ εε:ℚhε:ε > 0N1:ℕha:∀ j ≥ N1, ∀ k ≥ N1, Section_4_3.dist (a j) (a k) ≤ ε / 2N2:ℕhb:∀ j ≥ N2, ∀ k ≥ N2, Section_4_3.dist (b j) (b k) ≤ ε / 2j:ℕhj:j ≥ max N1 N2k:ℕhk:k ≥ max N1 N2h1:Section_4_3.dist (a j) (a k) ≤ ε / 2⊢ k ≥ N2 a:ℕ → ℚb:ℕ → ℚha✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ εε:ℚhε:ε > 0N1:ℕha:∀ j ≥ N1, ∀ k ≥ N1, Section_4_3.dist (a j) (a k) ≤ ε / 2N2:ℕhb:∀ j ≥ N2, ∀ k ≥ N2, Section_4_3.dist (b j) (b k) ≤ ε / 2j:ℕhj:j ≥ max N1 N2k:ℕhk:k ≥ max N1 N2h1:Section_4_3.dist (a j) (a k) ≤ ε / 2h2:Section_4_3.dist (b j) (b k) ≤ ε / 2⊢ Section_4_3.dist ((a + b) j) ((a + b) k) ≤ εa:ℕ → ℚb:ℕ → ℚha✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ εε:ℚhε:ε > 0N1:ℕha:∀ j ≥ N1, ∀ k ≥ N1, Section_4_3.dist (a j) (a k) ≤ ε / 2N2:ℕhb:∀ j ≥ N2, ∀ k ≥ N2, Section_4_3.dist (b j) (b k) ≤ ε / 2j:ℕhj:j ≥ max N1 N2k:ℕhk:k ≥ max N1 N2h1:Section_4_3.dist (a j) (a k) ≤ ε / 2⊢ j ≥ N2a:ℕ → ℚb:ℕ → ℚha✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εhb✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ εε:ℚhε:ε > 0N1:ℕha:∀ j ≥ N1, ∀ k ≥ N1, Section_4_3.dist (a j) (a k) ≤ ε / 2N2:ℕhb:∀ j ≥ N2, ∀ k ≥ N2, Section_4_3.dist (b j) (b k) ≤ ε / 2j:ℕhj:j ≥ max N1 N2k:ℕhk:k ≥ max N1 N2h1:Section_4_3.dist (a j) (a k) ≤ ε / 2⊢ k ≥ N2 try All goals completed! 🐙 a:ℕ → ℚb:ℕ → ℚε:ℚN1:ℕN2:ℕj:ℕk:ℕh1:|a j - a k| ≤ ε / 2h2:|b j - b k| ≤ ε / 2ha✝:∀ (ε : ℚ), 0 < ε → ∃ N, ∀ (j : ℕ), N ≤ j → ∀ (k : ℕ), N ≤ k → |a j - a k| ≤ εhb✝:∀ (ε : ℚ), 0 < ε → ∃ N, ∀ (j : ℕ), N ≤ j → ∀ (k : ℕ), N ≤ k → |b j - b k| ≤ εhε:0 < εha:∀ (j : ℕ), N1 ≤ j → ∀ (k : ℕ), N1 ≤ k → |a j - a k| ≤ ε / 2hb:∀ (j : ℕ), N2 ≤ j → ∀ (k : ℕ), N2 ≤ k → |b j - b k| ≤ ε / 2hj:N1 ≤ j ∧ N2 ≤ jhk:N1 ≤ k ∧ N2 ≤ k⊢ |a j + b j - (a k + b k)| ≤ ε; a:ℕ → ℚb:ℕ → ℚε:ℚN1:ℕN2:ℕj:ℕk:ℕh1:(ε / 2).Close (a j) (a k)h2:(ε / 2).Close (b j) (b k)ha✝:∀ (ε : ℚ), 0 < ε → ∃ N, ∀ (j : ℕ), N ≤ j → ∀ (k : ℕ), N ≤ k → |a j - a k| ≤ εhb✝:∀ (ε : ℚ), 0 < ε → ∃ N, ∀ (j : ℕ), N ≤ j → ∀ (k : ℕ), N ≤ k → |b j - b k| ≤ εhε:0 < εha:∀ (j : ℕ), N1 ≤ j → ∀ (k : ℕ), N1 ≤ k → |a j - a k| ≤ ε / 2hb:∀ (j : ℕ), N2 ≤ j → ∀ (k : ℕ), N2 ≤ k → |b j - b k| ≤ ε / 2hj:N1 ≤ j ∧ N2 ≤ jhk:N1 ≤ k ∧ N2 ≤ k⊢ ε.Close (a j + b j) (a k + b k) a:ℕ → ℚb:ℕ → ℚε:ℚN1:ℕN2:ℕj:ℕk:ℕh1:(ε / 2).Close (a j) (a k)h2:(ε / 2).Close (b j) (b k)ha✝:∀ (ε : ℚ), 0 < ε → ∃ N, ∀ (j : ℕ), N ≤ j → ∀ (k : ℕ), N ≤ k → |a j - a k| ≤ εhb✝:∀ (ε : ℚ), 0 < ε → ∃ N, ∀ (j : ℕ), N ≤ j → ∀ (k : ℕ), N ≤ k → |b j - b k| ≤ εhε:0 < εha:∀ (j : ℕ), N1 ≤ j → ∀ (k : ℕ), N1 ≤ k → |a j - a k| ≤ ε / 2hb:∀ (j : ℕ), N2 ≤ j → ∀ (k : ℕ), N2 ≤ k → |b j - b k| ≤ ε / 2hj:N1 ≤ j ∧ N2 ≤ jhk:N1 ≤ k ∧ N2 ≤ k⊢ ε = ε / 2 + ε / 2 All goals completed! 🐙

Lemma 5.3.7 (Sum of equivalent sequences is equivalent)

theorem Sequence.add_equiv_left {a a':ℕ → ℚ} (b:ℕ → ℚ) (haa': Equiv a a') : Equiv (a + b) (a' + b) := a:ℕ → ℚa':ℕ → ℚb:ℕ → ℚhaa':Equiv a a'⊢ Equiv (a + b) (a' + b) -- This proof is written to follow the structure of the original text. a:ℕ → ℚa':ℕ → ℚb:ℕ → ℚhaa':∀ ε > 0, ε.EventuallyClose ↑a ↑a'⊢ ∀ ε > 0, ε.EventuallyClose ↑(a + b) ↑(a' + b) a:ℕ → ℚa':ℕ → ℚb:ℕ → ℚhaa'✝:∀ ε > 0, ε.EventuallyClose ↑a ↑a'ε:ℚhε:ε > 0haa':ε.EventuallyClose ↑a ↑a'⊢ ε.EventuallyClose ↑(a + b) ↑(a' + b) a:ℕ → ℚa':ℕ → ℚb:ℕ → ℚhaa'✝:∀ ε > 0, ε.EventuallyClose ↑a ↑a'ε:ℚhε:ε > 0haa':∃ N, ε.CloseSeq ((↑a).from N) ((↑a').from N)⊢ ∃ N, ε.CloseSeq ((↑(a + b)).from N) ((↑(a' + b)).from N) a:ℕ → ℚa':ℕ → ℚb:ℕ → ℚhaa'✝:∀ ε > 0, ε.EventuallyClose ↑a ↑a'ε:ℚhε:ε > 0N:ℤhaa':ε.CloseSeq ((↑a).from N) ((↑a').from N)⊢ ∃ N, ε.CloseSeq ((↑(a + b)).from N) ((↑(a' + b)).from N); a:ℕ → ℚa':ℕ → ℚb:ℕ → ℚhaa'✝:∀ ε > 0, ε.EventuallyClose ↑a ↑a'ε:ℚhε:ε > 0N:ℤhaa':ε.CloseSeq ((↑a).from N) ((↑a').from N)⊢ ε.CloseSeq ((↑(a + b)).from N) ((↑(a' + b)).from N) a:ℕ → ℚa':ℕ → ℚb:ℕ → ℚε:ℚN:ℤhaa'✝:∀ (ε : ℚ), 0 < ε → ε.EventuallyClose ↑a ↑a'hε:0 < εhaa':∀ (n : ℤ), 0 ≤ n → N ≤ n → 0 ≤ n → N ≤ n → ε.Close (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0) (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a' n.toNat else 0 else 0)⊢ ∀ (n : ℤ), 0 ≤ n → N ≤ n → 0 ≤ n → N ≤ n → ε.Close (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a n.toNat + b n.toNat else 0 else 0) (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a' n.toNat + b n.toNat else 0 else 0) a:ℕ → ℚa':ℕ → ℚb:ℕ → ℚε:ℚN:ℤhaa'✝¹:∀ (ε : ℚ), 0 < ε → ε.EventuallyClose ↑a ↑a'hε:0 < εhaa'✝:∀ (n : ℤ), 0 ≤ n → N ≤ n → 0 ≤ n → N ≤ n → ε.Close (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0) (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a' n.toNat else 0 else 0)n:ℤhn:0 ≤ nhN:N ≤ na✝¹:0 ≤ na✝:N ≤ nhaa':ε.Close (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0) (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a' n.toNat else 0 else 0)⊢ ε.Close (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a n.toNat + b n.toNat else 0 else 0) (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a' n.toNat + b n.toNat else 0 else 0) a:ℕ → ℚa':ℕ → ℚb:ℕ → ℚε:ℚN:ℤhaa'✝¹:∀ (ε : ℚ), 0 < ε → ε.EventuallyClose ↑a ↑a'hε:0 < εhaa'✝:∀ (n : ℤ), 0 ≤ n → N ≤ n → 0 ≤ n → N ≤ n → ε.Close (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0) (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a' n.toNat else 0 else 0)n:ℤhn:TruehN:Truea✝¹:Truea✝:Truehaa':ε.Close (a n.toNat) (a' n.toNat)⊢ ε.Close (a n.toNat + b n.toNat) (a' n.toNat + b n.toNat) a:ℕ → ℚa':ℕ → ℚb:ℕ → ℚε:ℚN:ℤhaa'✝¹:∀ (ε : ℚ), 0 < ε → ε.EventuallyClose ↑a ↑a'hε:0 < εhaa'✝:∀ (n : ℤ), 0 ≤ n → N ≤ n → 0 ≤ n → N ≤ n → ε.Close (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0) (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a' n.toNat else 0 else 0)n:ℤhn:TruehN:Truea✝¹:Truea✝:Truehaa':ε.Close (a n.toNat) (a' n.toNat)⊢ ε = ε + 0 All goals completed! 🐙

Lemma 5.3.7 (Sum of equivalent sequences is equivalent)

theorem Sequence.add_equiv_right {b b':ℕ → ℚ} (a:ℕ → ℚ) (hbb': Equiv b b') : Equiv (a + b) (a + b') := b:ℕ → ℚb':ℕ → ℚa:ℕ → ℚhbb':Equiv b b'⊢ Equiv (a + b) (a + b') simp_rw b:ℕ → ℚb':ℕ → ℚa:ℕ → ℚhbb':Equiv b b'⊢ Equiv (a + b) (a + b')add_comm]; All goals completed! 🐙

Lemma 5.3.7 (Sum of equivalent sequences is equivalent)

theorem Sequence.add_equiv {a b a' b':ℕ → ℚ} (haa': Equiv a a') (hbb': Equiv b b') : Equiv (a + b) (a' + b') := equiv_trans (add_equiv_left _ haa') (add_equiv_right _ hbb')

Definition 5.3.4 (Addition of reals)

noncomputable instance Real.add_inst : Add Real where add := fun x y ↦ Quotient.liftOn₂ x y (fun a b ↦ LIM (a + b)) (x:Realy:Real⊢ ∀ (a₁ b₁ a₂ b₂ : CauchySequence), a₁ ≈ a₂ → b₁ ≈ b₂ → (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) + fun n ↦ b.seq ↑n)) a₁ b₁ = (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) + fun n ↦ b.seq ↑n)) a₂ b₂ intro a x:Realy:Reala:CauchySequenceb:CauchySequence⊢ ∀ (a₂ b₂ : CauchySequence), a ≈ a₂ → b ≈ b₂ → (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) + fun n ↦ b.seq ↑n)) a b = (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) + fun n ↦ b.seq ↑n)) a₂ b₂ x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequence⊢ ∀ (b₂ : CauchySequence), a ≈ a' → b ≈ b₂ → (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) + fun n ↦ b.seq ↑n)) a b = (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) + fun n ↦ b.seq ↑n)) a' b₂ x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequence⊢ a ≈ a' → b ≈ b' → (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) + fun n ↦ b.seq ↑n)) a b = (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) + fun n ↦ b.seq ↑n)) a' b' x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencea✝:a ≈ a'⊢ b ≈ b' → (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) + fun n ↦ b.seq ↑n)) a b = (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) + fun n ↦ b.seq ↑n)) a' b' x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencea✝¹:a ≈ a'a✝:b ≈ b'⊢ (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) + fun n ↦ b.seq ↑n)) a b = (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) + fun n ↦ b.seq ↑n)) a' b' x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencea✝¹:a ≈ a'a✝:b ≈ b'⊢ LIM ((fun n ↦ a.seq ↑n) + fun n ↦ b.seq ↑n) = LIM ((fun n ↦ a'.seq ↑n) + fun n ↦ b'.seq ↑n) x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencea✝¹:a ≈ a'a✝:b ≈ b'⊢ Sequence.Equiv ((fun n ↦ a.seq ↑n) + fun n ↦ b.seq ↑n) ((fun n ↦ a'.seq ↑n) + fun n ↦ b'.seq ↑n)x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencea✝¹:a ≈ a'a✝:b ≈ b'⊢ (↑((fun n ↦ a.seq ↑n) + fun n ↦ b.seq ↑n)).IsCauchyx:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencea✝¹:a ≈ a'a✝:b ≈ b'⊢ (↑((fun n ↦ a'.seq ↑n) + fun n ↦ b'.seq ↑n)).IsCauchy x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencea✝¹:a ≈ a'a✝:b ≈ b'⊢ Sequence.Equiv ((fun n ↦ a.seq ↑n) + fun n ↦ b.seq ↑n) ((fun n ↦ a'.seq ↑n) + fun n ↦ b'.seq ↑n) All goals completed! 🐙 all_goals x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencea✝¹:a ≈ a'a✝:b ≈ b'⊢ (↑fun n ↦ a'.seq ↑n).IsCauchyx:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencea✝¹:a ≈ a'a✝:b ≈ b'⊢ (↑fun n ↦ b'.seq ↑n).IsCauchy x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencea✝¹:a ≈ a'a✝:b ≈ b'⊢ (↑fun n ↦ a'.seq ↑n).IsCauchyx:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencea✝¹:a ≈ a'a✝:b ≈ b'⊢ (↑fun n ↦ b'.seq ↑n).IsCauchy x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencea✝¹:a ≈ a'a✝:b ≈ b'⊢ b'.IsCauchy x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencea✝¹:a ≈ a'a✝:b ≈ b'⊢ a'.IsCauchyx:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencea✝¹:a ≈ a'a✝:b ≈ b'⊢ b'.IsCauchy All goals completed! 🐙 )

Definition 5.3.4 (Addition of reals)

theorem Real.LIM_add {a b:ℕ → ℚ} (ha: (a:Sequence).IsCauchy) (hb: (b:Sequence).IsCauchy) : LIM a + LIM b = LIM (a + b) := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ LIM a + LIM b = LIM (a + b) simp_rw a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ LIM a + LIM b = LIM (a + b)LIM_def ha, LIM_def hb, LIM_def (Sequence.IsCauchy.add ha hb)] a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ ⟦CauchySequence.mk' ⋯⟧ = LIM ((fun n ↦ (CauchySequence.mk' ha).seq ↑n) + fun n ↦ (CauchySequence.mk' hb).seq ↑n) a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ ⟦CauchySequence.mk' ⋯⟧ = ⟦if h : (↑((fun n ↦ (↑a).seq ↑n) + fun n ↦ (↑b).seq ↑n)).IsCauchy then CauchySequence.mk' ⋯ else 0⟧; All goals completed! 🐙

Proposition 5.3.10 (Product of Cauchy sequences is Cauchy)

theorem declaration uses `sorry`Sequence.IsCauchy.mul {a b:ℕ → ℚ} (ha: (a:Sequence).IsCauchy) (hb: (b:Sequence).IsCauchy) : (a * b:Sequence).IsCauchy := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ (↑(a * b)).IsCauchy All goals completed! 🐙

Proposition 5.3.10 (Product of equivalent sequences is equivalent) / Exercise 5.3.2

theorem declaration uses `sorry`Sequence.mul_equiv_left {a a':ℕ → ℚ} (b:ℕ → ℚ) (hb : (b:Sequence).IsCauchy) (haa': Equiv a a') : Equiv (a * b) (a' * b) := a:ℕ → ℚa':ℕ → ℚb:ℕ → ℚhb:(↑b).IsCauchyhaa':Equiv a a'⊢ Equiv (a * b) (a' * b) All goals completed! 🐙

Proposition 5.3.10 (Product of equivalent sequences is equivalent) / Exercise 5.3.2

theorem Sequence.mul_equiv_right {b b':ℕ → ℚ} (a:ℕ → ℚ) (ha : (a:Sequence).IsCauchy) (hbb': Equiv b b') : Equiv (a * b) (a * b') := b:ℕ → ℚb':ℕ → ℚa:ℕ → ℚha:(↑a).IsCauchyhbb':Equiv b b'⊢ Equiv (a * b) (a * b') simp_rw b:ℕ → ℚb':ℕ → ℚa:ℕ → ℚha:(↑a).IsCauchyhbb':Equiv b b'⊢ Equiv (a * b) (a * b')mul_comm]; All goals completed! 🐙

Proposition 5.3.10 (Product of equivalent sequences is equivalent) / Exercise 5.3.2

theorem Sequence.mul_equiv {a b a' b':ℕ → ℚ} (ha : (a:Sequence).IsCauchy) (hb' : (b':Sequence).IsCauchy) (haa': Equiv a a') (hbb': Equiv b b') : Equiv (a * b) (a' * b') := equiv_trans (mul_equiv_right _ ha hbb') (mul_equiv_left _ hb' haa')

Definition 5.3.9 (Product of reals)

noncomputable instance Real.mul_inst : Mul Real where mul := fun x y ↦ Quotient.liftOn₂ x y (fun a b ↦ LIM (a * b)) (x:Realy:Real⊢ ∀ (a₁ b₁ a₂ b₂ : CauchySequence), a₁ ≈ a₂ → b₁ ≈ b₂ → (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) * fun n ↦ b.seq ↑n)) a₁ b₁ = (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) * fun n ↦ b.seq ↑n)) a₂ b₂ intro a x:Realy:Reala:CauchySequenceb:CauchySequence⊢ ∀ (a₂ b₂ : CauchySequence), a ≈ a₂ → b ≈ b₂ → (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) * fun n ↦ b.seq ↑n)) a b = (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) * fun n ↦ b.seq ↑n)) a₂ b₂ x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequence⊢ ∀ (b₂ : CauchySequence), a ≈ a' → b ≈ b₂ → (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) * fun n ↦ b.seq ↑n)) a b = (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) * fun n ↦ b.seq ↑n)) a' b₂ x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequence⊢ a ≈ a' → b ≈ b' → (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) * fun n ↦ b.seq ↑n)) a b = (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) * fun n ↦ b.seq ↑n)) a' b' x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'⊢ b ≈ b' → (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) * fun n ↦ b.seq ↑n)) a b = (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) * fun n ↦ b.seq ↑n)) a' b' x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) * fun n ↦ b.seq ↑n)) a b = (fun a b ↦ LIM ((fun n ↦ a.seq ↑n) * fun n ↦ b.seq ↑n)) a' b' x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ LIM ((fun n ↦ a.seq ↑n) * fun n ↦ b.seq ↑n) = LIM ((fun n ↦ a'.seq ↑n) * fun n ↦ b'.seq ↑n) x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ Sequence.Equiv ((fun n ↦ a.seq ↑n) * fun n ↦ b.seq ↑n) ((fun n ↦ a'.seq ↑n) * fun n ↦ b'.seq ↑n)x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ (↑((fun n ↦ a.seq ↑n) * fun n ↦ b.seq ↑n)).IsCauchyx:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ (↑((fun n ↦ a'.seq ↑n) * fun n ↦ b'.seq ↑n)).IsCauchy x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ Sequence.Equiv ((fun n ↦ a.seq ↑n) * fun n ↦ b.seq ↑n) ((fun n ↦ a'.seq ↑n) * fun n ↦ b'.seq ↑n) exact Sequence.mul_equiv (x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ (↑fun n ↦ a.seq ↑n).IsCauchy x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ a.IsCauchy; All goals completed! 🐙) (x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ (↑fun n ↦ b'.seq ↑n).IsCauchy x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ b'.IsCauchy; All goals completed! 🐙) haa' hbb' all_goals x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ (↑fun n ↦ a'.seq ↑n).IsCauchyx:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ (↑fun n ↦ b'.seq ↑n).IsCauchy x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ (↑fun n ↦ a'.seq ↑n).IsCauchyx:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ (↑fun n ↦ b'.seq ↑n).IsCauchy x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ b'.IsCauchy x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ a'.IsCauchyx:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ b'.IsCauchy All goals completed! 🐙 )
theorem Real.LIM_mul {a b:ℕ → ℚ} (ha: (a:Sequence).IsCauchy) (hb: (b:Sequence).IsCauchy) : LIM a * LIM b = LIM (a * b) := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ LIM a * LIM b = LIM (a * b) simp_rw a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ LIM a * LIM b = LIM (a * b)LIM_def ha, LIM_def hb, LIM_def (Sequence.IsCauchy.mul ha hb)] a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ ⟦CauchySequence.mk' ⋯⟧ = LIM ((fun n ↦ (CauchySequence.mk' ha).seq ↑n) * fun n ↦ (CauchySequence.mk' hb).seq ↑n) a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ ⟦CauchySequence.mk' ⋯⟧ = ⟦if h : (↑((fun n ↦ (↑a).seq ↑n) * fun n ↦ (↑b).seq ↑n)).IsCauchy then CauchySequence.mk' ⋯ else 0⟧; All goals completed! 🐙instance Real.instRatCast : RatCast Real where ratCast := fun q ↦ Quotient.mk _ (CauchySequence.mk' (a := fun _ ↦ q) (Sequence.IsCauchy.const q))theorem Real.ratCast_def (q:ℚ) : (q:Real) = LIM (fun _ ↦ q) := q:ℚ⊢ ↑q = LIM fun x ↦ q q:ℚ⊢ ↑q = ⟦CauchySequence.mk' ?m.5⟧q:ℚ⊢ (↑fun x ↦ q).IsCauchy; All goals completed! 🐙

Exercise 5.3.3

@[simp] theorem declaration uses `sorry`Real.ratCast_inj (q r:ℚ) : (q:Real) = (r:Real) ↔ q = r := q:ℚr:ℚ⊢ ↑q = ↑r ↔ q = r All goals completed! 🐙
instance Real.instOfNat {n:ℕ} : OfNat Real n where ofNat := ((n:ℚ):Real)instance Real.instNatCast : NatCast Real where natCast n := ((n:ℚ):Real)@[simp] theorem Real.LIM.zero : LIM (fun _ ↦ (0:ℚ)) = 0 := ⊢ (LIM fun x ↦ 0) = 0 ⊢ ↑0 = 0; All goals completed! 🐙instance Real.instIntCast : IntCast Real where intCast n := ((n:ℚ):Real)

ratCast distributes over addition

theorem declaration uses `sorry`Real.ratCast_add (a b:ℚ) : (a:Real) + (b:Real) = (a+b:ℚ) := a:ℚb:ℚ⊢ ↑a + ↑b = ↑(a + b) All goals completed! 🐙

ratCast distributes over multiplication

theorem declaration uses `sorry`Real.ratCast_mul (a b:ℚ) : (a:Real) * (b:Real) = (a*b:ℚ) := a:ℚb:ℚ⊢ ↑a * ↑b = ↑(a * b) All goals completed! 🐙
noncomputable instance Real.instNeg : Neg Real where neg x := ((-1:ℚ):Real) * x

ratCast commutes with negation

theorem declaration uses `sorry`Real.neg_ratCast (a:ℚ) : -(a:Real) = (-a:ℚ) := a:ℚ⊢ -↑a = ↑(-a) All goals completed! 🐙

It may be possible to omit the IsCauchy hypothesis here.

theorem declaration uses `sorry`Real.neg_LIM (a:ℕ → ℚ) (ha: (a:Sequence).IsCauchy) : -LIM a = LIM (-a) := a:ℕ → ℚha:(↑a).IsCauchy⊢ -LIM a = LIM (-a) All goals completed! 🐙
theorem declaration uses `sorry`Sequence.IsCauchy.neg (a:ℕ → ℚ) (ha: (a:Sequence).IsCauchy) : ((-a:ℕ → ℚ):Sequence).IsCauchy := a:ℕ → ℚha:(↑a).IsCauchy⊢ (↑(-a)).IsCauchy All goals completed! 🐙

Proposition 5.3.11 (laws of algebra)

noncomputable instance declaration uses `sorry`Real.addGroup_inst : AddGroup Real := AddGroup.ofLeftAxioms (⊢ ∀ (a b c : Real), a + b + c = a + (b + c) All goals completed! 🐙) (⊢ ∀ (a : Real), 0 + a = a All goals completed! 🐙) (⊢ ∀ (a : Real), -a + a = 0 All goals completed! 🐙)
theorem Real.sub_eq_add_neg (x y:Real) : x - y = x + (-y) := rfltheorem declaration uses `sorry`Sequence.IsCauchy.sub {a b:ℕ → ℚ} (ha: (a:Sequence).IsCauchy) (hb: (b:Sequence).IsCauchy) : ((a-b:ℕ → ℚ):Sequence).IsCauchy := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ (↑(a - b)).IsCauchy All goals completed! 🐙

LIM distributes over subtraction

theorem declaration uses `sorry`Real.LIM_sub {a b:ℕ → ℚ} (ha: (a:Sequence).IsCauchy) (hb: (b:Sequence).IsCauchy) : LIM a - LIM b = LIM (a - b) := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ LIM a - LIM b = LIM (a - b) All goals completed! 🐙

ratCast distributes over subtraction

theorem declaration uses `sorry`Real.ratCast_sub (a b:ℚ) : (a:Real) - (b:Real) = (a-b:ℚ) := a:ℚb:ℚ⊢ ↑a - ↑b = ↑(a - b) All goals completed! 🐙

Proposition 5.3.11 (laws of algebra)

noncomputable instance declaration uses `sorry`Real.instAddCommGroup : AddCommGroup Real where add_comm := ⊢ ∀ (a b : Real), a + b = b + a All goals completed! 🐙

Proposition 5.3.11 (laws of algebra)

noncomputable instance declaration uses `sorry`Real.instCommMonoid : CommMonoid Real where mul_comm := ⊢ ∀ (a b : Real), a * b = b * a All goals completed! 🐙 mul_assoc := ⊢ ∀ (a b c : Real), a * b * c = a * (b * c) All goals completed! 🐙 one_mul := ⊢ ∀ (a : Real), 1 * a = a All goals completed! 🐙 mul_one := ⊢ ∀ (a : Real), a * 1 = a All goals completed! 🐙

Proposition 5.3.11 (laws of algebra)

noncomputable instance declaration uses `sorry`Real.instCommRing : CommRing Real where left_distrib := ⊢ ∀ (a b c : Real), a * (b + c) = a * b + a * c All goals completed! 🐙 right_distrib := ⊢ ∀ (a b c : Real), (a + b) * c = a * c + b * c All goals completed! 🐙 zero_mul := ⊢ ∀ (a : Real), 0 * a = 0 All goals completed! 🐙 mul_zero := ⊢ ∀ (a : Real), a * 0 = 0 All goals completed! 🐙 mul_assoc := ⊢ ∀ (a b c : Real), a * b * c = a * (b * c) All goals completed! 🐙 natCast_succ := ⊢ ∀ (n : ℕ), ↑(n + 1) = ↑n + 1 All goals completed! 🐙 intCast_negSucc := ⊢ ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1) All goals completed! 🐙
abbrev declaration uses `sorry`Real.ratCast_hom : ℚ →+* Real where toFun := RatCast.ratCast map_zero' := ⊢ RatCast.ratCast 0 = 0 All goals completed! 🐙 map_one' := ⊢ RatCast.ratCast 1 = 1 All goals completed! 🐙 map_add' := ⊢ ∀ (x y : ℚ), RatCast.ratCast (x + y) = RatCast.ratCast x + RatCast.ratCast y All goals completed! 🐙 map_mul' := ⊢ ∀ (x y : ℚ), RatCast.ratCast (x * y) = RatCast.ratCast x * RatCast.ratCast y All goals completed! 🐙

Definition 5.3.12 (sequences bounded away from zero). Sequences are indexed to start from zero as this is more convenient for Mathlib purposes.

abbrev BoundedAwayZero (a:ℕ → ℚ) : Prop := ∃ (c:ℚ), c > 0 ∧ ∀ n, |a n| ≥ c
theorem bounded_away_zero_def (a:ℕ → ℚ) : BoundedAwayZero a ↔ ∃ (c:ℚ), c > 0 ∧ ∀ n, |a n| ≥ c := a:ℕ → ℚ⊢ BoundedAwayZero a ↔ ∃ c > 0, ∀ (n : ℕ), |a n| ≥ c All goals completed! 🐙/-- Examples 5.3.13 -/ example : BoundedAwayZero (fun n ↦ (-1)^n) := ⊢ BoundedAwayZero fun n ↦ (-1) ^ n ⊢ 1 > 0 ∧ ∀ (n : ℕ), |(fun n ↦ (-1) ^ n) n| ≥ 1; All goals completed! 🐙/-- Examples 5.3.13 -/ declaration uses `sorry`example : ¬ BoundedAwayZero (fun n ↦ 10^(-(n:ℤ)-1)) := ⊢ ¬BoundedAwayZero fun n ↦ 10 ^ (-↑n - 1) All goals completed! 🐙/-- Examples 5.3.13 -/ declaration uses `sorry`example : ¬ BoundedAwayZero (fun n ↦ 1 - 10^(-(n:ℤ))) := ⊢ ¬BoundedAwayZero fun n ↦ 1 - 10 ^ (-↑n) All goals completed! 🐙/-- Examples 5.3.13 -/ example : BoundedAwayZero (fun n ↦ 10^(n+1)) := ⊢ BoundedAwayZero fun n ↦ 10 ^ (n + 1) use 1, ⊢ 1 > 0 All goals completed! 🐙 n:ℕ⊢ |(fun n ↦ 10 ^ (n + 1)) n| ≥ 1; n:ℕ⊢ |10 ^ (n + 1)| ≥ 1 n:ℕ⊢ 10 ^ (n + 1) ≥ 10 ^ 0 n:ℕ⊢ 1 ≤ 10n:ℕ⊢ 0 ≤ n + 1 n:ℕ⊢ 1 ≤ 10n:ℕ⊢ 0 ≤ n + 1 All goals completed! 🐙/-- Examples 5.3.13 -/ declaration uses `sorry`example : ¬ ((fun (n:ℕ) ↦ (10:ℚ)^(n+1)):Sequence).IsBounded := ⊢ ¬(↑fun n ↦ 10 ^ (n + 1)).IsBounded All goals completed! 🐙

Lemma 5.3.14

theorem declaration uses `sorry`Real.boundedAwayZero_of_nonzero {x:Real} (hx: x ≠ 0) : ∃ a:ℕ → ℚ, (a:Sequence).IsCauchy ∧ BoundedAwayZero a ∧ x = LIM a := x:Realhx:x ≠ 0⊢ ∃ a, (↑a).IsCauchy ∧ BoundedAwayZero a ∧ x = LIM a -- This proof is written to follow the structure of the original text. b:ℕ → ℚhb:(↑b).IsCauchyhx:LIM b ≠ 0⊢ ∃ a, (↑a).IsCauchy ∧ BoundedAwayZero a ∧ LIM b = LIM a b:ℕ → ℚhb:(↑b).IsCauchyhx:¬LIM b = LIM fun x ↦ 0⊢ ∃ a, (↑a).IsCauchy ∧ BoundedAwayZero a ∧ LIM b = LIM a b:ℕ → ℚhb:(↑b).IsCauchyhx:¬∀ ε > 0, ∃ N, ∀ n ≥ N, |b n - 0| ≤ ε⊢ ∃ a, (↑a).IsCauchy ∧ BoundedAwayZero a ∧ LIM b = LIM a b:ℕ → ℚhb:(↑b).IsCauchyhx:∃ x, 0 < x ∧ ∀ (x_1 : ℕ), ∃ x_2, x_1 ≤ x_2 ∧ x < |b x_2|⊢ ∃ a, (↑a).IsCauchy ∧ BoundedAwayZero a ∧ LIM b = LIM a b:ℕ → ℚhb:(↑b).IsCauchyε:ℚhε:0 < εhx:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|⊢ ∃ a, (↑a).IsCauchy ∧ BoundedAwayZero a ∧ LIM b = LIM a b:ℕ → ℚhb:(↑b).IsCauchyε:ℚhε:0 < εhx:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ ε / 2⊢ ∃ a, (↑a).IsCauchy ∧ BoundedAwayZero a ∧ LIM b = LIM a b:ℕ → ℚhb:(↑b).IsCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|⊢ ∃ a, (↑a).IsCauchy ∧ BoundedAwayZero a ∧ LIM b = LIM a have how : ∀ j ≥ N, |b j| ≥ ε/2 := x:Realhx:x ≠ 0⊢ ∃ a, (↑a).IsCauchy ∧ BoundedAwayZero a ∧ x = LIM a All goals completed! 🐙 b:ℕ → ℚhb:(↑b).IsCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n ↦ if n < n₀ then ε / 2 else b n⊢ ∃ a, (↑a).IsCauchy ∧ BoundedAwayZero a ∧ LIM b = LIM a have not_hard : Sequence.Equiv a b := x:Realhx:x ≠ 0⊢ ∃ a, (↑a).IsCauchy ∧ BoundedAwayZero a ∧ x = LIM a All goals completed! 🐙 b:ℕ → ℚhb:(↑b).IsCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n ↦ if n < n₀ then ε / 2 else b nnot_hard:Sequence.Equiv a bha:(↑a).IsCauchy⊢ ∃ a, (↑a).IsCauchy ∧ BoundedAwayZero a ∧ LIM b = LIM a refine ⟨ a, ha, ?_, b:ℕ → ℚhb:(↑b).IsCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n ↦ if n < n₀ then ε / 2 else b nnot_hard:Sequence.Equiv a bha:(↑a).IsCauchy⊢ LIM b = LIM a All goals completed! 🐙 ⟩ b:ℕ → ℚhb:(↑b).IsCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n ↦ if n < n₀ then ε / 2 else b nnot_hard:Sequence.Equiv a bha:(↑a).IsCauchy⊢ ∃ c > 0, ∀ (n : ℕ), |a n| ≥ c b:ℕ → ℚhb:(↑b).IsCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n ↦ if n < n₀ then ε / 2 else b nnot_hard:Sequence.Equiv a bha:(↑a).IsCauchy⊢ ∀ (n : ℕ), |a n| ≥ ε / 2 b:ℕ → ℚhb:(↑b).IsCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n ↦ if n < n₀ then ε / 2 else b nnot_hard:Sequence.Equiv a bha:(↑a).IsCauchyn:ℕ⊢ |a n| ≥ ε / 2; b:ℕ → ℚhb:(↑b).IsCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n ↦ if n < n₀ then ε / 2 else b nnot_hard:Sequence.Equiv a bha:(↑a).IsCauchyn:ℕhn:n < n₀⊢ |a n| ≥ ε / 2b:ℕ → ℚhb:(↑b).IsCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n ↦ if n < n₀ then ε / 2 else b nnot_hard:Sequence.Equiv a bha:(↑a).IsCauchyn:ℕhn:¬n < n₀⊢ |a n| ≥ ε / 2 b:ℕ → ℚhb:(↑b).IsCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n ↦ if n < n₀ then ε / 2 else b nnot_hard:Sequence.Equiv a bha:(↑a).IsCauchyn:ℕhn:n < n₀⊢ |a n| ≥ ε / 2b:ℕ → ℚhb:(↑b).IsCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n ↦ if n < n₀ then ε / 2 else b nnot_hard:Sequence.Equiv a bha:(↑a).IsCauchyn:ℕhn:¬n < n₀⊢ |a n| ≥ ε / 2 b:ℕ → ℚhb:(↑b).IsCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n ↦ if n < n₀ then ε / 2 else b nnot_hard:Sequence.Equiv a bha:(↑a).IsCauchyn:ℕhn:¬n < n₀⊢ ε / 2 ≤ |b n| All goals completed! 🐙

This result was not explicitly stated in the text, but is needed in the theory. It's a good exercise, so I'm setting it as such.

theorem declaration uses `sorry`Real.lim_of_boundedAwayZero {a:ℕ → ℚ} (ha: BoundedAwayZero a) (ha_cauchy: (a:Sequence).IsCauchy) : LIM a ≠ 0 := a:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchy⊢ LIM a ≠ 0 All goals completed! 🐙
theorem Real.nonzero_of_boundedAwayZero {a:ℕ → ℚ} (ha: BoundedAwayZero a) (n: ℕ) : a n ≠ 0 := a:ℕ → ℚha:BoundedAwayZero an:ℕ⊢ a n ≠ 0 a:ℕ → ℚn:ℕc:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ c⊢ a n ≠ 0; a:ℕ → ℚn:ℕc:ℚhc:c > 0ha:|a n| ≥ c⊢ a n ≠ 0; a:ℕ → ℚn:ℕc:ℚhc:c > 0ha:a n = 0⊢ |a n| < c; All goals completed! 🐙

Lemma 5.3.15

theorem Real.inv_isCauchy_of_boundedAwayZero {a:ℕ → ℚ} (ha: BoundedAwayZero a) (ha_cauchy: (a:Sequence).IsCauchy) : ((a⁻¹:ℕ → ℚ):Sequence).IsCauchy := a:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchy⊢ (↑a⁻¹).IsCauchy -- This proof is written to follow the structure of the original text. a:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchyha':∀ (n : ℕ), a n ≠ 0⊢ (↑a⁻¹).IsCauchy a:ℕ → ℚha:∃ c > 0, ∀ (n : ℕ), |a n| ≥ cha_cauchy:(↑a).IsCauchyha':∀ (n : ℕ), a n ≠ 0⊢ (↑a⁻¹).IsCauchy; a:ℕ → ℚha_cauchy:(↑a).IsCauchyha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ c⊢ (↑a⁻¹).IsCauchy simp_rw a:ℕ → ℚha_cauchy:(↑a).IsCauchyha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ c⊢ (↑a⁻¹).IsCauchySequence.IsCauchy.coe, Section_4_3.dist_eq] at ha_cauchy ⊢ intro ε a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cha_cauchy:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ εε:ℚhε:ε > 0⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a⁻¹ j - a⁻¹ k| ≤ ε; specialize ha_cauchy (c^2 * ε) (a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cha_cauchy:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ εε:ℚhε:ε > 0⊢ c ^ 2 * ε > 0 All goals completed! 🐙) a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕha_cauchy:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ c ^ 2 * ε⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a⁻¹ j - a⁻¹ k| ≤ ε; a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕha_cauchy:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ c ^ 2 * ε⊢ ∀ j ≥ N, ∀ k ≥ N, |a⁻¹ j - a⁻¹ k| ≤ ε; a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕha_cauchy✝:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ c ^ 2 * εn:ℕhn:n ≥ Nm:ℕhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ |a⁻¹ n - a⁻¹ m| ≤ ε calc _ = |(a m - a n) / (a m * a n)| := a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕha_cauchy✝:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ c ^ 2 * εn:ℕhn:n ≥ Nm:ℕhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ |a⁻¹ n - a⁻¹ m| = |(a m - a n) / (a m * a n)| a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕha_cauchy✝:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ c ^ 2 * εn:ℕhn:n ≥ Nm:ℕhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ a⁻¹ n - a⁻¹ m = (a m - a n) / (a m * a n); a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕha_cauchy✝:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ c ^ 2 * εn:ℕhn:n ≥ Nm:ℕhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ (a n)⁻¹ - (a m)⁻¹ = (a m - a n) / (a m * a n); All goals completed! 🐙 _ ≤ |a m - a n| / c^2 := a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕha_cauchy✝:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ c ^ 2 * εn:ℕhn:n ≥ Nm:ℕhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ |(a m - a n) / (a m * a n)| ≤ |a m - a n| / c ^ 2 a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕha_cauchy✝:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ c ^ 2 * εn:ℕhn:n ≥ Nm:ℕhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ |a m - a n| / (|a m| * |a n|) ≤ |a m - a n| / (c * c); a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕha_cauchy✝:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ c ^ 2 * εn:ℕhn:n ≥ Nm:ℕhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ c ≤ |a m|a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕha_cauchy✝:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ c ^ 2 * εn:ℕhn:n ≥ Nm:ℕhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ c ≤ |a n| a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕha_cauchy✝:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ c ^ 2 * εn:ℕhn:n ≥ Nm:ℕhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ c ≤ |a m|a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕha_cauchy✝:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ c ^ 2 * εn:ℕhn:n ≥ Nm:ℕhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ c ≤ |a n| All goals completed! 🐙 _ = |a n - a m| / c^2 := a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕha_cauchy✝:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ c ^ 2 * εn:ℕhn:n ≥ Nm:ℕhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ |a m - a n| / c ^ 2 = |a n - a m| / c ^ 2 All goals completed! 🐙 _ ≤ (c^2 * ε) / c^2 := a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕha_cauchy✝:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ c ^ 2 * εn:ℕhn:n ≥ Nm:ℕhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ |a n - a m| / c ^ 2 ≤ c ^ 2 * ε / c ^ 2 All goals completed! 🐙 _ = ε := a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕha_cauchy✝:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ c ^ 2 * εn:ℕhn:n ≥ Nm:ℕhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ c ^ 2 * ε / c ^ 2 = ε All goals completed! 🐙

Lemma 5.3.17 (Reciprocation is well-defined)

theorem Real.inv_of_equiv {a b:ℕ → ℚ} (ha: BoundedAwayZero a) (ha_cauchy: (a:Sequence).IsCauchy) (hb: BoundedAwayZero b) (hb_cauchy: (b:Sequence).IsCauchy) (hlim: LIM a = LIM b) : LIM a⁻¹ = LIM b⁻¹ := a:ℕ → ℚb:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchyhb:BoundedAwayZero bhb_cauchy:(↑b).IsCauchyhlim:LIM a = LIM b⊢ LIM a⁻¹ = LIM b⁻¹ -- This proof is written to follow the structure of the original text. a:ℕ → ℚb:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchyhb:BoundedAwayZero bhb_cauchy:(↑b).IsCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹⊢ LIM a⁻¹ = LIM b⁻¹ a:ℕ → ℚb:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchyhb:BoundedAwayZero bhb_cauchy:(↑b).IsCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹hainv_cauchy:(↑a⁻¹).IsCauchy⊢ LIM a⁻¹ = LIM b⁻¹ a:ℕ → ℚb:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchyhb:BoundedAwayZero bhb_cauchy:(↑b).IsCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹hainv_cauchy:(↑a⁻¹).IsCauchyhbinv_cauchy:(↑b⁻¹).IsCauchy⊢ LIM a⁻¹ = LIM b⁻¹ a:ℕ → ℚb:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchyhb:BoundedAwayZero bhb_cauchy:(↑b).IsCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹hainv_cauchy:(↑a⁻¹).IsCauchyhbinv_cauchy:(↑b⁻¹).IsCauchyhaainv_cauchy:(↑(a⁻¹ * a)).IsCauchy⊢ LIM a⁻¹ = LIM b⁻¹ a:ℕ → ℚb:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchyhb:BoundedAwayZero bhb_cauchy:(↑b).IsCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹hainv_cauchy:(↑a⁻¹).IsCauchyhbinv_cauchy:(↑b⁻¹).IsCauchyhaainv_cauchy:(↑(a⁻¹ * a)).IsCauchyhabinv_cauchy:(↑(a⁻¹ * b)).IsCauchy⊢ LIM a⁻¹ = LIM b⁻¹ have claim1 : P = LIM b⁻¹ := a:ℕ → ℚb:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchyhb:BoundedAwayZero bhb_cauchy:(↑b).IsCauchyhlim:LIM a = LIM b⊢ LIM a⁻¹ = LIM b⁻¹ a:ℕ → ℚb:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchyhb:BoundedAwayZero bhb_cauchy:(↑b).IsCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹hainv_cauchy:(↑a⁻¹).IsCauchyhbinv_cauchy:(↑b⁻¹).IsCauchyhaainv_cauchy:(↑(a⁻¹ * a)).IsCauchyhabinv_cauchy:(↑(a⁻¹ * b)).IsCauchy⊢ LIM (a⁻¹ * a * b⁻¹) = LIM b⁻¹ a:ℕ → ℚb:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchyhb:BoundedAwayZero bhb_cauchy:(↑b).IsCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹hainv_cauchy:(↑a⁻¹).IsCauchyhbinv_cauchy:(↑b⁻¹).IsCauchyhaainv_cauchy:(↑(a⁻¹ * a)).IsCauchyhabinv_cauchy:(↑(a⁻¹ * b)).IsCauchyn:ℕ⊢ (a⁻¹ * a * b⁻¹) n = b⁻¹ n; All goals completed! 🐙 have claim2 : P = LIM a⁻¹ := a:ℕ → ℚb:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchyhb:BoundedAwayZero bhb_cauchy:(↑b).IsCauchyhlim:LIM a = LIM b⊢ LIM a⁻¹ = LIM b⁻¹ a:ℕ → ℚb:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchyhb:BoundedAwayZero bhb_cauchy:(↑b).IsCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹hainv_cauchy:(↑a⁻¹).IsCauchyhbinv_cauchy:(↑b⁻¹).IsCauchyhaainv_cauchy:(↑(a⁻¹ * a)).IsCauchyhabinv_cauchy:(↑(a⁻¹ * b)).IsCauchyclaim1:P = LIM b⁻¹⊢ LIM (a⁻¹ * b * b⁻¹) = LIM a⁻¹ a:ℕ → ℚb:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchyhb:BoundedAwayZero bhb_cauchy:(↑b).IsCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹hainv_cauchy:(↑a⁻¹).IsCauchyhbinv_cauchy:(↑b⁻¹).IsCauchyhaainv_cauchy:(↑(a⁻¹ * a)).IsCauchyhabinv_cauchy:(↑(a⁻¹ * b)).IsCauchyclaim1:P = LIM b⁻¹n:ℕ⊢ (a⁻¹ * b * b⁻¹) n = a⁻¹ n; All goals completed! 🐙 All goals completed! 🐙

Definition 5.3.16 (Reciprocation of real numbers). Requires classical logic because we need to assign a "junk" value to the inverse of 0.

open Classical innoncomputable instance Real.instInv : Inv Real where inv x := if h: x ≠ 0 then LIM (boundedAwayZero_of_nonzero h).choose⁻¹ else 0
theorem Real.inv_def {a:ℕ → ℚ} (h: BoundedAwayZero a) (hc: (a:Sequence).IsCauchy) : (LIM a)⁻¹ = LIM a⁻¹ := a:ℕ → ℚh:BoundedAwayZero ahc:(↑a).IsCauchy⊢ (LIM a)⁻¹ = LIM a⁻¹ a:ℕ → ℚh:BoundedAwayZero ahc:(↑a).IsCauchyhx:LIM a ≠ 0⊢ (LIM a)⁻¹ = LIM a⁻¹ a:ℕ → ℚh:BoundedAwayZero ahc:(↑a).IsCauchyx:Real := LIM ahx:x ≠ 0⊢ x⁻¹ = LIM a⁻¹ a:ℕ → ℚh:BoundedAwayZero ahc:(↑a).IsCauchyx:Real := LIM ahx:x ≠ 0h1:(↑⋯.choose).IsCauchyh2:BoundedAwayZero ⋯.chooseh3:x = LIM ⋯.choose⊢ x⁻¹ = LIM a⁻¹ a:ℕ → ℚh:BoundedAwayZero ahc:(↑a).IsCauchyx:Real := LIM ahx:x ≠ 0h1:(↑⋯.choose).IsCauchyh2:BoundedAwayZero ⋯.chooseh3:x = LIM ⋯.choose⊢ (LIM fun i ↦ (⋯.choose i).inv) = LIM fun i ↦ (a i).inv All goals completed! 🐙@[simp] theorem Real.inv_zero : (0:Real)⁻¹ = 0 := ⊢ 0⁻¹ = 0 All goals completed! 🐙theorem declaration uses `sorry`Real.self_mul_inv {x:Real} (hx: x ≠ 0) : x * x⁻¹ = 1 := x:Realhx:x ≠ 0⊢ x * x⁻¹ = 1 All goals completed! 🐙theorem declaration uses `sorry`Real.inv_mul_self {x:Real} (hx: x ≠ 0) : x⁻¹ * x = 1 := x:Realhx:x ≠ 0⊢ x⁻¹ * x = 1 All goals completed! 🐙lemma BoundedAwayZero.const {q : ℚ} (hq : q ≠ 0) : BoundedAwayZero fun _ ↦ q := q:ℚhq:q ≠ 0⊢ BoundedAwayZero fun x ↦ q q:ℚhq:q ≠ 0⊢ |q| > 0 ∧ ∀ (n : ℕ), |(fun x ↦ q) n| ≥ |q|; All goals completed! 🐙theorem Real.inv_ratCast (q:ℚ) : (q:Real)⁻¹ = (q⁻¹:ℚ) := q:ℚ⊢ (↑q)⁻¹ = ↑q⁻¹ q:ℚh:q = 0⊢ (↑q)⁻¹ = ↑q⁻¹q:ℚh:¬q = 0⊢ (↑q)⁻¹ = ↑q⁻¹ q:ℚh:q = 0⊢ (↑q)⁻¹ = ↑q⁻¹ q:ℚh:q = 0⊢ 0⁻¹ = ↑0⁻¹; q:ℚh:q = 0⊢ 0 = ↑0; All goals completed! 🐙 simp_rw q:ℚh:¬q = 0⊢ (↑q)⁻¹ = ↑q⁻¹ratCast_def, inv_def (BoundedAwayZero.const h) (q:ℚh:¬q = 0⊢ (↑fun x ↦ q).IsCauchy All goals completed! 🐙)]; All goals completed! 🐙

Default definition of division.

noncomputable instance Real.instDivInvMonoid : DivInvMonoid Real where
theorem Real.div_eq (x y:Real) : x/y = x * y⁻¹ := rflnoncomputable instance declaration uses `sorry`Real.instField : Field Real where exists_pair_ne := ⊢ ∃ x y, x ≠ y All goals completed! 🐙 mul_inv_cancel := ⊢ ∀ (a : Real), a ≠ 0 → a * a⁻¹ = 1 All goals completed! 🐙 inv_zero := ⊢ 0⁻¹ = 0 All goals completed! 🐙 ratCast_def := ⊢ ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den All goals completed! 🐙 qsmul := _ nnqsmul := _theorem declaration uses `sorry`Real.mul_right_cancel₀ {x y z:Real} (hz: z ≠ 0) (h: x * z = y * z) : x = y := x:Realy:Realz:Realhz:z ≠ 0h:x * z = y * z⊢ x = y All goals completed! 🐙theorem declaration uses `sorry`Real.mul_right_nocancel : ¬ ∀ (x y z:Real), (hz: z = 0) → (x * z = y * z) → x = y := ⊢ ¬∀ (x y z : Real), z = 0 → x * z = y * z → x = y All goals completed! 🐙

Exercise 5.3.4

theorem declaration uses `sorry`Real.IsBounded.equiv {a b:ℕ → ℚ} (ha: (a:Sequence).IsBounded) (hab: Sequence.Equiv a b) : (b:Sequence).IsBounded := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsBoundedhab:Sequence.Equiv a b⊢ (↑b).IsBounded All goals completed! 🐙

Same as Sequence.­IsCauchy.­harmonic but reindexing the sequence as a₀ = 1, a₁ = 1/2, ... This form is more convenient for the upcoming proof of Theorem 5.5.9.

theorem Sequence.IsCauchy.harmonic' : ((fun n ↦ 1/((n:ℚ)+1): ℕ → ℚ):Sequence).IsCauchy := ⊢ (↑fun n ↦ 1 / (↑n + 1)).IsCauchy ⊢ ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (1 / (↑j + 1)) (1 / (↑k + 1)) ≤ ε; intro ε ε:ℚhε:ε > 0⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (1 / (↑j + 1)) (1 / (↑k + 1)) ≤ ε; ε:ℚhε:ε > 0N:ℤh1:N ≥ 1h2:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' 1 fun n ↦ 1 / ↑↑n).seq j) ((mk' 1 fun n ↦ 1 / ↑↑n).seq k) ≤ ε⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (1 / (↑j + 1)) (1 / (↑k + 1)) ≤ ε ε:ℚhε:ε > 0N:ℤh1:N ≥ 1h2:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' 1 fun n ↦ 1 / ↑↑n).seq j) ((mk' 1 fun n ↦ 1 / ↑↑n).seq k) ≤ ε⊢ ∀ j ≥ N.toNat, ∀ k ≥ N.toNat, Section_4_3.dist (1 / (↑j + 1)) (1 / (↑k + 1)) ≤ ε; intro j ε:ℚhε:ε > 0N:ℤh1:N ≥ 1h2:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' 1 fun n ↦ 1 / ↑↑n).seq j) ((mk' 1 fun n ↦ 1 / ↑↑n).seq k) ≤ εj:ℕa✝:j ≥ N.toNat⊢ ∀ k ≥ N.toNat, Section_4_3.dist (1 / (↑j + 1)) (1 / (↑k + 1)) ≤ ε ε:ℚhε:ε > 0N:ℤh1:N ≥ 1h2:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' 1 fun n ↦ 1 / ↑↑n).seq j) ((mk' 1 fun n ↦ 1 / ↑↑n).seq k) ≤ εj:ℕa✝:j ≥ N.toNatk:ℕ⊢ k ≥ N.toNat → Section_4_3.dist (1 / (↑j + 1)) (1 / (↑k + 1)) ≤ ε ε:ℚhε:ε > 0N:ℤh1:N ≥ 1h2:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' 1 fun n ↦ 1 / ↑↑n).seq j) ((mk' 1 fun n ↦ 1 / ↑↑n).seq k) ≤ εj:ℕa✝¹:j ≥ N.toNatk:ℕa✝:k ≥ N.toNat⊢ Section_4_3.dist (1 / (↑j + 1)) (1 / (↑k + 1)) ≤ ε; ε:ℚhε:ε > 0N:ℤh1:N ≥ 1h2:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' 1 fun n ↦ 1 / ↑↑n).seq j) ((mk' 1 fun n ↦ 1 / ↑↑n).seq k) ≤ εj:ℕa✝¹:j ≥ N.toNatk:ℕa✝:k ≥ N.toNat⊢ ↑j + 1 ≥ Nε:ℚhε:ε > 0N:ℤh1:N ≥ 1h2:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' 1 fun n ↦ 1 / ↑↑n).seq j) ((mk' 1 fun n ↦ 1 / ↑↑n).seq k) ≤ εj:ℕa✝¹:j ≥ N.toNatk:ℕa✝:k ≥ N.toNat⊢ ↑k + 1 ≥ Nε:ℚhε:ε > 0N:ℤh1:N ≥ 1j:ℕa✝¹:j ≥ N.toNatk:ℕa✝:k ≥ N.toNath2:Section_4_3.dist ((mk' 1 fun n ↦ 1 / ↑↑n).seq (↑j + 1)) ((mk' 1 fun n ↦ 1 / ↑↑n).seq (↑k + 1)) ≤ ε⊢ Section_4_3.dist (1 / (↑j + 1)) (1 / (↑k + 1)) ≤ ε ε:ℚhε:ε > 0N:ℤh1:N ≥ 1h2:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' 1 fun n ↦ 1 / ↑↑n).seq j) ((mk' 1 fun n ↦ 1 / ↑↑n).seq k) ≤ εj:ℕa✝¹:j ≥ N.toNatk:ℕa✝:k ≥ N.toNat⊢ ↑j + 1 ≥ Nε:ℚhε:ε > 0N:ℤh1:N ≥ 1h2:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' 1 fun n ↦ 1 / ↑↑n).seq j) ((mk' 1 fun n ↦ 1 / ↑↑n).seq k) ≤ εj:ℕa✝¹:j ≥ N.toNatk:ℕa✝:k ≥ N.toNat⊢ ↑k + 1 ≥ Nε:ℚhε:ε > 0N:ℤh1:N ≥ 1j:ℕa✝¹:j ≥ N.toNatk:ℕa✝:k ≥ N.toNath2:Section_4_3.dist ((mk' 1 fun n ↦ 1 / ↑↑n).seq (↑j + 1)) ((mk' 1 fun n ↦ 1 / ↑↑n).seq (↑k + 1)) ≤ ε⊢ Section_4_3.dist (1 / (↑j + 1)) (1 / (↑k + 1)) ≤ ε try All goals completed! 🐙 All goals completed! 🐙

Exercise 5.3.5

theorem declaration uses `sorry`Real.LIM.harmonic : LIM (fun n ↦ 1/((n:ℚ)+1)) = 0 := ⊢ (LIM fun n ↦ 1 / (↑n + 1)) = 0 All goals completed! 🐙
end Chapter5