finSuccEquiv — Mathlib

English

There is a natural equivalence between Fin(n+1) and Option Fin(n).

Русский

Существует естественная эквивалентность между Fin(n+1) и Option Fin(n).

LaTeX

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

Lean4

/-- Equivalence between `Fin (n + 1)` and `Option (Fin n)`.
This is a version of `Fin.pred` that produces `Option (Fin n)` instead of
requiring a proof that the input is not `0`. -/
def finSuccEquiv (n : ℕ) : Fin (n + 1) ≃ Option (Fin n) :=
  finSuccEquiv' 0

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