subsingleton_of_wellFoundedGT — Mathlib

English

If α ≃o β with β a linear order with WellFoundedGT, then Subsingleton (OrderIso α β).

Русский

Если существует изоморфизм порядка α ≃o β и β имеет WellFoundedGT, то таких изоморфизмов не более одного.

LaTeX

$$Subsingleton (OrderIso α β)$$

Lean4

instance subsingleton_of_wellFoundedGT [LinearOrder α] [WellFoundedGT α] [Preorder β] : Subsingleton (α ≃o β) :=
  by
  refine ⟨fun f g ↦ ?_⟩
  change f.dual.dual = g.dual.dual
  rw [Subsingleton.elim f.dual]

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