Commit 2022-10-27 07:38 c680de9e

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.