nmul_nadd_le

Mathlib.SetTheory.Ordinal.NaturalOps

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

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' \le a \cdot b + a' \cdot b'$$$

Lean4

theorem nmul_nadd_le {a b a' b' : NatOrdinal} (ha : a' ≤ a) (hb : b' ≤ b) : a' * b + a * b' ≤ a * b + a' * b' :=
  Ordinal.nmul_nadd_le ha hb

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

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

Разделы

Аффилиация

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