nadd_eq_add — Mathlib

English

The natural addition of ordinals equals the ordinal of the sum of their NatOrdinal representations: a ♯ b = toOrdinal(toNatOrdinal a + toNatOrdinal b).

Русский

Натуральное сложение ординалов равно ординалу суммы их представлений в NatOrdinal: a ♯ b = toOrdinal(toNatOrdinal a + toNatOrdinal b).

LaTeX

$$$$ a \# b = \text{toOrdinal}(\text{toNatOrdinal}(a) + \text{toNatOrdinal}(b)) $$$$

Lean4

theorem nadd_eq_add (a b : Ordinal) : a ♯ b = toOrdinal (toNatOrdinal a + toNatOrdinal b) :=
  rfl

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