two_nsmul_toReal_eq_two_mul_add_two_pi

English

For any angle θ, twice θ mapped to real equals 2θ.toReal + 2π if and only if θ.toReal ≤ −π/2.

Русский

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

LaTeX

$$$((2:\mathbb{N})\cdot \theta).toReal = 2\,\theta.toReal + 2\pi \;\iff\; \theta.toReal \le -\frac{\pi}{2}$$$

Lean4

theorem two_nsmul_toReal_eq_two_mul_add_two_pi {θ : Angle} :
    ((2 : ℕ) • θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2 :=
  by
  nth_rw 1 [← coe_toReal θ]
  rw [← coe_nsmul, two_nsmul, ← two_mul, toReal_coe_eq_self_add_two_pi_iff, Set.mem_Ioc]
  refine
    ⟨fun h => by linarith, fun h => ⟨by linarith [pi_pos, neg_pi_lt_toReal θ], (le_div_iff₀' (zero_lt_two' ℝ)).1 h⟩⟩

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