sign_mul_abs — Mathlib

English

For every EReal x, sign(x) times abs(x) equals x in EReal.

Русский

Для каждого x в EReal произведение sign(x) и |x| даёт сам x.

LaTeX

$$$ \operatorname{sign}(x) \cdot \operatorname{abs}(x) = x \quad \text{in } \mathrm{EReal} $$$

Lean4

@[simp]
protected theorem sign_mul_abs : ∀ x : EReal, (sign x * x.abs : EReal) = x
  | ⊥ => by simp
  | ⊤ => by simp
  | (x : ℝ) => by rw [sign_coe, coe_abs, ← coe_coe_sign, ← coe_mul, sign_mul_abs]

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