norm_mk_le

Mathlib.Analysis.Normed.Group.Quotient

URI: https://scilib.ai/kg/mathlib#Submodule.Quotient.norm_mk_le

English

For any m ∈ M, ∥mk m∥ ≤ ∥m∥.

Русский

Для любого m ∈ M выполняется ∥mk(m)∥ ≤ ∥m∥.

LaTeX

$$$\\|Submodule.Quotient.mk m\\| \\le \\|m\\|$$$

Lean4

theorem norm_mk_le (m : M) : ‖(Submodule.Quotient.mk m : M ⧸ S)‖ ≤ ‖m‖ :=
  norm_mk_le_norm

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

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

Разделы

Аффилиация

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