mathlib

c680de9e - feat(order/filter/ultrafilter): an ultrafilter is an atom in the lattice of filters (#17116)

feat(order/filter/ultrafilter): an ultrafilter is an atom in the lattice of filters (#17116) * add `filter.nontrivial`, `filter.Inf_ne_bot_of_directed`, and `filter.Inf_ne_bot_of_directed'`; * add `is_atom_iff` and `is_coatom_iff`; * generalize `ultrafilter.exists_le` to any partial order; * prove that a filter is an ultrafilter if and only if it is an atom in the lattice of filters.