le_self_nadd

Mathlib.SetTheory.Ordinal.NaturalOps

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

English

If a ≤ c, then a ≤ b ♯ c for any ordinals a,b,c.

Русский

Если a ≤ c, то для любых ординалов a,b выполняется a ≤ b ♯ c.

LaTeX

$$$\\forall a,b,c \\in \\mathrm{Ordinal},\\ a \\le c \\Rightarrow a \\le b \\sharp c$$$

Lean4

theorem le_self_nadd {a b} : a ≤ a ♯ b := by simpa using nadd_le_nadd_left (Ordinal.zero_le b) a

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

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

Разделы

Аффилиация

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