ofUnique — Mathlib

English

There exists an order isomorphism between any two types with a unique element, preserving the order.

Русский

Существует порядковый изоморфизм между любыми двумя типами, имеющими уникальный элемент, сохраняющий порядок.

LaTeX

$$$\exists \text{OrderIso}(\alpha,\beta)\; \text{при условии } [Unique\alpha], [Unique\beta], [Preorder]$$$

Lean4

/-- The order isomorphism `α ≃o β` when `α` and `β` are preordered types
containing unique elements. -/
@[simps!]
noncomputable def ofUnique (α β : Type*) [Unique α] [Unique β] [Preorder α] [Preorder β] : α ≃o β
    where
  toEquiv := Equiv.ofUnique α β
  map_rel_iff' := by simp

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