Commit 2026-08-21 02:09 1f290110

feat: Unitization R C₀(X, R) ≃ C(OnePoint X, R) (#42934) We construct in this PR various bundlings of the following maps:

• ZeroAtInftyContinuousMap.toOnePoint : C₀(X, R) → C(OnePoint X, R) : the extension of f : C₀(X, R) to the function which takes the value 0 at ∞
• ContinuousMap.toZeroAtInfty: C(OnePoint X, R) → C₀(X, R) : f ↦ fun x ↦ g x - g ∞

• ZeroAtInftyContinuousMap.unitizationEquiv : Unitization R C₀(X, R) ≃ C(OnePoint X, R) : lift ZeroAtInftyContinuousMap.toOnePoint to an equivalence from the Unitization, with inverse given by f ↦ .mk (f ∞, f.toZeroAtInfty)