Way Below implies There Exists Way Below Open Filter Subset of Way Above Closure
Theorem
Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below continuous lattice.
Let $x, y \in S$ such that
- $x \ll y$
where $\ll$ denotes the way below relation.
Then there exists a way below open filter in $L$: $y \in F \land F \subseteq x^\gg$
where $x^\gg$ denotes the way above closure of $x$.
Proof
We will prove that
- $x^\gg$ is way below open.
Let $z \in x^\gg$.
By definition of way above closure:
- $x \ll z$
By Way Below has Interpolation Property:
- $\exists x' \in S: x \ll x' \land x' \ll z$
Thus by definition of way above closure:
- $x' \in x^\gg$
Thus
- $x' \ll z$
$\Box$
Then:
- $\forall z \in x^\gg: \exists y \in x^\gg: y \ll z$
By Axiom of Choice define a mapping $f: x^\gg \to x^\gg$:
- $\forall z \in x^\gg: \map f z \ll z$
By definition of way above closure:
- $y \in x^\gg$
Define $V := \set {z^\succeq: \exists n \in \N: z = \map {f^n} y}$
We will prove that
- $\forall X, Y \in V: \exists Z \in V: X \cup Y \subseteq Z$
Let $X, Y \in V$.
By definition of $V$:
- $\exists z_1 \in S: X = z_1^\succeq \land \exists n_1 \in \N: z_1 = \map {f^{n_1} } y$
and
- $\exists z_2 \in S: Y = z_2^\succeq \land \exists n_2 \in \N: z_2 = \map {f^{n_2} } y$
We will prove that
- $\forall n, k \in \N: \map {f^{n + k} } y \preceq \map {f^n} y$
Let $n \in \N$.
Base Case:
By definition of reflexivity:
- $\map {f^{n + 0} } y \preceq \map {f^n} y$
Induction Hypothesis:
- $\map {f^{n + k} } y \preceq \map {f^n} y$
Induction Step:
By definition of $f$:
- $\map {f^{n + k + 1} } y \ll \map {f^{n + k} } y$
By Way Below implies Preceding:
- $\map {f^{n + k + 1} } y \preceq \map {f^{n + k} } y$
By Induction Hypothesis and definition of transitivity:
- $\map {f^{n + k + 1} } y \preceq \map {f^n} y$
$\Box$
Without loss of generality, suppose $n_1 \le n_2$
Then
- $\exists k \in \N: n_2 = n_1+k$
Then
- $z_2 \preceq z_1$
By Preceding iff Meet equals Less Operand:
- $z_1 \wedge z_2 = z_2$
By definition of $V$:
- $Z := \paren {z_1 \wedge z_2}^\succeq \in V$
- $z_1 \wedge z_2 \preceq z_1$ and $z_1 \wedge z_2 \preceq z_2$
By Upper Closure is Decreasing:
- $z_1^\succeq \subseteq Z$ and $z_2^\succeq \subseteq Z$
Thus by Union of Subsets is Subset:
- $X \cup Y \subseteq Z$
$\Box$
Define $F := \bigcup V$.
We will prove that
- $F$ is way below open.
Let $u \in F$.
By definition of union:
- $\exists Y \in V: u \in Y$
By definition of $V$:
- $\exists z \in S: Y = z^\succeq \land \exists n \in \N: z = \map {f^n} y$
By definition of $f$:
- $z \in x^\gg$
By definition of $f$:
- $\map f z \ll z$
Then
- $z' := \map f z = \map {f^{n + 1} } y$
By definition of $V$:
- ${z'}^\succeq \in V$
By definition of reflexivity:
- $z' \preceq z'$
By definition of upper closure of element:
- $z' \in {z'}^\succeq$
By definition of union:
- $z' \in F$
By definition of upper closure of element:
- $z \preceq u$
By Preceding and Way Below implies Way Below:
- $z' \ll u$
Hence
- $\exists g \in F: g \ll u$
$\Box$
By Upper Closure of Element is Filter:
- $\forall X \in V: X$ is a filtered upper section.
By Union of Upper Sections is Upper:
- $F$ is an upper section.
By Union of Filtered Sets is Filtered:
- $F$ is filtered.
By definition of filter:
- $F$ is a way below open filter in $L$.
Then:
- $\map {f^0} y = y$
By definition of $V$:
- $y^\succeq \in V$
By definitions of upper closure of element and reflexivity:
- $y \in y^\succeq$
By definition of union:
- $y \in F$
It remains to prove that
- $F \subseteq x^\gg$
Let $u \in F$.
By definition of union:
- $\exists Y \in V: u \in Y$
By definition of $V$:
- $\exists z \in S: Y = z^\succeq \land \exists n \in \N: z = \map {f^n} y$
By definition of $f$:
- $z \in x^\gg$
By definition of way above closure:
- $x \ll z$
By definition of upper closure of element:
- $z \preceq u$ and $x \preceq x$
By Preceding and Way Below implies Way Below:
- $x \ll u$
Thus by definition of way above closure:
- $u \in x^\gg$
$\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_6:8