subsingleton_of_wellFoundedLT — Mathlib

English

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

Русский

Если α — линейный порядок с хорошо упорядоченностью, то изоморфизм порядка α к β единственен.

LaTeX

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

Lean4

instance subsingleton_of_wellFoundedLT [LinearOrder α] [WellFoundedLT α] [Preorder β] : Subsingleton (α ≃o β) :=
  by
  refine ⟨fun f g ↦ ?_⟩
  rw [OrderIso.ext_iff, ← coe_toOrderEmbedding, ← coe_toOrderEmbedding, DFunLike.coe_fn_eq, ← OrderEmbedding.range_inj,
    coe_toOrderEmbedding, coe_toOrderEmbedding, range_eq, range_eq]

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