English
If the subspace is not dense, then the operator norm of the projection equals 1.
Русский
Если подпространство не плотное, то норма проекции равна единице.
LaTeX
$$$\\|S.normedMk\\| = 1 \\quad\\text{if } \\overline{S} \\neq M$$$
Lean4
/-- The operator norm of the projection is `1` if the subspace is not dense. -/
theorem norm_normedMk (S : AddSubgroup M) (h : (S.topologicalClosure : Set M) ≠ univ) : ‖S.normedMk‖ = 1 :=
by
refine le_antisymm (norm_normedMk_le S) ?_
obtain ⟨x, hx⟩ : ∃ x : M, 0 < ‖(x : M ⧸ S)‖ :=
by
refine (Set.nonempty_compl.2 h).imp fun x hx ↦ ?_
exact (norm_nonneg _).lt_of_ne' <| mt norm_mk_eq_zero_iff_mem_closure.1 hx
refine (le_mul_iff_one_le_left hx).1 ?_
exact norm_lift_apply_le S.normedMk (fun x ↦ (eq_zero_iff x).2) x
