toReal_nonneg_iff_sign_nonneg — Mathlib

English

0 ≤ θ.toReal if and only if 0 ≤ θ.sign.

Русский

0 ≤ θ.toReal тогда и только тогда, когда 0 ≤ θ.sign.

LaTeX

$$0 ≤ θ.toReal ↔ 0 ≤ θ.sign$$

Lean4

theorem toReal_nonneg_iff_sign_nonneg {θ : Angle} : 0 ≤ θ.toReal ↔ 0 ≤ θ.sign :=
  by
  rcases lt_trichotomy θ.toReal 0 with (h | h | h)
  · refine ⟨fun hn => False.elim (h.not_ge hn), fun hn => ?_⟩
    rw [toReal_neg_iff_sign_neg.1 h] at hn
    exact False.elim (hn.not_gt (by decide))
  · simp [h, sign, ← sin_toReal]
  · refine ⟨fun _ => ?_, fun _ => h.le⟩
    rw [sign, ← sin_toReal, sign_nonneg_iff]
    exact sin_nonneg_of_nonneg_of_le_pi h.le (toReal_le_pi θ)

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