sign_toReal — Mathlib

English

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

Русский

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

LaTeX

$$∀ {θ ≠ π}, sign(θ.toReal) = θ.sign$$

Lean4

@[simp]
theorem sign_toReal {θ : Angle} (h : θ ≠ π) : SignType.sign θ.toReal = θ.sign :=
  by
  rcases lt_trichotomy θ.toReal 0 with (ht | ht | ht)
  · simp [ht, toReal_neg_iff_sign_neg.1 ht]
  · simp [sign, ht, ← sin_toReal]
  ·
    rw [sign, ← sin_toReal, sign_pos ht,
      sign_pos (sin_pos_of_pos_of_lt_pi ht ((toReal_le_pi θ).lt_of_ne (toReal_eq_pi_iff.not.2 h)))]

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