Finite Infima Set and Upper Closure is Smallest Filter

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $L = \struct {S, \wedge, \preceq}$ be a meet semilattice.

Let $X$ be a non-empty subset of $S$.


Then

$X \subseteq \map {\operatorname {fininfs} } X^\succeq$ and
for every a filter $F$ in $L$: $\paren {X \subseteq F \implies \map {\operatorname {fininfs} } X^\succeq \subseteq F}$

where

$\map {\operatorname {fininfs} } X$ denotes the finite infima set of $X$,
$X^\succeq$ denotes the upper closure of $X$.


Proof

By Set is Subset of Finite Infima Set:

$X \subseteq \map {\operatorname {fininfs} } X$

By Upper Closure of Subset is Subset of Upper Closure:

$X^\succeq \subseteq \map {\operatorname {fininfs} } X^\succeq$

By Set is Subset of Upper Closure:

$X \subseteq X^\succeq$

Thus by Subset Relation is Transitive:

$X \subseteq \map {\operatorname {fininfs} } X^\succeq$

Let $F$ be a filter in $L$ such that

$X \subseteq F$

Let $x \in \map {\operatorname {fininfs} } X^\succeq$

By definition of upper closure of subset:

$\exists y \in \map {\operatorname{fininfs} } X: y \preceq x$

By definition of finite infima set:

$\exists A \in \map {\operatorname {Fin} } X: y = \inf A \land A$ admits an infimum

where $\map {\operatorname {Fin} } X$ denotes the set of all finite subsets of $S$.

By Subset Relation is Transitive:

$A \subseteq F$

By Filtered in Meet Semilattice with Finite Infima:

$A \ne \O \implies \inf A \in F$

By Infimum of Empty Set is Greatest Element and Top in Filter:

$A = \O \implies \inf A = \top \in F$

where $\top$ denotes the greatest element of $S$.

So

$y \in F$

Thus by definition of upper section:

$x \in F$

$\blacksquare$


Sources