le_of_nadd_le_nadd_left

Mathlib.SetTheory.Ordinal.NaturalOps

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

English

If a ♯ b ≤ a ♯ c, then b ≤ c for all a, b, c.

Русский

Если a ♯ b ≤ a ♯ c, тогда b ≤ c для всех a, b, c.

LaTeX

$$$$ a \# b \le a \# c \Rightarrow b \le c $$$$

Lean4

theorem le_of_nadd_le_nadd_left : ∀ {a b c}, a ♯ b ≤ a ♯ c → b ≤ c :=
  @le_of_add_le_add_left NatOrdinal _ _ _

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

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

Разделы

Аффилиация

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