mathlib

f596077f - feat(geometry/manifold/instances): sphere is a topological manifold (#5591)

feat(geometry/manifold/instances): sphere is a topological manifold (#5591) Construct stereographic projection, as a local homeomorphism from the unit sphere in an inner product space `E` to a hyperplane in `E`. Make a charted space instance for the sphere, with these stereographic projections as the atlas. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>