finSuccEquiv'_at — Mathlib

English

There is a natural bijection between Fin(n+1) and Option(Fin(n)) with the null element corresponding to i itself.

Русский

Существует естественная биекция между Fin(n+1) и Option(Fin(n)) с нулевым элементом, соответствующим i.

LaTeX

$$$\\mathrm{Fin}(n+1) \\cong \\mathrm{Option}(\\mathrm{Fin}(n))$$$

Lean4

@[simp]
theorem finSuccEquiv'_at (i : Fin (n + 1)) : (finSuccEquiv' i) i = none := by simp [finSuccEquiv']

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