succAbove_inj — Mathlib

English

For any p, succAbove p is injective: if succAbove p i = succAbove p j then i = j.

Русский

Для любого p отображение succAbove p инъективно: если succAbove p i = succAbove p j, тогда i = j.

LaTeX

$$$\forall p:\mathrm{Fin}(n+1), \forall i,j:\mathrm{Fin}(n), (\mathrm{succAbove}(p)(i) = \mathrm{succAbove}(p)(j)) \Rightarrow i = j$$$

Lean4

@[simp]
theorem succAbove_inj : succAbove p i = succAbove p j ↔ i = j :=
  (strictMono_succAbove p).injective.eq_iff

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