two_zsmul_toReal_eq_two_mul_sub_two_pi

English

For any angle θ, the real value of twice θ with integer doubling equals 2θ.toReal − 2π if and only if θ.toReal > π/2.

Русский

Для любого угла θ реальное значение двойного угла с целочисленным удвоением равно 2θ.toReal − 2π тогда и только тогда, когда θ.toReal > π/2.

LaTeX

$$$((2:\mathbb{Z})\cdot \theta).toReal = 2\,\theta.toReal - 2\pi \;\iff\; \tfrac{\pi}{2} < \theta.toReal$$$

Lean4

theorem two_zsmul_toReal_eq_two_mul_sub_two_pi {θ : Angle} :
    ((2 : ℤ) • θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal := by
  rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul_sub_two_pi]

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