Аналіз I, Глава 6.4

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:

Lim sup and lim inf of sequences
Limit points of sequences
Comparison and squeeze tests
Completeness of the reals

abbrev Real.adherent (ε:ℝ) (a:Chapter6.Sequence) (x:ℝ) := ∃ n ≥ a.m, ε.close (a n) x

abbrev Real.continually_adherent (ε:ℝ) (a:Chapter6.Sequence) (x:ℝ) :=
  ∀ N ≥ a.m, ε.adherent (a.from N) x

namespace Chapter6

abbrev Sequence.limit_point (a:Sequence) (x:ℝ) : Prop :=
  ∀ ε > (0:ℝ), ε.continually_adherent a x

theorem declaration uses 'sorry'Sequence.limit_point_def (a:Sequence) (x:ℝ) :
  a.limit_point x ↔ ∀ ε > 0, ∀ N ≥ a.m, ∃ n ≥ N, |a n - x| ≤ ε := bya:Sequencex:ℝ⊢ a.limit_point x ↔ ∀ ε > 0, ∀ N ≥ a.m, ∃ n ≥ N, |a.seq n - x| ≤ ε
    unfold limit_point Real.continually_adherent Real.adherenta:Sequencex:ℝ⊢ (∀ ε > 0, ∀ N ≥ a.m, ∃ n ≥ (a.from N).m, ε.close ((a.from N).seq n) x) ↔ ∀ ε > 0, ∀ N ≥ a.m, ∃ n ≥ N, |a.seq n - x| ≤ ε
    sorryAll goals completed! 🐙

noncomputable abbrev Example_6_4_3 : Sequence := (fun (n:ℕ) ↦ 1 - (10:ℝ)^(-(n:ℤ)-1))

Приклад 6.4.3

declaration uses 'sorry'example : (0.1:ℝ).adherent Example_6_4_3 0.8 := by⊢ Real.adherent 0.1 Example_6_4_3 0.8 sorryAll goals completed! 🐙

Приклад 6.4.3

declaration uses 'sorry'example : ¬ (0.1:ℝ).continually_adherent Example_6_4_3 0.8 := by⊢ ¬Real.continually_adherent 0.1 Example_6_4_3 0.8 sorryAll goals completed! 🐙

Приклад 6.4.3

declaration uses 'sorry'example : (0.1:ℝ).continually_adherent Example_6_4_3 1 := by⊢ Real.continually_adherent 0.1 Example_6_4_3 1 sorryAll goals completed! 🐙

Приклад 6.4.3

declaration uses 'sorry'example : Example_6_4_3.limit_point 1 := by⊢ Example_6_4_3.limit_point 1 sorryAll goals completed! 🐙

noncomputable abbrev Example_6_4_4 : Sequence :=
  (fun (n:ℕ) ↦ (-1:ℝ)^n * (1 + (10:ℝ)^(-(n:ℤ)-1)))

Приклад 6.4.4

declaration uses 'sorry'example : (0.1:ℝ).adherent Example_6_4_4 1 := by⊢ Real.adherent 0.1 Example_6_4_4 1 sorryAll goals completed! 🐙

Приклад 6.4.4

declaration uses 'sorry'example : (0.1:ℝ).continually_adherent Example_6_4_4 1 := by⊢ Real.continually_adherent 0.1 Example_6_4_4 1 sorryAll goals completed! 🐙

Приклад 6.4.4

declaration uses 'sorry'example : Example_6_4_4.limit_point 1 := by⊢ Example_6_4_4.limit_point 1 sorryAll goals completed! 🐙

Приклад 6.4.4

declaration uses 'sorry'example : Example_6_4_4.limit_point (-1) := by⊢ Example_6_4_4.limit_point (-1) sorryAll goals completed! 🐙

Приклад 6.4.4

declaration uses 'sorry'example : ¬ Example_6_4_4.limit_point 0 := by⊢ ¬Example_6_4_4.limit_point 0 sorryAll goals completed! 🐙

Твердження 6.4.5 / Вправа 6.4.1

theorem declaration uses 'sorry'Sequence.limit_point_of_limit {a:Sequence} {x:ℝ} (h: a.tendsTo x) : a.limit_point x := bya:Sequencex:ℝh:a.tendsTo x⊢ a.limit_point x
  sorryAll goals completed! 🐙

A technical issue uncovered by the formalization: the upper and lower sequences of a real sequence take values in the extended reals rather than the reals, so the definitions need to be adjusted accordingly.

noncomputable abbrev Sequence.upperseq (a:Sequence) : ℤ → EReal := fun N ↦ (a.from N).sup

noncomputable abbrev Sequence.limsup (a:Sequence) : EReal :=
  sInf { x | ∃ N ≥ a.m, x = a.upperseq N }

noncomputable abbrev Sequence.lowerseq (a:Sequence) : ℤ → EReal := fun N ↦ (a.from N).inf

noncomputable abbrev Sequence.liminf (a:Sequence) : EReal :=
  sSup { x | ∃ N ≥ a.m, x = a.lowerseq N }

noncomputable abbrev Example_6_4_7 : Sequence := (fun (n:ℕ) ↦ (-1:ℝ)^n * (1 + (10:ℝ)^(-(n:ℤ)-1)))

declaration uses 'sorry'example (n:ℕ) :
    Example_6_4_7.upperseq n = if Even n then 1 + (10:ℝ)^(-(n:ℤ)-1) else 1 + (10:ℝ)^(-(n:ℤ)-2) := byn:ℕ⊢ Example_6_4_7.upperseq ↑n = ↑(if Even n then 1 + 10 ^ (-↑n - 1) else 1 + 10 ^ (-↑n - 2))
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_7.limsup = 1 := by⊢ Example_6_4_7.limsup = 1 sorryAll goals completed! 🐙

declaration uses 'sorry'example (n:ℕ) :
    Example_6_4_7.lowerseq n
    = if Even n then -(1 + (10:ℝ)^(-(n:ℤ)-2)) else -(1 + (10:ℝ)^(-(n:ℤ)-1)) := byn:ℕ⊢ Example_6_4_7.lowerseq ↑n = ↑(if Even n then -(1 + 10 ^ (-↑n - 2)) else -(1 + 10 ^ (-↑n - 1)))
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_7.liminf = -1 := by⊢ Example_6_4_7.liminf = -1 sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_7.sup = (1.1:ℝ) := by⊢ Example_6_4_7.sup = ↑1.1 sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_7.inf = (-1.01:ℝ) := by⊢ Example_6_4_7.inf = ↑(-1.01) sorryAll goals completed! 🐙

noncomputable abbrev Example_6_4_8 : Sequence := (fun (n:ℕ) ↦ if Even n then (n+1:ℝ) else -(n:ℝ)-1)

declaration uses 'sorry'example (n:ℕ) : Example_6_4_8.upperseq n = ⊤ := byn:ℕ⊢ Example_6_4_8.upperseq ↑n = ⊤ sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_8.limsup = ⊤ := by⊢ Example_6_4_8.limsup = ⊤ sorryAll goals completed! 🐙

declaration uses 'sorry'example (n:ℕ) : Example_6_4_8.lowerseq n = ⊥ := byn:ℕ⊢ Example_6_4_8.lowerseq ↑n = ⊥ sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_8.liminf = ⊥ := by⊢ Example_6_4_8.liminf = ⊥ sorryAll goals completed! 🐙

noncomputable abbrev Example_6_4_9 : Sequence :=
  (fun (n:ℕ) ↦ if Even n then (n+1:ℝ)⁻¹ else -(n+1:ℝ)⁻¹)

declaration uses 'sorry'example (n:ℕ) : Example_6_4_9.upperseq n = if Even n then (n+1:ℝ)⁻¹ else -(n+2:ℝ)⁻¹ := byn:ℕ⊢ Example_6_4_9.upperseq ↑n = ↑(if Even n then (↑n + 1)⁻¹ else -(↑n + 2)⁻¹) sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_9.limsup = 0 := by⊢ Example_6_4_9.limsup = 0 sorryAll goals completed! 🐙

declaration uses 'sorry'example (n:ℕ) : Example_6_4_9.lowerseq n = if Even n then -(n+2:ℝ)⁻¹ else -(n+1:ℝ)⁻¹ := byn:ℕ⊢ Example_6_4_9.lowerseq ↑n = ↑(if Even n then -(↑n + 2)⁻¹ else -(↑n + 1)⁻¹) sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_9.liminf = 0 := by⊢ Example_6_4_9.liminf = 0 sorryAll goals completed! 🐙

noncomputable abbrev Example_6_4_10 : Sequence := (fun (n:ℕ) ↦ (n+1:ℝ))

declaration uses 'sorry'example (n:ℕ) : Example_6_4_10.upperseq n = ⊤ := byn:ℕ⊢ Example_6_4_10.upperseq ↑n = ⊤ sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_9.limsup = ⊤ := by⊢ Example_6_4_9.limsup = ⊤ sorryAll goals completed! 🐙

declaration uses 'sorry'example (n:ℕ) : Example_6_4_9.lowerseq n = n+1 := byn:ℕ⊢ Example_6_4_9.lowerseq ↑n = ↑n + 1 sorryAll goals completed! 🐙

declaration uses 'sorry'example : Example_6_4_9.liminf = ⊤ := by⊢ Example_6_4_9.liminf = ⊤ sorryAll goals completed! 🐙

Твердження 6.4.12(a)

theorem Sequence.gt_limsup_bounds {a:Sequence} {x:EReal} (h: x > a.limsup) :
    ∃ N ≥ a.m, ∀ n ≥ N, a n < x := bya:Sequencex:ERealh:x > a.limsup⊢ ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) < x
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  unfold Sequence.limsup at ha:Sequencex:ERealh:x > sInf {x | ∃ N ≥ a.m, x = a.upperseq N}⊢ ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) < x
  simp [sInf_lt_iff] at ha:Sequencex:ERealh:∃ a_1, (∃ N, a.m ≤ N ∧ a_1 = a.upperseq N) ∧ a_1 < x⊢ ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) < x
  obtain ⟨aN, ⟨ N, ⟨ hN, haN ⟩ ⟩, ha ⟩ := hintro.intro.intro.introa:Sequencex:ERealaN:ERealha:aN < xN:ℤhN:a.m ≤ NhaN:aN = a.upperseq N⊢ ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) < x
  use Nha:Sequencex:ERealaN:ERealha:aN < xN:ℤhN:a.m ≤ NhaN:aN = a.upperseq N⊢ N ≥ a.m ∧ ∀ n ≥ N, ↑(a.seq n) < x
  simp [hN]ha:Sequencex:ERealaN:ERealha:aN < xN:ℤhN:a.m ≤ NhaN:aN = a.upperseq N⊢ ∀ (n : ℤ), N ≤ n → ↑(a.seq n) < x
  simp [haN, Sequence.upperseq] at haha:Sequencex:ERealaN:ERealN:ℤhN:a.m ≤ NhaN:aN = a.upperseq Nha:(a.from N).sup < x⊢ ∀ (n : ℤ), N ≤ n → ↑(a.seq n) < x
  intro n hnha:Sequencex:ERealaN:ERealN:ℤhN:a.m ≤ NhaN:aN = a.upperseq Nha:(a.from N).sup < xn:ℤhn:N ≤ n⊢ ↑(a.seq n) < x
  have hn' : n ≥ (a.from N).m := bya:Sequencex:ERealh:x > a.limsup⊢ ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) < x simp [hN, hn]All goals completed! 🐙
  convert lt_of_le_of_lt ((a.from N).le_sup hn') ha using 1h.e'_3a:Sequencex:ERealaN:ERealN:ℤhN:a.m ≤ NhaN:aN = a.upperseq Nha:(a.from N).sup < xn:ℤhn:N ≤ nhn':n ≥ (a.from N).m⊢ ↑(a.seq n) = ↑((a.from N).seq n)
  simp [hn, hN.trans hn]All goals completed! 🐙

Твердження 6.4.12(a)

theorem declaration uses 'sorry'Sequence.lt_liminf_bounds {a:Sequence} {y:EReal} (h: y < a.liminf) :
    ∃ N ≥ a.m, ∀ n ≥ N, a n > y := bya:Sequencey:ERealh:y < a.liminf⊢ ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) > y
  sorryAll goals completed! 🐙

Твердження 6.4.12(b)

theorem Sequence.lt_limsup_bounds {a:Sequence} {x:EReal} (h: x < a.limsup) {N:ℤ} (hN: N ≥ a.m) :
    ∃ n ≥ N, a n > x := bya:Sequencex:ERealh:x < a.limsupN:ℤhN:N ≥ a.m⊢ ∃ n ≥ N, ↑(a.seq n) > x
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  unfold Sequence.limsup at ha:Sequencex:ERealh:x < sInf {x | ∃ N ≥ a.m, x = a.upperseq N}N:ℤhN:N ≥ a.m⊢ ∃ n ≥ N, ↑(a.seq n) > x
  have hx : x < a.upperseq N := bya:Sequencex:ERealh:x < a.limsupN:ℤhN:N ≥ a.m⊢ ∃ n ≥ N, ↑(a.seq n) > x
    apply lt_of_lt_of_le h (sInf_le _)a:Sequencex:ERealh:x < sInf {x | ∃ N ≥ a.m, x = a.upperseq N}N:ℤhN:N ≥ a.m⊢ a.upperseq N ∈ {x | ∃ N ≥ a.m, x = a.upperseq N}
    simpa:Sequencex:ERealh:x < sInf {x | ∃ N ≥ a.m, x = a.upperseq N}N:ℤhN:N ≥ a.m⊢ ∃ N_1, a.m ≤ N_1 ∧ a.upperseq N = a.upperseq N_1; use NAll goals completed! 🐙
  unfold Sequence.upperseq at hxa:Sequencex:ERealh:x < sInf {x | ∃ N ≥ a.m, x = a.upperseq N}N:ℤhN:N ≥ a.mhx:x < (a.from N).sup⊢ ∃ n ≥ N, ↑(a.seq n) > x
  replace hx := Sequence.exists_between_lt_sup hxa:Sequencex:ERealh:x < sInf {x | ∃ N ≥ a.m, x = a.upperseq N}N:ℤhN:N ≥ a.mhx:∃ n ≥ (a.from N).m, x < ↑((a.from N).seq n) ∧ ↑((a.from N).seq n) ≤ (a.from N).sup⊢ ∃ n ≥ N, ↑(a.seq n) > x
  obtain ⟨ n, hn, hxn, _ ⟩ := hxintro.intro.introa:Sequencex:ERealh:x < sInf {x | ∃ N ≥ a.m, x = a.upperseq N}N:ℤhN:N ≥ a.mn:ℤhn:n ≥ (a.from N).mhxn:x < ↑((a.from N).seq n)right✝:↑((a.from N).seq n) ≤ (a.from N).sup⊢ ∃ n ≥ N, ↑(a.seq n) > x
  simp [Sequence.from, hN] at hnintro.intro.introa:Sequencex:ERealh:x < sInf {x | ∃ N ≥ a.m, x = a.upperseq N}N:ℤhN:N ≥ a.mn:ℤhxn:x < ↑((a.from N).seq n)right✝:↑((a.from N).seq n) ≤ (a.from N).suphn:N ≤ n⊢ ∃ n ≥ N, ↑(a.seq n) > x
  use n, hnrighta:Sequencex:ERealh:x < sInf {x | ∃ N ≥ a.m, x = a.upperseq N}N:ℤhN:N ≥ a.mn:ℤhxn:x < ↑((a.from N).seq n)right✝:↑((a.from N).seq n) ≤ (a.from N).suphn:N ≤ n⊢ ↑(a.seq n) > x
  convert gt_iff_lt.mpr hxn using 1h.e'_3a:Sequencex:ERealh:x < sInf {x | ∃ N ≥ a.m, x = a.upperseq N}N:ℤhN:N ≥ a.mn:ℤhxn:x < ↑((a.from N).seq n)right✝:↑((a.from N).seq n) ≤ (a.from N).suphn:N ≤ n⊢ ↑(a.seq n) = ↑((a.from N).seq n)
  simp [hn, hN.trans hn]All goals completed! 🐙

Твердження 6.4.12(b)

theorem declaration uses 'sorry'Sequence.gt_liminf_bounds {a:Sequence} {x:EReal} (h: x > a.liminf) {N:ℤ} (hN: N ≥ a.m) :
    ∃ n ≥ N, a n < x := bya:Sequencex:ERealh:x > a.liminfN:ℤhN:N ≥ a.m⊢ ∃ n ≥ N, ↑(a.seq n) < x
  sorryAll goals completed! 🐙

Твердження 6.4.12(c) / Вправа 6.4.3

theorem declaration uses 'sorry'Sequence.inf_le_liminf (a:Sequence) : a.inf ≤ a.liminf := bya:Sequence⊢ a.inf ≤ a.liminf sorryAll goals completed! 🐙

Твердження 6.4.12(c) / Вправа 6.4.3

theorem declaration uses 'sorry'Sequence.liminf_le_limsup (a:Sequence) : a.liminf ≤ a.limsup := bya:Sequence⊢ a.liminf ≤ a.limsup sorryAll goals completed! 🐙

Твердження 6.4.12(c) / Вправа 6.4.3

theorem declaration uses 'sorry'Sequence.limsup_le_sup (a:Sequence) : a.limsup ≤ a.sup := bya:Sequence⊢ a.limsup ≤ a.sup sorryAll goals completed! 🐙

Твердження 6.4.12(d) / Вправа 6.4.3

theorem declaration uses 'sorry'Sequence.limit_point_between_liminf_limsup {a:Sequence} {c:ℝ} (h: a.limit_point c) :
  a.liminf ≤ c ∧ c ≤ a.limsup := bya:Sequencec:ℝh:a.limit_point c⊢ a.liminf ≤ ↑c ∧ ↑c ≤ a.limsup
  sorryAll goals completed! 🐙

Твердження 6.4.12(e) / Вправа 6.4.3

theorem declaration uses 'sorry'Sequence.limit_point_of_limsup {a:Sequence} {L_plus:ℝ} (h: a.limsup = L_plus) :
    a.limit_point L_plus := bya:SequenceL_plus:ℝh:a.limsup = ↑L_plus⊢ a.limit_point L_plus
  sorryAll goals completed! 🐙

Твердження 6.4.12(e) / Вправа 6.4.3

theorem declaration uses 'sorry'Sequence.limit_point_of_liminf {a:Sequence} {L_minus:ℝ} (h: a.liminf = L_minus) :
    a.limit_point L_minus := bya:SequenceL_minus:ℝh:a.liminf = ↑L_minus⊢ a.limit_point L_minus
  sorryAll goals completed! 🐙

Твердження 6.4.12(f) / Вправа 6.4.3

theorem declaration uses 'sorry'Sequence.tendsTo_iff_eq_limsup_liminf {a:Sequence} (c:ℝ) :
  a.tendsTo c ↔ a.liminf = c ∧ a.limsup = c := bya:Sequencec:ℝ⊢ a.tendsTo c ↔ a.liminf = ↑c ∧ a.limsup = ↑c
  sorryAll goals completed! 🐙

Лема 6.4.13 (Comparison principle) / Вправа 6.4.4

theorem declaration uses 'sorry'Sequence.sup_mono {a b:Sequence} (hm: a.m = b.m) (hab: ∀ n ≥ a.m, a n ≤ b n) :
    a.sup ≤ b.sup := bya:Sequenceb:Sequencehm:a.m = b.mhab:∀ n ≥ a.m, a.seq n ≤ b.seq n⊢ a.sup ≤ b.sup sorryAll goals completed! 🐙

Лема 6.4.13 (Comparison principle) / Вправа 6.4.4

theorem declaration uses 'sorry'Sequence.inf_mono {a b:Sequence} (hm: a.m = b.m) (hab: ∀ n ≥ a.m, a n ≤ b n) :
    a.inf ≤ b.inf := bya:Sequenceb:Sequencehm:a.m = b.mhab:∀ n ≥ a.m, a.seq n ≤ b.seq n⊢ a.inf ≤ b.inf sorryAll goals completed! 🐙

Лема 6.4.13 (Comparison principle) / Вправа 6.4.4

theorem declaration uses 'sorry'Sequence.limsup_mono {a b:Sequence} (hm: a.m = b.m) (hab: ∀ n ≥ a.m, a n ≤ b n) :
    a.limsup ≤ b.limsup := bya:Sequenceb:Sequencehm:a.m = b.mhab:∀ n ≥ a.m, a.seq n ≤ b.seq n⊢ a.limsup ≤ b.limsup sorryAll goals completed! 🐙

Лема 6.4.13 (Comparison principle) / Вправа 6.4.4

theorem declaration uses 'sorry'Sequence.liminf_mono {a b:Sequence} (hm: a.m = b.m) (hab: ∀ n ≥ a.m, a n ≤ b n) :
    a.liminf ≤ b.liminf := bya:Sequenceb:Sequencehm:a.m = b.mhab:∀ n ≥ a.m, a.seq n ≤ b.seq n⊢ a.liminf ≤ b.liminf sorryAll goals completed! 🐙

Наслідок 6.4.14 (Squeeze test) / Вправа 6.4.5

theorem declaration uses 'sorry'Sequence.lim_of_between {a b c:Sequence} {L:ℝ} (hm: b.m = a.m ∧ c.m = a.m)
  (hab: ∀ n ≥ a.m, a n ≤ b n ∧ b n ≤ c n) (ha: a.tendsTo L) (hb: b.tendsTo L) :
    c.tendsTo L := bya:Sequenceb:Sequencec:SequenceL:ℝhm:b.m = a.m ∧ c.m = a.mhab:∀ n ≥ a.m, a.seq n ≤ b.seq n ∧ b.seq n ≤ c.seq nha:a.tendsTo Lhb:b.tendsTo L⊢ c.tendsTo L sorryAll goals completed! 🐙

Приклад 6.4.15

declaration uses 'sorry'example : ((fun (n:ℕ) ↦ 2/(n+1:ℝ)):Sequence).tendsTo 0 := by⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => 2 / (↑n + 1)) n.toNat else 0, vanish := ⋯ }.tendsTo 0
  sorryAll goals completed! 🐙

Приклад 6.4.15

declaration uses 'sorry'example : ((fun (n:ℕ) ↦ -2/(n+1:ℝ)):Sequence).tendsTo 0 := by⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => -2 / (↑n + 1)) n.toNat else 0, vanish := ⋯ }.tendsTo 0
  sorryAll goals completed! 🐙

Приклад 6.4.15

declaration uses 'sorry'example : ((fun (n:ℕ) ↦ (-1)^n/(n+1:ℝ) + 1 / (n+1)^2):Sequence).tendsTo 0 := by⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => (-1) ^ n / (↑n + 1) + 1 / (↑n + 1) ^ 2) n.toNat else 0,
      vanish := ⋯ }.tendsTo
  0
  sorryAll goals completed! 🐙

Приклад 6.4.15

declaration uses 'sorry'example : ((fun (n:ℕ) ↦ (2:ℝ)^(-(n:ℤ))):Sequence).tendsTo 0 := by⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => 2 ^ (-↑n)) n.toNat else 0, vanish := ⋯ }.tendsTo 0
  sorryAll goals completed! 🐙

abbrev Sequence.abs (a:Sequence) : Sequence where
  m := a.m
  seq := fun n ↦ |a n|
  vanish := bya:Sequence⊢ ∀ n < a.m, |a.seq n| = 0
    intro n hna:Sequencen:ℤhn:n < a.m⊢ |a.seq n| = 0
    simp [a.vanish n hn]All goals completed! 🐙

Наслідок 6.4.17 (Zero test for sequences) / Вправа 6.4.7

theorem declaration uses 'sorry'Sequence.tendsTo_zero_iff (a:Sequence) :
  a.tendsTo (0:ℝ) ↔ a.abs.tendsTo (0:ℝ) := bya:Sequence⊢ a.tendsTo 0 ↔ a.abs.tendsTo 0
  sorryAll goals completed! 🐙

This helper lemma, implicit in the textbook proofs of Theorem 6.4.18 and Theorem 6.6.8, is made explicit here.

theorem Sequence.finite_limsup_liminf_of_bounded {a:Sequence} (hbound: a.isBounded) :
    (∃ L_plus:ℝ, a.limsup = L_plus) ∧ (∃ L_minus:ℝ, a.liminf = L_minus) := bya:Sequencehbound:a.isBounded⊢ (∃ L_plus, a.limsup = ↑L_plus) ∧ ∃ L_minus, a.liminf = ↑L_minus
  obtain ⟨ M, hMpos, hbound ⟩ := hboundintro.introa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy M⊢ (∃ L_plus, a.limsup = ↑L_plus) ∧ ∃ L_minus, a.liminf = ↑L_minus
  unfold Sequence.BoundedBy at hboundintro.introa:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ M⊢ (∃ L_plus, a.limsup = ↑L_plus) ∧ ∃ L_minus, a.liminf = ↑L_minus
  have hlimsup_bound : a.limsup ≤ M := bya:Sequencehbound:a.isBounded⊢ (∃ L_plus, a.limsup = ↑L_plus) ∧ ∃ L_minus, a.liminf = ↑L_minus
    apply a.limsup_le_sup.transa:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ M⊢ a.sup ≤ ↑M
    apply sup_le_upperha:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ M⊢ ∀ n ≥ a.m, ↑(a.seq n) ≤ ↑M
    intro n hNha:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mn:ℤhN:n ≥ a.m⊢ ↑(a.seq n) ≤ ↑M
    simpha:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mn:ℤhN:n ≥ a.m⊢ a.seq n ≤ M
    exact (le_abs_self _).trans (hbound n)All goals completed! 🐙
  have hliminf_bound : -M ≤ a.liminf := bya:Sequencehbound:a.isBounded⊢ (∃ L_plus, a.limsup = ↑L_plus) ∧ ∃ L_minus, a.liminf = ↑L_minus
    apply LE.le.trans _ a.inf_le_liminfa:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhlimsup_bound:a.limsup ≤ ↑M⊢ -↑M ≤ a.inf
    apply inf_ge_lowerha:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhlimsup_bound:a.limsup ≤ ↑M⊢ ∀ n ≥ a.m, ↑(a.seq n) ≥ -↑M
    intro n hNha:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhlimsup_bound:a.limsup ≤ ↑Mn:ℤhN:n ≥ a.m⊢ ↑(a.seq n) ≥ -↑M
    simp [←EReal.coe_neg]ha:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhlimsup_bound:a.limsup ≤ ↑Mn:ℤhN:n ≥ a.m⊢ -M ≤ a.seq n
    rw [neg_le]ha:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhlimsup_bound:a.limsup ≤ ↑Mn:ℤhN:n ≥ a.m⊢ -a.seq n ≤ M
    exact (neg_le_abs _).trans (hbound n)All goals completed! 🐙
  constructorintro.intro.lefta:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhlimsup_bound:a.limsup ≤ ↑Mhliminf_bound:-↑M ≤ a.liminf⊢ ∃ L_plus, a.limsup = ↑L_plusintro.intro.righta:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhlimsup_bound:a.limsup ≤ ↑Mhliminf_bound:-↑M ≤ a.liminf⊢ ∃ L_minus, a.liminf = ↑L_minus
  .intro.intro.lefta:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhlimsup_bound:a.limsup ≤ ↑Mhliminf_bound:-↑M ≤ a.liminf⊢ ∃ L_plus, a.limsup = ↑L_plus use a.limsup.toRealha:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhlimsup_bound:a.limsup ≤ ↑Mhliminf_bound:-↑M ≤ a.liminf⊢ a.limsup = ↑a.limsup.toReal
    apply (EReal.coe_toReal _ _).symma:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhlimsup_bound:a.limsup ≤ ↑Mhliminf_bound:-↑M ≤ a.liminf⊢ a.limsup ≠ ⊤a:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhlimsup_bound:a.limsup ≤ ↑Mhliminf_bound:-↑M ≤ a.liminf⊢ a.limsup ≠ ⊥
    .a:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhlimsup_bound:a.limsup ≤ ↑Mhliminf_bound:-↑M ≤ a.liminf⊢ a.limsup ≠ ⊤ contrapose! hlimsup_bounda:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhliminf_bound:-↑M ≤ a.liminfhlimsup_bound:a.limsup = ⊤⊢ ↑M < a.limsup
      simp [hlimsup_bound]All goals completed! 🐙
    replace hliminf_bound := hliminf_bound.trans a.liminf_le_limsupa:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhlimsup_bound:a.limsup ≤ ↑Mhliminf_bound:-↑M ≤ a.limsup⊢ a.limsup ≠ ⊥
    contrapose! hliminf_bounda:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhlimsup_bound:a.limsup ≤ ↑Mhliminf_bound:a.limsup = ⊥⊢ a.limsup < -↑M
    simp [hliminf_bound, ←EReal.coe_neg]All goals completed! 🐙
  use a.liminf.toRealha:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhlimsup_bound:a.limsup ≤ ↑Mhliminf_bound:-↑M ≤ a.liminf⊢ a.liminf = ↑a.liminf.toReal
  apply (EReal.coe_toReal _ _).symma:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhlimsup_bound:a.limsup ≤ ↑Mhliminf_bound:-↑M ≤ a.liminf⊢ a.liminf ≠ ⊤a:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhlimsup_bound:a.limsup ≤ ↑Mhliminf_bound:-↑M ≤ a.liminf⊢ a.liminf ≠ ⊥
  .a:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhlimsup_bound:a.limsup ≤ ↑Mhliminf_bound:-↑M ≤ a.liminf⊢ a.liminf ≠ ⊤ replace hlimsup_bound := a.liminf_le_limsup.trans hlimsup_bounda:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhliminf_bound:-↑M ≤ a.liminfhlimsup_bound:a.liminf ≤ ↑M⊢ a.liminf ≠ ⊤
    contrapose! hlimsup_bounda:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhliminf_bound:-↑M ≤ a.liminfhlimsup_bound:a.liminf = ⊤⊢ ↑M < a.liminf
    simp [hlimsup_bound]All goals completed! 🐙
  contrapose! hliminf_bounda:SequenceM:ℝhMpos:M ≥ 0hbound:∀ (n : ℤ), |a.seq n| ≤ Mhlimsup_bound:a.limsup ≤ ↑Mhliminf_bound:a.liminf = ⊥⊢ a.liminf < -↑M
  simp [hliminf_bound, ←EReal.coe_neg]All goals completed! 🐙

Теорема 6.4.18 (Completeness of the reals)

theorem Sequence.Cauchy_iff_convergent (a:Sequence) :
  a.isCauchy ↔ a.convergent := bya:Sequence⊢ a.isCauchy ↔ a.convergent
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  refine ⟨ ?_, Cauchy_of_convergent ⟩a:Sequence⊢ a.isCauchy → a.convergent
  intro ha:Sequenceh:a.isCauchy⊢ a.convergent
  obtain ⟨ ⟨ L_plus, hL_plus ⟩, ⟨ L_minus, hL_minus ⟩ ⟩ :=
    finite_limsup_liminf_of_bounded (bounded_of_cauchy h)intro.intro.introa:Sequenceh:a.isCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minus⊢ a.convergent
  use L_minusha:Sequenceh:a.isCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minus⊢ a.tendsTo L_minus
  rw [tendsTo_iff_eq_limsup_liminf]ha:Sequenceh:a.isCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minus⊢ a.liminf = ↑L_minus ∧ a.limsup = ↑L_minus
  simp [hL_minus, hL_plus]ha:Sequenceh:a.isCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minus⊢ L_plus = L_minus
  have hlow : 0 ≤ L_plus - L_minus := bya:Sequence⊢ a.isCauchy ↔ a.convergent
    have := a.liminf_le_limsupa:Sequenceh:a.isCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minusthis:a.liminf ≤ a.limsup⊢ 0 ≤ L_plus - L_minus
    simp [hL_minus, hL_plus] at thisa:Sequenceh:a.isCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minusthis:L_minus ≤ L_plus⊢ 0 ≤ L_plus - L_minus
    linarithAll goals completed! 🐙
  have hup (ε:ℝ) (hε: ε>0) : L_plus - L_minus ≤ 2*ε := bya:Sequence⊢ a.isCauchy ↔ a.convergent
    specialize h ε hεa:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0h:ε.eventuallySteady a⊢ L_plus - L_minus ≤ 2 * ε
    obtain ⟨ N, hN, hsteady ⟩ := hintro.introa:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.steady (a.from N)⊢ L_plus - L_minus ≤ 2 * ε
    unfold Real.steady Real.close at hsteadyintro.introa:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:∀ n ≥ (a.from N).m, ∀ m ≥ (a.from N).m, dist ((a.from N).seq n) ((a.from N).seq m) ≤ ε⊢ L_plus - L_minus ≤ 2 * ε
    have hN0 : N ≥ (a.from N).m := bya:Sequence⊢ a.isCauchy ↔ a.convergent
      simp [Sequence.from, hN]All goals completed! 🐙
    have hN1 : (a.from N).seq N = a.seq N := bya:Sequence⊢ a.isCauchy ↔ a.convergent
      simp [Sequence.from, hN]All goals completed! 🐙
    have h1 : (a N - ε:ℝ) ≤ (a.from N).inf := bya:Sequence⊢ a.isCauchy ↔ a.convergent
      apply inf_ge_lowerha:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:∀ n ≥ (a.from N).m, ∀ m ≥ (a.from N).m, dist ((a.from N).seq n) ((a.from N).seq m) ≤ εhN0:N ≥ (a.from N).mhN1:(a.from N).seq N = a.seq N⊢ ∀ n ≥ (a.from N).m, ↑((a.from N).seq n) ≥ ↑(a.seq N - ε)
      intro n hnha:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:∀ n ≥ (a.from N).m, ∀ m ≥ (a.from N).m, dist ((a.from N).seq n) ((a.from N).seq m) ≤ εhN0:N ≥ (a.from N).mhN1:(a.from N).seq N = a.seq Nn:ℤhn:n ≥ (a.from N).m⊢ ↑((a.from N).seq n) ≥ ↑(a.seq N - ε)
      specialize hsteady n hn N hN0ha:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhN0:N ≥ (a.from N).mhN1:(a.from N).seq N = a.seq Nn:ℤhn:n ≥ (a.from N).mhsteady:dist ((a.from N).seq n) ((a.from N).seq N) ≤ ε⊢ ↑((a.from N).seq n) ≥ ↑(a.seq N - ε)
      rw [ge_iff_le, EReal.coe_le_coe_iff]ha:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhN0:N ≥ (a.from N).mhN1:(a.from N).seq N = a.seq Nn:ℤhn:n ≥ (a.from N).mhsteady:dist ((a.from N).seq n) ((a.from N).seq N) ≤ ε⊢ a.seq N - ε ≤ (a.from N).seq n
      rw [Real.dist_eq, hN1, abs_le'] at hsteadyha:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhN0:N ≥ (a.from N).mhN1:(a.from N).seq N = a.seq Nn:ℤhn:n ≥ (a.from N).mhsteady:(a.from N).seq n - a.seq N ≤ ε ∧ -((a.from N).seq n - a.seq N) ≤ ε⊢ a.seq N - ε ≤ (a.from N).seq n
      linarithAll goals completed! 🐙
    have h2 : (a.from N).inf ≤ L_minus := bya:Sequence⊢ a.isCauchy ↔ a.convergent
      simp_rw [←hL_minus, Sequence.liminf, Sequence.lowerseq]a:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:∀ n ≥ (a.from N).m, ∀ m ≥ (a.from N).m, dist ((a.from N).seq n) ((a.from N).seq m) ≤ εhN0:N ≥ (a.from N).mhN1:(a.from N).seq N = a.seq Nh1:↑(a.seq N - ε) ≤ (a.from N).inf⊢ (a.from N).inf ≤ sSup {x | ∃ N ≥ a.m, x = (a.from N).inf}
      apply le_sSupaa:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:∀ n ≥ (a.from N).m, ∀ m ≥ (a.from N).m, dist ((a.from N).seq n) ((a.from N).seq m) ≤ εhN0:N ≥ (a.from N).mhN1:(a.from N).seq N = a.seq Nh1:↑(a.seq N - ε) ≤ (a.from N).inf⊢ (a.from N).inf ∈ {x | ∃ N ≥ a.m, x = (a.from N).inf}
      simpaa:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:∀ n ≥ (a.from N).m, ∀ m ≥ (a.from N).m, dist ((a.from N).seq n) ((a.from N).seq m) ≤ εhN0:N ≥ (a.from N).mhN1:(a.from N).seq N = a.seq Nh1:↑(a.seq N - ε) ≤ (a.from N).inf⊢ ∃ N_1, a.m ≤ N_1 ∧ (a.from N).inf = (a.from N_1).inf; use NAll goals completed! 🐙
    have h3 : (a.from N).sup ≤ (a N + ε:ℝ) := bya:Sequence⊢ a.isCauchy ↔ a.convergent
      apply sup_le_upperha:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:∀ n ≥ (a.from N).m, ∀ m ≥ (a.from N).m, dist ((a.from N).seq n) ((a.from N).seq m) ≤ εhN0:N ≥ (a.from N).mhN1:(a.from N).seq N = a.seq Nh1:↑(a.seq N - ε) ≤ (a.from N).infh2:(a.from N).inf ≤ ↑L_minus⊢ ∀ n ≥ (a.from N).m, ↑((a.from N).seq n) ≤ ↑(a.seq N + ε)
      intro n hnha:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:∀ n ≥ (a.from N).m, ∀ m ≥ (a.from N).m, dist ((a.from N).seq n) ((a.from N).seq m) ≤ εhN0:N ≥ (a.from N).mhN1:(a.from N).seq N = a.seq Nh1:↑(a.seq N - ε) ≤ (a.from N).infh2:(a.from N).inf ≤ ↑L_minusn:ℤhn:n ≥ (a.from N).m⊢ ↑((a.from N).seq n) ≤ ↑(a.seq N + ε)
      specialize hsteady n hn N hN0ha:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhN0:N ≥ (a.from N).mhN1:(a.from N).seq N = a.seq Nh1:↑(a.seq N - ε) ≤ (a.from N).infh2:(a.from N).inf ≤ ↑L_minusn:ℤhn:n ≥ (a.from N).mhsteady:dist ((a.from N).seq n) ((a.from N).seq N) ≤ ε⊢ ↑((a.from N).seq n) ≤ ↑(a.seq N + ε)
      rw [EReal.coe_le_coe_iff]ha:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhN0:N ≥ (a.from N).mhN1:(a.from N).seq N = a.seq Nh1:↑(a.seq N - ε) ≤ (a.from N).infh2:(a.from N).inf ≤ ↑L_minusn:ℤhn:n ≥ (a.from N).mhsteady:dist ((a.from N).seq n) ((a.from N).seq N) ≤ ε⊢ (a.from N).seq n ≤ a.seq N + ε
      rw [Real.dist_eq, hN1, abs_le'] at hsteadyha:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhN0:N ≥ (a.from N).mhN1:(a.from N).seq N = a.seq Nh1:↑(a.seq N - ε) ≤ (a.from N).infh2:(a.from N).inf ≤ ↑L_minusn:ℤhn:n ≥ (a.from N).mhsteady:(a.from N).seq n - a.seq N ≤ ε ∧ -((a.from N).seq n - a.seq N) ≤ ε⊢ (a.from N).seq n ≤ a.seq N + ε
      linarithAll goals completed! 🐙
    have h4 : L_plus ≤ (a.from N).sup := bya:Sequence⊢ a.isCauchy ↔ a.convergent
      simp_rw [←hL_plus, Sequence.limsup, Sequence.upperseq]a:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:∀ n ≥ (a.from N).m, ∀ m ≥ (a.from N).m, dist ((a.from N).seq n) ((a.from N).seq m) ≤ εhN0:N ≥ (a.from N).mhN1:(a.from N).seq N = a.seq Nh1:↑(a.seq N - ε) ≤ (a.from N).infh2:(a.from N).inf ≤ ↑L_minush3:(a.from N).sup ≤ ↑(a.seq N + ε)⊢ sInf {x | ∃ N ≥ a.m, x = (a.from N).sup} ≤ (a.from N).sup
      apply sInf_leaa:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:∀ n ≥ (a.from N).m, ∀ m ≥ (a.from N).m, dist ((a.from N).seq n) ((a.from N).seq m) ≤ εhN0:N ≥ (a.from N).mhN1:(a.from N).seq N = a.seq Nh1:↑(a.seq N - ε) ≤ (a.from N).infh2:(a.from N).inf ≤ ↑L_minush3:(a.from N).sup ≤ ↑(a.seq N + ε)⊢ (a.from N).sup ∈ {x | ∃ N ≥ a.m, x = (a.from N).sup}
      simpaa:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:∀ n ≥ (a.from N).m, ∀ m ≥ (a.from N).m, dist ((a.from N).seq n) ((a.from N).seq m) ≤ εhN0:N ≥ (a.from N).mhN1:(a.from N).seq N = a.seq Nh1:↑(a.seq N - ε) ≤ (a.from N).infh2:(a.from N).inf ≤ ↑L_minush3:(a.from N).sup ≤ ↑(a.seq N + ε)⊢ ∃ N_1, a.m ≤ N_1 ∧ (a.from N).sup = (a.from N_1).sup; use NAll goals completed! 🐙
    replace h1 := h1.trans h2intro.introa:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:∀ n ≥ (a.from N).m, ∀ m ≥ (a.from N).m, dist ((a.from N).seq n) ((a.from N).seq m) ≤ εhN0:N ≥ (a.from N).mhN1:(a.from N).seq N = a.seq Nh2:(a.from N).inf ≤ ↑L_minush3:(a.from N).sup ≤ ↑(a.seq N + ε)h4:↑L_plus ≤ (a.from N).suph1:↑(a.seq N - ε) ≤ ↑L_minus⊢ L_plus - L_minus ≤ 2 * ε
    replace h4 := h4.trans h3intro.introa:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:∀ n ≥ (a.from N).m, ∀ m ≥ (a.from N).m, dist ((a.from N).seq n) ((a.from N).seq m) ≤ εhN0:N ≥ (a.from N).mhN1:(a.from N).seq N = a.seq Nh2:(a.from N).inf ≤ ↑L_minush3:(a.from N).sup ≤ ↑(a.seq N + ε)h1:↑(a.seq N - ε) ≤ ↑L_minush4:↑L_plus ≤ ↑(a.seq N + ε)⊢ L_plus - L_minus ≤ 2 * ε
    rw [EReal.coe_le_coe_iff] at h1 h4intro.introa:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minusε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:∀ n ≥ (a.from N).m, ∀ m ≥ (a.from N).m, dist ((a.from N).seq n) ((a.from N).seq m) ≤ εhN0:N ≥ (a.from N).mhN1:(a.from N).seq N = a.seq Nh2:(a.from N).inf ≤ ↑L_minush3:(a.from N).sup ≤ ↑(a.seq N + ε)h1:a.seq N - ε ≤ L_minush4:L_plus ≤ a.seq N + ε⊢ L_plus - L_minus ≤ 2 * ε
    linarithAll goals completed! 🐙
  rcases le_iff_lt_or_eq.mp hlow with hlow | hlowh.inla:Sequenceh:a.isCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow✝:0 ≤ L_plus - L_minushup:∀ ε > 0, L_plus - L_minus ≤ 2 * εhlow:0 < L_plus - L_minus⊢ L_plus = L_minush.inra:Sequenceh:a.isCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow✝:0 ≤ L_plus - L_minushup:∀ ε > 0, L_plus - L_minus ≤ 2 * εhlow:0 = L_plus - L_minus⊢ L_plus = L_minus
  .h.inla:Sequenceh:a.isCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow✝:0 ≤ L_plus - L_minushup:∀ ε > 0, L_plus - L_minus ≤ 2 * εhlow:0 < L_plus - L_minus⊢ L_plus = L_minus specialize hup ((L_plus - L_minus)/3) (bya:Sequenceh:a.isCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow✝:0 ≤ L_plus - L_minushup:∀ ε > 0, L_plus - L_minus ≤ 2 * εhlow:0 < L_plus - L_minus⊢ (L_plus - L_minus) / 3 > 0 positivityAll goals completed! 🐙)
    linarithAll goals completed! 🐙
  linarithAll goals completed! 🐙

Вправа 6.4.6

theorem declaration uses 'sorry'Sequence.sup_not_strict_mono : ∃ (a b:ℕ → ℝ), (∀ n, a n < b n) ∧ (a:Sequence).sup ≠ (b:Sequence).sup := by⊢ ∃ a b,
  (∀ (n : ℕ), a n < b n) ∧
    { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.sup ≠
      { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.sup
  sorryAll goals completed! 🐙

/- Вправа 6.4.7 -/

def declaration uses 'sorry'Sequence.tendsTo_real_iff :
  Decidable (∀ (a:Sequence) (x:ℝ), a.tendsTo x ↔ a.abs.tendsTo x) := by⊢ Decidable (∀ (a : Sequence) (x : ℝ), a.tendsTo x ↔ a.abs.tendsTo x)
  -- The first line of this construction should be `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙

This definition is needed for Exercises 6.4.8 and 6.4.9.

abbrev Sequence.extended_limit_point (a:Sequence) (x:EReal) : Prop := if x = ⊤ then ¬ a.bddAbove else if x = ⊥ then ¬ a.bddBelow else a.limit_point x.toReal

Вправа 6.4.8

theorem declaration uses 'sorry'Sequence.extended_limit_point_of_limsup (a:Sequence) : a.extended_limit_point a.limsup := bya:Sequence⊢ a.extended_limit_point a.limsup sorryAll goals completed! 🐙

Вправа 6.4.8

theorem declaration uses 'sorry'Sequence.extended_limit_point_of_liminf (a:Sequence) : a.extended_limit_point a.liminf := bya:Sequence⊢ a.extended_limit_point a.liminf sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Sequence.extended_limit_point_le_limsup {a:Sequence} {L:EReal} (h:a.extended_limit_point L): L ≤ a.limsup := bya:SequenceL:ERealh:a.extended_limit_point L⊢ L ≤ a.limsup sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Sequence.extended_limit_point_ge_liminf {a:Sequence} {L:EReal} (h:a.extended_limit_point L): L ≥ a.liminf := bya:SequenceL:ERealh:a.extended_limit_point L⊢ L ≥ a.liminf sorryAll goals completed! 🐙

Вправа 6.4.9

theorem declaration uses 'sorry'Sequence.exists_three_limit_points : ∃ a:Sequence, ∀ L:EReal, a.extended_limit_point L ↔ L = ⊥ ∨ L = 0 ∨ L = ⊤ := by⊢ ∃ a, ∀ (L : EReal), a.extended_limit_point L ↔ L = ⊥ ∨ L = 0 ∨ L = ⊤ sorryAll goals completed! 🐙

Вправа 6.4.10

theorem declaration uses 'sorry'Sequence.limit_points_of_limit_points {a b:Sequence} {c:ℝ} (hab: ∀ n ≥ b.m, a.limit_point (b n)) (hbc: b.limit_point c) : a.limit_point c := bya:Sequenceb:Sequencec:ℝhab:∀ n ≥ b.m, a.limit_point (b.seq n)hbc:b.limit_point c⊢ a.limit_point c sorryAll goals completed! 🐙

end Chapter6