succ_succAbove_succ — Mathlib

English

For any n, (1 : Fin(n+3)).succAbove 1 = 2.

Русский

Для любого n, (1 : Fin(n+3)).succAbove 1 = 2.

LaTeX

$$$\forall n \in \mathbb{N},\ (1 : \mathrm{Fin}(n+3)).succAbove(1) = 2.$$$

Lean4

/-- `succ` commutes with `succAbove`. -/
@[simp]
theorem succ_succAbove_succ {n : ℕ} (i : Fin (n + 1)) (j : Fin n) : i.succ.succAbove j.succ = (i.succAbove j).succ :=
  by
  obtain h | h := i.lt_or_ge (succ j)
  · rw [succAbove_of_lt_succ _ _ h, succAbove_succ_of_lt _ _ h]
  · rwa [succAbove_of_castSucc_lt _ _ h, succAbove_succ_of_le, succ_castSucc]

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