English
For a fixed pivot p ∈ Fin(n+1), the map i → p.succAbove(i) is injective.
Русский
Для фиксированного опорного элемента p ∈ Fin(n+1) отображение i ↦ p.succAbove(i) инъективно.
LaTeX
$$$\forall n \in \mathbb{N},\ \forall p \in \mathrm{Fin}(n+1),\ \mathrm{Injective}(\lambda i:\mathrm{Fin}(n), p \succAbove i).$$$
Lean4
/-- Given a fixed pivot `p : Fin (n + 1)`, `p.succAbove` is injective. -/
theorem succAbove_right_injective : Injective p.succAbove :=
by
rintro i j hij
unfold succAbove at hij
split_ifs at hij with hi hj hj
· exact castSucc_injective _ hij
· rw [hij] at hi
cases hj <| Nat.lt_trans j.castSucc_lt_succ hi
· rw [← hij] at hj
cases hi <| Nat.lt_trans i.castSucc_lt_succ hj
· exact succ_injective _ hij
