mathlib3

5f5bcd85 - feat(order/filter/ultrafilter): add some comap_inf_principal lemmas (#11495)

feat(order/filter/ultrafilter): add some comap_inf_principal lemmas (#11495) ...in the setting of ultrafilters These lemmas are useful to prove e.g. that the continuous image of a compact set is compact in the setting of convergence spaces. Co-authored-by: Patrick Massot <patrickmassot@free.fr>