homeomorphCircle'_apply_mk — Mathlib

English

For every real x, the canonical identification between the additive circle and the ordinary circle is given by the exponential map; in particular, the image is the point e^{i x} on the unit circle.

Русский

Для любого действительного x каноническое соответствие между аддитивным кругом и единичной окружностью задается экспоненциальным отображением; соответственно точка полученная равна e^{i x} на единичной окружности.

LaTeX

$$$\\forall x \\in \\mathbb{R},\\; h'(x) = \\exp(i x) \\;=\\; \\mathrm{Circle.exp}(x)$$$

Lean4

theorem homeomorphCircle'_apply_mk (x : ℝ) : homeomorphCircle' x = Circle.exp x :=
  rfl

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