abs_eq_zero_iff — Mathlib

English

For every x in EReal, the absolute value is zero if and only if x is zero.

Русский

Для любого x из EReal модуль равен нулю тогда и только тогда, когда x равно нулю.

LaTeX

$$$ \forall x \in \mathrm{EReal},\ \operatorname{abs}(x) = 0 \iff x = 0 $$$

Lean4

@[simp]
theorem abs_eq_zero_iff {x : EReal} : x.abs = 0 ↔ x = 0 :=
  by
  induction x
  · simp only [abs_bot, ENNReal.top_ne_zero, bot_ne_zero]
  · simp only [abs_def, coe_eq_zero, ENNReal.ofReal_eq_zero, abs_nonpos_iff]
  · simp only [abs_top, ENNReal.top_ne_zero, top_ne_zero]

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