two_nsmul_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}, \\\\Big((2 : \\\\mathbb{N}) \\\\cdot \\\\theta).toReal = 2 * \\\\theta.toReal \\\\iff \\\\theta.toReal ∈ (-\\\\pi / 2) (\\\\pi / 2)$$$

Lean4

theorem two_nsmul_toReal_eq_two_mul {θ : Angle} :
    ((2 : ℕ) • θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2) :=
  mod_cast nsmul_toReal_eq_mul two_ne_zero

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