Commit 2021-03-06 17:06 16ef2913

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

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): coproduct of cofinite filters is the cofinite filter, coproduct of cocompact filters is the cocompact filter, and

(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