English
For p ∈ Fin n and i ∈ Fin(n+1), predAbove(p,i) is the element of Fin n obtained by removing the coordinate corresponding to p from i; equivalently, it subtracts one from i when i > p, else keeps i as is via castPred.
Русский
Для p ∈ Fin n и i ∈ Fin(n+1) predAbove(p,i) — это элемент Fin n, получаемый удалением координаты p из i; эквивалентно вычитанию единицы из i, когда i > p, иначе сохранение i через castPred.
LaTeX
$$$\\text{predAbove}(p,i) = \\begin{cases} \\text{pred}\\, i \\,(\\text{Fin.ne\_zero\_of\_lt } h) & \\text{если } castSucc\, p < i,\\\\ castPred\\, i (\\text{Fin.ne\_of\_lt}(\\text{Fin.not\_lt.1 } h) ) & \\text{иначе} \\end{cases}$$$
Lean4
/-- `predAbove p i` surjects `i : Fin (n+1)` into `Fin n` by subtracting one if `p < i`. -/
def predAbove (p : Fin n) (i : Fin (n + 1)) : Fin n :=
if h : castSucc p < i then pred i (Fin.ne_zero_of_lt h)
else castPred i (Fin.ne_of_lt <| Fin.lt_of_le_of_lt (Fin.not_lt.1 h) (castSucc_lt_last _))
