nadd_comm — Mathlib

English

For all ordinals a and b, the natural addition is commutative: a ♯ b = b ♯ a.

Русский

Для любых ординалов a и b натуральное сложение выпукло симметрично: a ♯ b = b ♯ a.

LaTeX

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

Lean4

theorem nadd_comm (a b) : a ♯ b = b ♯ a := by
  rw [nadd, nadd, max_comm]
  congr <;> ext x <;> cases x <;> apply congr_arg _ (nadd_comm _ _)
termination_by (a, b)

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