continuous_iff_from_discrete — Mathlib

English

For a discrete space X, a map f: OnePoint X → Y is continuous iff it is cofinite-continuous (i.e., continuous on X in the discrete topology).

Русский

Для дискретного пространства X отображение f: OnePoint X → Y непрерывно тогда и только тогда, когда оно непрерывно на X в дискретной топологии (кофинитная непрерывность).

LaTeX

$$$\text{Continuous } f \iff \text{Tendsto } f \text{ на cofinite} \ (\mathcal{N} f(\infty))$$$

Lean4

theorem continuous_iff_from_discrete {Y : Type*} [TopologicalSpace Y] [DiscreteTopology X] (f : OnePoint X → Y) :
    Continuous f ↔ Tendsto (fun x : X ↦ f x) cofinite (𝓝 (f ∞)) := by
  simp [continuous_iff, cocompact_eq_cofinite, continuous_of_discreteTopology]

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