instAddLeftReflectLE

Mathlib.SetTheory.Ordinal.NaturalOps

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

English

Left addition reflects ≤: a ≤ b holds if and only if a + c ≤ b + c for NatOrdinal.

Русский

Левое сложение отражает неравенство: a ≤ b тогда и только тогда, когда a + c ≤ b + c (NatOrdinal).

LaTeX

$$$$ (a \le b) \iff (a + c \le b + c) $$$$

Lean4

instance : AddLeftReflectLE NatOrdinal.{u} :=
  ⟨fun a b c h => by
    by_contra! h'
    exact h.not_gt (add_lt_add_left h' a)⟩

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

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

Разделы

Аффилиация

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