Аналіз I, Розділ 6, Епілог

In this (technical) epilogue, we show that various operations and properties we have defined for "Chapter 6" sequences Chapter6.Sequence : TypeChapter6.Sequence are equivalent to Mathlib operations. Note however that Mathlib's operations are defined in far greater generality than the setting of real-valued sequences, in particular using the language of filters.

Identification with the Cauchy sequence support in unknown identifier 'Mathlib.Algebra.Order.CauSeq.Basic'Mathlib.Algebra.Order.CauSeq.Basic

theorem Chapter6.Sequence.Cauchy_iff_CauSeq (a: ℕ → ℝ) :
    (a:Sequence).isCauchy ↔ IsCauSeq _root_.abs a := bya:ℕ → ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ↔ IsCauSeq _root_.abs a
  simp_rw [isCauchy_of_coe, Real.dist_eq, IsCauSeq]a:ℕ → ℝ⊢ (∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε) ↔ ∀ ε > 0, ∃ i, ∀ j ≥ i, |a j - a i| < ε
  constructormpa:ℕ → ℝ⊢ (∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε) → ∀ ε > 0, ∃ i, ∀ j ≥ i, |a j - a i| < εmpra:ℕ → ℝ⊢ (∀ ε > 0, ∃ i, ∀ j ≥ i, |a j - a i| < ε) → ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε
  .mpa:ℕ → ℝ⊢ (∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε) → ∀ ε > 0, ∃ i, ∀ j ≥ i, |a j - a i| < ε intro h ε hεmpa:ℕ → ℝh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ εε:ℝhε:ε > 0⊢ ∃ i, ∀ j ≥ i, |a j - a i| < ε
    specialize h (ε/2) (half_pos hε)mpa:ℕ → ℝε:ℝhε:ε > 0h:∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε / 2⊢ ∃ i, ∀ j ≥ i, |a j - a i| < ε
    obtain ⟨ N, h ⟩ := hmp.introa:ℕ → ℝε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε / 2⊢ ∃ i, ∀ j ≥ i, |a j - a i| < ε
    use Nha:ℕ → ℝε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε / 2⊢ ∀ j ≥ N, |a j - a N| < ε
    intro n hnha:ℕ → ℝε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε / 2n:ℕhn:n ≥ N⊢ |a n - a N| < ε
    specialize h n hn N (le_refl _)ha:ℕ → ℝε:ℝhε:ε > 0N:ℕn:ℕhn:n ≥ Nh:|a n - a N| ≤ ε / 2⊢ |a n - a N| < ε
    linarithAll goals completed! 🐙
  intro h ε hεmpra:ℕ → ℝh:∀ ε > 0, ∃ i, ∀ j ≥ i, |a j - a i| < εε:ℝhε:ε > 0⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε
  specialize h (ε/2) (half_pos hε)mpra:ℕ → ℝε:ℝhε:ε > 0h:∃ i, ∀ j ≥ i, |a j - a i| < ε / 2⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε
  obtain ⟨ N, h ⟩ := hmpr.introa:ℕ → ℝε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, |a j - a N| < ε / 2⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε
  use Nha:ℕ → ℝε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, |a j - a N| < ε / 2⊢ ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε
  intro n hn m hmha:ℕ → ℝε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, |a j - a N| < ε / 2n:ℕhn:n ≥ Nm:ℕhm:m ≥ N⊢ |a n - a m| ≤ ε
  calc
    _ ≤ |a n - a N| + |a m - a N| := bya:ℕ → ℝε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, |a j - a N| < ε / 2n:ℕhn:n ≥ Nm:ℕhm:m ≥ N⊢ |a n - a m| ≤ |a n - a N| + |a m - a N| rw [abs_sub_comm (a m) (a N)]a:ℕ → ℝε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, |a j - a N| < ε / 2n:ℕhn:n ≥ Nm:ℕhm:m ≥ N⊢ |a n - a m| ≤ |a n - a N| + |a N - a m|; exact abs_sub_le _ _ _All goals completed! 🐙
    _ ≤ ε/2 + ε/2 := bya:ℕ → ℝε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, |a j - a N| < ε / 2n:ℕhn:n ≥ Nm:ℕhm:m ≥ N⊢ |a n - a N| + |a m - a N| ≤ ε / 2 + ε / 2 apply le_of_lthaba:ℕ → ℝε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, |a j - a N| < ε / 2n:ℕhn:n ≥ Nm:ℕhm:m ≥ N⊢ |a n - a N| + |a m - a N| < ε / 2 + ε / 2; gcongrhab.h₁a:ℕ → ℝε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, |a j - a N| < ε / 2n:ℕhn:n ≥ Nm:ℕhm:m ≥ N⊢ |a n - a N| < ε / 2hab.h₂a:ℕ → ℝε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, |a j - a N| < ε / 2n:ℕhn:n ≥ Nm:ℕhm:m ≥ N⊢ |a m - a N| < ε / 2; exact h n hnhab.h₂a:ℕ → ℝε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, |a j - a N| < ε / 2n:ℕhn:n ≥ Nm:ℕhm:m ≥ N⊢ |a m - a N| < ε / 2; exact h m hmAll goals completed! 🐙
    _ = _ := bya:ℕ → ℝε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, |a j - a N| < ε / 2n:ℕhn:n ≥ Nm:ℕhm:m ≥ N⊢ ε / 2 + ε / 2 = ε linarithAll goals completed! 🐙

Identification with the Cauchy sequence support in unknown identifier 'Mathlib.Topology.UniformSpace.Cauchy'Mathlib.Topology.UniformSpace.Cauchy

theorem Chapter6.Sequence.Cauchy_iff_CauchySeq (a: ℕ → ℝ) :
    (a:Sequence).isCauchy ↔ CauchySeq a := bya:ℕ → ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ↔ CauchySeq a
  rw [Cauchy_iff_CauSeq]a:ℕ → ℝ⊢ IsCauSeq _root_.abs a ↔ CauchySeq a
  convert isCauSeq_iff_cauchySeqAll goals completed! 🐙

Identifiction with Filter.Tendsto.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) (l₁ : Filter α) (l₂ : Filter β) : PropFilter.Tendsto

theorem Chapter6.Sequence.tendsto_iff_Tendsto (a: ℕ → ℝ) (L:ℝ) :
    (a:Sequence).tendsTo L ↔ Filter.Tendsto a Filter.atTop (nhds L) := bya:ℕ → ℝL:ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.tendsTo L ↔
  Filter.Tendsto a Filter.atTop (nhds L)
  rw [Metric.tendsto_atTop, tendsTo_iff]a:ℕ → ℝL:ℝ⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, |{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq n - L| ≤ ε) ↔
  ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a n) L < ε
  constructormpa:ℕ → ℝL:ℝ⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, |{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq n - L| ≤ ε) →
  ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a n) L < εmpra:ℕ → ℝL:ℝ⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a n) L < ε) →
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq n - L| ≤ ε
  .mpa:ℕ → ℝL:ℝ⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, |{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq n - L| ≤ ε) →
  ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a n) L < ε intro h ε hεmpa:ℕ → ℝL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, |{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq n - L| ≤ εε:ℝhε:ε > 0⊢ ∃ N, ∀ n ≥ N, dist (a n) L < ε
    specialize h (ε/2) (half_pos hε)mpa:ℕ → ℝL:ℝε:ℝhε:ε > 0h:∃ N, ∀ n ≥ N, |{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq n - L| ≤ ε / 2⊢ ∃ N, ∀ n ≥ N, dist (a n) L < ε
    obtain ⟨ N, hN ⟩ := hmp.introa:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, |{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq n - L| ≤ ε / 2⊢ ∃ N, ∀ n ≥ N, dist (a n) L < ε
    use N.toNatha:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, |{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq n - L| ≤ ε / 2⊢ ∀ n ≥ N.toNat, dist (a n) L < ε
    intro n hnha:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, |{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq n - L| ≤ ε / 2n:ℕhn:n ≥ N.toNat⊢ dist (a n) L < ε
    specialize hN n (Int.toNat_le.mp hn)ha:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℤn:ℕhn:n ≥ N.toNathN:|{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq ↑n - L| ≤ ε / 2⊢ dist (a n) L < ε
    simp at hNha:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℤn:ℕhn:n ≥ N.toNathN:|a n - L| ≤ ε / 2⊢ dist (a n) L < ε
    rw [Real.dist_eq]ha:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℤn:ℕhn:n ≥ N.toNathN:|a n - L| ≤ ε / 2⊢ |a n - L| < ε
    linarithAll goals completed! 🐙
  intro h ε hεmpra:ℕ → ℝL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a n) L < εε:ℝhε:ε > 0⊢ ∃ N, ∀ n ≥ N, |{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq n - L| ≤ ε
  specialize h ε hεmpra:ℕ → ℝL:ℝε:ℝhε:ε > 0h:∃ N, ∀ n ≥ N, dist (a n) L < ε⊢ ∃ N, ∀ n ≥ N, |{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq n - L| ≤ ε
  obtain ⟨ N, hN ⟩ := hmpr.introa:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℕhN:∀ n ≥ N, dist (a n) L < ε⊢ ∃ N, ∀ n ≥ N, |{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq n - L| ≤ ε
  use Nha:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℕhN:∀ n ≥ N, dist (a n) L < ε⊢ ∀ n ≥ ↑N, |{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq n - L| ≤ ε
  intro n hnha:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℕhN:∀ n ≥ N, dist (a n) L < εn:ℤhn:n ≥ ↑N⊢ |{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq n - L| ≤ ε
  have hpos : n ≥ 0 := LE.le.trans (bya:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℕhN:∀ n ≥ N, dist (a n) L < εn:ℤhn:n ≥ ↑N⊢ 0 ≤ ↑N positivityAll goals completed! 🐙) hn
  rw [ge_iff_le, ←Int.le_toNat hpos] at hnha:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℕhN:∀ n ≥ N, dist (a n) L < εn:ℤhn:N ≤ n.toNathpos:n ≥ 0⊢ |{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq n - L| ≤ ε
  specialize hN n.toNat hnha:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℕn:ℤhn:N ≤ n.toNathpos:n ≥ 0hN:dist (a n.toNat) L < ε⊢ |{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq n - L| ≤ ε
  simp [hpos, ←Real.dist_eq]ha:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℕn:ℤhn:N ≤ n.toNathpos:n ≥ 0hN:dist (a n.toNat) L < ε⊢ dist (a n.toNat) L ≤ ε
  exact le_of_lt hNAll goals completed! 🐙

theorem Chapter6.Sequence.tendsto_iff_Tendsto' (a: Sequence) (L:ℝ) : a.tendsTo L ↔ Filter.Tendsto a.seq Filter.atTop (nhds L) := bya:SequenceL:ℝ⊢ a.tendsTo L ↔ Filter.Tendsto a.seq Filter.atTop (nhds L)
  rw [Metric.tendsto_atTop, tendsTo_iff]a:SequenceL:ℝ⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ ε) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a.seq n) L < ε
  constructormpa:SequenceL:ℝ⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ ε) → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a.seq n) L < εmpra:SequenceL:ℝ⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a.seq n) L < ε) → ∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ ε
  .mpa:SequenceL:ℝ⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ ε) → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a.seq n) L < ε intro h ε hεmpa:SequenceL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ εε:ℝhε:ε > 0⊢ ∃ N, ∀ n ≥ N, dist (a.seq n) L < ε
    specialize h (ε/2) (half_pos hε)mpa:SequenceL:ℝε:ℝhε:ε > 0h:∃ N, ∀ n ≥ N, |a.seq n - L| ≤ ε / 2⊢ ∃ N, ∀ n ≥ N, dist (a.seq n) L < ε
    obtain ⟨ N, hN ⟩ := hmp.introa:SequenceL:ℝε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, |a.seq n - L| ≤ ε / 2⊢ ∃ N, ∀ n ≥ N, dist (a.seq n) L < ε
    use Nha:SequenceL:ℝε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, |a.seq n - L| ≤ ε / 2⊢ ∀ n ≥ N, dist (a.seq n) L < ε
    intro n hnha:SequenceL:ℝε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, |a.seq n - L| ≤ ε / 2n:ℤhn:n ≥ N⊢ dist (a.seq n) L < ε
    specialize hN n hnha:SequenceL:ℝε:ℝhε:ε > 0N:ℤn:ℤhn:n ≥ NhN:|a.seq n - L| ≤ ε / 2⊢ dist (a.seq n) L < ε
    rw [Real.dist_eq]ha:SequenceL:ℝε:ℝhε:ε > 0N:ℤn:ℤhn:n ≥ NhN:|a.seq n - L| ≤ ε / 2⊢ |a.seq n - L| < ε
    linarithAll goals completed! 🐙
  intro h ε hεmpra:SequenceL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a.seq n) L < εε:ℝhε:ε > 0⊢ ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ ε
  specialize h ε hεmpra:SequenceL:ℝε:ℝhε:ε > 0h:∃ N, ∀ n ≥ N, dist (a.seq n) L < ε⊢ ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ ε
  obtain ⟨ N, hN ⟩ := hmpr.introa:SequenceL:ℝε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, dist (a.seq n) L < ε⊢ ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ ε
  use Nha:SequenceL:ℝε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, dist (a.seq n) L < ε⊢ ∀ n ≥ N, |a.seq n - L| ≤ ε
  intro n hnha:SequenceL:ℝε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, dist (a.seq n) L < εn:ℤhn:n ≥ N⊢ |a.seq n - L| ≤ ε
  rw [ge_iff_le] at hnha:SequenceL:ℝε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, dist (a.seq n) L < εn:ℤhn:N ≤ n⊢ |a.seq n - L| ≤ ε
  specialize hN n hnha:SequenceL:ℝε:ℝhε:ε > 0N:ℤn:ℤhn:N ≤ nhN:dist (a.seq n) L < ε⊢ |a.seq n - L| ≤ ε
  simp [←Real.dist_eq]ha:SequenceL:ℝε:ℝhε:ε > 0N:ℤn:ℤhn:N ≤ nhN:dist (a.seq n) L < ε⊢ dist (a.seq n) L ≤ ε
  exact le_of_lt hNAll goals completed! 🐙

theorem Chapter6.Sequence.converges_iff_Tendsto (a: ℕ → ℝ) :
    (a:Sequence).convergent ↔ ∃ L, Filter.Tendsto a Filter.atTop (nhds L) := bya:ℕ → ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.convergent ↔
  ∃ L, Filter.Tendsto a Filter.atTop (nhds L)
  simp_rw [←tendsto_iff_Tendsto]All goals completed! 🐙

theorem Chapter6.Sequence.converges_iff_Tendsto' (a: Sequence) : a.convergent ↔ ∃ L, Filter.Tendsto a.seq Filter.atTop (nhds L) := bya:Sequence⊢ a.convergent ↔ ∃ L, Filter.Tendsto a.seq Filter.atTop (nhds L)
  simp_rw [←tendsto_iff_Tendsto']All goals completed! 🐙

A technicality: CauSeq.IsComplete ℝ : (abv : ℝ → ?m.102647) → [IsAbsoluteValue abv] → PropCauSeq.IsComplete ℝ was established for abs.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α_root_.abs but not for Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝnorm.

instance inst_real_complete : CauSeq.IsComplete ℝ norm := by⊢ CauSeq.IsComplete ℝ norm
  convert Real.instIsCompleteAbsAll goals completed! 🐙

Identification with CauSeq.lim.{u_1, u_2} {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] [CauSeq.IsComplete β abv] (s : CauSeq β abv) : βCauSeq.lim

theorem Chapter6.Sequence.lim_eq_CauSeq_lim (a:ℕ → ℝ) (ha: (a:Sequence).isCauchy) :
    Chapter6.lim (a:Sequence) = CauSeq.lim  ⟨ a, (Cauchy_iff_CauSeq a).mp ha⟩ := bya:ℕ → ℝha:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy⊢ lim { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } = CauSeq.lim ⟨a, ⋯⟩
  have h1 := CauSeq.tendsto_limit ⟨ a, (Cauchy_iff_CauSeq a).mp ha⟩a:ℕ → ℝha:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyh1:Filter.Tendsto (↑⟨a, ⋯⟩) Filter.atTop (nhds (CauSeq.lim ⟨a, ⋯⟩))⊢ lim { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } = CauSeq.lim ⟨a, ⋯⟩
  have h2 := lim_def ((a:Sequence).Cauchy_iff_convergent.mp ha)a:ℕ → ℝha:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyh1:Filter.Tendsto (↑⟨a, ⋯⟩) Filter.atTop (nhds (CauSeq.lim ⟨a, ⋯⟩))h2:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.tendsTo
  (lim { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ })⊢ lim { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } = CauSeq.lim ⟨a, ⋯⟩
  rw [←tendsto_iff_Tendsto] at h1a:ℕ → ℝha:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyh1:{ m := 0, seq := fun n => if n ≥ 0 then ↑⟨a, ⋯⟩ n.toNat else 0, vanish := ⋯ }.tendsTo (CauSeq.lim ⟨a, ⋯⟩)h2:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.tendsTo
  (lim { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ })⊢ lim { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } = CauSeq.lim ⟨a, ⋯⟩
  by_contra! ha:ℕ → ℝha:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyh1:{ m := 0, seq := fun n => if n ≥ 0 then ↑⟨a, ⋯⟩ n.toNat else 0, vanish := ⋯ }.tendsTo (CauSeq.lim ⟨a, ⋯⟩)h2:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.tendsTo
  (lim { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ })h:lim { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } ≠ CauSeq.lim ⟨a, ⋯⟩⊢ False
  replace h := (a:Sequence).tendsTo_unique ha:ℕ → ℝha:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyh1:{ m := 0, seq := fun n => if n ≥ 0 then ↑⟨a, ⋯⟩ n.toNat else 0, vanish := ⋯ }.tendsTo (CauSeq.lim ⟨a, ⋯⟩)h2:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.tendsTo
  (lim { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ })h:¬({ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.tendsTo
      (lim { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }) ∧
    { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.tendsTo (CauSeq.lim ⟨a, ⋯⟩))⊢ False
  tautoAll goals completed! 🐙

Identification with Bornology.IsBounded.{u_2} {α : Type u_2} [Bornology α] (s : Set α) : PropBornology.IsBounded

theorem Chapter6.Sequence.isBounded_iff_isBounded_range (a:ℕ → ℝ):
    (a:Sequence).isBounded ↔ Bornology.IsBounded (Set.range a) := bya:ℕ → ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isBounded ↔ Bornology.IsBounded (Set.range a)
  simp [isBounded_def, BoundedBy_def, Metric.isBounded_iff]a:ℕ → ℝ⊢ (∃ M, 0 ≤ M ∧ ∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ M) ↔ ∃ C, ∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ C
  constructormpa:ℕ → ℝ⊢ (∃ M, 0 ≤ M ∧ ∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ M) → ∃ C, ∀ (a_2 a_3 : ℕ), dist (a a_2) (a a_3) ≤ Cmpra:ℕ → ℝ⊢ (∃ C, ∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ C) → ∃ M, 0 ≤ M ∧ ∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ M
  .mpa:ℕ → ℝ⊢ (∃ M, 0 ≤ M ∧ ∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ M) → ∃ C, ∀ (a_2 a_3 : ℕ), dist (a a_2) (a a_3) ≤ C intro hmpa:ℕ → ℝh:∃ M, 0 ≤ M ∧ ∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ M⊢ ∃ C, ∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ C
    obtain ⟨ M, hM, h ⟩ := hmp.intro.introa:ℕ → ℝM:ℝhM:0 ≤ Mh:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ M⊢ ∃ C, ∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ C
    use 2*Mha:ℕ → ℝM:ℝhM:0 ≤ Mh:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ M⊢ ∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ 2 * M
    intro n mha:ℕ → ℝM:ℝhM:0 ≤ Mh:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ Mn:ℕm:ℕ⊢ dist (a n) (a m) ≤ 2 * M
    calc
      _ = |a n - a m| := Real.dist_eq _ _
      _ ≤ |a n| + |a m| := abs_sub _ _
      _ ≤ M + M := bya:ℕ → ℝM:ℝhM:0 ≤ Mh:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ Mn:ℕm:ℕ⊢ |a n| + |a m| ≤ M + M gcongrh₁a:ℕ → ℝM:ℝhM:0 ≤ Mh:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ Mn:ℕm:ℕ⊢ |a n| ≤ Mh₂a:ℕ → ℝM:ℝhM:0 ≤ Mh:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ Mn:ℕm:ℕ⊢ |a m| ≤ M; convert h nh₂a:ℕ → ℝM:ℝhM:0 ≤ Mh:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ Mn:ℕm:ℕ⊢ |a m| ≤ M; convert h mAll goals completed! 🐙
      _ = _ := bya:ℕ → ℝM:ℝhM:0 ≤ Mh:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ Mn:ℕm:ℕ⊢ M + M = 2 * M ringAll goals completed! 🐙
  intro hmpra:ℕ → ℝh:∃ C, ∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ C⊢ ∃ M, 0 ≤ M ∧ ∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ M
  obtain ⟨ C, h ⟩ := hmpr.introa:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ C⊢ ∃ M, 0 ≤ M ∧ ∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ M
  have : C ≥ 0 := bya:ℕ → ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isBounded ↔ Bornology.IsBounded (Set.range a)
    specialize h 0 0a:ℕ → ℝC:ℝh:dist (a 0) (a 0) ≤ C⊢ C ≥ 0
    simp at ha:ℕ → ℝC:ℝh:0 ≤ C⊢ C ≥ 0
    assumptionAll goals completed! 🐙
  refine ⟨ C + |a 0|, bya:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:C ≥ 0⊢ 0 ≤ C + |a 0| positivityAll goals completed! 🐙, ?_ ⟩
  intro nmpr.introa:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:C ≥ 0n:ℤ⊢ |if 0 ≤ n then a n.toNat else 0| ≤ C + |a 0|
  by_cases hn: n ≥ 0posa:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:C ≥ 0n:ℤhn:n ≥ 0⊢ |if 0 ≤ n then a n.toNat else 0| ≤ C + |a 0|nega:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:C ≥ 0n:ℤhn:¬n ≥ 0⊢ |if 0 ≤ n then a n.toNat else 0| ≤ C + |a 0|
  all_goals simp [hn]nega:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:C ≥ 0n:ℤhn:¬n ≥ 0⊢ 0 ≤ C + |a 0|
  .posa:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:C ≥ 0n:ℤhn:n ≥ 0⊢ |a n.toNat| ≤ C + |a 0| calc
      _ ≤ |a n.toNat - a 0| + |a 0| := bya:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:C ≥ 0n:ℤhn:n ≥ 0⊢ |a n.toNat| ≤ |a n.toNat - a 0| + |a 0|
        convert abs_add_le _ _h.e'_3.h.e'_4a:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:C ≥ 0n:ℤhn:n ≥ 0⊢ a n.toNat = a n.toNat - a 0 + a 0convert_4a:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:C ≥ 0n:ℤhn:n ≥ 0⊢ AddLeftMono ℝ
        .h.e'_3.h.e'_4a:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:C ≥ 0n:ℤhn:n ≥ 0⊢ a n.toNat = a n.toNat - a 0 + a 0 abelAll goals completed! 🐙
        infer_instanceAll goals completed! 🐙
      _ ≤ C + |a 0| := bya:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:C ≥ 0n:ℤhn:n ≥ 0⊢ |a n.toNat - a 0| + |a 0| ≤ C + |a 0| gcongrbca:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:C ≥ 0n:ℤhn:n ≥ 0⊢ |a n.toNat - a 0| ≤ C; rw [←Real.dist_eq]bca:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:C ≥ 0n:ℤhn:n ≥ 0⊢ dist (a n.toNat) (a 0) ≤ C; convert h n.toNat 0All goals completed! 🐙
  positivityAll goals completed! 🐙

theorem declaration uses 'sorry'Chapter6.Sequence.sup_eq_sSup (a:ℕ → ℝ):
    (a:Sequence).sup = sSup (Set.range (fun n ↦ (a n:EReal))) := bya:ℕ → ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.sup = sSup (Set.range fun n => ↑(a n)) sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Chapter6.Sequence.inf_eq_sInf (a:ℕ → ℝ):
    (a:Sequence).inf = sInf (Set.range (fun n ↦ (a n:EReal))) := bya:ℕ → ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.inf = sInf (Set.range fun n => ↑(a n)) sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Chapter6.Sequence.bddAbove_iff (a:ℕ → ℝ):
    (a:Sequence).bddAbove ↔ BddAbove (Set.range a) := bya:ℕ → ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.bddAbove ↔ BddAbove (Set.range a) sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Chapter6.Sequence.bddBelow_iff (a:ℕ → ℝ):
    (a:Sequence).bddBelow ↔ BddBelow (Set.range a) := bya:ℕ → ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.bddBelow ↔ BddBelow (Set.range a) sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Chapter6.Sequence.Monotone_iff (a:ℕ → ℝ): (a:Sequence).isMonotone ↔ Monotone a := bya:ℕ → ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isMonotone ↔ Monotone a sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Chapter6.Sequence.Antitone_iff (a:ℕ → ℝ): (a:Sequence).isAntitone ↔ Antitone a := bya:ℕ → ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isAntitone ↔ Antitone a sorryAll goals completed! 🐙

Identification with unknown constant 'Filter.MapClusterPt'Filter.MapClusterPt

theorem Chapter6.Sequence.limit_point_iff (a:ℕ → ℝ) (L:ℝ) :
    (a:Sequence).limit_point L ↔ MapClusterPt L Filter.atTop a := bya:ℕ → ℝL:ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.limit_point L ↔ MapClusterPt L Filter.atTop a
  simp_rw [limit_point_def, mapClusterPt_iff_frequently,
           Filter.frequently_atTop, Metric.mem_nhds_iff]a:ℕ → ℝL:ℝ⊢ (∀ ε > 0, ∀ N ≥ 0, ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε) ↔
  ∀ (s : Set ℝ), (∃ ε > 0, Metric.ball L ε ⊆ s) → ∀ (a_2 : ℕ), ∃ b ≥ a_2, a b ∈ s
  constructormpa:ℕ → ℝL:ℝ⊢ (∀ ε > 0, ∀ N ≥ 0, ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε) →
  ∀ (s : Set ℝ), (∃ ε > 0, Metric.ball L ε ⊆ s) → ∀ (a_3 : ℕ), ∃ b ≥ a_3, a b ∈ smpra:ℕ → ℝL:ℝ⊢ (∀ (s : Set ℝ), (∃ ε > 0, Metric.ball L ε ⊆ s) → ∀ (a_2 : ℕ), ∃ b ≥ a_2, a b ∈ s) →
  ∀ ε > 0, ∀ N ≥ 0, ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε
  .mpa:ℕ → ℝL:ℝ⊢ (∀ ε > 0, ∀ N ≥ 0, ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε) →
  ∀ (s : Set ℝ), (∃ ε > 0, Metric.ball L ε ⊆ s) → ∀ (a_3 : ℕ), ∃ b ≥ a_3, a b ∈ s intro h s hs Nmpa:ℕ → ℝL:ℝh:∀ ε > 0, ∀ N ≥ 0, ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ εs:Set ℝhs:∃ ε > 0, Metric.ball L ε ⊆ sN:ℕ⊢ ∃ b ≥ N, a b ∈ s
    obtain ⟨ ε, hε, hεs ⟩ := hsmp.intro.introa:ℕ → ℝL:ℝh:∀ ε > 0, ∀ N ≥ 0, ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ εs:Set ℝN:ℕε:ℝhε:ε > 0hεs:Metric.ball L ε ⊆ s⊢ ∃ b ≥ N, a b ∈ s
    specialize h (ε/2) (half_pos hε) N (bya:ℕ → ℝL:ℝh:∀ ε > 0, ∀ N ≥ 0, ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ εs:Set ℝN:ℕε:ℝhε:ε > 0hεs:Metric.ball L ε ⊆ s⊢ ↑N ≥ 0 positivityAll goals completed! 🐙)
    obtain ⟨ n, hn1, hn2 ⟩ := hmp.intro.intro.intro.introa:ℕ → ℝL:ℝs:Set ℝN:ℕε:ℝhε:ε > 0hεs:Metric.ball L ε ⊆ sn:ℤhn1:n ≥ ↑Nhn2:|(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε / 2⊢ ∃ b ≥ N, a b ∈ s
    have hn : n ≥ 0 := LE.le.trans (bya:ℕ → ℝL:ℝs:Set ℝN:ℕε:ℝhε:ε > 0hεs:Metric.ball L ε ⊆ sn:ℤhn1:n ≥ ↑Nhn2:|(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε / 2⊢ 0 ≤ ↑N positivityAll goals completed! 🐙) hn1
    refine ⟨ n.toNat, ?_, ?_ ⟩mp.intro.intro.intro.intro.refine_1a:ℕ → ℝL:ℝs:Set ℝN:ℕε:ℝhε:ε > 0hεs:Metric.ball L ε ⊆ sn:ℤhn1:n ≥ ↑Nhn2:|(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε / 2hn:n ≥ 0⊢ n.toNat ≥ Nmp.intro.intro.intro.intro.refine_2a:ℕ → ℝL:ℝs:Set ℝN:ℕε:ℝhε:ε > 0hεs:Metric.ball L ε ⊆ sn:ℤhn1:n ≥ ↑Nhn2:|(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε / 2hn:n ≥ 0⊢ a n.toNat ∈ s
    .mp.intro.intro.intro.intro.refine_1a:ℕ → ℝL:ℝs:Set ℝN:ℕε:ℝhε:ε > 0hεs:Metric.ball L ε ⊆ sn:ℤhn1:n ≥ ↑Nhn2:|(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε / 2hn:n ≥ 0⊢ n.toNat ≥ N rwa [ge_iff_le, Int.le_toNat hn]mp.intro.intro.intro.intro.refine_1a:ℕ → ℝL:ℝs:Set ℝN:ℕε:ℝhε:ε > 0hεs:Metric.ball L ε ⊆ sn:ℤhn1:n ≥ ↑Nhn2:|(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε / 2hn:n ≥ 0⊢ ↑N ≤ n
    apply hεsmp.intro.intro.intro.intro.refine_2.aa:ℕ → ℝL:ℝs:Set ℝN:ℕε:ℝhε:ε > 0hεs:Metric.ball L ε ⊆ sn:ℤhn1:n ≥ ↑Nhn2:|(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε / 2hn:n ≥ 0⊢ a n.toNat ∈ Metric.ball L ε
    simp [Real.dist_eq, hn] at hn2 ⊢mp.intro.intro.intro.intro.refine_2.aa:ℕ → ℝL:ℝs:Set ℝN:ℕε:ℝhε:ε > 0hεs:Metric.ball L ε ⊆ sn:ℤhn1:n ≥ ↑Nhn:n ≥ 0hn2:|a n.toNat - L| ≤ ε / 2⊢ |a n.toNat - L| < ε
    linarithAll goals completed! 🐙
  intro h ε hε N hNmpra:ℕ → ℝL:ℝh:∀ (s : Set ℝ), (∃ ε > 0, Metric.ball L ε ⊆ s) → ∀ (a_2 : ℕ), ∃ b ≥ a_2, a b ∈ sε:ℝhε:ε > 0N:ℤhN:N ≥ 0⊢ ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε
  specialize h (Metric.ball L ε) ⟨ ε, hε, fun ⦃a⦄ a ↦ a ⟩ N.toNatmpra:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℤhN:N ≥ 0h:∃ b ≥ N.toNat, a b ∈ Metric.ball L ε⊢ ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε
  obtain ⟨ n, hn1, hn2 ⟩ := hmpr.intro.introa:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℤhN:N ≥ 0n:ℕhn1:n ≥ N.toNathn2:a n ∈ Metric.ball L ε⊢ ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε
  have hn : n ≥ 0 := bya:ℕ → ℝL:ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.limit_point L ↔ MapClusterPt L Filter.atTop a positivityAll goals completed! 🐙
  refine ⟨ n, ?_, ?_ ⟩mpr.intro.intro.refine_1a:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℤhN:N ≥ 0n:ℕhn1:n ≥ N.toNathn2:a n ∈ Metric.ball L εhn:n ≥ 0⊢ ↑n ≥ Nmpr.intro.intro.refine_2a:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℤhN:N ≥ 0n:ℕhn1:n ≥ N.toNathn2:a n ∈ Metric.ball L εhn:n ≥ 0⊢ |(if ↑n ≥ 0 then a (↑n).toNat else 0) - L| ≤ ε
  .mpr.intro.intro.refine_1a:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℤhN:N ≥ 0n:ℕhn1:n ≥ N.toNathn2:a n ∈ Metric.ball L εhn:n ≥ 0⊢ ↑n ≥ N rwa [ge_iff_le, ←Int.toNat_le]mpr.intro.intro.refine_1a:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℤhN:N ≥ 0n:ℕhn1:n ≥ N.toNathn2:a n ∈ Metric.ball L εhn:n ≥ 0⊢ N.toNat ≤ n
  simp [Real.dist_eq, hn] at hn2 ⊢mpr.intro.intro.refine_2a:ℕ → ℝL:ℝε:ℝhε:ε > 0N:ℤhN:N ≥ 0n:ℕhn1:n ≥ N.toNathn:n ≥ 0hn2:|a n - L| < ε⊢ |a n - L| ≤ ε
  linarithAll goals completed! 🐙

Identification with Filter.limsup.{u_1, u_2} {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] (u : β → α) (f : Filter β) : αFilter.limsup

theorem declaration uses 'sorry'Chapter6.Sequence.limsup_eq (a:ℕ → ℝ) :
    (a:Sequence).limsup = Filter.limsup (fun n ↦ (a n:EReal)) Filter.atTop := bya:ℕ → ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.limsup =
  Filter.limsup (fun n => ↑(a n)) Filter.atTop
  simp_rw [Filter.limsup_eq, Filter.eventually_atTop]a:ℕ → ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.limsup =
  sInf {a_1 | ∃ a_2, ∀ b ≥ a_2, ↑(a b) ≤ a_1}
  sorryAll goals completed! 🐙

Identification with Filter.liminf.{u_1, u_2} {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] (u : β → α) (f : Filter β) : αFilter.liminf

theorem declaration uses 'sorry'Chapter6.Sequence.liminf_eq (a:ℕ → ℝ) :
    (a:Sequence).liminf = Filter.liminf (fun n ↦ (a n:EReal)) Filter.atTop := bya:ℕ → ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.liminf =
  Filter.liminf (fun n => ↑(a n)) Filter.atTop
  simp_rw [Filter.liminf_eq, Filter.eventually_atTop]a:ℕ → ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.liminf =
  sSup {a_1 | ∃ a_2, ∀ b ≥ a_2, a_1 ≤ ↑(a b)}
  sorryAll goals completed! 🐙