mathlib

456e5af8 - feat(order/filter/*, topology/subset_properties): Filter Coprod (#7073)

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 Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>