succAbove_right_inj — Mathlib

English

For all i,j ∈ Fin(n), p.succAbove(i) = p.succAbove(j) iff i = j.

Русский

Для всех i,j ∈ Fin(n) выполняется p.succAbove(i) = p.succAbove(j) тогда и лишь тогда i = j.

LaTeX

$$$\forall n \in \mathbb{N},\ \forall p \in \mathrm{Fin}(n+1),\ \forall i,j \in \mathrm{Fin}(n),\ p.succAbove(i) = p.succAbove(j) \iff i = j.$$$

Lean4

/-- Given a fixed pivot `p : Fin (n + 1)`, `p.succAbove` is injective. -/
theorem succAbove_right_inj : p.succAbove i = p.succAbove j ↔ i = j :=
  succAbove_right_injective.eq_iff

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