norm_mk_eq_zero — Mathlib

English

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

Русский

При замыкании S верно: ∥mk m∥ = 0 тогда и только тогда, когда m ∈ S.

LaTeX

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

Lean4

/-- The norm of the image of `m : M` in the quotient by a closed subgroup `S` is zero if and only if
`m ∈ S`. -/
@[to_additive /-- The norm of the image of `m : M` in the quotient by a closed subgroup `S` is zero
    if and only if `m ∈ S`. -/
    ]
theorem norm_mk_eq_zero [hS : IsClosed (S : Set M)] : ‖(m : M ⧸ S)‖ = 0 ↔ m ∈ S := by
  rw [norm_mk_eq_zero_iff_mem_closure, hS.closure_eq, SetLike.mem_coe]

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