addNat_inj

Mathlib.Order.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.addNat_inj

English

For every n, m, i and j in Fin(n), i.addNat m = j.addNat m iff i = j.

Русский

Для любого n, m, i,j ∈ Fin(n), i.addNat m = j.addNat m ⇔ i = j.

LaTeX

$$$\forall {n:\mathbb{N}} (m:\mathbb{N})\; {i,j:\mathrm{Fin}(n)},\; i.addNat\, m = j.addNat\, m \iff i = j$$$

Lean4

@[simp]
theorem addNat_inj (m) {i j : Fin n} : i.addNat m = j.addNat m ↔ i = j :=
  (strictMono_addNat _).injective.eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru