norm_eq_zero_iff — Mathlib

English

The global norm is zero exactly when some local norm is zero.

Русский

Глобальная норма равна нулю тогда и только тогда, когда нулевая локальная норма на некотором месте.

LaTeX

$$$ \|x\| = 0 \iff \exists w, \operatorname{normAtPlace}(w, x) = 0 $$$

Lean4

protected theorem norm_eq_zero_iff {x : mixedSpace K} : mixedEmbedding.norm x = 0 ↔ ∃ w, normAtPlace w x = 0 := by
  simp_rw [mixedEmbedding.norm, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, prod_eq_zero_iff, mem_univ, true_and,
    pow_eq_zero_iff mult_ne_zero]

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