norm_mk_le_norm — Mathlib

English

The norm of the quotient element mk m equals the norm of the representative m in M.

Русский

Норма элемента фактор-группы mk m равна норме представителя m в M.

LaTeX

$$$\|mk\, m\| = \|m\|$$$

Lean4

/-- The norm of the projection is smaller or equal to the norm of the original element. -/
@[to_additive /-- The norm of the projection is smaller or equal to the norm of the original element. -/
    ]
theorem norm_mk_le_norm : ‖(m : M ⧸ S)‖ ≤ ‖m‖ :=
  (infDist_le_dist_of_mem (by simp)).trans_eq (dist_one_left _)

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