Commit 2023-07-15 22:54 cd8b72bc

View on Github →

feat: port Geometry.Manifold.Instances.Sphere (#5571)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/Instances/Sphere.lean

added theorem ContMDiff.codRestrict_sphere

added theorem contDiffOn_stereoToFun

added theorem contDiff_stereoInvFunAux

added theorem contMDiff_coe_sphere

added theorem contMDiff_expMapCircle

added theorem contMDiff_neg_sphere

added theorem continuousOn_stereoToFun

added theorem continuous_stereoInvFun

added theorem finrank_real_complex_fact'

added theorem hasFDerivAt_stereoInvFunAux

added theorem hasFDerivAt_stereoInvFunAux_comp_coe

added theorem mfderiv_coe_sphere_injective

added theorem range_mfderiv_coe_sphere

added theorem sphere_ext_iff

added def stereoInvFun

added def stereoInvFunAux

added theorem stereoInvFunAux_apply

added theorem stereoInvFunAux_mem

added theorem stereoInvFun_apply

added theorem stereoInvFun_ne_north_pole

added def stereoToFun

added theorem stereoToFun_apply

added theorem stereo_left_inv

added theorem stereo_right_inv

added def stereographic'

added theorem stereographic'_source

added theorem stereographic'_symm_apply

added theorem stereographic'_target

added def stereographic

added theorem stereographic_apply

added theorem stereographic_apply_neg

added theorem stereographic_neg_apply

added theorem stereographic_source

added theorem stereographic_target