Way Below in Complete Lattice

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\struct {S, \vee, \wedge, \preceq}$ be a complete lattice.

Let $x, y \in S$.


Then

$x \ll y$

if and only if

$\forall X \subseteq S: y \preceq \sup X \implies \exists A \in \map {\operatorname {Fin} } X: x \preceq \sup A$

where

$\ll$ denotes the way below relation,
$\map {\operatorname {Fin} } X$ denotes the set of all finite subsets of $X$.


Proof

Sufficient Condition

Let

$x \ll y$

Let $X \subseteq S$ such that

$y \preceq \sup X$

By Set of Finite Suprema is Directed:

$\set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$ is directed.

By definition of union:

$\bigcup \map {\operatorname {Fin} } X \setminus \set \O = X$

By Supremum of Suprema:

$\sup X = \sup \set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$

By definition of way below relation:

$\exists z \in \set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}: x \preceq z$

Thus

$\exists A \in \map {\operatorname {Fin} } X: x \preceq \sup A$

$\Box$

Necessary Condition

Let

$\forall X \subseteq S: y \preceq \sup X \implies \exists A \in \map {\operatorname {Fin} } X: x \preceq \sup A$

Let $D$ be a directed subset of $S$ such that

$y \preceq \sup D$

By assumption:

$\exists A \in \map {\operatorname {Fin} } D: x \preceq \sup A$

By Directed iff Finite Subsets have Upper Bounds:

$\exists u \in D: u$ is upper bound for $A$

By definition of supremum:

$\sup A \preceq u$

Thus by definition of transitivity:

$x \preceq u$

Thus by definition of way below relation:

$x \ll y$

$\blacksquare$


Sources