mathlib3

5dc8c1cf - feat(order/filter/n_ary): Add lemma equating map₂ to map on the product (#13490)

feat(order/filter/n_ary): Add lemma equating map₂ to map on the product (#13490) Proof that map₂ is the image of the corresponding function `α × β → γ`. Discussion: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/filter.20map.E2.82.82.20as.20map