subsingleton_of_wellFoundedLT' — Mathlib

English

If β is a well-founded linear order and α is a preorder, then there is at most one order isomorphism α ≃o β.

Русский

Пусть β — линейный порядок с хорошо основанной структурой; тогда существует не более одного порядкового изоморфизма α ≃o β.

LaTeX

$$Subsingleton (α ≃o β)$$

Lean4

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

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