abs_toReal_neg_coe_eq_self_iff — Mathlib

English

For any θ ∈ ℝ, |(θ : Angle).toReal| = θ iff 0 ≤ θ ∧ θ ≤ π.

Русский

Для любого θ ∈ ℝ: |(θ : Angle).toReal| = θ тогда и только тогда, когда 0 ≤ θ ≤ π.

LaTeX

$$$\\\\forall {\\\\theta : Real}, \\\\Big| (\\\\theta : Angle).toReal \\\\Big| = \\\\theta \\\\iff 0 \\\\le \\\\theta \land \\\\theta \\\\le \\\\\pi$$$

Lean4

theorem abs_toReal_neg_coe_eq_self_iff {θ : ℝ} : |(-θ : Angle).toReal| = θ ↔ 0 ≤ θ ∧ θ ≤ π :=
  by
  refine ⟨fun h => h ▸ ⟨abs_nonneg _, abs_toReal_le_pi _⟩, fun h => ?_⟩
  by_cases hnegpi : θ = π; · simp [hnegpi, Real.pi_pos.le]
  rw [← coe_neg,
    toReal_coe_eq_self_iff.2 ⟨neg_lt_neg (lt_of_le_of_ne h.2 hnegpi), (neg_nonpos.2 h.1).trans Real.pi_pos.le⟩, abs_neg,
    abs_eq_self.2 h.1]

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