toReal_coe_eq_self_add_two_pi_iff

English

Let θ ∈ ℝ. The equality (θ : Angle).toReal = θ + 2π holds exactly when θ ∈ (-3π, -π].

Русский

Пусть θ ∈ ℝ. Равенство (θ : Angle).toReal = θ + 2π верно тогда и только тогда, когда θ ∈ (-3π, -π].

LaTeX

$$$((\theta : \text{Angle}).toReal = \theta + 2\pi) \;\iff\; \theta \in (-3\pi, -\pi]$$$

Lean4

theorem toReal_coe_eq_self_add_two_pi_iff {θ : ℝ} : (θ : Angle).toReal = θ + 2 * π ↔ θ ∈ Set.Ioc (-3 * π) (-π) := by
  convert @toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff θ (-1) using 2 <;> norm_num

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