add_le_nadd — Mathlib

English

Addition is bounded above by natural addition: a + b ≤ a ♯ b.

Русский

Сложение не превышает натуральное сложение: a + b ≤ a ♯ b.

LaTeX

$$$a + b \le a \# b$$$

Lean4

theorem add_le_nadd : a + b ≤ a ♯ b := by
  induction b using limitRecOn with
  | zero => simp
  | succ c h => rwa [add_succ, nadd_succ, succ_le_succ_iff]
  | limit c hc H =>
    rw [(isNormal_add_right a).apply_of_isSuccLimit hc, Ordinal.iSup_le_iff]
    rintro ⟨i, hi⟩
    exact (H i hi).trans (nadd_le_nadd_left hi.le a)

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