le_nadd_self — Mathlib

English

For all ordinals a and b, a ≤ b ♯ a; i.e., increasing the right addend by b never decreases the value.

Русский

Пусть a и b — ординалы. Тогда a ≤ b ♯ a; т.е. увеличение правого слагаемого не уменьшает величину.

LaTeX

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

Lean4

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

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