Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-30 22:44 f596077f

View on Github →

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.

Estimated changes

added theorem abs_sq_eq
added theorem times_cont_diff.inv
added theorem times_cont_diff_on.div
added theorem times_cont_diff_on.inv
added theorem coe_norm
added def stereo_inv_fun
added theorem stereo_inv_fun_apply
added theorem stereo_inv_fun_aux_mem
added theorem stereo_left_inv
added theorem stereo_right_inv
added def stereo_to_fun
added theorem stereo_to_fun_apply
added def stereographic'
added theorem stereographic'_source
added theorem stereographic'_target
added def stereographic
added theorem stereographic_source
added theorem stereographic_target
added theorem continuous_on.smul