mathlib3

d3cdcd83 - feat(order/filter/basic): add lemma `le_prod_map_fst_snd` (#11901)

feat(order/filter/basic): add lemma `le_prod_map_fst_snd` (#11901) A lemma relating filters on products and the filter-product of the projections. This lemma is particularly useful when proving the continuity of a function on a product space using filters. Discussion: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Some.20missing.20prod.20stuff