continuous_iff_from_nat — Mathlib

English

Let f map the one-point compactification of the natural numbers into a topological space Y. Then f is continuous if and only if the sequence x ↦ f(x) converges to f(∞) in Y along the natural numbers; i.e., f is continuous exactly when f(n) → f(∞) as n → ∞.

Русский

Пусть f: OnePoint ℕ → Y; тогда f непрерывно тогда и только тогда, когда последовательность f(n) сходится к f(∞) в Y по направлению к бесконечности, т.е. f(n) → f(∞) при n → ∞.

LaTeX

$$$\\text{Continuous}(f) \\iff \\operatorname{Tendsto}(\\lambda n:\\mathbb{N}.\\, f(n))\\_{\\mathrm{atTop}}(\\mathcal{N}(f(\\infty))).$$$

Lean4

theorem continuous_iff_from_nat {Y : Type*} [TopologicalSpace Y] (f : OnePoint ℕ → Y) :
    Continuous f ↔ Tendsto (fun x : ℕ ↦ f x) atTop (𝓝 (f ∞)) := by
  rw [continuous_iff_from_discrete, Nat.cofinite_eq_atTop]

Похожие утверждения