orderIsoSubtype — Mathlib

English

There is an order isomorphism between Fin n and the subtype {i | i < n}.

Русский

Существует упорядоченное изоморфизм между Fin(n) и подтипом {i | i < n}.

LaTeX

$$$\mathrm{Fin}(n) \cong_o \{ i \mid i < n \}$$$

Lean4

/-- The equivalence `Fin n ≃ {i // i < n}` is an order isomorphism. -/
@[simps! apply symm_apply]
def orderIsoSubtype : Fin n ≃o { i // i < n } :=
  equivSubtype.toOrderIso (by simp [Monotone]) (by simp [Monotone])

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