The construction of the real numbers

Аналіз I, Розділ 5.3: Побудова дійсних чисел

Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

  • Поняття формального границі послідовності Коші.

  • Побудова типу дійсних чисел Chapter5.Real : TypeChapter5.Real.

  • Базові арифметичні операції та властивості.

Підказки від попередніх користувачів

Користувачі супровідного матеріалу, які виконали вправи в цьому розділі, можуть надсилати свої поради майбутнім користувачам цього розділу як PRи.

  • (Додайте підказку тут)

namespace Chapter5

Клас послідовностей Коші, що починаються з нуля

@[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! 🐙

Послідовність, що починається з нуля і є Коші, можна розглядати як послідовність Коші.

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! 🐙

Твердження 5.3.3 / Вправа 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! 🐙

Твердження 5.3.3 / Вправа 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! 🐙

Будь-яка стала послідовність є послідовністю Коші.

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 /-- У Lean зручно присвоювати "порожнє" значення 0 для `LIM a`, коли `a` не є послідовністю Коші. Це вимагає класичної логіки, оскільки властивість бути послідовністю Коші не є обчислюваною або вирішуваною. -/ 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! 🐙

Визначення 5.3.1 (Дійсні числа)

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! 🐙

Визначення 5.3.1 (Дійсні числа)

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

Лема 5.3.6 (Сума послідовностей Коші є послідовністю Коші.)

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 -- Доведення написане так, щоб відповідати структурі оригінального тексту. 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! 🐙

Лема 5.3.7 (Сума еквівалентних послідовностей є еквівалентною.)

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) -- Доведення написане так, щоб відповідати структурі оригінального тексту. 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! 🐙

Лема 5.3.7 (Сума еквівалентних послідовностей є еквівалентною)

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! 🐙

Лема 5.3.7 (Сума еквівалентних послідовностей є еквівалентною)

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')

Визначення 5.3.4 (Додавання дійсних чисел)

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! 🐙 )

Визначення 5.3.4 (Додавання дійсних чисел)

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! 🐙

Твердження 5.3.10 (Добуток послідовностей Коші є послідовністю Коші)

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! 🐙

Твердження 5.3.10 (Добуток еквівалентних послідовностей є еквівалентним) / Вправа 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 (Добуток еквівалентних послідовностей є еквівалентним) / Вправа 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 (Добуток еквівалентних послідовностей є еквівалентним) / Вправа 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')

Визначення 5.3.9 (Добуток дійсних чисел)

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! 🐙

Вправа 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 розподіляється щодо додавання

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 розподіляється щодо множення

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 комутує з запереченням

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

Можливо, тут можна опустити гіпотезу про послідовність Коші.

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! 🐙

Твердження 5.3.11 (закони алгебри)

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 розподіляється щодо віднімання

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 розподіляється щодо віднімання

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

Твердження 5.3.11 (закони алгебри)

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

Твердження 5.3.11 (закони алгебри)

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! 🐙

Твердження 5.3.11 (закони алгебри)

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! 🐙

Визначення 5.3.12 (послідовності, обмежені від нуля). Послідовності індексуються так, щоб починатися з нуля, оскільки це зручніше для цілей Mathlib.

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! 🐙

Приклади 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! 🐙

Приклади 5.3.13

declaration uses 'sorry'example : ¬ BoundedAwayZero (fun n ↦ 10^(-(n:ℤ)-1)) := ⊢ ¬BoundedAwayZero fun n => 10 ^ (-↑n - 1) All goals completed! 🐙

Приклади 5.3.13

declaration uses 'sorry'example : ¬ BoundedAwayZero (fun n ↦ 1 - 10^(-(n:ℤ))) := ⊢ ¬BoundedAwayZero fun n => 1 - 10 ^ (-↑n) All goals completed! 🐙

Приклади 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! 🐙

Приклади 5.3.13

declaration uses 'sorry'example : ¬ ((fun (n:ℕ) ↦ (10:ℚ)^(n+1)):Sequence).IsBounded := ⊢ ¬(↑fun n => 10 ^ (n + 1)).IsBounded All goals completed! 🐙

Лема 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 -- Доведення написане так, щоб відповідати структурі оригінального тексту. 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! 🐙

Цей результат не був явно зазначений у тексті, але потрібен у теорії. Це гарна вправа, тож я залишаю її як таку.

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! 🐙

Лема 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 -- Доведення написане так, щоб відповідати структурі оригінального тексту. 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! 🐙

Лема 5.3.17 (Операція взяття оберненого числа визначена коректно)

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⁻¹ -- цей доказ написан так, щоб співпадати із структурою оригінального тексту. 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 /-- Визначення 5.3.16 (Взяття оберненого числа дійсних чисел). Вимагає класичної логіки, оскільки потрібно присвоїти "сміттєве" значення оберненому 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! 🐙

Стандартне визначення ділення

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! 🐙

Вправа 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! 🐙

Те саме, що Chapter5.Sequence.IsCauchy.harmonic : (Sequence.mk' 1 fun n => 1 / ↑↑n).IsCauchySequence.IsCauchy.harmonic, але з перенумерацією послідовності як a₀ = 1, a₁ = 1/2, ... Ця форма зручніша для майбутнього доведення Теореми 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! 🐙

Вправа 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