two_zsmul_toReal_eq_two_mul — Mathlib

English

For any θ, ((2 : ℤ) • θ).toReal = 2 * θ.toReal iff θ.toReal ∈ (-π/2, π/2).

Русский

Для любого θ: ((2 : ℤ) • θ).toReal = 2 * θ.toReal тогда и только тогда, когда θ.toReal ∈ (-π/2, π/2).

LaTeX

$$$\\\\forall {\\\\theta : Real.Angle}, \\\\( (2 : \\\\mathbb{Z}) \\\\cdot \\\\theta).toReal = 2 * \\\\theta.toReal \\\\iff \\\\theta.toReal ∈ (-\\\\pi / 2) (\\\\pi / 2)$$$

Lean4

theorem two_zsmul_toReal_eq_two_mul {θ : Angle} :
    ((2 : ℤ) • θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2) := by
  rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul]

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