finSuccAboveEquiv — Mathlib

English

finSuccAboveEquiv p is an order isomorphism between Fin(n) and { x ∈ Fin(n+1) | x ≠ p }.

Русский

finSuccAboveEquiv p — порядковое изоморфизм между Fin(n) и { x ∈ Fin(n+1) | x ≠ p }.

LaTeX

$$$$ \\mathrm{finSuccAboveEquiv}(p) : \\mathrm{Fin}(n) \\simeq \\{ x \\in \\mathrm{Fin}(n+1) \\mid x \\neq p \\}. $$$$

Lean4

/-- `Fin.succAbove` as an order isomorphism between `Fin n` and `{x : Fin (n + 1) // x ≠ p}`. -/
def finSuccAboveEquiv (p : Fin (n + 1)) : Fin n ≃ { x : Fin (n + 1) // x ≠ p } :=
  .optionSubtype p ⟨(finSuccEquiv' p).symm, rfl⟩

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