norm_ne_zero_iff — Mathlib

English

The global norm is nonzero if and only if every local norm is nonzero: norm x ≠ 0 iff ∀ w, normAtPlace w x ≠ 0.

Русский

Глобальная норма отлична от нуля тогда и только тогда, когда каждая локальная норма отлична от нуля.

LaTeX

$$$\text{mixedEmbedding}.\operatorname{norm}(x) \neq 0 \quad\iff\quad \forall w, \operatorname{normAtPlace}(w, x) \neq 0.$$$

Lean4

protected theorem norm_ne_zero_iff {x : mixedSpace K} : mixedEmbedding.norm x ≠ 0 ↔ ∀ w, normAtPlace w x ≠ 0 :=
  by
  rw [← not_iff_not]
  simp_rw [ne_eq, mixedEmbedding.norm_eq_zero_iff, not_not, not_forall, not_not]

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