English
Away from the hole at p, the map p.predAbove followed by p.succAbove is the identity on Fin(n+1) except at p.succ.
Русский
Вне дырки по p, композиция p.predAbove и p.succAbove действует как тождество на Fin(n+1) за исключением p.succ.
LaTeX
$$$\forall p \in \mathrm{Fin}(n),\ \forall i \in \mathrm{Fin}(n+1),\ i \neq p.succ \Rightarrow p.predAbove(i).succAbove = i$$$
Lean4
/-- Sending `Fin (n+1)` to `Fin n` by subtracting one from anything above `p`
then back to `Fin (n+1)` with a gap around `p.succ` is the identity away from `p.succ`. -/
@[simp]
theorem succ_succAbove_predAbove {n : ℕ} {p : Fin n} {i : Fin (n + 1)} (h : i ≠ p.succ) :
p.succ.succAbove (p.predAbove i) = i :=
by
obtain h | h := Fin.lt_or_lt_of_ne h
· rw [predAbove_of_le_castSucc _ _ (le_castSucc_iff.2 h), succAbove_castPred_of_lt _ _ h]
· rw [predAbove_of_castSucc_lt _ _ (Fin.lt_of_le_of_lt (p.castSucc_le_succ) h), succAbove_pred_of_lt _ _ h]
