coe_abs — Mathlib

English

The absolute value of the real-coerced element in EReal, when viewed again in EReal, matches the real absolute value.

Русский

Абсолютное значение образованного из Real элемента в EReal совпадает с действительным модулем числа.

LaTeX

$$$ \big(((x : \mathrm{EReal}).abs) : \mathrm{EReal}\big) = (|x| : \mathrm{EReal}) $$$

Lean4

@[simp]
theorem coe_abs (x : ℝ) : ((x : EReal).abs : EReal) = (|x| : ℝ) := by
  rw [abs_def, ← Real.coe_nnabs, ENNReal.ofReal_coe_nnreal]; rfl

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