finSuccEquiv'_last_apply — Mathlib

English

If i ≠ Fin.last n, then finSuccEquiv' (Fin.last n) i equals i.castLT (Fin.val_lt_last h).

Русский

Если i ≠ Fin.last n, то finSuccEquiv'(Fin.last n) i = i.castLT (Fin.val_lt_last h).

LaTeX

$$$$ \\forall i \\; (h : i \\neq \\mathrm{Fin.last}(n)), \\; \\mathrm{finSuccEquiv}'(\\mathrm{Fin.last}(n))\,i = i.\\mathrm{castLT}( \\mathrm{Fin.val\\_lt\\_last}(h) ). $$$$

Lean4

theorem finSuccEquiv'_last_apply {i : Fin (n + 1)} (h : i ≠ Fin.last n) :
    finSuccEquiv' (Fin.last n) i = Fin.castLT i (Fin.val_lt_last h) := by simp

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