continuous_iff_convergent — Mathlib

English

For any topological space Y, a function f: ℕ ∪ {∞} → Y is continuous if and only if the sequence f(n) converges to f(∞) in Y.

Русский

Для любого топологического пространства Y функция f: ℕ ∪ {∞} → Y непрерывна тогда и только тогда, когда последовательность f(n) сходится к f(∞) в Y.

LaTeX

$$$\text{Continuous}(f) \iff \operatorname{Tendsto}(\lambda n. f(n))_{n\to\infty} (\mathcal{N}(f(\infty)))$$$

Lean4

theorem continuous_iff_convergent {Y : Type*} [TopologicalSpace Y] (f : ℕ∪{∞} → Y) :
    Continuous f ↔ Tendsto (fun x : ℕ ↦ f x) atTop (𝓝 (f ∞)) :=
  continuous_iff_from_nat f

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