Commit 2020-10-05 19:45 88c76ab9

feat(order/filter/ultrafilter): Add variant of exists_ultrafilter. (#4436) The lemma exists_ultrafilter tells us that any proper filter can be extended to an ultrafilter (using Zorn's lemma). This PR adds a variant, called exists_ultrafilter_of_finite_inter_nonempty which says that any collection of sets S can be extended to an ultrafilter whenever it satisfies the property that the intersection of any finite subcollection T is nonempty.