toCircle — Mathlib

English

The Real.Angle toCircle map sends an angle to the corresponding point on the unit circle by applying the exponential map.

Русский

Отображение Real.Angle toCircle переводит угол в соответствующую точку на единичной окружности через экспоненту.

LaTeX

$$$$ \operatorname{toCircle}\,[x] = \exp(x) \,\text{(modulo the period, i.e., on the quotient).} $$$$

Lean4

/-- `Circle.exp`, applied to a `Real.Angle`. -/
noncomputable def toCircle (θ : Angle) : Circle :=
  Circle.periodic_exp.lift θ

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