nnnorm_mul₃_le

Mathlib.Analysis.Normed.Ring.Basic

URI: https://scilib.ai/kg/mathlib#nnnorm_mul₃_le

English

In a nonunital seminormed ring, ‖a b c‖₊ ≤ ‖a‖₊ ‖b‖₊ ‖c‖₊.

Русский

В неединичном полугруппе NNReal: ‖a b c‖₊ ≤ ‖a‖₊ ‖b‖₊ ‖c‖₊.

LaTeX

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

Lean4

theorem nnnorm_mul₃_le : ‖a * b * c‖₊ ≤ ‖a‖₊ * ‖b‖₊ * ‖c‖₊ :=
  nnnorm_mul_le_of_le (norm_mul_le ..) le_rfl

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

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

Разделы

Аффилиация

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