English
For maps f: X → Y between topological spaces, continuity of the extension OnePoint.map f is equivalent to f being continuous and f tending to a limit at infinity in the coclosedCompact filter.
Русский
Для отображения f: X → Y непрерывность расширения OnePoint.map f равносильна тому, что f непрерывно на X и что при бесконечности f стремится к пределу в фильтре coclosedCompact.
LaTeX
$$$\\text{Continuous}(\\mathrm{OnePoint.map} f) \\iff \\text{Continuous}(f) \\wedge \\operatorname{Tendsto}(f, \\mathrm{coclosedCompact}(X), \\mathrm{coclosedCompact}(Y)).$$$
Lean4
theorem continuous_map_iff [TopologicalSpace Y] {f : X → Y} :
Continuous (OnePoint.map f) ↔ Continuous f ∧ Tendsto f (coclosedCompact X) (coclosedCompact Y) :=
by
simp_rw [continuous_iff, map_some, ← comap_coe_nhds_infty, tendsto_comap_iff, map_infty,
isOpenEmbedding_coe.isInducing.continuous_iff (Y := Y)]
exact and_comm
