norm_le_zero_iff' — Mathlib

English

In a NormedGroup, the norm vanishes exactly at the identity: ‖a‖ = 0 iff a = 1.

Русский

В нормированной группе норма нулю равна только тождественному элементу: ‖a‖ = 0 эквивалентно a = 1.

LaTeX

$$$\displaystyle \|a\| = 0 \iff a = 1$$$

Lean4

@[to_additive (attr := simp) norm_le_zero_iff]
theorem norm_le_zero_iff' : ‖a‖ ≤ 0 ↔ a = 1 := by rw [← dist_one_right, dist_le_zero]

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