English
castPred is the map Fin(n+1) → Fin n that sends i to the previous index, provided i is not the last element.
Русский
castPred — отображение Fin(n+1) → Fin(n), отправляющее i на предыдущий индекс, если i не последний.
LaTeX
$$$$ \\text{castPred is a function } (i : \\mathrm{Fin}(n+1)) \\to \\mathrm{Fin}(n) \\text{ defined by } \\operatorname{castPred}(i,h) = \\operatorname{castLT}(i, \\operatorname{val\\_lt\\_last}(h)). $$$$
Lean4
/-- `castPred i` sends `i : Fin (n + 1)` to `Fin n` as long as i ≠ last n. -/
@[inline]
def castPred (i : Fin (n + 1)) (h : i ≠ last n) : Fin n :=
castLT i (val_lt_last h)
