abs_toReal_eq_pi_div_two_iff — Mathlib

English

For any θ, |θ.toReal| = π/2 iff θ = π/2 or θ = −π/2.

Русский

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

LaTeX

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

Lean4

theorem abs_toReal_eq_pi_div_two_iff {θ : Angle} : |θ.toReal| = π / 2 ↔ θ = (π / 2 : ℝ) ∨ θ = (-π / 2 : ℝ) := by
  rw [abs_eq (div_nonneg Real.pi_pos.le two_pos.le), ← neg_div, toReal_eq_pi_div_two_iff, toReal_eq_neg_pi_div_two_iff]

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