Theorems · Definition · order theory

OrderIso.toGaloisCoinsertion

{α : Type u} → {β : Type v} → [inst : Preorder α] → [inst_1 : Preorder β] → (e : α ≃o β) → GaloisCoinsertion ⇑e ⇑e.symm

Makes a Galois coinsertion from an order-preserving bijection.

Defined in

Mathlib.Order.GaloisConnection.Basic

Cited by

1 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Quot.sound

Assumes

PreorderPreorder