cycleRange_succAbove — Mathlib

English

For i in Fin(n+1) and j in Fin n, i.cycleRange(i.succAbove j) equals j.succ.

Русский

Для i из Fin(n+1) и j из Fin n, i.cycleRange(i.succAbove j) = j.succ.

LaTeX

$$$ i: \mathrm{Fin}(n+1),\ j: \mathrm{Fin}(n) \Rightarrow i.\mathrm{cycleRange}(i.\mathrm{succAbove} j) = j.\mathrm{succ} $$$

Lean4

@[simp]
theorem cycleRange_succAbove (i : Fin (n + 1)) (j : Fin n) : i.cycleRange (i.succAbove j) = j.succ :=
  by
  rcases lt_or_ge (castSucc j) i with h | h
  · rw [Fin.succAbove_of_castSucc_lt _ _ h, Fin.cycleRange_of_lt h, Fin.coeSucc_eq_succ]
  · rw [Fin.succAbove_of_le_castSucc _ _ h, Fin.cycleRange_of_gt (Fin.le_castSucc_iff.mp h)]

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