Theorems · Definition · order theory

GaloisConnection

{α : Type u} → {β : Type v} → [Preorder α] → [Preorder β] → (α → β) → (β → α) → Prop

A Galois connection is a pair of functions l and u satisfying l a ≤ b ↔ a ≤ u b. They are special cases of adjoint functors in category theory, but do not depend on the category theory library in mathlib.

Defined in

Mathlib.Order.GaloisConnection.Defs

Cited by

253 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 6 definitions · uses no axioms

Assumes

PreorderPreorder