toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff

English

For any real θ and integer k, (Real.Angle.coe θ).toReal = θ − 2 k π iff θ ∈ Ioc ((2 k − 1) π) ((2 k + 1) π).

Русский

Для любого действительного θ и целого k: Real.Angle.coe θ .toReal = θ − 2 k π эквивалентно θ ∈ Ioc ((2 k − 1) π) ((2 k + 1) π).

LaTeX

$$$\\\\forall {\\\\theta : Real} {k : Int}, \\\\Big( Real.Angle.coe \\\\theta\\\\).toReal = \\\\theta - 2 * k * π \\\\iff \\\\theta ∈ \\\\mathrm{Ioc} ((2 * k - 1 : \\Real) * π) ((2 * k + 1) * π)$$$

Lean4

theorem toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff {θ : ℝ} {k : ℤ} :
    (θ : Angle).toReal = θ - 2 * k * π ↔ θ ∈ Set.Ioc ((2 * k - 1 : ℝ) * π) ((2 * k + 1) * π) :=
  by
  rw [← sub_zero (θ : Angle), ← zsmul_zero k, ← coe_two_pi, ← coe_zsmul, ← coe_sub, zsmul_eq_mul, ← mul_assoc,
    mul_comm (k : ℝ), toReal_coe_eq_self_iff, Set.mem_Ioc]
  exact ⟨fun h => ⟨by linarith, by linarith⟩, fun h => ⟨by linarith, by linarith⟩⟩

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