Upper Way Below Open Subset Complement is Non Empty implies There Exists Maximal Element of Complement

From ProofWiki
Jump to navigation Jump to search

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$


By Singleton is Chain:

$\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$

By Set is Subset of Union:

$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$

By Chain is Directed:

$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