Definition 1.4.17 (Filter). A filter $F$ on a lattice $L$ is a subset of $L$ with the following properties:

• $F\ne \varnothing$

• $F$ is a terminal segment of $L$ (i.e., if $f\le x$ and $f\in F$, then $x\in F$)

• $F$ is closed under finite meets