finSuccEquiv'_last_apply_castSucc

English

For i in Fin(n), finSuccEquiv'(Fin.last n) (Fin.castSucc i) = i.

Русский

Для i ∈ Fin(n) выполняется finSuccEquiv'(Fin.last n)(Fin.castSucc i) = i.

LaTeX

$$$$ \\forall i \\in \\mathrm{Fin}(n), \\; \\mathrm{finSuccEquiv}'(\\mathrm{Fin.last}(n))(\\mathrm{Fin.castSucc}(i)) = i. $$$$

Lean4

theorem finSuccEquiv'_last_apply_castSucc (i : Fin n) : finSuccEquiv' (Fin.last n) (Fin.castSucc i) = i := by
  rw [← Fin.succAbove_last, finSuccEquiv'_succAbove]

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