toReal — Mathlib

English

The map Real.Angle.toReal sends an angle to the unique real representative in the interval (-π, π].

Русский

Отображение Real.Angle.toReal переводит угол в уникальный действительный представитель в интервале (-π, π].

LaTeX

$$$\operatorname{toReal}(\theta) \in (-\pi, \pi] \;\wedge\; \theta - \operatorname{toReal}(\theta) \in 2\pi\mathbb{Z}$$$

Lean4

/-- Convert a `Real.Angle` to a real number in the interval `Ioc (-π) π`. -/
def toReal (θ : Angle) : ℝ :=
  (toIocMod_periodic two_pi_pos (-π)).lift θ

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