succ_succAbove_one — Mathlib

English

succAbove with pivot 1 behaves like standard successor on the inner Fin, illustrating a standard shift property.

Русский

succAbove с опорой 1 ведёт себя как стандартный переход к следующему внутри Fin, демонстрируя свойство сдвига.

LaTeX

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

Lean4

/-- By moving `succ` to the outside of this expression, we create opportunities for further
simplification using `succAbove_zero` or `succ_succAbove_zero`. -/
@[simp]
theorem succ_succAbove_one {n : ℕ} [NeZero n] (i : Fin (n + 1)) : i.succ.succAbove 1 = (i.succAbove 0).succ :=
  by
  rw [← succ_zero_eq_one']
  exact succ_succAbove_succ i 0

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