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

Definition 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| < ε

Definition 9.10.13 (Limit at infinity)