Upper Way Below Open Subset Complement is Non Empty implies There Exists Maximal Element of Complement
Theorem
Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $X$ be upper way below open subset of $S$.
Let $x \in S$ such that
- $x \in \relcomp S X$
Then
- $\exists m \in S: x \preceq m \land m = \max \relcomp S X$
Proof
Define $A := \set {C \in \map {\mathit {Chains} } L: C \subseteq \relcomp S X \land x \in C}$
where $\map {\mathit {Chains} } L$ denotes the set of all chains of $L$.
We will prove that
- $\forall Z: Z \ne \O \land Z \subseteq A \land \paren {\forall X, Y \in Z: X \subseteq Y \lor Y \subseteq X} \implies \bigcup Z \in A$
Let $Z$ such that
- $Z \ne \O \land Z \subseteq A \land \paren {\forall X, Y \in Z: X \subseteq Y \lor Y \subseteq X}$
We will prove that
- $\bigcup Z$ is a chain of $L$
Let $a, b \in \bigcup Z$
By definition of union:
- $\exists Y_1 \in Z: a \in Y_1$
and
- $\exists Y_2 \in Z: b \in Y_2$
By assumption:
- $Y_1 \subseteq Y_2$ or $Y_2 \subseteq Y_1$
By definition of subset:
- $a, b \in Y_1$ or $a, b \in Y_2$
By definition of $A$:
- $Y_1, Y_2 \in \map {\mathit {Chains} } L$
Thus by definition of connected relation
- $a \preceq b$ or $b \preceq a$
$\Box$
By definition of non-empty set:
- $\exists Y: Y \in Z$
By definition of $A$:
- $x \in Y$
By definition of union:
- $x \in \bigcup Z$
By definition of $A$:
- $\forall Y \in Z: Y \subseteq \relcomp S X$
By Union of Subsets is Subset/Set of Sets:
- $\bigcup Z \subseteq \relcomp S X$
Thus by definition of $A$
- $\bigcup Z \in A$
$\Box$
- $\set x$ is a chain of $L$.
By definition of $A$:
- $\set x \in A$
By Zorn's Lemma:
- $\exists Y \in A: Y$ is a maximal element of $A$.
By definition of maximal element:
- $\forall Z \in A: Y \subseteq Z \implies Y = Z$
By definition of $A$:
- $Y \in \map {\mathit {Chains} } L \land Y \subseteq \relcomp S X \land x \in Y$
By definition of supremum:
- $\sup Y$ is upper bound for $Y$.
By definition of upper bound:
- $x \preceq \sup Y$
We will prove that
- $\lnot \exists y \in S: y \in \relcomp S X \land y \succ \sup Y$
Aiming for a contradiction, suppose
- $\exists y \in S: y \in \relcomp S X \land y \succ \sup Y$
By definition of antisymmetry:
- $y \notin Y$
By definition of $\succ$
- $\sup Y \preceq y$
We wiil prove that
- $Y \cup \set y$ is a chain of $L$.
Let $a, b \in Y \cup \set y$
Case $a, b \in Y$.
Thus by definition of connected relation:
- $a \preceq b$ or $b \preceq a$
Case $a \in Y \land b \in \set y$
By definition of singleton:
- $b = y$
By definition of supremum:
- $a \preceq \sup Y$
By definition of transitivity:
- $a \preceq b$
Thus
- $a \preceq b$ or $b \preceq a$
Case $a \in \set y \land b \in Y$
Analogical case as previous.
Case $a, b \in \set y$
By definition of singleton:
- $ a = y$ and $b = y$
Be definition of reflexivity:
- $a \preceq b$
Thus
- $a \preceq b$ or $b \preceq a$
$\Box$
By definitions of singleton and subset:
- $\set y \subseteq \relcomp S X$
By Union of Subsets is Subset:
- $Y \cup \set y \subseteq \relcomp S X$
By definition of union:
- $x \in Y \cup \set y$
By definition of $A$:
- $Y \cup \set y \in A$
- $Y \subseteq Y \cup \set y$
Then
- $Y = Y \cup \set y$
By definitions of union and singleton:
- $y \in Y$
This contradicts $y \notin Y$.
$\Box$
We will prove that
- $\sup Y \in \relcomp S X$
Aiming for a contradiction, suppose
- $\sup Y \in X$
By definition of way below open:
- $\exists y \in X: y \ll \sup Y$
- $Y$ is directed.
By definition of way below relation:
- $\exists d \in Y: y \preceq d$
By definition of upper section:
- $d \in X$
Thus it contradicts $d \in \relcomp S X$ by definition of subset.
$\Box$
By definition of maximal element
- $\sup Y = \max \relcomp S X$
Hence
- $\exists m \in S: x \preceq m \land m = \max \relcomp S X$
$\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_6:9