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$.
- $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$
- $Y \subseteq x^{\succeq_L}$
- $\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