Set of Finite Suprema is Directed
Jump to navigation
Jump to search
Theorem
Let $\struct {S, \vee, \preceq}$ be a join semilattice.
Let $X$ be a non-empty subset of $S$.
Then
- $\set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$ is directed.
where $\map {\operatorname {Fin} } X$ denotes the set of all finite subsets of $X$.
Proof
By Existence of Non-Empty Finite Suprema in Join Semilattice:
- for every $A \in \map {\operatorname {Fin} } S$ if $A \ne \O$, then $A$ admits a supremum.
By definition of non-empty set:
- $\exists a: a \in X$
By definitions of subset and singleton:
- $\set x \subseteq X$
- $\set x$ is finite
By definitions of non-empty set and singleton:
- $\set x \ne \O$
By definition of $\operatorname {Fin}$:
- $\sup {\set x} \in \set {\sup A: A \in \map {\operatorname{Fin} } X \land A \ne \O}$
Thus by definition:
- $\set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$ is a non-empty set.
Let $x, y \in \set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$
Then
- $\exists A \in \map {\operatorname {Fin} } X: x = \sup A$ and $A \ne \O$
and
- $\exists B \in \map {\operatorname {Fin} } X: y = \sup B$ and $B \ne \O$
By Finite Union of Finite Sets is Finite:
- $A \cup B$ is finite
By Union of Subsets is Subset:
- $A \cup B \subseteq X$
By definitions of non-empty set and union:
- $A \cup B \ne \O$
By definition of $\operatorname {Fin}$:
- $\map \sup {A \cup B} \in \set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$
- $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:
- $\set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$ is directed.
$\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:funcreg 21