Theorems · Definition · order theory

LowerAdjoint.closed

{α : Type u_1} → {β : Type u_4} → [inst : Preorder α] → [inst_1 : Preorder β] → {u : β → α} → LowerAdjoint u → Set α

An element x is closed for l : LowerAdjoint u if it is a fixed point: u (l x) = x

Defined in

Mathlib.Order.Closure

Cited by

9 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

PreorderPreorder