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

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:

• Bare-bones API for the Mathlib versions of adherent at infinity, and limits at infinity.

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

Визначення 9.10.1 (Infinite adherent point). We use ¬ BddAbove X as our notation for +∞ being an adherent point

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 (Limit at infinity)