neg_coe_abs_toReal_of_sign_nonpos

English

If θ.sign ≤ 0, then -↑|θ.toReal| = θ.

Русский

Если θ.sign ≤ 0, то -↑|θ.toReal| = θ.

LaTeX

$$θ.sign ≤ 0 ⇒ -↑|θ.toReal| = θ$$

Lean4

theorem neg_coe_abs_toReal_of_sign_nonpos {θ : Angle} (h : θ.sign ≤ 0) : -↑|θ.toReal| = θ :=
  by
  rw [SignType.nonpos_iff] at h
  rcases h with (h | h)
  · rw [abs_of_neg (toReal_neg_iff_sign_neg.2 h), coe_neg, neg_neg, coe_toReal]
  · rw [sign_eq_zero_iff] at h
    rcases h with (rfl | rfl) <;> simp [abs_of_pos Real.pi_pos]

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