orderIsoSingleton — Mathlib

English

There exists an order isomorphism between Fin(1) and the singleton set {a} in an ordered type α, for any a.

Русский

Существует порядок-изоморфизм между Fin(1) и множеством-одиночкой {a} в упорядоченном множестве α, для любого a.

LaTeX

$$$\mathrm{Fin}(1) \cong_o \{a\} \subseteq \alpha.$$$

Lean4

/-- This is the order isomorphism from `Fin 1` to a finset `{a}`. -/
noncomputable def orderIsoSingleton (a : α) : Fin 1 ≃o ({ a } : Finset α) :=
  OrderIso.ofUnique _ _

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