One-point compactification of Euclidean space is homeomorphic to the sphere.

noncomputable def onePointHyperplaneHomeoUnitSphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {v : E} (hv : ‖v‖ = 1) : OnePoint ↥(ℝ ∙ v)ᗮ ≃ₜ ↑(Metric.sphere 0 1)

A homeomorphism from the one-point compactification of a hyperplane in Euclidean space to the sphere.

Equations

• onePointHyperplaneHomeoUnitSphere hv = OnePoint.equivOfIsEmbeddingOfRangeEq ⟨v, ⋯⟩ ↑(stereographic hv).symm ⋯ ⋯

noncomputable def onePointEquivSphereOfFinrankEq {ι : Type u_1} {V : Type u_2} [Fintype ι] [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [T2Space V] (h : Module.finrank ℝ V + 1 = Fintype.card ι) : OnePoint V ≃ₜ ↑(Metric.sphere 0 1)

A homeomorphism from the one-point compactification of a finite-dimensional real vector space to the sphere.

Equations

• onePointEquivSphereOfFinrankEq h = (↑⋯.some).onePointCongr.trans (onePointHyperplaneHomeoUnitSphere ⋯)