finSuccEquiv'_succAbove — Mathlib

English

For any i and j, the application of the equivalence to i and i.succAbove j yields Some j.

Русский

Для любых i и j отображение применяет i и i.succAbove(j) → Some(j).

LaTeX

$$$\\mathrm{finSuccEquiv'}\\; i\\; (i.\\mathrm{succAbove}\\; j) = \\mathrm{Some}(j)$$$

Lean4

@[simp]
theorem finSuccEquiv'_succAbove (i : Fin (n + 1)) (j : Fin n) : finSuccEquiv' i (i.succAbove j) = some j :=
  @Fin.insertNth_apply_succAbove n (fun _ => Option (Fin n)) i _ _ _

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