PartialIso

Mathlib.Order.CountableDenseLinearOrder

URI: https://scilib.ai/kg/mathlib#Order.PartialIso

Lean4

/-- The type of partial order isomorphisms between `α` and `β` defined on finite subsets.
A partial order isomorphism is encoded as a finite subset of `α × β`, consisting
of pairs which should be identified. -/
def PartialIso : Type _ :=
  { f : Finset (α × β) // ∀ p ∈ f, ∀ q ∈ f, cmp (Prod.fst p) (Prod.fst q) = cmp (Prod.snd p) (Prod.snd q) }

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru