instChartedSpaceEuclideanSpaceRealFinOfNatNatCircle

English

The unit circle in ℂ is a charted space modeled on Euclidean space of dimension 1 over ℝ, i.e., EuclideanSpace(ℝ, Fin 1).

Русский

Единичная окружность в ℂ является картированным пространством, моделируемым на Евклидово пространство размерности 1 над ℝ.

LaTeX

$$The unit circle in $\mathbb{C}$ is a charted space modelled on $\mathrm{EuclideanSpace}(\mathbb{R}, \mathrm{Fin}(1))$.$$

Lean4

/-- The unit circle in `ℂ` is a charted space modelled on `EuclideanSpace ℝ (Fin 1)`.  This
follows by definition from the corresponding result for `Metric.Sphere`. -/
instance : ChartedSpace (EuclideanSpace ℝ (Fin 1)) Circle :=
  EuclideanSpace.instChartedSpaceSphere

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