toReal_coe_eq_self_iff_mem_Ioc

Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

URI: https://scilib.ai/kg/mathlib#Real.Angle.toReal_coe_eq_self_iff_mem_Ioc

English

For θ ∈ ℝ, (θ : Angle).toReal = θ iff θ ∈ Ioc(−π, π).

Русский

Для θ ∈ ℝ, (θ : Angle).toReal = θ эквивалентно θ ∈ Ioc(−π, π).

LaTeX

$$$(\theta : \Angle).toReal = \theta \iff \theta \in \mathrm{Ioc}(-\pi, \pi)$$$

Lean4

theorem toReal_coe_eq_self_iff_mem_Ioc {θ : ℝ} : (θ : Angle).toReal = θ ↔ θ ∈ Set.Ioc (-π) π := by
  rw [toReal_coe_eq_self_iff, ← Set.mem_Ioc]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru