Image of Operator Generated by Closure System is Set of Closure System

Theorem

Let $L = \struct {X, \vee, \wedge, \preceq}$ be a complete lattice.

Let $S = \struct {T, \precsim}$ be a closure system of $L$.

Then $\map {\operatorname {operator} } S \sqbrk X = T$

where $\map {\operatorname {operator} } S$ denotes the operator generated by $S$.

Proof

Define $f = \map {\operatorname {operator} } S$.

$\subseteq$

Let $x \in f \sqbrk X$.

By definition of image of mapping:

$\exists y \in X: x = \map f y$

Define $Y = y^\succeq \cap T$

By definition of complete lattice:

$Y$ admits an infimum in $L$.

By Intersection is Subset:

$Y \subseteq T$

By definition of closure system:

$S$ inherits infima.

By definition of infima inheriting:

$Y$ admits an infimum in $S$ and $\inf_S Y = \inf_L Y$

Thus by definition of operator generated by $S$:

$x \in T$

$\Box$

$\supseteq$

Let $x \in T$.

By definition of ordered subset:

$T \subseteq X$

By definition of subset:

$x \in X$

Define $Y = x^{\succeq_L} \cap T$

By definitions of upper closure of element and reflexivity:

$x \in x^{\succeq_L}$

By definition of intersection:

$x \in Y$

By definitions of infimum and lower bound:

$\inf_L Y \preceq x$

By Intersection is Subset:

$Y \subseteq x^{\succeq_L}$

By Infimum of Subset:

$\inf_L x^{\succeq_L} \preceq \inf_L Y$

By Infimum of Upper Closure of Element:

$x \preceq \inf_L Y$

By definition of antisymmetry:

$x = \inf_L Y$

By definition of operator generated by $S$:

$x = \map f x$

Thus by definition of image of mapping:

$x \in f \sqbrk X$

$\Box$

Hence by definition of set equality:

$f \sqbrk X = T$

$\blacksquare$

Sources

• 1980: G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M.W. Mislove and D.S. Scott: A Compendium of Continuous Lattices

• Mizar article WAYBEL10:18