normedMk_eq_zero_iff — Mathlib

English

The projection normedMk is zero if and only if every element has zero norm.

Русский

Проекция normedMk равна нулю тогда и только тогда, когда у каждого элемента нулевая норма.

LaTeX

$$$ \\mathrm{normedMk} = 0 \\;\\Longleftrightarrow\\; \\forall x, \\|x\\| = 0 $$$

Lean4

/-- The projection is `0` if and only if all the elements have norm `0`. -/
theorem normedMk_eq_zero_iff : normedMk (M := M) = 0 ↔ ∀ (x : M), ‖x‖ = 0 :=
  by
  constructor
  · intro h x
    rw [SeparationQuotient.mk_eq_zero_iff.mp]
    have : normedMk x = 0 := by
      rw [h]
      simp only [zero_apply]
    rw [← this]
    simp
  · intro h
    ext x
    simpa [← norm_eq_zero] using h x

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