nnnorm_mul_le'

Mathlib.Analysis.Normed.Group.Basic

URI: https://scilib.ai/kg/mathlib#nnnorm_mul_le'

English

The NNReal norm is subadditive under multiplication: ‖a·b‖₊ ≤ ‖a‖₊ + ‖b‖₊.

Русский

NNReal-норма подадирует на умножение: ‖a·b‖₊ ≤ ‖a‖₊ + ‖b‖₊.

LaTeX

$$$\\|a \\star b\\|_+ \\le \\|a\\|_+ + \\|b\\|_+$$$

Lean4

@[to_additive nnnorm_add_le]
theorem nnnorm_mul_le' (a b : E) : ‖a * b‖₊ ≤ ‖a‖₊ + ‖b‖₊ :=
  NNReal.coe_le_coe.1 <| norm_mul_le' a b

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

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

Разделы

Аффилиация

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