Commit 2022-02-09 17:14 d3cdcd83
View on Github →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