abs_toReal_le_pi

Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

English

For every θ, |θ.toReal| ≤ π.

Русский

Для любого θ выполняется |θ.toReal| ≤ π.

LaTeX

$$$\\\\forall (\\\\theta : Real.Angle), \\\\left|\\\\theta.toReal\\\\right| \\\\le \\\\pi$$$

Lean4

theorem abs_toReal_le_pi (θ : Angle) : |θ.toReal| ≤ π :=
  abs_le.2 ⟨(neg_pi_lt_toReal _).le, toReal_le_pi _⟩

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

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

Разделы

Аффилиация

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