English
A map f: OnePoint X → Y is continuous iff its restriction to X is continuous and f has a limit at ∞ along coclosedCompact.
Русский
Функция f: OnePoint X → Y непрерывна тогда и только тогда, когда её ограничение на X непрерывно и f имеет предел в бесконечности вдоль coclosedCompact.
LaTeX
$$$\text{Continuous } f \iff \big( \text{Tendsto } (f \circ (\uparrow)) (coclosedCompact X) (\mathcal{N}(f(\infty))) \big) \land \big( \text{Continuous } (f \circ (\uparrow)) \big)$$$
Lean4
theorem continuous_iff {Y : Type*} [TopologicalSpace Y] (f : OnePoint X → Y) :
Continuous f ↔ Tendsto (fun x : X ↦ f x) (coclosedCompact X) (𝓝 (f ∞)) ∧ Continuous (fun x : X ↦ f x) := by
simp only [continuous_iff_continuousAt, OnePoint.forall, continuousAt_coe, continuousAt_infty', Function.comp_def]
