mathlib3

16ef2913 - feat(order/filter/*, topology/subset_properties): define "coproduct" of two filters (#6372)

feat(order/filter/*, topology/subset_properties): define "coproduct" of two filters (#6372) Define the "coproduct" of two filters (unclear if this is really a categorical coproduct) as ```lean protected def coprod (f : filter α) (g : filter β) : filter (α × β) := f.comap prod.fst ⊔ g.comap prod.snd ``` and prove the three lemmas which motivated this construction ([Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Filter.20golf)): coproduct of cofinite filters is the cofinite filter, coproduct of cocompact filters is the cocompact filter, and ```lean (tendsto f a c) → (tendsto g b d) → (tendsto (prod.map f g) (a.coprod b) (c.coprod d)) ``` Co-authored by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored by: Patrick Massot <patrickmassot@free.fr>