Theorems · Inductive type · order theory

GaloisInsertion

{α : Type u_2} → {β : Type u_3} → [Preorder α] → [Preorder β] → (α → β) → (β → α) → Type (max u_2 u_3)

A Galois insertion is a Galois connection where l ∘ u = id. It also contains a constructive choice function, to give better definitional equalities when lifting order structures. Dual to GaloisCoinsertion

Defined in

Mathlib.Order.GaloisConnection.Defs

Cited by

35 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

PreorderPreorder