refactor(order/filter): refactor filters infi and bases (leanprover-c…

…ommunity#2384)

This PR expands what Yury wrote about filter bases, and takes the opportunity to bring long overdue clarification to our treatment of infimums of filters (and also improve documentation and ordering in
filter.basic). I'm sorry it mixes reorganization and some new content, but this was hard to avoid (I do keep what motivated all this for a later PR).

The fundamental problem is that the infimum construction remained mysterious in filter.basic. All lemmas about it assume a directed family of filters. Yet there are many uses of infimums without this condition, notatably things like `⨅ i, principal (s i)` without condition on the indexed family of sets `s`.

Related to this, `filter.generate` stayed mysterious. It was used only as a technical device to lift the complete lattice structure from `set (set a)`. However it has a perfectly valid mathematical existence,
as explained by the lemma 
```lean
lemma sets_iff_generate {s : set (set α)} {f : filter α} : f ≤ filter.generate s ↔ s ⊆ f.sets
```
which justifies the docstring of `generate`: `generate g` is the smallest filter containing the sets `g`.

As an example of the mess this created, consider:
https://github.com/leanprover-community/mathlib/blob/e758263/src/topology/bases.lean#L25 
```lean
def has_countable_basis (f : filter α) : Prop :=
∃ s : set (set α), countable s ∧ f = ⨅ t ∈ s, principal t
```
As it stands, this definition is not clearly related to asking for the existence of a countable `s` such that `f = generate s`.

Here the main mathematical content this PR adds in this direction:

```lean
lemma mem_generate_iff (s : set $ set α) {U : set α} : U ∈ generate s ↔
∃ t ⊆ s, finite t ∧ ⋂₀ t ⊆ U

lemma infi_eq_generate (s : ι → filter α) : infi s = generate (⋃ i, (s
i).sets) 

lemma mem_infi_iff {ι} {s : ι → filter α} {U : set α} : (U ∈ ⨅ i, s i) ↔
  ∃ I : set ι, finite I ∧ ∃ V : {i | i ∈ I} → set α, (∀ i, V i ∈ s i) ∧
  (⋂ i, V i) ⊆ U
```

All the other changes in filter.basic are either:
* moving out stuff that should have been in other files (such as the lemmas that used to be at
the very top of this file)
* reordering lemmas so that we can have section headers and things are easier to find, 
* adding to the module docstring. This module docstring contains more mathematical explanation than our usual ones. I feel this is needed because many people think filters are exotic (whereas I'm more and more convinced we should teach filters).

The reordering stuff makes it clear we could split this file into a linear chain of files, like we did with topology, but this is open for discussion.

Next I added a lot to `filter.bases`. Here the issue is filter bases are used in two different ways. If you already have a filter, but you want to point out it suffices to use certain sets in it. Here you want to use Yury's `has_basis`. Or you can start with a (small) family of sets having nice properties, and build a filter out of it. Currently we don't have this in mathlib, but this is crucial for incoming PRs from the perfectoid project. For instance, in order to define the I-adic topology, you start with powers of I, make a filter and then make a topology. This also reduces the gap with Bourbaki which uses filter bases everywhere.

I turned `has_basis` into a single field structure. It makes it very slightly less convenient to prove (you need an extra pair of angle brackets) but much easier to extend when you want to record more
properties of the basis, like being countable or decreasing. Also I proved the fundamental property that `f.has_basis p s` implies that `s` (filtered by `p`) actually *is* a filter basis. This is of course easy but crucial to connect with real world maths.

At the end of this file, I moved the countable filter basis stuff that is currently in topology.bases (aiming for first countable topologies) except that I used the foundational work on filter.basic to clearly prove all different formulations. In particular:
```lean
lemma generate_eq_generate_inter (s : set (set α)) : generate s = generate (sInter '' { t | finite t ∧ t ⊆ s})
```
clarifies things because the right-hand colleciton is countable if `s` is, and has the nice directedness condition.

I also took the opportunity to simplify a proof in topology.sequences, showcasing the power of the newly introduced
```lean
lemma has_antimono_basis.tendsto [semilattice_sup ι] [nonempty ι] {l :
filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_antimono_basis p s)
{φ : ι → α} (h : ∀ i : ι, φ i ∈ s i) : tendsto φ at_top l
```
(I will add more to that sequences file in the next PR).

docs/theories/topology.md

@@ -1,7 +1,7 @@
 # Maths in lean : Topological Spaces.
 
 The `topological_space` typeclass is defined in mathlib,
-in `topology/basic.lean`. There are over 4500
+in `topology/basic.lean`. There are about 18000
 lines of code in `topology` at the time of writing,
 covering the basics of topological spaces, continuous functions,
 topological groups and rings, and infinite sums. These docs

src/data/set/finite.lean

@@ -368,6 +368,24 @@ begin
   exact ⟨x, ⟨hx, hf _⟩⟩,
 end
 
+lemma eq_finite_Union_of_finite_subset_Union  {ι} {s : ι → set α} {t : set α} (tfin : finite t) (h : t ⊆ ⋃ i, s i) :
+  ∃ I : set ι, (finite I) ∧ ∃ σ : {i | i ∈ I} → set α,
+     (∀ i, finite (σ i)) ∧ (∀ i, σ i ⊆ s i) ∧ t = ⋃ i, σ i :=
+let ⟨I, Ifin, hI⟩ := finite_subset_Union tfin h in
+⟨I, Ifin, λ x, s x ∩ t,
+    λ i, finite_subset tfin (inter_subset_right _ _),
+    λ i, inter_subset_left _ _,
+    begin
+      ext x,
+      rw mem_Union,
+      split,
+      { intro x_in,
+        rcases mem_Union.mp (hI x_in) with ⟨i, _, ⟨hi, rfl⟩, H⟩,
+        use [i, hi, H, x_in] },
+      { rintros ⟨i, hi, H⟩,
+        exact H }
+    end⟩
+
 lemma finite_range_ite {p : α → Prop} [decidable_pred p] {f g : α → β} (hf : finite (range f))
   (hg : finite (range g)) : finite (range (λ x, if p x then f x else g x)) :=
 finite_subset (finite_union hf hg) range_ite_subset

src/data/set/lattice.lean

@@ -197,6 +197,14 @@ theorem diff_Inter (s : set β) (t : ι → set β) :
   s \ (⋂ i, t i) = ⋃ i, s \ t i :=
 by rw [diff_eq, compl_Inter, inter_Union]; refl
 
+lemma directed_on_Union {r} {ι : Sort v} {f : ι → set α} (hd : directed (⊆) f)
+  (h : ∀x, directed_on r (f x)) : directed_on r (⋃x, f x) :=
+by simp only [directed_on, exists_prop, mem_Union, exists_imp_distrib]; exact
+assume a₁ b₁ fb₁ a₂ b₂ fb₂,
+let ⟨z, zb₁, zb₂⟩ := hd b₁ b₂,
+    ⟨x, xf, xa₁, xa₂⟩ := h z a₁ (zb₁ fb₁) a₂ (zb₂ fb₂) in
+⟨x, ⟨z, xf⟩, xa₁, xa₂⟩
+
 /- bounded unions and intersections -/
 
 theorem mem_bUnion_iff {s : set α} {t : α → set β} {y : β} :
@@ -385,6 +393,13 @@ theorem sUnion_union (S T : set (set α)) : ⋃₀ (S ∪ T) = ⋃₀ S ∪ ⋃
 
 theorem sInter_union (S T : set (set α)) : ⋂₀ (S ∪ T) = ⋂₀ S ∩ ⋂₀ T := Inf_union
 
+theorem sInter_Union (s : ι → set (set α)) : ⋂₀ (⋃ i, s i) = ⋂ i, ⋂₀ s i :=
+begin
+  ext x,
+  simp only [mem_Union, mem_Inter, mem_sInter, exists_imp_distrib],
+  split ; tauto
+end
+
 @[simp] theorem sUnion_insert (s : set α) (T : set (set α)) : ⋃₀ (insert s T) = s ∪ ⋃₀ T := Sup_insert
 
 @[simp] theorem sInter_insert (s : set α) (T : set (set α)) : ⋂₀ (insert s T) = s ∩ ⋂₀ T := Inf_insert

src/measure_theory/bochner_integration.lean

@@ -1026,7 +1026,7 @@ variables [normed_group β] [second_countable_topology β] [normed_space ℝ β]
   [measurable_space β] [borel_space β]
           [normed_group γ] [second_countable_topology γ] [normed_space ℝ γ] [complete_space γ]
   [measurable_space γ] [borel_space γ]
-  
+
 /-- The Bochner integral -/
 def integral (f : α → β) : β :=
 if hf : measurable f ∧ integrable f
@@ -1151,7 +1151,7 @@ end
 /-- Lebesgue dominated convergence theorem for filters with a countable basis -/
 lemma tendsto_integral_filter_of_dominated_convergence {ι} {l : filter ι}
   {F : ι → α → β} {f : α → β} (bound : α → ℝ)
-  (hl_cb : l.has_countable_basis)
+  (hl_cb : l.is_countably_generated)
   (hF_meas : ∀ᶠ n in l, measurable (F n))
   (f_measurable : measurable f)
   (h_bound : ∀ᶠ n in l, ∀ₘ a, ∥F n a∥ ≤ bound a)

src/measure_theory/integration.lean

@@ -1177,7 +1177,7 @@ end
 /-- Dominated convergence theorem for filters with a countable basis -/
 lemma tendsto_lintegral_filter_of_dominated_convergence {ι} {l : filter ι}
   {F : ι → α → ennreal} {f : α → ennreal} (bound : α → ennreal)
-  (hl_cb : l.has_countable_basis)
+  (hl_cb : l.is_countably_generated)
   (hF_meas : ∀ᶠ n in l, measurable (F n))
   (h_bound : ∀ᶠ n in l, ∀ₘ a, F n a ≤ bound a)
   (h_fin : lintegral bound < ⊤)

src/measure_theory/set_integral.lean

@@ -306,7 +306,7 @@ begin
 end
 
 -- TODO : prove this for an encodable type
--- by proving an encodable version of `filter.has_countable_basis_at_top_finset_nat`
+-- by proving an encodable version of `filter.is_countably_generated_at_top_finset_nat `
 lemma integral_on_Union (s : ℕ → set α) (f : α → β) (hm : ∀i, is_measurable (s i))
   (hd : ∀ i j, i ≠ j → s i ∩ s j = ∅) (hfm : measurable_on (Union s) f) (hfi : integrable_on (Union s) f) :
   (∫ a in (Union s), f a) = ∑i, ∫ a in s i, f a :=
@@ -322,7 +322,7 @@ begin
   rw this,
   refine tendsto_integral_filter_of_dominated_convergence _ _ _ _ _ _ _,
   { exact indicator (Union s) (λ a, ∥f a∥) },
-  { exact has_countable_basis_at_top_finset_nat },
+  { exact is_countably_generated_at_top_finset_nat },
   { refine univ_mem_sets' (λ n, _),
     simp only [mem_set_of_eq],
     refine hfm.subset (is_measurable.Union (λ i, is_measurable.Union_Prop (λh, hm _)))

src/order/complete_lattice.lean

@@ -667,6 +667,10 @@ lemma infi_subtype' {p : ι → Prop} {f : ∀ i, p i → α} :
   (⨅ i (h : p i), f i h) = (⨅ x : subtype p, f x.val x.property) :=
 (@infi_subtype _ _ _ p (λ x, f x.val x.property)).symm
 
+lemma infi_subtype'' {ι} (s : set ι) (f : ι → α) :
+(⨅ i : s, f i) = ⨅ (t : ι) (H : t ∈ s), f t :=
+infi_subtype
+
 theorem supr_subtype {p : ι → Prop} {f : subtype p → α} : (⨆ x, f x) = (⨆ i (h:p i), f ⟨i, h⟩) :=
 le_antisymm
   (supr_le $ assume ⟨i, h⟩, le_supr_of_le i $ le_supr (λh:p i, f ⟨i, h⟩) _)