Theorems · Inductive type · order theory

LowerAdjoint

{α : Type u_1} → {β : Type u_4} → [Preorder α] → [Preorder β] → (β → α) → Type (max u_1 u_4)

A lower adjoint of u on the preorder α is a function l such that l and u form a Galois connection. It allows us to define closure operators whose output does not match the input. In practice, u is often (↑) : β → α.

Defined in

Mathlib.Order.Closure

Cited by

38 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

PreorderPreorder