English
There is a natural bijection between Fin(n+1) and Option(Fin n), given by inserting None at position i and Some x elsewhere.
Русский
Существует естественная биекция между Fin(n+1) и Option(Fin n), отображение Инь на позицию i, вставляющее None, а далее Some.
LaTeX
$$$\\mathrm{Fin}(n+1) \\cong \\mathrm{Option}(\\mathrm{Fin}(n))$$$
Lean4
/-- An equivalence that removes `i` and maps it to `none`.
This is a version of `Fin.predAbove` that produces `Option (Fin n)` instead of
mapping both `i.castSucc` and `i.succ` to `i`. -/
def finSuccEquiv' (i : Fin (n + 1)) : Fin (n + 1) ≃ Option (Fin n)
where
toFun := i.insertNth none some
invFun x := x.casesOn' i (Fin.succAbove i)
left_inv x := Fin.succAboveCases i (by simp) (fun j => by simp) x
right_inv x := by cases x <;> simp
