castSucc_pred_add_one_eq — Mathlib

English

castPred is the map from Fin(n+1) to Fin n that sends an element to the previous rank, provided the element is not the last one.

Русский

castPred переводит элемент Fin(n+1) в Fin(n) по предыдущему рангу при условии, что элемент не последний.

LaTeX

$$$$ \\text{castPred is the map } (i: \\mathrm{Fin}(n+1)) \\to \\mathrm{Fin}(n) \\text{ given by } i \\mapsto \\operatorname{castLT}(i, \\operatorname{val\\_lt\\_last}(h)). $$$$

Lean4

theorem castSucc_pred_add_one_eq {a : Fin (n + 1)} (ha : a ≠ 0) : (a.pred ha).castSucc + 1 = a := by simp

Похожие утверждения