nadd_right_cancel_iff — Mathlib

English

Let a, b, c be ordinals. The operation of natural addition with a on the right is injective in the left argument: if b ♯ a = c ♯ a, then b = c.

Русский

Пусть a, b и c — ординалы. Операция натурального сложения справа от a инъективна по первому аргументу: если b ♯ a = c ♯ a, то b = c.

LaTeX

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

Lean4

@[simp]
theorem nadd_right_cancel_iff : ∀ {a b c}, b ♯ a = c ♯ a ↔ b = c :=
  @add_right_cancel_iff NatOrdinal _ _

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