castSucc_pred_eq_pred_castSucc — Mathlib

English

Applying pred to a in Fin(n+1) and then casting succ is the same as casting succ first and then applying pred with the appropriate zero-condition.

Русский

Применение pred к a в Fin(n+1) с последующим castSucc эквивалентно применению castSucc к a, затем pred с соответствующей нулевой проверкой.

LaTeX

$$$$ \\forall {n} \\; {a} \\in \\mathrm{Fin}(n+1) \\; (ha): (a.pred ha).\\operatorname{castSucc} = (\\operatorname{castSucc} a).pred (\\operatorname{castSucc\\_ne\_zero\_iff}.\\operatorname{mpr} ha). $$$$

Lean4

theorem castSucc_pred_eq_pred_castSucc {a : Fin (n + 1)} (ha : a ≠ 0) :
    (a.pred ha).castSucc = (castSucc a).pred (castSucc_ne_zero_iff.mpr ha) :=
  rfl

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