forall_normAtPlace_eq_zero_iff — Mathlib

English

A vector x in the mixed space is zero iff all its norms at every place vanish.

Русский

Вектор x в смешанном пространстве нулевой тогда и только тогда, когда все его нормы на местах равны нулю.

LaTeX

$$$(\forall w, \operatorname{normAtPlace}(w)(x) = 0) \iff x = 0.$$$

Lean4

theorem forall_normAtPlace_eq_zero_iff {x : mixedSpace K} : (∀ w, normAtPlace w x = 0) ↔ x = 0 :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · ext w
    · exact norm_eq_zero.mp (normAtPlace_apply_of_isReal w.prop _ ▸ h w.1)
    · exact norm_eq_zero.mp (normAtPlace_apply_of_isComplex w.prop _ ▸ h w.1)
  · simp_rw [h, map_zero, implies_true]

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