Closure operators on a partial order #
We define (bundled) closure operators on a partial order as an monotone (increasing), extensive (inflationary) and idempotent function. We define closed elements for the operator as elements which are fixed by it.
Note that there is close connection to Galois connections and Galois insertions: every closure
operator induces a Galois insertion (from the set of closed elements to the underlying type), and
every Galois connection induces a closure operator (namely the composition). In particular,
a Galois insertion can be seen as a general case of a closure operator, where the inclusion is given
by coercion, see
- to_preorder_hom : α →ₘ α
- le_closure' : ∀ (x : α), x ≤ c.to_preorder_hom.to_fun x
- idempotent' : ∀ (x : α), c.to_preorder_hom.to_fun (c.to_preorder_hom.to_fun x) = c.to_preorder_hom.to_fun x
A closure operator on the partial order
α is a monotone function which is extensive (every
is less than its closure) and idempotent.
Constructor for a closure operator using the weaker idempotency axiom:
f (f x) ≤ f x.
Convenience constructor for a closure operator using the weaker minimality axiom:
x ≤ f y → f x ≤ f y, which is sometimes easier to prove in practice.
Expanded out version of
p implies being closed. This constructor should be used when
you already know a sufficient condition for being closed and using
mem_mk₃_closed will avoid you
the (slight) hassle of having to prove it both inside and outside the constructor.
This lemma shows that the image of
x of a closure operator built from the
p, the property that was fed into it.
closure_le_closed_iff_le but with the
p that was fed into the
This lemma shows that the
p fed into the
mk₃ constructor implies being closed.
The set of closed elements has a Galois insertion to the underlying type.
Every Galois connection induces a closure operator given by the composition. This is the partial order version of the statement that every adjunction induces a monad.