Up-Complete Lower Bounded Join Semilattice is Complete
Theorem
Let $\struct {S, \preceq}$ be an up-complete lower bounded join semillattice.
Then $\struct {S, \preceq}$ is complete.
Proof
Let $X$ be a subset of $S$.
In the case when $X = \O$:
by definition of lower bounded:
- $\exists L \in S: L$ is lower bound for $S$.
By definition of empty set:
- $L$ is upper bound for $X$.
By definition of lower bound:
- $\forall x \in S: x$ is upper bound for $X \implies L \preceq x$
Thus by definition
- $L$ is a supremum of $X$.
Thus:
- $X$ admint a supremum.
$\Box$
In the case when $X \ne \O$:
Define
- $Y := \set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$
where $\map {\operatorname {Fin} } X$ denotes the set of all finite subsets of $X$.
By Existence of Non-Empty Finite Suprema in Join Semilattice
- all suprema in $Y$ exist,
By definition of non-empty set:
We will prove that
- $Y$ is directed
Let $x, y \in Y$.
By definition of $Y$:
- $\exists A \in \map {\operatorname {Fin} } X \setminus \set \O: x = \sup A$
and
- $\exists B \in \map {\operatorname {Fin} } X \setminus \set \O: y = \sup B$
By Finite Union of Finite Sets is Finite:
- $A \cup B$ is finite
- $A \cup B \ne \O$
By Union is Smallest Superset:
- $A \cup B \subseteq X$
By definition of $Y$:
- $\map \sup {A \cup B} \in Y$
- $A \subseteq A \cup B$ and $B \subseteq A \cup B$
Thus by Supremum of Subset:
- $x \preceq \map \sup {A \cup B}$ and $y \preceq \map \sup {A \cup B}$
Thus by definition:
- $Y$ is directed.
By definition up-complete:
- $Y$ admits a supremum
By definition of supremum
- $\sup Y$ is upper bound for $Y$
We will prove that
- $X \subseteq Y$
Let $x \in X$.
By definitions of subset and singleton:
- $\set x \subseteq X$
- $\set x$ is finite
- $\set x \ne \O$
By definition of $Y$:
- $\sup {\set x} \in Y$
Thus by Supremum of Singleton:
- $x \in Y$
By Upper Bound is Upper Bound for Subset:
- $\sup Y$ is upper bound for $X$
We will prove that
- $\forall x \in S: x$ is upper bound for $X \implies \sup Y \preceq x$
Let $x \in S$ such that
- $x$ is upper bound for $X$
We will prove as sublemma that
- $x$ is upper bound for $Y$
Let $y \in Y$.
By definition of $Y$:
- $\exists A \in \map {\operatorname {Fin} } X \setminus \set \O: y = \sup A$
By definition of $\operatorname {Fin}$:
- $A \subseteq X$
By Upper Bound is Upper Bound for Subset
- $x$ is upper bound for $A$
Thus by definition of supremum:
- $y \preceq x$
Thus by definition
- $x$ is upper bound for $Y$
This ends the proof of sublemma.
Thus by definition of supremum:
- $\sup Y \preceq x$
This ends the proof of lemma.
By definition
- $\sup Y$ is a supremum of $X$
and thus:
- $X$ admits a supremum.
$\Box$
Thus result follows by Lattice is Complete iff it Admits All Suprema.
$\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_0:condreg 13