norm_mk_eq_zero_iff_mem_closure — Mathlib

English

The norm of the image mk m in the quotient is zero if and only if m lies in the closure of S.

Русский

Норма изображения mk m в фактор-группе равна нулю тогда и только тогда, когда m лежит в замыкании S.

LaTeX

$$$\| (m : M ⧸ S) \| = 0 \iff m \in \operatorname{closure}(S)$$$

Lean4

/-- The norm of the image of `m : M` in the quotient by `S` is zero if and only if `m` belongs
to the closure of `S`. -/
@[to_additive /-- The norm of the image of `m : M` in the quotient by `S` is zero if and only if `m`
    belongs to the closure of `S`. -/
    ]
theorem norm_mk_eq_zero_iff_mem_closure : ‖(m : M ⧸ S)‖ = 0 ↔ m ∈ closure (S : Set M) :=
  by
  rw [norm_mk, ← mem_closure_iff_infDist_zero]
  exact ⟨1, S.one_mem⟩

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