instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere

English

The sphere is a manifold modeled on Euclidean space of dimension n, with charts given by stereographic projections.

Русский

Сфера является многообразием, моделируемым евклидовым пространством размерности n; чарты заданы стереографическими проекциями.

LaTeX

$$$\\text{IsManifold}(\\text{sphere}(0,E), \\omega, \\text{sphere})$$$

Lean4

instance (n : ℕ) : IsManifold (𝓡 n) ω (sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) :=
  haveI := Fact.mk (@finrank_euclideanSpace_fin ℝ _ (n + 1))
  EuclideanSpace.instIsManifoldSphere

Похожие утверждения