Theorems · Theorem · order theory

ClosureOperator.ofCompletePred_apply

∀ {α : Type u_1} [inst : CompleteLattice α] (p : α → Prop) (hsinf : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)) (a : α),
  (ClosureOperator.ofCompletePred p hsinf) a = ⨅ b, ↑b

Defined in

Mathlib.Order.Closure

Cited by

7 results in Mathlib

Foundations

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

Assumes

CompleteLattice