toReal_eq_pi_iff

Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

English

For any θ, θ.toReal = π/2 if and only if θ = π/2.

Русский

Для любого θ: θ.toReal = π/2 тогда и только тогда, когда θ = π/2.

LaTeX

$$$\\\\forall {\\\\theta : Real.Angle}, \\\\theta.toReal = \\\\frac{\\\\pi}{2} \\\\iff \\\\theta = \\\\(\\\\frac{\\\\pi}{2} : Angle)$$$$

Lean4

@[simp]
theorem toReal_eq_pi_iff {θ : Angle} : θ.toReal = π ↔ θ = π := by rw [← toReal_inj, toReal_pi]

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

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

Разделы

Аффилиация

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