Supremum of Meet Image of Directed Set
Theorem
Let $\struct {S, \preceq}$ be an up-complete meet semilattice.
Let $f: S \times S \to S$ be a mapping such that:
- $\forall \tuple {x, y} \in S \times S: \map f {x, y} = x \wedge y$
Let $D$ be directed subset of $S \times S$ in the simple order product $\struct {S \times S, \precsim}$ of $\struct {S, \preceq}$ and $\struct {S, \preceq}$.
Then:
- $\map \sup {\map {f^\to} D} = \sup \set {x \wedge y: x \in \map {\pr_1^\to} D, y \in \map {\pr_2^\to} D}$
where
- $\pr_1$ denotes the first projection on $S \times S$
- $\pr_2$ denotes the second projection on $S \times S$
- $\map {\pr_1^\to} D$ denotes the image of $D$ under $\pr_1$.
Proof
By definition of image of set:
- $\map {f^\to} D = \set {x \wedge y: \tuple {x, y} \in D}$
By definition of subset:
- $\map {f^\to} D \subseteq \set {x \wedge y: x \in \map {\pr_1^\to} D, y \in \map {\pr_2^\to} D}$
By Up-Complete Product/Lemma 2:
- $D_1 := \map {\pr_1^\to} D$ is directed
and
- $D_2 := \map {\pr_2^\to} D$ is directed.
By Meet of Directed Subsets is Directed:
- $\set {x \wedge y: x \in D_1, y \in D_2}$ is directed.
By definition of up-complete:
- $\set {x \wedge y: x \in D_1, y \in D_2}$ admits a supremum.
- $f$ is increasing mapping.
By Image of Directed Subset under Increasing Mapping is Directed:
- $\map {f^\to} D$ is directed.
By definition of up-complete:
- $\map {f^\to} D$ admits a supremum.
- $\map \sup {\map {f^\to} D} \preceq \sup \set {x \wedge y: x \in D_1, y \in D_2}$
We will prove that
- $\set {x \wedge y: x \in D_1, y \in D_2} \subseteq \paren {\map {f^\to} D}^\preceq$
where
- $\paren {\map {f^\to} D}^\preceq$ denotes the lower closure of $\map {f^\to} D$.
Let $z \in \set {x \wedge y: x \in D_1, y \in D_2}$.
Then
- $\exists x \in D_1, y \in D_2: z = x \wedge y$
By definition of image of set:
- $\exists \tuple {a, b} \in D: \map {\pr_1} {a, b} = x$
and
- $\exists \tuple {c, d} \in D: \map {\pr_2} {c, d} = y$:
By definition of first projection and second projection:
- $a = x$ and $d = y$
By definition of directed subset:
- $\exists \tuple {g, h} \in D: \tuple {x, b} \precsim \tuple {g, h} \land \tuple {c, y} \precsim \tuple {g, h}$
By definition of simple order product:
- $x \preceq g$ and $y \preceq h$
By Meet Semilattice is Ordered Structure:
- $x \wedge y \preceq g \wedge h \in \set {x \wedge y: \tuple {x, y} \in D}$
Thus by definition of lower closure:
- $z \in \paren {\map {f^\to} D}^\preceq$
$\Box$
By Supremum of Lower Closure of Set:
- $\paren {\map {f^\to} D}^\preceq$ admits a supremum
and
- $\map \sup {\map {f^\to} D}^\preceq = \map \sup {\map {f^\to} D}$
- $\sup \set {x \wedge y: x \in D_1, y \in D_2} \preceq \map \sup {\map {f^\to} D}$
Thus by definition of antisymmetry:
- $\map \sup {\map {f^\to} D} = \sup \set {x \wedge y: x \in D_1, y \in D_2}$
$\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_2:33