English
The unit sphere in a real inner product space E is a real-analytic manifold modelled on Euclidean space of dimension n, via the stereographic atlas.
Русский
Единичная сфера в реальном пространстве E является аналитическим многообразием, модeлируемым евклидовым пространством размерности n, через атлас стереографической проекции.
LaTeX
$$$IsManifold(\\text{sphere}(0,E), \\omega, \\text{sphere})$$$
Lean4
/-- The unit sphere in an `n + 1`-dimensional inner product space `E` is an analytic manifold,
modelled on the Euclidean space of dimension `n`. -/
instance instIsManifoldSphere {n : ℕ} [Fact (finrank ℝ E = n + 1)] : IsManifold (𝓡 n) ω (sphere (0 : E) 1) :=
isManifold_of_contDiffOn (𝓡 n) ω (sphere (0 : E) 1)
(by
rintro _ _ ⟨v, rfl⟩ ⟨v', rfl⟩
let U := (OrthonormalBasis.fromOrthogonalSpanSingleton (𝕜 := ℝ) n (ne_zero_of_mem_unit_sphere v)).repr
let U' := (OrthonormalBasis.fromOrthogonalSpanSingleton (𝕜 := ℝ) n (ne_zero_of_mem_unit_sphere v')).repr
have H₁ :=
U'.contDiff.comp_contDiffOn
(contDiffOn_stereoToFun (n := ω))
-- Porting note: need to help with implicit variables again
have H₂ :=
(contDiff_stereoInvFunAux (m := ω) (v := v.val) |>.comp (ℝ ∙ (v : E))ᗮ.subtypeL.contDiff).comp U.symm.contDiff
convert H₁.comp_inter (H₂.contDiffOn : ContDiffOn ℝ ω _ Set.univ) using 1
-- -- squeezed from `ext, simp [sphere_ext_iff, stereographic'_symm_apply, real_inner_comm]`
simp only [OpenPartialHomeomorph.trans_toPartialEquiv, OpenPartialHomeomorph.symm_toPartialEquiv,
PartialEquiv.trans_source, PartialEquiv.symm_source, stereographic'_target, stereographic'_source]
simp only [modelWithCornersSelf_coe, modelWithCornersSelf_coe_symm, Set.range_id, Set.inter_univ, Set.univ_inter,
Set.compl_singleton_eq, Set.preimage_setOf_eq]
simp only [id, comp_apply, Submodule.subtypeL_apply, OpenPartialHomeomorph.coe_coe_symm, innerSL_apply, Ne,
sphere_ext_iff, real_inner_comm (v' : E)]
rfl)
