finSuccEquiv'_ne_last_apply — Mathlib

English

For i, j with hi ≠ last and hj ≠ i, finSuccEquiv' i j equals (i.castLT (val_lt_last hi)).predAbove j.

Русский

Для i, j со свойствами hi ≠ last и hj ≠ i имеем finSuccEquiv' i j = (i.castLT (val_lt_last hi)).predAbove j.

LaTeX

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

Lean4

theorem finSuccEquiv'_ne_last_apply {i j : Fin (n + 1)} (hi : i ≠ Fin.last n) (hj : j ≠ i) :
    finSuccEquiv' i j = (i.castLT (Fin.val_lt_last hi)).predAbove j :=
  by
  rcases Fin.exists_succAbove_eq hj with ⟨j, rfl⟩
  rcases Fin.exists_castSucc_eq.2 hi with ⟨i, rfl⟩
  simp

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