English
Away from the hole at p, composing predAbove with succAbove after shifting by castSucc yields the identity: for i ≠ castSucc(p), p.castSucc.succAbove(p.predAbove(i)) = i.
Русский
Вне дырки в p, композиция predAbove и succAbove после переноса через castSucc дает тождество: для i ≠ castSucc(p) выполняется p.castSucc.succAbove(p.predAbove(i)) = i.
LaTeX
$$$\forall p \in \mathrm{Fin}(n),\ \forall i \in \mathrm{Fin}(n+1),\ i \neq p.castSucc \Rightarrow p.castSucc.succAbove(p.predAbove(i)) = 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` is the identity away from `p`. -/
@[simp]
theorem succAbove_predAbove {p : Fin n} {i : Fin (n + 1)} (h : i ≠ castSucc p) :
p.castSucc.succAbove (p.predAbove i) = i :=
by
obtain h | h := Fin.lt_or_lt_of_ne h
· rw [predAbove_of_le_castSucc _ _ (Fin.le_of_lt h), succAbove_castPred_of_lt _ _ h]
· rw [predAbove_of_castSucc_lt _ _ h, succAbove_pred_of_lt _ _ h]
