contMDiff_circleExp — Mathlib

English

The map t ↦ exp(i t) from ℝ to the unit circle is analytic.

Русский

Отображение $t \mapsto e^{it}$ от ℝ к единичной окружности аналитично.

LaTeX

$$The map $\mathbb{R} \to \mathbb{S}^1$, $t \mapsto e^{it}$ is ContMDiff of class appropriate to the circle.$$

Lean4

/-- The map `fun t ↦ exp (t * I)` from `ℝ` to the unit circle in `ℂ` is analytic. -/
theorem contMDiff_circleExp {m : WithTop ℕ∞} : ContMDiff 𝓘(ℝ, ℝ) (𝓡 1) m Circle.exp :=
  (contDiff_exp.comp (contDiff_id.smul contDiff_const)).contMDiff.codRestrict_sphere _

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