English
Two equivalent embeddings of Fin n into Fin(n+2) via holes at i and j are equal: (i.succAbove j).succAbove ((j.predAbove i).succAbove k) = i.succAbove (j.succAbove k).
Русский
Две эквивалентные вложения Fin n в Fin(n+2) через дырки i и j равны: (i.succAbove j).succAbove ((j.predAbove i).succAbove k) = i.succAbove (j.succAbove k).
LaTeX
$$$\forall i : \mathrm{Fin}(n+2),\forall j : \mathrm{Fin}(n+1),\forall k : \mathrm{Fin}(n),\ (i.succAbove j).succAbove ((j.predAbove i).succAbove k) = i.succAbove (j.succAbove k)$$$
Lean4
theorem succAbove_succAbove_predAbove {n : ℕ} (i : Fin (n + 1)) (j : Fin n) :
(i.succAbove j).succAbove (j.predAbove i) = i := by
cases Fin.lt_or_le j.castSucc i with
| inl h => rw [succAbove_of_castSucc_lt _ _ h, succAbove_predAbove (Fin.ne_of_gt h)]
| inr h => rw [succAbove_of_le_castSucc _ _ h, succ_succAbove_predAbove (Fin.ne_of_lt <| le_castSucc_iff.mp h)]
