The construction of the real numbers

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 : TypeChapter5.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 Cauchy sequence.

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.instSetoidopen Classical in /-- 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. -/ noncomputable 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:?_mvar.71543 := id (congrArg (fun x => x.seq _fvar.71257) _fvar.70786)⊢ 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:?_mvar.72290 := Quotient.exact _fvar.72286⊢ 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) ≤ ε 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) ≤ ε 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:?_mvar.74364 := @_fvar.74087 _fvar.74351 ?_mvar.74365 _fvar.74357 ?_mvar.74366⊢ 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:?_mvar.74364 := @_fvar.74087 _fvar.74351 ?_mvar.74365 _fvar.74357 ?_mvar.74366⊢ 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:?_mvar.74364 := @_fvar.74087 _fvar.74351 ?_mvar.74365 _fvar.74357 ?_mvar.74366h2:?_mvar.74780 := @_fvar.74172 _fvar.74351 ?_mvar.74781 _fvar.74357 ?_mvar.74782⊢ 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:?_mvar.74364 := @_fvar.74087 _fvar.74351 ?_mvar.74365 _fvar.74357 ?_mvar.74366⊢ 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:?_mvar.74364 := @_fvar.74087 _fvar.74351 ?_mvar.74365 _fvar.74357 ?_mvar.74366⊢ 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:?_mvar.74364 := @_fvar.74087 _fvar.74351 ?_mvar.74365 _fvar.74357 ?_mvar.74366h2:?_mvar.74780 := @_fvar.74172 _fvar.74351 ?_mvar.74781 _fvar.74357 ?_mvar.74782⊢ 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:?_mvar.74364 := @_fvar.74087 _fvar.74351 ?_mvar.74365 _fvar.74357 ?_mvar.74366⊢ 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:?_mvar.74364 := @_fvar.74087 _fvar.74351 ?_mvar.74365 _fvar.74357 ?_mvar.74366⊢ k ≥ N2 try All goals completed! 🐙 a:ℕ → ℚb:ℕ → ℚε:ℚN1:ℕN2:ℕj:ℕk:ℕh1:|@_fvar.73887 _fvar.74351 - @_fvar.73887 _fvar.74357| ≤ _fvar.73952 / 2 := @_fvar.74087 _fvar.74351 ?_mvar.74365 _fvar.74357 ?_mvar.74366h2:|@_fvar.73888 _fvar.74351 - @_fvar.73888 _fvar.74357| ≤ _fvar.73952 / 2 := @_fvar.74172 _fvar.74351 ?_mvar.74781 _fvar.74357 ?_mvar.74782ha✝:∀ (ε : ℚ), 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') b:ℕ → ℚb':ℕ → ℚa:ℕ → ℚhbb':Equiv b b'⊢ Equiv (b + a) (b' + a); 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₂ 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) a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ ⟦CauchySequence.mk' ha⟧ + ⟦CauchySequence.mk' hb⟧ = ⟦CauchySequence.mk' ⋯⟧ a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ CauchySequence.mk' ⋯ = if h : (↑((fun n => (CauchySequence.mk' ha).seq ↑n) + fun n => (CauchySequence.mk' hb).seq ↑n)).IsCauchy then CauchySequence.mk' h 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') b:ℕ → ℚb':ℕ → ℚa:ℕ → ℚha:(↑a).IsCauchyhbb':Equiv b b'⊢ Equiv (b * a) (b' * a); 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₂ 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) a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ ⟦CauchySequence.mk' ha⟧ * ⟦CauchySequence.mk' hb⟧ = ⟦CauchySequence.mk' ⋯⟧ a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ CauchySequence.mk' ⋯ = if h : (↑((fun n => (CauchySequence.mk' ha).seq ↑n) * fun n => (CauchySequence.mk' hb).seq ↑n)).IsCauchy then CauchySequence.mk' h 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 Cauchy sequence 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'Real.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'declaration uses 'sorry'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'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'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'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'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'declaration uses 'sorry'declaration uses 'sorry'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 ≥ _fvar.280226, |@_fvar.259327 j| ≥ _fvar.280083 / 2 := ?_mvar.280360a:ℕ → ℚ := fun n => if n < _fvar.280237 then _fvar.280083 / 2 else @_fvar.259327 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 ≥ _fvar.280226, |@_fvar.259327 j| ≥ _fvar.280083 / 2 := ?_mvar.280360a:ℕ → ℚ := fun n => if n < _fvar.280237 then _fvar.280083 / 2 else @_fvar.259327 nnot_hard:Chapter5.Sequence.Equiv _fvar.280457 _fvar.259327 := ?_mvar.280598ha:?_mvar.280609 := (Chapter5.Sequence.isCauchy_of_equiv _fvar.280599).mpr _fvar.259349⊢ ∃ 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 ≥ _fvar.280226, |@_fvar.259327 j| ≥ _fvar.280083 / 2 := sorrya:ℕ → ℚ := fun n => if n < _fvar.280237 then _fvar.280083 / 2 else @_fvar.259327 nnot_hard:Chapter5.Sequence.Equiv _fvar.280457 _fvar.259327 := sorryha:(↑_fvar.280457).IsCauchy := (Chapter5.Sequence.isCauchy_of_equiv _fvar.280599).mpr _fvar.259349⊢ 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 ≥ _fvar.280226, |@_fvar.259327 j| ≥ _fvar.280083 / 2 := ?_mvar.280360a:ℕ → ℚ := fun n => if n < _fvar.280237 then _fvar.280083 / 2 else @_fvar.259327 nnot_hard:Chapter5.Sequence.Equiv _fvar.280457 _fvar.259327 := ?_mvar.280598ha:?_mvar.280609 := (Chapter5.Sequence.isCauchy_of_equiv _fvar.280599).mpr _fvar.259349⊢ ∃ 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 ≥ _fvar.280226, |@_fvar.259327 j| ≥ _fvar.280083 / 2 := ?_mvar.280360a:ℕ → ℚ := fun n => if n < _fvar.280237 then _fvar.280083 / 2 else @_fvar.259327 nnot_hard:Chapter5.Sequence.Equiv _fvar.280457 _fvar.259327 := ?_mvar.280598ha:?_mvar.280609 := (Chapter5.Sequence.isCauchy_of_equiv _fvar.280599).mpr _fvar.259349⊢ ∀ (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 ≥ _fvar.280226, |@_fvar.259327 j| ≥ _fvar.280083 / 2 := ?_mvar.280360a:ℕ → ℚ := fun n => if n < _fvar.280237 then _fvar.280083 / 2 else @_fvar.259327 nnot_hard:Chapter5.Sequence.Equiv _fvar.280457 _fvar.259327 := ?_mvar.280598ha:?_mvar.280609 := (Chapter5.Sequence.isCauchy_of_equiv _fvar.280599).mpr _fvar.259349n:ℕ⊢ |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 ≥ _fvar.280226, |@_fvar.259327 j| ≥ _fvar.280083 / 2 := ?_mvar.280360a:ℕ → ℚ := fun n => if n < _fvar.280237 then _fvar.280083 / 2 else @_fvar.259327 nnot_hard:Chapter5.Sequence.Equiv _fvar.280457 _fvar.259327 := ?_mvar.280598ha:?_mvar.280609 := (Chapter5.Sequence.isCauchy_of_equiv _fvar.280599).mpr _fvar.259349n:ℕ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 ≥ _fvar.280226, |@_fvar.259327 j| ≥ _fvar.280083 / 2 := ?_mvar.280360a:ℕ → ℚ := fun n => if n < _fvar.280237 then _fvar.280083 / 2 else @_fvar.259327 nnot_hard:Chapter5.Sequence.Equiv _fvar.280457 _fvar.259327 := ?_mvar.280598ha:?_mvar.280609 := (Chapter5.Sequence.isCauchy_of_equiv _fvar.280599).mpr _fvar.259349n:ℕ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 ≥ _fvar.280226, |@_fvar.259327 j| ≥ _fvar.280083 / 2 := ?_mvar.280360a:ℕ → ℚ := fun n => if n < _fvar.280237 then _fvar.280083 / 2 else @_fvar.259327 nnot_hard:Chapter5.Sequence.Equiv _fvar.280457 _fvar.259327 := ?_mvar.280598ha:?_mvar.280609 := (Chapter5.Sequence.isCauchy_of_equiv _fvar.280599).mpr _fvar.259349n:ℕ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 ≥ _fvar.280226, |@_fvar.259327 j| ≥ _fvar.280083 / 2 := ?_mvar.280360a:ℕ → ℚ := fun n => if n < _fvar.280237 then _fvar.280083 / 2 else @_fvar.259327 nnot_hard:Chapter5.Sequence.Equiv _fvar.280457 _fvar.259327 := ?_mvar.280598ha:?_mvar.280609 := (Chapter5.Sequence.isCauchy_of_equiv _fvar.280599).mpr _fvar.259349n:ℕ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 ≥ _fvar.280226, |@_fvar.259327 j| ≥ _fvar.280083 / 2 := ?_mvar.280360a:ℕ → ℚ := fun n => if n < _fvar.280237 then _fvar.280083 / 2 else @_fvar.259327 nnot_hard:Chapter5.Sequence.Equiv _fvar.280457 _fvar.259327 := ?_mvar.280598ha:?_mvar.280609 := (Chapter5.Sequence.isCauchy_of_equiv _fvar.280599).mpr _fvar.259349n:ℕ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 : ℕ), @_fvar.291418 n ≠ 0 := fun n => Chapter5.Real.nonzero_of_boundedAwayZero _fvar.291419 n⊢ (↑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 a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cha_cauchy:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε⊢ ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a⁻¹ j - a⁻¹ k| ≤ ε 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 m * a n = a n * a m ∨ a m - a n = 0; 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:Chapter5.Real := Chapter5.LIM _fvar.344091⁻¹ * Chapter5.LIM _fvar.344091 * Chapter5.LIM _fvar.344092⁻¹⊢ LIM a⁻¹ = LIM b⁻¹ a:ℕ → ℚb:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchyhb:BoundedAwayZero bhb_cauchy:(↑b).IsCauchyhlim:LIM a = LIM bP:Chapter5.Real := Chapter5.LIM _fvar.344091⁻¹ * Chapter5.LIM _fvar.344091 * Chapter5.LIM _fvar.344092⁻¹hainv_cauchy:?_mvar.344453 := Chapter5.Real.inv_isCauchy_of_boundedAwayZero _fvar.344093 _fvar.344094⊢ LIM a⁻¹ = LIM b⁻¹ a:ℕ → ℚb:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchyhb:BoundedAwayZero bhb_cauchy:(↑b).IsCauchyhlim:LIM a = LIM bP:Chapter5.Real := Chapter5.LIM _fvar.344091⁻¹ * Chapter5.LIM _fvar.344091 * Chapter5.LIM _fvar.344092⁻¹hainv_cauchy:?_mvar.344453 := Chapter5.Real.inv_isCauchy_of_boundedAwayZero _fvar.344093 _fvar.344094hbinv_cauchy:?_mvar.344472 := Chapter5.Real.inv_isCauchy_of_boundedAwayZero _fvar.344095 _fvar.344096⊢ LIM a⁻¹ = LIM b⁻¹ a:ℕ → ℚb:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchyhb:BoundedAwayZero bhb_cauchy:(↑b).IsCauchyhlim:LIM a = LIM bP:Chapter5.Real := Chapter5.LIM _fvar.344091⁻¹ * Chapter5.LIM _fvar.344091 * Chapter5.LIM _fvar.344092⁻¹hainv_cauchy:?_mvar.344453 := Chapter5.Real.inv_isCauchy_of_boundedAwayZero _fvar.344093 _fvar.344094hbinv_cauchy:?_mvar.344472 := Chapter5.Real.inv_isCauchy_of_boundedAwayZero _fvar.344095 _fvar.344096haainv_cauchy:?_mvar.344489 := Chapter5.Sequence.IsCauchy.mul _fvar.344463 _fvar.344094⊢ LIM a⁻¹ = LIM b⁻¹ a:ℕ → ℚb:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchyhb:BoundedAwayZero bhb_cauchy:(↑b).IsCauchyhlim:LIM a = LIM bP:Chapter5.Real := Chapter5.LIM _fvar.344091⁻¹ * Chapter5.LIM _fvar.344091 * Chapter5.LIM _fvar.344092⁻¹hainv_cauchy:?_mvar.344453 := Chapter5.Real.inv_isCauchy_of_boundedAwayZero _fvar.344093 _fvar.344094hbinv_cauchy:?_mvar.344472 := Chapter5.Real.inv_isCauchy_of_boundedAwayZero _fvar.344095 _fvar.344096haainv_cauchy:?_mvar.344489 := Chapter5.Sequence.IsCauchy.mul _fvar.344463 _fvar.344094habinv_cauchy:?_mvar.344514 := Chapter5.Sequence.IsCauchy.mul _fvar.344463 _fvar.344096⊢ 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:Chapter5.Real := Chapter5.LIM _fvar.344091⁻¹ * Chapter5.LIM _fvar.344091 * Chapter5.LIM _fvar.344092⁻¹hainv_cauchy:?_mvar.344453 := Chapter5.Real.inv_isCauchy_of_boundedAwayZero _fvar.344093 _fvar.344094hbinv_cauchy:?_mvar.344472 := Chapter5.Real.inv_isCauchy_of_boundedAwayZero _fvar.344095 _fvar.344096haainv_cauchy:?_mvar.344489 := Chapter5.Sequence.IsCauchy.mul _fvar.344463 _fvar.344094habinv_cauchy:?_mvar.344514 := Chapter5.Sequence.IsCauchy.mul _fvar.344463 _fvar.344096⊢ LIM (a⁻¹ * a * b⁻¹) = LIM b⁻¹ a:ℕ → ℚb:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchyhb:BoundedAwayZero bhb_cauchy:(↑b).IsCauchyhlim:LIM a = LIM bP:Chapter5.Real := Chapter5.LIM _fvar.344091⁻¹ * Chapter5.LIM _fvar.344091 * Chapter5.LIM _fvar.344092⁻¹hainv_cauchy:?_mvar.344453 := Chapter5.Real.inv_isCauchy_of_boundedAwayZero _fvar.344093 _fvar.344094hbinv_cauchy:?_mvar.344472 := Chapter5.Real.inv_isCauchy_of_boundedAwayZero _fvar.344095 _fvar.344096haainv_cauchy:?_mvar.344489 := Chapter5.Sequence.IsCauchy.mul _fvar.344463 _fvar.344094habinv_cauchy:?_mvar.344514 := Chapter5.Sequence.IsCauchy.mul _fvar.344463 _fvar.344096n:ℕ⊢ (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:Chapter5.Real := Chapter5.LIM _fvar.344091⁻¹ * Chapter5.LIM _fvar.344091 * Chapter5.LIM _fvar.344092⁻¹hainv_cauchy:?_mvar.344453 := Chapter5.Real.inv_isCauchy_of_boundedAwayZero _fvar.344093 _fvar.344094hbinv_cauchy:?_mvar.344472 := Chapter5.Real.inv_isCauchy_of_boundedAwayZero _fvar.344095 _fvar.344096haainv_cauchy:?_mvar.344489 := Chapter5.Sequence.IsCauchy.mul _fvar.344463 _fvar.344094habinv_cauchy:?_mvar.344514 := Chapter5.Sequence.IsCauchy.mul _fvar.344463 _fvar.344096claim1:_fvar.344363 = Chapter5.LIM _fvar.344092⁻¹ := ?_mvar.344613⊢ LIM (a⁻¹ * b * b⁻¹) = LIM a⁻¹ a:ℕ → ℚb:ℕ → ℚha:BoundedAwayZero aha_cauchy:(↑a).IsCauchyhb:BoundedAwayZero bhb_cauchy:(↑b).IsCauchyhlim:LIM a = LIM bP:Chapter5.Real := Chapter5.LIM _fvar.344091⁻¹ * Chapter5.LIM _fvar.344091 * Chapter5.LIM _fvar.344092⁻¹hainv_cauchy:?_mvar.344453 := Chapter5.Real.inv_isCauchy_of_boundedAwayZero _fvar.344093 _fvar.344094hbinv_cauchy:?_mvar.344472 := Chapter5.Real.inv_isCauchy_of_boundedAwayZero _fvar.344095 _fvar.344096haainv_cauchy:?_mvar.344489 := Chapter5.Sequence.IsCauchy.mul _fvar.344463 _fvar.344094habinv_cauchy:?_mvar.344514 := Chapter5.Sequence.IsCauchy.mul _fvar.344463 _fvar.344096claim1:_fvar.344363 = Chapter5.LIM _fvar.344092⁻¹ := ?_mvar.344613n:ℕ⊢ (a⁻¹ * b * b⁻¹) n = a⁻¹ n; All goals completed! 🐙 All goals completed! 🐙
open Classical in /-- Definition 5.3.16 (Reciprocation of real numbers). Requires classical logic because we need to assign a "junk" value to the inverse of 0. -/ noncomputable instance Real.instInv : Inv Real where inv x := if h: x ≠ 0 then LIM (boundedAwayZero_of_nonzero h).choose⁻¹ else 0theorem 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:Chapter5.Real := Chapter5.LIM _fvar.371055hx:x ≠ 0⊢ x⁻¹ = LIM a⁻¹ a:ℕ → ℚh:BoundedAwayZero ahc:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.371055hx:x ≠ 0h1:(↑⋯.choose).IsCauchyh2:BoundedAwayZero ⋯.chooseh3:x = LIM ⋯.choose⊢ x⁻¹ = LIM a⁻¹ a:ℕ → ℚh:BoundedAwayZero ahc:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.371055hx:x ≠ 0h1:(↑⋯.choose).IsCauchyh2:BoundedAwayZero ⋯.chooseh3:x = LIM ⋯.choose⊢ LIM ⋯.choose⁻¹ = LIM a⁻¹ 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 [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'declaration uses 'sorry'declaration uses 'sorry'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 Chapter5.Sequence.IsCauchy.harmonic : (Sequence.mk' 1 fun n => 1 / ↑↑n).IsCauchySequence.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)) ≤ ε; ε:ℚ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)) ≤ ε; ε:ℚ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