Let is a set. A filter (on ) is by definition a non-empty set of subsets of such that . Note that unlike some other authors I do not require .
For greater clarity I will use filter objects instead of filters. Below I will describe the properties of filter objects without exact definition and the proofs. You can look here for the formalistic behind.
I will denote the set of all filters objects on a set as . Filter objects are bijectively related with filters by the bijection “” from the set of filter objects to the set of filters. A filter object corresponding to principal filter generated by a set is equal to . (Thus the set of subsets of is a subset of .)
Formal definition of filter objects in the framework of ZF is given here. We will not need the exact definition of filter objects, but only the facts that “” is a bijection from filter objects to filters and that a filter object corresponding to principal filter generated by a set is equal to .
I will define the order on the set of filter objects by the formula for every filter objects and . This order well-agrees with the order of sets on .
with the above defined order is a complete lattice. (See this draft article for a proof.)