norm_normedMk_le — Mathlib

English

The operator norm of the projection map normedMk: M → SeparationQuotient M is at most 1.

Русский

Операторная норма отображения проекции normedMk: M → SeparationQuotient M не превышает 1.

LaTeX

$$$ \\| \\mathrm{normedMk} \\ (M := M) \\| \\le 1 $$$

Lean4

/-- The operator norm of the projection is at most `1`. -/
theorem norm_normedMk_le : ‖normedMk (M := M)‖ ≤ 1 :=
  NormedAddGroupHom.opNorm_le_bound _ zero_le_one fun m => by simp

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