Def onePointHyperplaneHomeoUnitSphere

Modification history

2025-06-05 15:01
Mathlib/Topology/Compactification/OnePoint/Sphere.lean
feat: One-point compactification of Euclidean space homeomorphic to sphere (#18711) …
Added onePointHyperplaneHomeoUnitSphereView on Github →