norm_trivial_quotient_mk — Mathlib

English

If the closure of S is all of M, then the operator norm of S.normedMk is 0.

Русский

Если замыкание S равно M, норма проекции равна нулю.

LaTeX

$$$\\|S.normedMk\\| = 0 \\quad\\text{iff } (S.topologicalClosure : Set M) = Set.univ$$$

Lean4

/-- The operator norm of the projection is `0` if the subspace is dense. -/
theorem norm_trivial_quotient_mk (S : AddSubgroup M) (h : (S.topologicalClosure : Set M) = Set.univ) :
    ‖S.normedMk‖ = 0 :=
  by
  refine le_antisymm (opNorm_le_bound _ le_rfl fun x => ?_) (norm_nonneg _)
  have hker : x ∈ S.normedMk.ker.topologicalClosure :=
    by
    rw [S.ker_normedMk, ← SetLike.mem_coe, h]
    trivial
  rw [ker_normedMk] at hker
  simp [norm_mk_eq_zero_iff_mem_closure.mpr hker]

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