Way Below implies There Exists Way Below Open Filter Subset of Way Above Closure

From ProofWiki
Jump to navigation Jump to search

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$

By Meet Precedes Operands:

$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

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