toReal_neg_iff_sign_neg — Mathlib

English

If θ ≠ π, then sign(θ.toReal) equals θ.sign.

Русский

Если θ ≠ π, то sign(θ.toReal) равно θ.sign.

LaTeX

$$θ ≠ π ⇒ sign(θ.toReal) = θ.sign$$

Lean4

theorem toReal_neg_iff_sign_neg {θ : Angle} : θ.toReal < 0 ↔ θ.sign = -1 :=
  by
  rw [sign, ← sin_toReal, sign_eq_neg_one_iff]
  rcases lt_trichotomy θ.toReal 0 with (h | h | h)
  · exact ⟨fun _ => Real.sin_neg_of_neg_of_neg_pi_lt h (neg_pi_lt_toReal θ), fun _ => h⟩
  · simp [h]
  ·
    exact
      ⟨fun hn => False.elim (h.asymm hn), fun hn =>
        False.elim (hn.not_ge (sin_nonneg_of_nonneg_of_le_pi h.le (toReal_le_pi θ)))⟩

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