Well Inside Elements Form Filter

From ProofWiki
Jump to navigation Jump to search


This article needs proofreading.
Please check it for mathematical errors.
If you believe there are none, please remove {{Proofread}} from the code.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{Proofread}} from the code.


Theorem

Let $L = \struct{S, \vee, \wedge, \preceq}$ be a distributive lattice with greatest element $\top$ and smallest element $\bot$.

Let $\eqslantless$ denote the well inside relation on $L$.


Then:

$\forall a \in S : \set{b \in S: a \eqslantless b}$ is a lattice filter


Proof

Let $a \in S$.

Let $F = \set{b \in S: a \eqslantless b}$.

$F$ is an Upper Section

Let $b \in F$ and $c \in S : b \preceq c$.


By Ordering Axiom $(3)$: Antisymmetry:

$a \preceq a$

Hence we have:

$a \preceq a \eqslantless b \preceq c$


From Well Inside Relation Extends to Predecessor and Successor:

$a \eqslantless c$

Hence:

$c \in F$


It follows that $F$ is an upper section by definition.

$\Box$

$F$ is a Meet Subsemilattice

Let $b, c \in F$.

By definition of well inside relation:

$\exists x, y \in S : a \wedge x = \bot, b \vee x = \top, a \wedge y = \bot, c \vee y = \top$


We have:

\(\ds \paren{b \wedge c} \vee \paren{x \vee y}\) \(=\) \(\ds \paren{b \vee \paren{x \vee y} } \wedge \paren{c \vee \paren{x \vee y} }\) Definition of Distributive Lattice
\(\ds \) \(=\) \(\ds \paren{b \vee \paren{x \vee y} } \wedge \paren{c \vee \paren{y \vee x} }\) Join is Commutative
\(\ds \) \(=\) \(\ds \paren{\paren{b \vee x} \vee y} \wedge \paren{\paren{c \vee y} \vee x}\) Join is Associative
\(\ds \) \(=\) \(\ds \paren{\top \vee y} \wedge \paren{\top \vee x}\) as $\paren{b \vee x} = \top, \paren{c \vee y} = \top$
\(\ds \) \(=\) \(\ds \top \wedge \top\) Successor is Supremum
\(\ds \) \(=\) \(\ds \top\) Meet is Idempotent


Also we have:

\(\ds a \wedge \paren{x \vee y}\) \(=\) \(\ds \paren{a \wedge x} \vee \paren{a \wedge y}\) Definition of Distributive Lattice
\(\ds \) \(=\) \(\ds \bot \vee \bot\) as $\paren{a \wedge x} = \bot, \paren{a \wedge y} = \bot$
\(\ds \) \(=\) \(\ds \bot\) Join is Idempotent


By definition of well inside relation:

$a \eqslantless b \wedge c$

By definition of $F$:

$b \wedge c \in F$


It follows that $F$ is an meet subsemilattice by definition.

$\Box$


It follows that $F$ is a lattice filter by definition.


The result follows.

$\blacksquare$


Sources

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