nadd_left_comm — Mathlib

English

Natural addition is commutative on the left: a ♯ (b ♯ c) = b ♯ (a ♯ c) for all ordinals a,b,c.

Русский

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

LaTeX

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

Lean4

theorem nadd_left_comm : ∀ a b c, a ♯ (b ♯ c) = b ♯ (a ♯ c) :=
  @add_left_comm NatOrdinal _

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