normedMk — Mathlib

English

For any m and closed S, ∥mk m∥ = 0 if and only if m ∈ S.

Русский

Для любого m и замыкания S верно: ∥mk m∥ = 0 ⇔ m ∈ S.

LaTeX

$$$\| (m : M ⧸ S) \| = 0 \iff m \in S$$$

Lean4

/-- The morphism from a seminormed group to the quotient by a subgroup. -/
noncomputable def normedMk (S : AddSubgroup M) : NormedAddGroupHom M (M ⧸ S)
    where
  __ := QuotientAddGroup.mk' S
  bound' := ⟨1, fun m => by simpa [one_mul] using norm_mk_le_norm⟩

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