nnnorm_mul_le

Mathlib.Analysis.Normed.Ring.Basic

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

English

In a nonunital seminormed ring, the NNReal norm is submultiplicative: ‖a b‖₊ ≤ ‖a‖₊ ‖b‖₊.

Русский

В неединичном полугруппе с нормой NNReal, нормa умножения удовлетворяет неравенству: \|ab\|₊ ≤ \|a\|₊ \|b\|₊.

LaTeX

$$$\|a b\|_{+} \leq \|a\|_{+} \|b\|_{+}$$$

Lean4

theorem nnnorm_mul_le (a b : α) : ‖a * b‖₊ ≤ ‖a‖₊ * ‖b‖₊ :=
  norm_mul_le a b

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

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

Разделы

Аффилиация

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