English
There is a bijection between continuous maps from OnePoint X to Y (with X infinite discrete) and pairs (f, L) where f: X → Y is arbitrary and L is a limit point of f along cofinite convergence.
Русский
Существует bi-екция между непрерывными отображениями OnePoint X → Y и парами (f, L) с f: X → Y и ограничением предела L вдоль кофинитного сходства.
LaTeX
$$Equiv (ContinuousMap (OnePoint X) Y) (Subtype (\lambda f => Exists L, Tendsto (fun x => f x) cofinite (nhds L)))$$
Lean4
/-- Continuous maps out of the one point compactification of an infinite discrete space to a Hausdorff
space correspond bijectively to "convergent" maps out of the discrete space.
-/
noncomputable def continuousMapDiscreteEquiv (Y : Type*) [DiscreteTopology X] [TopologicalSpace Y] [T2Space Y]
[Infinite X] : C(OnePoint X, Y) ≃ { f : X → Y // ∃ L, Tendsto (fun x : X ↦ f x) cofinite (𝓝 L) }
where
toFun f := ⟨(f ·), ⟨f ∞, continuous_iff_from_discrete _ |>.mp (map_continuous f)⟩⟩
invFun
f :=
{ toFun := fun x =>
match x with
| ∞ => Classical.choose f.2
| some x => f.1 x
continuous_toFun := continuous_iff_from_discrete _ |>.mpr <| Classical.choose_spec f.2 }
left_inv
f := by
ext x
refine OnePoint.rec ?_ ?_ x
· refine tendsto_nhds_unique ?_ (continuous_iff_from_discrete _ |>.mp <| map_continuous f)
let f' : { f : X → Y // ∃ L, Tendsto (fun x : X ↦ f x) cofinite (𝓝 L) } :=
⟨fun x ↦ f x, ⟨f ∞, continuous_iff_from_discrete f |>.mp <| map_continuous f⟩⟩
exact Classical.choose_spec f'.property
· simp
