English
succAbove p i embeds Fin n into Fin(n+1) by inserting a hole around p; it equals castSucc i if castSucc i < p, otherwise it equals i.succ.
Русский
succAbove p i встраивает Fin n в Fin(n+1) с зазором вокруг p: равно castSucc i, если castSucc i < p, иначе i.succ.
LaTeX
$$$ \operatorname{succAbove}(p,i) = \begin{cases} \operatorname{castSucc}(i), & \text{if } \operatorname{castSucc}(i) < p, \\ i\text{.succ}, & \text{otherwise}. \end{cases} $$$
Lean4
/-- `succAbove p i` embeds `Fin n` into `Fin (n + 1)` with a hole around `p`. -/
def succAbove (p : Fin (n + 1)) (i : Fin n) : Fin (n + 1) :=
if castSucc i < p then i.castSucc else i.succ
