one_succAbove_succ — Mathlib

English

For any j ∈ Fin n, (1 : Fin(n+2)).succAbove j.succ = j.succ.succ.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem one_succAbove_succ {n : ℕ} (j : Fin n) : (1 : Fin (n + 2)).succAbove j.succ = j.succ.succ := by
  have := succ_succAbove_succ 0 j; rwa [succ_zero_eq_one, zero_succAbove] at this

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