instChartedSpaceEuclideanSpaceRealFinElemHAddNatOfNatSphere

English

The unit sphere in a real inner product space E is a charted space modelled on the Euclidean space of dimension n, via stereographic projection.

Русский

Единичная сфера в пространстве E над R является пространством с чартами, смоделированным на евклидово пространство размерности n посредством проекции стереографической.

LaTeX

$$$\\text{ChartedSpace}(\\mathbb{R}^{n}, \\omega) (\\text{sphere}(0,E))$$$

Lean4

instance (n : ℕ) : ChartedSpace (EuclideanSpace ℝ (Fin n)) (sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) :=
  have := Fact.mk (@finrank_euclideanSpace_fin ℝ _ (n + 1))
  EuclideanSpace.instChartedSpaceSphere

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