unique_of_wellFoundedGT — Mathlib

English

For any linear order α with WellFoundedGT α, there exists a unique order automorphism α ≃o α; in particular, the only order isomorphism from α to itself is the identity.

Русский

Пусть α — линейный порядок, удовлетворяющий WellFoundedGT α. Тогда существует единственный изоморфизм порядка α ≃o α; в частности, единственный порядок-автоморфизм α → α — тождественный переход.

LaTeX

$$$\exists! f:\alpha \simeq_o \alpha$$$

Lean4

instance unique_of_wellFoundedGT [LinearOrder α] [WellFoundedGT α] : Unique (α ≃o α) :=
  Unique.mk' _

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