English
For every a in EReal, the product of its sign and the inverse of its absolute value equals its inverse: (sign a) · (|a|)^{-1} = a^{-1}.
Русский
Пусть a ∈ EReal. Тогда произведение знака числа и обратного модуля равно обратному: (sign a) · (|a|)^{-1} = a^{-1}.
LaTeX
$$$ (\operatorname{sign}(a)) \cdot (|a|)^{-1} = a^{-1} $$$
Lean4
theorem sign_mul_inv_abs (a : EReal) : (sign a) * (a.abs : EReal)⁻¹ = a⁻¹ := by
induction a with
| bot
| top => simp
| coe a =>
rcases lt_trichotomy a 0 with (a_neg | rfl | a_pos)
·
rw [sign_coe, _root_.sign_neg a_neg, coe_neg_one, neg_one_mul, ← inv_neg, abs_def a, coe_ennreal_ofReal,
max_eq_left (abs_nonneg a), ← coe_neg |a|, abs_of_neg a_neg, neg_neg]
· rw [coe_zero, sign_zero, SignType.coe_zero, abs_zero, coe_ennreal_zero, inv_zero, mul_zero]
· rw [sign_coe, _root_.sign_pos a_pos, SignType.coe_one, one_mul]
simp only [abs_def a, coe_ennreal_ofReal, abs_nonneg, max_eq_left]
congr
exact abs_of_pos a_pos
