sign_inv — Mathlib

English

For all real r, sign(r)⁻¹ = sign(r⁻¹).

Русский

Для любого r ∈ ℝ выполняется sign(r)⁻¹ = sign(r⁻¹).

LaTeX

$$$ \text{sign}(r)^{-1} = \text{sign}(r^{-1}) $$$

Lean4

@[simp]
theorem sign_inv (r : ℝ) : sign r⁻¹ = sign r :=
  by
  obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
  · rw [sign_of_neg hn, sign_of_neg (inv_lt_zero.mpr hn)]
  · rw [sign_zero, inv_zero, sign_zero]
  · rw [sign_of_pos hp, sign_of_pos (inv_pos.mpr hp)]

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