lt_of_nadd_lt_nadd_right

Mathlib.SetTheory.Ordinal.NaturalOps

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

English

If b ♯ a < c ♯ a, then b < c for any a, b, c.

Русский

Если b ♯ a < c ♯ a, то b < c для любых a, b, c.

LaTeX

$$$$ b \# a < c \# a \Rightarrow b < c $$$$

Lean4

theorem lt_of_nadd_lt_nadd_right : ∀ {a b c}, b ♯ a < c ♯ a → b < c :=
  @lt_of_add_lt_add_right NatOrdinal _ _ _

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

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

Разделы

Аффилиация

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