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>

Author: hrmacbeth

src/order/filter/basic.lean

@@ -2405,6 +2405,86 @@ by simp only [tendsto_def, mem_prod_iff, prod_sub_preimage_iff, exists_prop, iff
 
 end prod
 
+/-! ### Coproducts of filters -/
+
+section coprod
+variables {s : set α} {t : set β} {f : filter α} {g : filter β}
+
+/-- Coproduct of filters. -/
+protected def coprod (f : filter α) (g : filter β) : filter (α × β) :=
+f.comap prod.fst ⊔ g.comap prod.snd
+
+lemma mem_coprod_iff {s : set (α×β)} {f : filter α} {g : filter β} :
+  s ∈ f.coprod g ↔ ((∃ t₁ ∈ f, prod.fst ⁻¹' t₁ ⊆ s) ∧ (∃ t₂ ∈ g, prod.snd ⁻¹' t₂ ⊆ s)) :=
+by simp [filter.coprod]
+
+@[mono] lemma coprod_mono {f₁ f₂ : filter α} {g₁ g₂ : filter β} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) :
+  f₁.coprod g₁ ≤ f₂.coprod g₂ :=
+sup_le_sup (comap_mono hf) (comap_mono hg)
+
+lemma principal_coprod_principal (s : set α) (t : set β) :
+  (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ.prod tᶜ)ᶜ :=
+begin
+  rw [filter.coprod, comap_principal, comap_principal, sup_principal],
+  congr,
+  ext x,
+  simp ; tauto,
+end
+
+-- this inequality can be strict; see `map_const_principal_coprod_map_id_principal` and 
+-- `map_prod_map_const_id_principal_coprod_principal` below.
+lemma map_prod_map_coprod_le {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x}
+  {f₁ : filter α₁} {f₂ : filter α₂} {m₁ : α₁ → β₁} {m₂ : α₂ → β₂} :
+  map (prod.map m₁ m₂) (f₁.coprod f₂) ≤ (map m₁ f₁).coprod (map m₂ f₂) :=
+begin
+  intros s,
+  simp only [mem_map, mem_coprod_iff],
+  rintros ⟨⟨u₁, hu₁, h₁⟩, ⟨u₂, hu₂, h₂⟩⟩,
+  refine ⟨⟨m₁ ⁻¹' u₁, hu₁, λ _ hx, h₁ _⟩, ⟨m₂ ⁻¹' u₂, hu₂, λ _ hx, h₂ _⟩⟩; convert hx
+end
+
+/-- Characterization of the coproduct of the `filter.map`s of two principal filters `𝓟 {a}` and
+`𝓟 {i}`, the first under the constant function `λ a, b` and the second under the identity function.
+Together with the next lemma, `map_prod_map_const_id_principal_coprod_principal`, this provides an
+example showing that the inequality in the lemma `map_prod_map_coprod_le` can be strict. -/
+lemma map_const_principal_coprod_map_id_principal {α β ι : Type*} (a : α) (b : β) (i : ι) :
+  (map (λ _ : α, b) (𝓟 {a})).coprod (map id (𝓟 {i}))
+  = 𝓟 (({b} : set β).prod (univ : set ι) ∪ (univ : set β).prod {i}) :=
+begin
+  rw [map_principal, map_principal, principal_coprod_principal],
+  congr,
+  ext ⟨b', i'⟩,
+  simp,
+  tauto,
+end
+
+/-- Characterization of the `filter.map` of the coproduct of two principal filters `𝓟 {a}` and
+`𝓟 {i}`, under the `prod.map` of two functions, respectively the constant function `λ a, b` and the
+identity function.  Together with the previous lemma,
+`map_const_principal_coprod_map_id_principal`, this provides an example showing that the inequality
+in the lemma `map_prod_map_coprod_le` can be strict. -/
+lemma map_prod_map_const_id_principal_coprod_principal {α β ι : Type*} (a : α) (b : β) (i : ι) :
+  map (prod.map (λ _ : α, b) id) ((𝓟 {a}).coprod (𝓟 {i}))
+  = 𝓟 (({b} : set β).prod (univ : set ι)) :=
+begin
+  rw [principal_coprod_principal, map_principal],
+  congr,
+  ext ⟨b', i'⟩,
+  split,
+  { rintros ⟨⟨a'', i''⟩, h₁, ⟨h₂, h₃⟩⟩,
+    simp },
+  { rintros ⟨h₁, h₂⟩,
+    use (a, i'),
+    simpa using h₁.symm }
+end
+
+lemma tendsto.prod_map_coprod {δ : Type*} {f : α → γ} {g : β → δ} {a : filter α} {b : filter β}
+  {c : filter γ} {d : filter δ} (hf : tendsto f a c) (hg : tendsto g b d) :
+  tendsto (prod.map f g) (a.coprod b) (c.coprod d) :=
+map_prod_map_coprod_le.trans (coprod_mono hf hg)
+
+end coprod
+
 end filter
 
 open_locale filter

src/order/filter/cofinite.lean

@@ -48,6 +48,24 @@ lemma frequently_cofinite_iff_infinite {p : α → Prop} :
 by simp only [filter.frequently, filter.eventually, mem_cofinite, compl_set_of, not_not,
   set.infinite]
 
+/-- The coproduct of the cofinite filters on two types is the cofinite filter on their product. -/
+lemma coprod_cofinite {β : Type*} :
+  (cofinite : filter α).coprod (cofinite : filter β) = cofinite :=
+begin
+  ext S,
+  simp only [mem_coprod_iff, exists_prop, mem_comap_sets, mem_cofinite],
+  split,
+  { rintro ⟨⟨A, hAf, hAS⟩, B, hBf, hBS⟩,
+    rw [← compl_subset_compl, ← preimage_compl] at hAS hBS,
+    exact (hAf.prod hBf).subset (subset_inter hAS hBS) },
+  { intro hS,
+    refine ⟨⟨(prod.fst '' Sᶜ)ᶜ, _, _⟩, ⟨(prod.snd '' Sᶜ)ᶜ, _, _⟩⟩,
+    { simpa using hS.image prod.fst },
+    { simpa [compl_subset_comm] using subset_preimage_image prod.fst Sᶜ },
+    { simpa using hS.image prod.snd },
+    { simpa [compl_subset_comm] using subset_preimage_image prod.snd Sᶜ } },
+end
+
 end filter
 
 open filter

src/topology/subset_properties.lean

@@ -654,6 +654,34 @@ instance [compact_space α] [compact_space β] : compact_space (α ⊕ β) :=
   exact (compact_range continuous_inl).union (compact_range continuous_inr)
 end⟩
 
+/-- The coproduct of the cocompact filters on two topological spaces is the cocompact filter on
+their product. -/
+lemma filter.coprod_cocompact {β : Type*} [topological_space β]:
+  (filter.cocompact α).coprod (filter.cocompact β) = filter.cocompact (α × β) :=
+begin
+  ext S,
+  simp only [mem_coprod_iff, exists_prop, mem_comap_sets, filter.mem_cocompact],
+  split,
+  { rintro ⟨⟨A, ⟨t, ht, hAt⟩, hAS⟩, B, ⟨t', ht', hBt'⟩, hBS⟩,
+    refine ⟨t.prod t', ht.prod ht', _⟩,
+    refine subset.trans _ (union_subset hAS hBS),
+    rw compl_subset_comm at ⊢ hAt hBt',
+    refine subset.trans _ (set.prod_mono hAt hBt'),
+    intros x,
+    simp only [compl_union, mem_inter_eq, mem_prod, mem_preimage, mem_compl_eq],
+    tauto },
+  { rintros ⟨t, ht, htS⟩,
+    refine ⟨⟨(prod.fst '' t)ᶜ, _, _⟩, ⟨(prod.snd '' t)ᶜ, _, _⟩⟩,
+    { exact ⟨prod.fst '' t, ht.image continuous_fst, subset.rfl⟩ },
+    { rw preimage_compl,
+      rw compl_subset_comm at ⊢ htS,
+      exact subset.trans htS (subset_preimage_image prod.fst _) },
+    { exact ⟨prod.snd '' t, ht.image continuous_snd, subset.rfl⟩ },
+    { rw preimage_compl,
+      rw compl_subset_comm at ⊢ htS,
+      exact subset.trans htS (subset_preimage_image prod.snd _) } }
+end
+
 section tychonoff
 variables {ι : Type*} {π : ι → Type*} [∀ i, topological_space (π i)]