finSuccAboveOrderIso — Mathlib

English

There is an order isomorphism between Fin(n) and the subtype { x : Fin(n+1) | x ≠ p } given by succAbove.

Русский

Существует изоморфизм порядков между Fin(n) и подтипом { x : Fin(n+1) | x ≠ p }, заданный succAbove.

LaTeX

$$$\mathrm{Fin}(n) \cong_o \{ x : \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 finSuccAboveOrderIso (p : Fin (n + 1)) : Fin n ≃o { x : Fin (n + 1) // x ≠ p }
    where
  __ := finSuccAboveEquiv p
  map_rel_iff' := p.succAboveOrderEmb.map_rel_iff'

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