*): golf `ultrafilter.exists_ultrafilter_of_finite_inter_nonempty` (#17096)

Commit

3 years ago

chore(order/filter/*): golf `ultrafilter.exists_ultrafilter_of_finite_inter_nonempty` (#17096)

Author

urkud

Parents