Аналіз I, Розділ 9.3: Граничні значення функцій

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

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

Границі неперервних функцій
Зв'язок із поняттями збіжності фільтрів у Mathlib
Закони щодо границь для функцій

Технічна заувага: у тексті функції Unknown identifier `f`f, які розглядаються, визначені лише на підмножинах Unknown identifier `X`X множини ℝ : Typeℝ і не визначені поза ними. Проте в Lean це призводить до незручних приведень типів при спробах обмежити Unknown identifier `f`f до різних підмножин Unknown identifier `X`X (які технічно не є безпосередньо підмножинами ℝ : Typeℝ, хоча їх можна привести до таких). Щоб уникнути цієї проблеми, ми відходимо від тексту й вважаємо, що наші функції визначені на всьому ℝ : Typeℝ (зрозуміло, що їм присвоюються "сміттеві" значення поза областю Unknown identifier `X`X).

Визначення 9.3.1

abbrev Real.CloseFn (ε:ℝ) (X:Set ℝ) (f: ℝ → ℝ) (L:ℝ) : Prop :=
  ∀ x ∈ X, |f x - L| < ε

Визначення 9.3.3

abbrev Real.CloseNear (ε:ℝ) (X:Set ℝ) (f: ℝ → ℝ) (L:ℝ) (x₀:ℝ) : Prop :=
  ∃ δ > 0, ε.CloseFn (X ∩ .Ioo (x₀-δ) (x₀+δ)) f L

namespace Chapter9

Приклад 9.3.2

declaration uses 'sorry'example : (5:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 4 := by⊢ Real.CloseFn 5 (Set.Icc 1 3) (fun x => x ^ 2) 4 sorryAll goals completed! 🐙

Приклад 9.3.2

declaration uses 'sorry'example : (0.41:ℝ).CloseFn (.Icc 1.9 2.1) (fun x ↦ x^2) 4 := by⊢ Real.CloseFn 0.41 (Set.Icc 1.9 2.1) (fun x => x ^ 2) 4 sorryAll goals completed! 🐙

Приклад 9.3.4

declaration uses 'sorry'example: ¬(0.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 4 := by⊢ ¬Real.CloseFn 0.1 (Set.Icc 1 3) (fun x => x ^ 2) 4
  sorryAll goals completed! 🐙

Приклад 9.3.4

declaration uses 'sorry'example: (0.1:ℝ).CloseNear (.Icc 1 3) (fun x ↦ x^2) 4 2 := by⊢ Real.CloseNear 0.1 (Set.Icc 1 3) (fun x => x ^ 2) 4 2
  sorryAll goals completed! 🐙

Приклад 9.3.5

declaration uses 'sorry'example: ¬(0.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 9 := by⊢ ¬Real.CloseFn 0.1 (Set.Icc 1 3) (fun x => x ^ 2) 9
  sorryAll goals completed! 🐙

Приклад 9.3.5

declaration uses 'sorry'example: (0.1:ℝ).CloseNear (.Icc 1 3) (fun x ↦ x^2) 9 3 := by⊢ Real.CloseNear 0.1 (Set.Icc 1 3) (fun x => x ^ 2) 9 3
  sorryAll goals completed! 🐙

Визначення 9.3.6 (Збіжність функцій у точці)

abbrev Convergesto (X:Set ℝ) (f: ℝ → ℝ) (L:ℝ) (x₀:ℝ) : Prop := ∀ ε > (0:ℝ), ε.CloseNear X f L x₀

Зв'язок із поняттями збіжності фільтрів у Mathlib

theorem Convergesto.iff (X:Set ℝ) (f: ℝ → ℝ) (L:ℝ) (x₀:ℝ) :
  Convergesto X f L x₀ ↔ (nhdsWithin x₀ X).Tendsto f (nhds L) := byX:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto X f L x₀ ↔ Filter.Tendsto f (nhdsWithin x₀ X) (nhds L)
  unfold Convergesto Real.CloseNear Real.CloseFn nhdsWithinX:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ (∀ ε > 0, ∃ δ > 0, ∀ x ∈ X ∩ Set.Ioo (x₀ - δ) (x₀ + δ), |f x - L| < ε) ↔
  Filter.Tendsto f (nhds x₀ ⊓ Filter.principal X) (nhds L)
  rw [LinearOrderedAddCommGroup.tendsto_nhds]X:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ (∀ ε > 0, ∃ δ > 0, ∀ x ∈ X ∩ Set.Ioo (x₀ - δ) (x₀ + δ), |f x - L| < ε) ↔
  ∀ ε > 0, ∀ᶠ (b : ℝ) in nhds x₀ ⊓ Filter.principal X, |f b - L| < ε
  peel with ε hεh.hX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0⊢ (∃ δ > 0, ∀ x ∈ X ∩ Set.Ioo (x₀ - δ) (x₀ + δ), |f x - L| < ε) ↔
  ∀ᶠ (b : ℝ) in nhds x₀ ⊓ Filter.principal X, |f b - L| < ε
  rw [Filter.eventually_inf_principal]h.hX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0⊢ (∃ δ > 0, ∀ x ∈ X ∩ Set.Ioo (x₀ - δ) (x₀ + δ), |f x - L| < ε) ↔ ∀ᶠ (x : ℝ) in nhds x₀, x ∈ X → |f x - L| < ε
  simp [Filter.Eventually, mem_nhds_iff_exists_Ioo_subset]h.hX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0⊢ (∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε) ↔
  ∃ l u, (l < x₀ ∧ x₀ < u) ∧ Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}
  constructorh.h.mpX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0⊢ (∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε) →
  ∃ l u, (l < x₀ ∧ x₀ < u) ∧ Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h.h.mprX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0⊢ (∃ l u, (l < x₀ ∧ x₀ < u) ∧ Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}) →
  ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε
  .h.h.mpX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0⊢ (∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε) →
  ∃ l u, (l < x₀ ∧ x₀ < u) ∧ Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε} intro ⟨ δ, _, _ ⟩h.h.mpX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0δ:ℝleft✝:0 < δright✝:∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε⊢ ∃ l u, (l < x₀ ∧ x₀ < u) ∧ Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}; use x₀-δ, x₀+δ, byX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0δ:ℝleft✝:0 < δright✝:∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε⊢ x₀ - δ < x₀ ∧ x₀ < x₀ + δ grindAll goals completed! 🐙
    intro _rightX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0δ:ℝleft✝:0 < δright✝:∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < εa✝:ℝ⊢ a✝ ∈ Set.Ioo (x₀ - δ) (x₀ + δ) → a✝ ∈ {x | x ∈ X → |f x - L| < ε}; simprightX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0δ:ℝleft✝:0 < δright✝:∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < εa✝:ℝ⊢ x₀ - δ < a✝ → a✝ < x₀ + δ → a✝ ∈ X → |f a✝ - L| < ε; grindAll goals completed! 🐙
  intro ⟨ l, u, ⟨ _, _ ⟩, h ⟩h.h.mprX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}⊢ ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε
  have h1 : 0 < x₀ - l := byX:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto X f L x₀ ↔ Filter.Tendsto f (nhdsWithin x₀ X) (nhds L) linarithAll goals completed! 🐙
  have h2 : 0 < u - x₀ := byX:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto X f L x₀ ↔ Filter.Tendsto f (nhdsWithin x₀ X) (nhds L) linarithAll goals completed! 🐙
  set δ := min (x₀ - l) (u - x₀)h.h.mprX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < _fvar.2615 - _fvar.43897 := ?_mvar.44185h2:0 < _fvar.43898 - _fvar.2615 := ?_mvar.44774δ:ℝ := min (_fvar.2615 - _fvar.43897) (_fvar.43898 - _fvar.2615)⊢ ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε
  observe hδ1 : δ ≤ x₀ - lh.h.mprX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < _fvar.2615 - _fvar.43897 := ?_mvar.44185h2:0 < _fvar.43898 - _fvar.2615 := ?_mvar.44774δ:ℝ := min (_fvar.2615 - _fvar.43897) (_fvar.43898 - _fvar.2615)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - l⊢ ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε
  observe hδ2 : δ ≤ u - x₀h.h.mprX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < _fvar.2615 - _fvar.43897 := ?_mvar.44185h2:0 < _fvar.43898 - _fvar.2615 := ?_mvar.44774δ:ℝ := min (_fvar.2615 - _fvar.43897) (_fvar.43898 - _fvar.2615)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - lhδ2:min (x₀ - l) (u - x₀) ≤ u - x₀⊢ ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε
  use δ, (byX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < _fvar.2615 - _fvar.43897 := 
  lt_of_not_ge fun a =>
    Mathlib.Tactic.Linarith.lt_irrefl
      (Eq.mp
        (congrArg (fun _a => _a < 0)
          (Mathlib.Tactic.Ring.of_eq
            (Mathlib.Tactic.Ring.add_congr
              (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.43897)
                (Mathlib.Tactic.Ring.atom_pf _fvar.2615)
                (Mathlib.Tactic.Ring.sub_pf
                  (Mathlib.Tactic.Ring.neg_add
                    (Mathlib.Tactic.Ring.neg_mul _fvar.2615 (Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                            (Eq.refl (Int.negOfNat 1))))))
                    Mathlib.Tactic.Ring.neg_zero)
                  (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.43897 ^ Nat.rawCast 1 * Nat.rawCast 1)
                    (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.2615 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
              (Mathlib.Tactic.Ring.sub_congr
                (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.2615)
                  (Mathlib.Tactic.Ring.atom_pf _fvar.43897)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul _fvar.43897 (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_gt (_fvar.43897 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)
                      (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.2615 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
                (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
                  (Mathlib.Tactic.Ring.add_pf_add_zero
                    (_fvar.43897 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast +
                      (_fvar.2615 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
              (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.43897 (Nat.rawCast 1)
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.2615 (Nat.rawCast 1)
                    (Mathlib.Meta.NormNum.IsInt.to_isNat
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                        (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                        (Eq.refl (Int.ofNat 0)))))
                  (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
            (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
        (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.sub_neg_of_lt _fvar.43899)
          (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)))h2:0 < _fvar.43898 - _fvar.2615 := 
  lt_of_not_ge fun a =>
    Mathlib.Tactic.Linarith.lt_irrefl
      (Eq.mp
        (congrArg (fun _a => _a < 0)
          (Mathlib.Tactic.Ring.of_eq
            (Mathlib.Tactic.Ring.add_congr
              (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.2615)
                (Mathlib.Tactic.Ring.atom_pf _fvar.43898)
                (Mathlib.Tactic.Ring.sub_pf
                  (Mathlib.Tactic.Ring.neg_add
                    (Mathlib.Tactic.Ring.neg_mul _fvar.43898 (Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                            (Eq.refl (Int.negOfNat 1))))))
                    Mathlib.Tactic.Ring.neg_zero)
                  (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.2615 ^ Nat.rawCast 1 * Nat.rawCast 1)
                    (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.43898 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
              (Mathlib.Tactic.Ring.sub_congr
                (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.43898)
                  (Mathlib.Tactic.Ring.atom_pf _fvar.2615)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul _fvar.2615 (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_gt (_fvar.2615 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)
                      (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.43898 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
                (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
                  (Mathlib.Tactic.Ring.add_pf_add_zero
                    (_fvar.2615 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast +
                      (_fvar.43898 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
              (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.2615 (Nat.rawCast 1)
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.43898 (Nat.rawCast 1)
                    (Mathlib.Meta.NormNum.IsInt.to_isNat
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                        (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                        (Eq.refl (Int.ofNat 0)))))
                  (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
            (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
        (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.sub_neg_of_lt _fvar.43900)
          (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)))δ:ℝ := min (_fvar.2615 - _fvar.43897) (_fvar.43898 - _fvar.2615)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - lhδ2:min (x₀ - l) (u - x₀) ≤ u - x₀⊢ 0 < δ positivityAll goals completed! 🐙); intro x hxX _ _rightX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < _fvar.2615 - _fvar.43897 := ?_mvar.44185h2:0 < _fvar.43898 - _fvar.2615 := ?_mvar.44774δ:ℝ := min (_fvar.2615 - _fvar.43897) (_fvar.43898 - _fvar.2615)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - lhδ2:min (x₀ - l) (u - x₀) ≤ u - x₀x:ℝhxX:x ∈ Xa✝¹:x₀ - δ < xa✝:x < x₀ + δ⊢ |f x - L| < ε
  specialize h (show x ∈ .Ioo l u byX:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto X f L x₀ ↔ Filter.Tendsto f (nhdsWithin x₀ X) (nhds L) simpX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < _fvar.2615 - _fvar.43897 := 
  lt_of_not_ge fun a =>
    Mathlib.Tactic.Linarith.lt_irrefl
      (Eq.mp
        (congrArg (fun _a => _a < 0)
          (Mathlib.Tactic.Ring.of_eq
            (Mathlib.Tactic.Ring.add_congr
              (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.43897)
                (Mathlib.Tactic.Ring.atom_pf _fvar.2615)
                (Mathlib.Tactic.Ring.sub_pf
                  (Mathlib.Tactic.Ring.neg_add
                    (Mathlib.Tactic.Ring.neg_mul _fvar.2615 (Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                            (Eq.refl (Int.negOfNat 1))))))
                    Mathlib.Tactic.Ring.neg_zero)
                  (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.43897 ^ Nat.rawCast 1 * Nat.rawCast 1)
                    (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.2615 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
              (Mathlib.Tactic.Ring.sub_congr
                (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.2615)
                  (Mathlib.Tactic.Ring.atom_pf _fvar.43897)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul _fvar.43897 (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_gt (_fvar.43897 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)
                      (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.2615 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
                (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
                  (Mathlib.Tactic.Ring.add_pf_add_zero
                    (_fvar.43897 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast +
                      (_fvar.2615 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
              (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.43897 (Nat.rawCast 1)
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.2615 (Nat.rawCast 1)
                    (Mathlib.Meta.NormNum.IsInt.to_isNat
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                        (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                        (Eq.refl (Int.ofNat 0)))))
                  (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
            (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
        (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.sub_neg_of_lt _fvar.43899)
          (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)))h2:0 < _fvar.43898 - _fvar.2615 := 
  lt_of_not_ge fun a =>
    Mathlib.Tactic.Linarith.lt_irrefl
      (Eq.mp
        (congrArg (fun _a => _a < 0)
          (Mathlib.Tactic.Ring.of_eq
            (Mathlib.Tactic.Ring.add_congr
              (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.2615)
                (Mathlib.Tactic.Ring.atom_pf _fvar.43898)
                (Mathlib.Tactic.Ring.sub_pf
                  (Mathlib.Tactic.Ring.neg_add
                    (Mathlib.Tactic.Ring.neg_mul _fvar.43898 (Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                            (Eq.refl (Int.negOfNat 1))))))
                    Mathlib.Tactic.Ring.neg_zero)
                  (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.2615 ^ Nat.rawCast 1 * Nat.rawCast 1)
                    (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.43898 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
              (Mathlib.Tactic.Ring.sub_congr
                (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.43898)
                  (Mathlib.Tactic.Ring.atom_pf _fvar.2615)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul _fvar.2615 (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_gt (_fvar.2615 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)
                      (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.43898 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
                (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
                  (Mathlib.Tactic.Ring.add_pf_add_zero
                    (_fvar.2615 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast +
                      (_fvar.43898 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
              (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.2615 (Nat.rawCast 1)
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.43898 (Nat.rawCast 1)
                    (Mathlib.Meta.NormNum.IsInt.to_isNat
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                        (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                        (Eq.refl (Int.ofNat 0)))))
                  (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
            (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
        (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.sub_neg_of_lt _fvar.43900)
          (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)))δ:ℝ := min (_fvar.2615 - _fvar.43897) (_fvar.43898 - _fvar.2615)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - lhδ2:min (x₀ - l) (u - x₀) ≤ u - x₀x:ℝhxX:x ∈ Xa✝¹:x₀ - δ < xa✝:x < x₀ + δ⊢ l < x ∧ x < u; grindAll goals completed! 🐙)
  simpa [hxX] using hAll goals completed! 🐙

Приклад 9.3.8

declaration uses 'sorry'example: Convergesto (.Icc 1 3) (fun x ↦ x^2) 4 2 := by⊢ Convergesto (Set.Icc 1 3) (fun x => x ^ 2) 4 2
  sorryAll goals completed! 🐙

Твердження 9.3.9 / Вправа 9.3.1

theorem declaration uses 'sorry'Convergesto.iff_conv {E:Set ℝ} (f: ℝ → ℝ) (L:ℝ) {x₀:ℝ} (h: AdherentPt x₀ E) :
  Convergesto E f L x₀ ↔ ∀ a:ℕ → ℝ, (∀ n:ℕ, a n ∈ E) →
  Filter.atTop.Tendsto a (nhds x₀) →
  Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds L) := byE:Set ℝf:ℝ → ℝL:ℝx₀:ℝh:AdherentPt x₀ E⊢ Convergesto E f L x₀ ↔
  ∀ (a : ℕ → ℝ),
    (∀ (n : ℕ), a n ∈ E) →
      Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds L)
  sorryAll goals completed! 🐙

theorem Convergesto.comp {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (hf: Convergesto E f L x₀) {a:ℕ → ℝ} (ha: ∀ n:ℕ, a n ∈ E) (hconv: Filter.atTop.Tendsto a (nhds x₀)) :
  Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds L) := byE:Set ℝf:ℝ → ℝL:ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)⊢ Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds L)
  rw [iff_conv f L h] at hfE:Set ℝf:ℝ → ℝL:ℝx₀:ℝh:AdherentPt x₀ Ehf:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ E) →
    Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds L)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)⊢ Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds L); solve_by_elimAll goals completed! 🐙

-- Ремарка 9.3.11: можливо, що це зауваження неточне — гіпотезу `AdherentPt x₀ E` може виявитися безпечно видалити в наведених вище теоремах. Формалізація може це прояснити! Якщо так, цю гіпотезу також можна буде видалити в кількох теоремах нижче.

Наслідок 9.3.13

theorem Convergesto.uniq {E:Set ℝ} {f: ℝ → ℝ} {L L':ℝ} {x₀:ℝ} (h: AdherentPt x₀ E)
  (hf: Convergesto E f L x₀) (hf': Convergesto E f L' x₀) : L = L' := byE:Set ℝf:ℝ → ℝL:ℝL':ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hf':Convergesto E f L' x₀⊢ L = L'
  -- цей доказ написан так, щоб співпадати із структурою оригінального тексту.
  let ⟨ a, ha, hconv ⟩ := (limit_of_AdherentPt _ _).mp hE:Set ℝf:ℝ → ℝL:ℝL':ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hf':Convergesto E f L' x₀a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)⊢ L = L'
  exact tendsto_nhds_unique (hf.comp h ha hconv) (hf'.comp h ha hconv)All goals completed! 🐙

Твердження 9.3.14 (Закони щодо границь функцій)

theorem Convergesto.add {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E)
  (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) :
  Convergesto E (f + g) (L + M) x₀ := byE:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f + g) (L + M) x₀
    -- цей доказ написан так, щоб співпадати із структурою оригінального тексту.
    rw [iff_conv _ _ h] at hf hg ⊢E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehf:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ E) →
    Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds L)hg:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ E) →
    Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => g (a n)) Filter.atTop (nhds M)⊢ ∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ E) →
    Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => (f + g) (a n)) Filter.atTop (nhds (L + M))
    intro a ha hconvE:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehf:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ E) →
    Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds L)hg:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ E) →
    Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => g (a n)) Filter.atTop (nhds M)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)⊢ Filter.Tendsto (fun n => (f + g) (a n)) Filter.atTop (nhds (L + M)); specialize hf a ha hconvE:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehg:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ E) →
    Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => g (a n)) Filter.atTop (nhds M)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)hf:Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds L)⊢ Filter.Tendsto (fun n => (f + g) (a n)) Filter.atTop (nhds (L + M)); specialize hg a ha hconvE:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ea:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)hf:Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds L)hg:Filter.Tendsto (fun n => g (a n)) Filter.atTop (nhds M)⊢ Filter.Tendsto (fun n => (f + g) (a n)) Filter.atTop (nhds (L + M))
    convert hf.add hg using 1All goals completed! 🐙

Твердження 9.3.14 (Закони щодо границь функцій) / Вправа 9.3.2

theorem declaration uses 'sorry'Convergesto.sub {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E)
  (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) :
  Convergesto E (f - g) (L - M) x₀ := byE:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f - g) (L - M) x₀
    sorryAll goals completed! 🐙

Твердження 9.3.14 (Закони щодо границь функцій) / Вправа 9.3.2

theorem declaration uses 'sorry'Convergesto.max {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E)
  (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) :
  Convergesto E (max f g) (max L M) x₀ := byE:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f ⊔ g) (Max.max L M) x₀
    sorryAll goals completed! 🐙

Твердження 9.3.14 (Закони щодо границь функцій) / Вправа 9.3.2

theorem declaration uses 'sorry'Convergesto.min {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E)
  (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) :
  Convergesto E (min f g) (min L M) x₀ := byE:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f ⊓ g) (Min.min L M) x₀
    sorryAll goals completed! 🐙

Твердження 9.3.14 (Закони щодо границь функцій) / Вправа 9.3.2

theorem declaration uses 'sorry'Convergesto.smul {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E)
  (hf: Convergesto E f L x₀) (c:ℝ) :
  Convergesto E (c • f) (c * L) x₀ := byE:Set ℝf:ℝ → ℝL:ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀c:ℝ⊢ Convergesto E (c • f) (c * L) x₀
    sorryAll goals completed! 🐙

Твердження 9.3.14 (Limit laws for functions) / Вправа 9.3.2

theorem declaration uses 'sorry'Convergesto.mul {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E)
  (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) :
  Convergesto E (f * g) (L * M) x₀ := byE:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f * g) (L * M) x₀
    sorryAll goals completed! 🐙

Твердження 9.3.14 (Закони щодо границь функцій) / Вправа 9.3.2. Гіпотезу в книзі про те, що Unknown identifier `g`g не звертається в нулі на Unknown identifier `E`E, можна опустити.

theorem declaration uses 'sorry'Convergesto.div {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (hM: M ≠ 0)
  (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) :
  Convergesto E (f / g) (L / M) x₀ := byE:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ EhM:M ≠ 0hf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f / g) (L / M) x₀
    sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Convergesto.const {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (c:ℝ)
  : Convergesto E (fun x ↦ c) c x₀ := byE:Set ℝx₀:ℝh:AdherentPt x₀ Ec:ℝ⊢ Convergesto E (fun x => c) c x₀
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Convergesto.id {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E)
  : Convergesto E (fun x ↦ x) x₀ x₀ := byE:Set ℝx₀:ℝh:AdherentPt x₀ E⊢ Convergesto E (fun x => x) x₀ x₀
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Convergesto.sq {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E)
  : Convergesto E (fun x ↦ x^2) x₀ (x₀^2) := byE:Set ℝx₀:ℝh:AdherentPt x₀ E⊢ Convergesto E (fun x => x ^ 2) x₀ (x₀ ^ 2)
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Convergesto.linear {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (c:ℝ)
  : Convergesto E (fun x ↦ c * x) x₀ (c * x₀) := byE:Set ℝx₀:ℝh:AdherentPt x₀ Ec:ℝ⊢ Convergesto E (fun x => c * x) x₀ (c * x₀)
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Convergesto.quadratic {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (c d:ℝ)
  : Convergesto E (fun x ↦ x^2 + c * x + d) x₀ (x₀^2 + c * x₀ + d) := byE:Set ℝx₀:ℝh:AdherentPt x₀ Ec:ℝd:ℝ⊢ Convergesto E (fun x => x ^ 2 + c * x + d) x₀ (x₀ ^ 2 + c * x₀ + d)
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Convergesto.restrict {X Y:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (h: AdherentPt x₀ X) (hf: Convergesto X f L x₀) (hY: Y ⊆ X) : Convergesto Y f L x₀ := byX:Set ℝY:Set ℝf:ℝ → ℝL:ℝx₀:ℝh:AdherentPt x₀ Xhf:Convergesto X f L x₀hY:Y ⊆ X⊢ Convergesto Y f L x₀
  sorryAll goals completed! 🐙

theorem Real.sign_def (x:ℝ) : Real.sign x = if x < 0 then -1 else if x > 0 then 1 else 0 := rfl

Приклад 9.3.16

theorem declaration uses 'sorry'Convergesto.sign_right : Convergesto (.Ioi 0) Real.sign 1 0 := by⊢ Convergesto (Set.Ioi 0) Real.sign 1 0 sorryAll goals completed! 🐙

Приклад 9.3.16

theorem declaration uses 'sorry'Convergesto.sign_left : Convergesto (.Iio 0) Real.sign (-1) 0 := by⊢ Convergesto (Set.Iio 0) Real.sign (-1) 0 sorryAll goals completed! 🐙

Приклад 9.3.16

theorem declaration uses 'sorry'Convergesto.sign_all : ¬ ∃ L, Convergesto (.univ) Real.sign L 0 := by⊢ ¬∃ L, Convergesto Set.univ Real.sign L 0 sorryAll goals completed! 🐙

noncomputable abbrev f_9_3_17 : ℝ → ℝ := fun x ↦ if x = 0 then 1 else 0

theorem declaration uses 'sorry'Convergesto.f_9_3_17_remove : Convergesto (.univ \ {0}) f_9_3_17 0 0 := by⊢ Convergesto (Set.univ \ {0}) f_9_3_17 0 0 sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Convergesto.f_9_3_17_all : ¬ ∃ L, Convergesto .univ f_9_3_17 L 0 := by⊢ ¬∃ L, Convergesto Set.univ f_9_3_17 L 0 sorryAll goals completed! 🐙

Твердження 9.3.18 / Вправа 9.3.3

theorem declaration uses 'sorry'Convergesto.local {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) {δ:ℝ} (hδ: δ > 0) :
  Convergesto E f L x₀ ↔ Convergesto (E ∩ .Ioo (x₀-δ) (x₀+δ)) f L x₀ := byE:Set ℝf:ℝ → ℝL:ℝx₀:ℝh:AdherentPt x₀ Eδ:ℝhδ:δ > 0⊢ Convergesto E f L x₀ ↔ Convergesto (E ∩ Set.Ioo (x₀ - δ) (x₀ + δ)) f L x₀
    sorryAll goals completed! 🐙

Приклад 9.3.19. Суть цього прикладу дещо втрачається через можливість прибрати гіпотезу про ненульовість Unknown identifier `g`g у відповідній частині твердження 9.3.14

declaration uses 'sorry'example : Convergesto .univ (fun x ↦ (x+2)/(x+1)) (4/3:ℝ) 2 := by⊢ Convergesto Set.univ (fun x => (x + 2) / (x + 1)) (4 / 3) 2 sorryAll goals completed! 🐙

Приклад 9.3.20

declaration uses 'sorry'example : Convergesto (.univ \ {1}) (fun x ↦ (x^2-1)/(x-1)) 2 1 := by⊢ Convergesto (Set.univ \ {1}) (fun x => (x ^ 2 - 1) / (x - 1)) 2 1 sorryAll goals completed! 🐙

open Classical in
/-- Приклад 9.3.21 -/
noncomputable abbrev f_9_3_21 : ℝ → ℝ := fun x ↦ if x ∈ (fun q:ℚ ↦ (q:ℝ)) '' .univ then 1 else 0

declaration uses 'sorry'example : Filter.atTop.Tendsto (fun n ↦ f_9_3_21 (1/n:ℝ)) (nhds 1) := by⊢ Filter.Tendsto (fun n => f_9_3_21 (1 / n)) Filter.atTop (nhds 1) sorryAll goals completed! 🐙

declaration uses 'sorry'example : Filter.atTop.Tendsto (fun n ↦ f_9_3_21 ((Real.sqrt 2)/n:ℝ)) (nhds 0) := by⊢ Filter.Tendsto (fun n => f_9_3_21 (√2 / n)) Filter.atTop (nhds 0) sorryAll goals completed! 🐙

declaration uses 'sorry'example : ¬ ∃ L, Convergesto .univ f_9_3_21 L 0 := by⊢ ¬∃ L, Convergesto Set.univ f_9_3_21 L 0 sorryAll goals completed! 🐙

/- Вправа 9.3.4: Сформулюйте визначення верхньої та нижньої границі (limit superior і limit inferior) для функцій і доведіть аналог твердження 9.3.9 для цих визначень. -/

Вправа 9.3.5 (Неперервна версія принципу стискування)

theorem declaration uses 'sorry'Convergesto.squeeze {E:Set ℝ} {f g h: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (had: AdherentPt x₀ E)
  (hfg: ∀ x ∈ E, f x ≤ g x) (hgh: ∀ x ∈ E, g x ≤ h x)
  (hf: Convergesto E f L x₀) (hh: Convergesto E h L x₀) :
  Convergesto E g L x₀ := byE:Set ℝf:ℝ → ℝg:ℝ → ℝh:ℝ → ℝL:ℝx₀:ℝhad:AdherentPt x₀ Ehfg:∀ x ∈ E, f x ≤ g xhgh:∀ x ∈ E, g x ≤ h xhf:Convergesto E f L x₀hh:Convergesto E h L x₀⊢ Convergesto E g L x₀
    sorryAll goals completed! 🐙

end Chapter9