Way Below in Lattice of Power Set
Theorem
Let $X$ be a set.
Let $L = \struct {\powerset X, \cup, \cap, \preceq}$ be a lattice of power set of $X$ where $\mathord\preceq = \mathord\subseteq \cap \paren {\powerset X \times \powerset X}$
Let $x, y \in \powerset X$.
Then $x \ll y$ if and only if
- for every a set $Y$ of subsets of $X$ such that $y \subseteq \bigcup Y$
- then there exists a finite subset $Z$ of $Y$: $x \subseteq \bigcup Z$
where $\ll$ denotes the way below relation.
Proof
Sufficient Condition
Let $x \ll y$
Let $Y$ be a set of subsets of $X$ such that
- $y \subseteq \bigcup Y$
By definitions of power set and subset:
- $Y \subseteq \powerset X$
By Power Set is Complete Lattice:
- $\bigcup Y = \sup Y$
By definition of $\preceq$:
- $y \preceq \sup Y$
By Way Below in Complete Lattice:
- there exists a finite subset $Z$ of $Y$: $x \preceq \sup Z$
By the proof of Power Set is Complete Lattice:
- $\bigcup Z = \sup Z$
Thus by definition of $\preceq$:
- there exists a finite subset $Z$ of $Y$: $x \subseteq \bigcup Z$
$\Box$
Necessary Condition
Suppose
- for every a set $Y$ of subsets of $X$ such that $y \subseteq \bigcup Y$
- then there exists a finite subset $Z$ of $Y$: $x \subseteq \bigcup Z$
We will prove that
- for every a subset $Y$ of $\powerset X$ such that $y \preceq \sup Y$
- then there exists a finite subset $Z$ of $Y$: $x \preceq \sup Z$
Let $Y$ be a subset of $\powerset X$ such that
- $y \preceq \sup Y$
By definition of power set:
By Power Set is Complete Lattice:
- $\bigcup Y = \sup Y$
By definition of $\preceq$:
- $y \subseteq \bigcup Y$
By assumption:
- there exists a finite subset $Z$ of $Y$: $x \subseteq \bigcup Z$
By the proof of Power Set is Complete Lattice:
- $\bigcup Z = \sup Z$
Thus by definition of $\preceq$:
- there exists a finite subset $Z$ of $Y$: $x \preceq \sup Z$
$\Box$
Thus by Way Below in Complete Lattice:
- $x \ll y$
$\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 WAYBEL_8:27