# Proper and Prime iff Ultrafilter in Boolean Lattice

## Theorem

Let $B = \left({S, \vee, \wedge, \neg, \preceq}\right)$ be a Boolean lattice.

Let $F$ be a filter in $B$.

Then

- $F$ is a proper subset of $S$ and $F$ is a prime filter in $B$

- $F$ is ultrafilter on $B$

## Proof

### Sufficient Condition

Let us assume

- $F$ is a proper subset of $S$ and $F$ is a prime filter in $B$.

Thus

- $F$ is a proper subset of $S$.

Let $G$ be a filter in $B$ such that

- $F \subseteq G$ and $F \ne G$.

By definitions of subset and set equality:

- $\exists x: x \in G \land x \notin F$

By definition of Boolean algebra:

- $x \vee \neg x = \top$

where $\top$ denotes the top of $B$.

By Top in Filter:

- $\top \in F$

By definition of prime filter:

- $\neg x \in F$

By definition of subset:

- $\neg x \in G$

By Filtered in Meet Semilattice:

- $x \wedge \neg x \in G$

By definition of Boolean algebra:

- $\bot \in G$

Thus by definition of subset:

- $G \subseteq S$

By definition of set equality it remains to prove that

- $S \subseteq G$

Let $y \in S$.

By definition of smallest element:

- $\bot \preceq y$

Thus by definition of upper set:

- $y \in G$

$\Box$

### Necessary Condition

Let $F$ be ultrafilter on $B$.

Thus by definition of ultrafilter:

- $F$ is proper subset of $S$.

Let $x \in S$.

Aiming for a contradiction suppose that

- $x \notin F$ and $\neg x \notin F$

By Finite Infima Set and Upper Closure is Smallest Filter:

- $F \cup \left\{ {x}\right\} \subseteq {\operatorname{fininfs}\left({F \cup \left\{ {x}\right\} }\right)}^\succeq$

- $\left\{ {x}\right\} \subseteq F \cup \left\{ {x}\right\}$ and $F \subseteq F \cup \left\{ {x}\right\}$

By definition of singleton:

- $x \in \left\{ {x}\right\}$

By definition of subset:

- $x \in {\operatorname{fininfs}\left({F \cup \left\{ {x}\right\} }\right)}^\succeq$

By Finite Infima Set and Upper Closure is Filter:

- ${\operatorname{fininfs}\left({F \cup \left\{ {x}\right\} }\right)}^\succeq$ is filter in $L$.

By Subset Relation is Transitive:

- $F \subseteq {\operatorname{fininfs}\left({F \cup \left\{ {x}\right\} }\right)}^\succeq$

By definition of ultrafilter:

- ${\operatorname{fininfs}\left({F \cup \left\{ {x}\right\} }\right)}^\succeq = S$

By Finite Subset Bounds Element of Finite Infima Set and Upper Closure:

- $\exists a \in S: a \in F \land \neg x \succeq a \wedge \inf \left\{ {x}\right\}$

By definition of greatest element:

- $a \preceq \top$

\(\displaystyle a\) | \(=\) | \(\displaystyle a \wedge \top\) | Preceding iff Meet equals Less Operand | ||||||||||

\(\displaystyle \) | \(=\) | \(\displaystyle a \wedge \left({x \vee \neg x}\right)\) | definition of Boolean algebra | ||||||||||

\(\displaystyle \) | \(=\) | \(\displaystyle a \wedge x \vee a \wedge \neg x\) | definition of distributive lattice |

- $\inf \left\{ {x}\right\} = x$

- $a \wedge \neg x \preceq \neg x$

By definition of infimum:

- $a \preceq \neg x$

By definition of upper set:

- $\neg x \in F$

This contradicts $\neg x \notin F$

Thus by Proof by Contradiction:

- $F$ is a prime filter by Filter is Prime iff For Every Element Element either Negation Belongs to Filter in Boolean Lattice.

$\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_7:22