nadd_lt_nadd_iff_left

Mathlib.SetTheory.Ordinal.NaturalOps

URI: https://scilib.ai/kg/mathlib#Ordinal.nadd_lt_nadd_iff_left

English

For all a, b, c, a ♯ b < a ♯ c iff b < c.

Русский

Для всех a, b, c верно: a ♯ b < a ♯ c эквивалентно b < c.

LaTeX

$$$$ a \# b < a \# c \iff b < c $$$$

Lean4

@[simp]
theorem nadd_lt_nadd_iff_left : ∀ (a) {b c}, a ♯ b < a ♯ c ↔ b < c :=
  @add_lt_add_iff_left NatOrdinal _ _ _ _

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

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

Разделы

Аффилиация

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