norm_normedMk_le

Mathlib.Analysis.Normed.Group.Quotient

URI: https://scilib.ai/kg/mathlib#AddSubgroup.norm_normedMk_le

← MathLib Explorer

English

The operator norm of the projection map is at most 1.

Русский

Операторная норма проекции не превышает единицы.

LaTeX

$$$\\|S.normedMk\\| \\le 1$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru