Equivalence of Definitions of Lattice Filter
Theorem
Let $\struct {S, \vee, \wedge, \preceq}$ be a lattice.
Let $F \subseteq S$ be a non-empty subset of $S$.
The following definitions of the concept of Lattice Filter are equivalent:
Definition 1
$F$ is a lattice filter of $S$ if and only if $F$ satisifes the lattice filter axioms:
\((\text {LF 1})\) | $:$ | $F$ is a sublattice of $S$: | \(\ds \forall x, y \in F:\) | \(\ds x \wedge y, x \vee y \in F \) | |||||
\((\text {LF 2})\) | $:$ | \(\ds \forall x \in F: \forall a \in S:\) | \(\ds x \vee a \in F \) |
Definition 2
$F$ is a lattice filter of $S$ if and only if $F$ is a meet semilattice filter.
Proof
Definition 1 implies Definition 2
Let $F$ satisify the lattice filter axioms.
To show that $F$ is a meet semilattice filter it is sufficient to show:
$F$ is a upper section of $S$: | \(\ds \forall x \in F: \forall y \in S:\) | \(\ds x \preceq y \implies y \in F \) |
Let $x \in F, y \in S : x \preceq y$.
By the lattice filter axioms, $F$ is a sublattice of $\struct {S, \vee, \wedge, \preceq}$, so:
- $x \vee y \in F$
From Preceding iff Join equals Larger Operand:
- $y = x \vee y$
Hence:
- $y \in F$
The result follows.
$\Box$
Definition 2 implies Definition 1
Let $F$ be a meet semilattice filter of $\struct {S, \wedge, \preceq}$.
To show that $F$ is a lattice filter of $\struct {S, \vee, \wedge, \preceq}$ it is sufficient to show:
- $\forall x \in F, a \in S: x \vee a \in F$
Let $x \in F, a \in S$.
By definition of join:
- $x \preceq x \vee a$
By definition of meet semilattice filter, $F$ is an upper section, so:
- $x \vee a \in F$
The result follows.
$\blacksquare$