Theorems · Definition · order theory

ClosureOperator.ofCompletePred

{α : Type u_1} →
  [inst : CompleteLattice α] → (p : α → Prop) → (∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)) → ClosureOperator α

Define a closure operator from a predicate that's preserved under infima.

Defined in

Mathlib.Order.Closure

Cited by

4 results in Mathlib

Foundations

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

Assumes

CompleteLattice