Way Below iff Preceding Finite Supremum

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 {\it Fin} X: x \preceq \sup A$

where

$\ll$ denotes the way below relation,
$\map {\it 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$

Define:

$F := \set {\sup A: A \in \map {\it Fin} X}$

By definition of union:

$X = \bigcup \map {\it Fin} X$

By Supremum of Suprema:

$\sup X = \sup F$

We will prove that:

$F$ is directed

Let $a, b \in F$.

By definition of $F$:

$\exists A \in \map {\it Fin} X: a = \sup A$

and

$\exists B \in \map {\it Fin} X: b = \sup B$

By Union of Subsets is Subset:

$A \cup B \subseteq X$

By Finite Union of Finite Sets is Finite:

$A \cup B$ is finite

By definition of ${\it Fin}$:

$A \cup B \in \map {\it Fin} X$

By definition of $F$:

$\map \sup {A \cup B} \in F$

By Set is Subset of Union:

$A \subseteq A \cup B$ and $B \subseteq A \cup B$

By Supremum of Subset:

$a \preceq \map \sup {A \cup B}$ and $b \preceq \map \sup {A \cup B}$

Thus by definition:

$F$ is directed


By definition of way below relation:

$\exists d \in F: x \preceq d$

Thus by definition of $F$:

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

$\Box$


Necessary Condition

Assume that:

$\forall X \subseteq S: y \preceq \sup X \implies \exists A \in \map {\it 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 {\it Fin} D: x \preceq \sup A$

By Directed iff Finite Subsets have Upper Bounds:

$\exists h \in D: \forall a \in A: a \preceq h$

By definition:

$h$ is upper bound for $A$

By definition of supremum:

$\sup A \preceq h$

Thus by definition of transitivity:

$x \preceq h$

Thus by definition of way below relation:

$x \ll y$

$\blacksquare$


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Way_Below_iff_Preceding_Finite_Supremum&oldid=587550"