Аналіз I, Розділ 9.10: Границі на нескінченності

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

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

• Базовий набір API для версій Mathlib щодо збіжності до нескінченності та границь на нескінченності.

theorem Chapter9.BddAbove.unbounded_iff (X : Set ℝ) : ¬BddAbove X ↔ ∀ (M : ℝ), ∃ x ∈ X, x > M

Визначення 9.10.1 (Нескінченна точка дотику). Ми використовуємо ¬ BddAbove X як позначення того, що +∞ є точкою дотику множини X.

theorem Chapter9.BddAbove.unbounded_iff' (X : Set ℝ) : ¬BddAbove X ↔ sSup ((fun (x : ℝ) => ↑x) '' X) = ⊤

theorem Chapter9.BddBelow.unbounded_iff (X : Set ℝ) : ¬BddBelow X ↔ ∀ (M : ℝ), ∃ x ∈ X, x < M

theorem Chapter9.BddBelow.unbounded_iff' (X : Set ℝ) : ¬BddBelow X ↔ sInf ((fun (x : ℝ) => ↑x) '' X) = ⊥

theorem Chapter9.Filter.Tendsto.AtTop.iff {X : Set ℝ} (f : ℝ → ℝ) (L : ℝ) : Filter.Tendsto f (Filter.atTop ⊓ Filter.principal X) (nhds L) ↔ ∀ ε > 0, ∃ (M : ℝ), ∀ x ∈ X ∩ Set.Ici M, |f x - L| < ε

Визначення 9.10.13 (Границя на нескінченності)