From ebeeee7f11bb0ca0b4e7a131b6647fe43fb568cc Mon Sep 17 00:00:00 2001
From: Patrick Massot <patrickmassot@free.fr>
Date: Wed, 29 Jul 2020 20:38:16 +0000
Subject: [PATCH] feat(filters): a couple more lemmas (#3625)

Random lemmas gathered while thinking about https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/nhds_left.20and.20nhds_right
---
 src/data/set/lattice.lean   | 15 +++++++++++++++
 src/order/filter/bases.lean | 33 +++++++++++++++++++++++++++++++++
 src/order/filter/basic.lean | 13 ++++++++++++-
 3 files changed, 60 insertions(+), 1 deletion(-)

diff --git a/src/data/set/lattice.lean b/src/data/set/lattice.lean
index db06f45864cdc..ebc68d4d84e9d 100644
--- a/src/data/set/lattice.lean
+++ b/src/data/set/lattice.lean
@@ -613,6 +613,21 @@ begin
   { rintro ⟨i, hx⟩, cases hf i ⟨x, hx⟩ with y hy, refine ⟨y, ⟨i, congr_arg subtype.val hy⟩⟩ }
 end
 
+lemma union_distrib_Inter_right {ι : Type*} (s : ι → set α) (t : set α) :
+  (⋂ i, s i) ∪ t = (⋂ i, s i ∪ t) :=
+begin
+  ext x,
+  rw [mem_union_eq, mem_Inter],
+  split ; finish
+end
+
+lemma union_distrib_Inter_left {ι : Type*} (s : ι → set α) (t : set α) :
+  t ∪ (⋂ i, s i) = (⋂ i, t ∪ s i) :=
+begin
+  rw [union_comm, union_distrib_Inter_right],
+  simp [union_comm]
+end
+
 section
 
 variables {p : Prop} {μ : p → set α}
diff --git a/src/order/filter/bases.lean b/src/order/filter/bases.lean
index dcd596c94dc6c..d4ec2a9fa2dd3 100644
--- a/src/order/filter/bases.lean
+++ b/src/order/filter/bases.lean
@@ -287,6 +287,17 @@ theorem has_basis.le_basis_iff (hl : l.has_basis p s) (hl' : l'.has_basis p' s')
   l ≤ l' ↔ ∀ i', p' i' → ∃ i (hi : p i), s i ⊆ s' i' :=
 by simp only [hl'.ge_iff, hl.mem_iff]
 
+lemma has_basis.ext (hl : l.has_basis p s) (hl' : l'.has_basis p' s')
+  (h : ∀ i, p i → ∃ i', p' i' ∧ s' i' ⊆ s i)
+  (h' : ∀ i', p' i' → ∃ i, p i ∧ s i ⊆ s' i') : l = l' :=
+begin
+  apply le_antisymm,
+  { rw hl.le_basis_iff hl',
+    simpa using h' },
+  { rw hl'.le_basis_iff hl,
+    simpa using h },
+end
+
 lemma has_basis.inf (hl : l.has_basis p s) (hl' : l'.has_basis p' s') :
   (l ⊓ l').has_basis (λ i : ι × ι', p i.1 ∧ p' i.2) (λ i, s i.1 ∩ s' i.2) :=
 ⟨begin
@@ -299,6 +310,23 @@ lemma has_basis.inf (hl : l.has_basis p s) (hl' : l'.has_basis p' s') :
     use [s i, i, hi, subset.refl _, s' i', i', hi', subset.refl _, H] }
 end⟩
 
+lemma has_basis.sup (hl : l.has_basis p s) (hl' : l'.has_basis p' s') :
+  (l ⊔ l').has_basis (λ i : ι × ι', p i.1 ∧ p' i.2) (λ i, s i.1 ∪ s' i.2) :=
+⟨begin
+  rintros t,
+  rw [mem_sup_sets, hl.mem_iff, hl'.mem_iff],
+  split,
+  { rintros ⟨⟨i, pi, hi⟩, ⟨i', pi', hi'⟩⟩,
+    use [(i, i'), pi, pi'],
+    finish },
+  { rintros ⟨⟨i, i'⟩, ⟨⟨pi, pi'⟩, h⟩⟩,
+    split,
+    { use [i, pi],
+      finish },
+    { use [i', pi'],
+      finish } }
+end⟩
+
 lemma has_basis.inf_principal (hl : l.has_basis p s) (s' : set α) :
   (l ⊓ 𝓟 s').has_basis p (λ i, s i ∩ s') :=
 ⟨λ t, by simp only [mem_inf_principal, hl.mem_iff, subset_def, mem_set_of_eq,
@@ -332,6 +360,11 @@ lemma has_basis_binfi_principal {s : β → set α} {S : set β} (h : directed_o
   exact λ _ _, principal_mono.2
 end⟩
 
+lemma has_basis_binfi_principal'
+  (h : ∀ i, p i → ∀ j, p j → ∃ k (h : p k), s k ⊆ s i ∧ s k ⊆ s j) (ne : ∃ i, p i) :
+  (⨅ i (h : p i), 𝓟 (s i)).has_basis p s :=
+filter.has_basis_binfi_principal h ne
+
 lemma has_basis.map (f : α → β) (hl : l.has_basis p s) :
   (l.map f).has_basis p (λ i, f '' (s i)) :=
 ⟨λ t, by simp only [mem_map, image_subset_iff, hl.mem_iff, preimage]⟩
diff --git a/src/order/filter/basic.lean b/src/order/filter/basic.lean
index dfb3df198c118..595c594a0494c 100644
--- a/src/order/filter/basic.lean
+++ b/src/order/filter/basic.lean
@@ -646,7 +646,7 @@ instance : bounded_distrib_lattice (filter α) :=
   ..filter.complete_lattice }
 
 /- the complementary version with ⨆i, f ⊓ g i does not hold! -/
-lemma infi_sup_eq {f : filter α} {g : ι → filter α} : (⨅ x, f ⊔ g x) = f ⊔ infi g :=
+lemma infi_sup_left {f : filter α} {g : ι → filter α} : (⨅ x, f ⊔ g x) = f ⊔ infi g :=
 begin
   refine le_antisymm _ (le_infi $ assume i, sup_le_sup_left (infi_le _ _) _),
   rintros t ⟨h₁, h₂⟩,
@@ -661,6 +661,17 @@ begin
     exact le_inf (infi_le _ _) ih }
 end
 
+lemma infi_sup_right {f : filter α} {g : ι → filter α} : (⨅ x, g x ⊔ f) = infi g ⊔ f :=
+by simp [sup_comm, ← infi_sup_left]
+
+lemma binfi_sup_right (p : ι → Prop) (f : ι → filter α) (g : filter α) :
+  (⨅ i (h : p i), (f i ⊔ g)) = (⨅ i (h : p i), f i) ⊔ g :=
+by rw [infi_subtype', infi_sup_right, infi_subtype']
+
+lemma binfi_sup_left (p : ι → Prop) (f : ι → filter α) (g : filter α) :
+  (⨅ i (h : p i), (g ⊔ f i)) = g ⊔ (⨅ i (h : p i), f i) :=
+by rw [infi_subtype', infi_sup_left, infi_subtype']
+
 lemma mem_infi_sets_finset {s : finset α} {f : α → filter β} :
   ∀t, t ∈ (⨅a∈s, f a) ↔ (∃p:α → set β, (∀a∈s, p a ∈ f a) ∧ (⋂a∈s, p a) ⊆ t) :=
 show ∀t, t ∈ (⨅a∈s, f a) ↔ (∃p:α → set β, (∀a∈s, p a ∈ f a) ∧ (⨅a∈s, p a) ≤ t),