nnnorm_mul_le_max

Mathlib.Analysis.Normed.Group.Ultra

URI: https://scilib.ai/kg/mathlib#IsUltrametricDist.nnnorm_mul_le_max

English

For all x,y in a normed group, ‖x·y‖₊ ≤ max(‖x‖₊, ‖y‖₊).

Русский

Для любых x,y в нормированной группе ‖x·y‖₊ ≤ max(‖x‖₊, ‖y‖₊).

LaTeX

$$$\\forall x,y,\\ ‖x y‖_+ \\le \\max(‖x‖_+, ‖y‖_+)$$$

Lean4

@[to_additive]
theorem nnnorm_mul_le_max (x y : S) : ‖x * y‖₊ ≤ max ‖x‖₊ ‖y‖₊ :=
  norm_mul_le_max _ _

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

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

Разделы

Аффилиация

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