instAddLeftStrictMono

Mathlib.SetTheory.Ordinal.NaturalOps

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

English

For NatOrdinal, left addition is strictly monotone: if a < b, then for every c, a + c < b + c.

Русский

Для NatOrdinal левая сумма инкрементирует порядок строго: если a < b, то для любого c выполняется a + c < b + c.

LaTeX

$$$$ a < b \Rightarrow a + c < b + c $$$$

Lean4

instance : AddLeftStrictMono NatOrdinal.{u} :=
  ⟨fun a _ _ h => nadd_lt_nadd_left h a⟩

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

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

Разделы

Аффилиация

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