Commit 2021-04-14 23:14 456e5af8

feat(order/filter/*, topology/subset_properties): Filter Coprod (#7073) Define the "coproduct" of many filters (not just two) as protected def Coprod (f : Π d, filter (κ d)) : filter (Π d, κ d) := ⨆ d : δ, (f d).comap (λ k, k d) and prove the three lemmas which motivated this construction: (finite!) coproduct of cofinite filters is the cofinite filter, coproduct of cocompact filters is the cocompact filter, and monotonicity; see also #6372 Co-authored by: Heather Macbeth @hrmacbeth