mul_add_lt

Mathlib.SetTheory.Ordinal.NaturalOps

URI: https://scilib.ai/kg/mathlib#NatOrdinal.mul_add_lt

English

If a' < a and b' < b then a'·b + a·b' < a·b + a'·b'.

Русский

Если a' < a и b' < b, то a'·b + a·b' < a·b + a'·b'.

LaTeX

$$$a' \cdot b + a \cdot b' < a \cdot b + a' \cdot b'$$$

Lean4

theorem mul_add_lt {a b a' b' : NatOrdinal} (ha : a' < a) (hb : b' < b) : a' * b + a * b' < a * b + a' * b' :=
  Ordinal.nmul_nadd_lt ha hb

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

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

Разделы

Аффилиация

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