subsingleton_of_wellFoundedGT' — Mathlib

English

If β is a linear order with WellFoundedGT β and α is a preorder, then there is at most one order isomorphism from α to β; all such isomorphisms coincide.

Русский

Пусть β — линейный порядок, у которого хорошо основанность по отношению '>' (WellFoundedGT β), и пусть α — произвольный предпорядок. Тогда существует не более одного изоморфизма порядка из α в β; все такие изоморфизмы совпадают.

LaTeX

$$$\operatorname{Subsingleton}(\alpha \simeq_o \beta)$$$

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]

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