feat(order/filter/countable_Inter): review (#11673)

- drop `_sets` in more names;
- add `filter.of_countable_Inter` and instances for
  `filter.map`/`filter.comap`;
- add docs.

src/order/filter/countable_Inter.lean

@@ -14,42 +14,50 @@ property: for any countable collection of sets `s ∈ l` their intersection belo
 
 Two main examples are the `residual` filter defined in `topology.metric_space.baire` and
 the `measure.ae` filter defined in `measure_theory.measure_space`.
+
+We reformulate the definition in terms of indexed intersection and in terms of `filter.eventually`
+and provide instances for some basic constructions (`⊥`, `⊤`, `filter.principal`, `filter.map`,
+`filter.comap`, `has_inf.inf`). We also provide a custom constructor `filter.of_countable_Inter`
+that deduces two axioms of a `filter` from the countable intersection property.
+
+## Tags
+filter, countable
 -/
 
 open set filter
 open_locale filter
 
-variables {ι α : Type*}
+variables {ι α β : Type*}
 
 /-- A filter `l` has the countable intersection property if for any countable collection
 of sets `s ∈ l` their intersection belongs to `l` as well. -/
 class countable_Inter_filter (l : filter α) : Prop :=
-(countable_sInter_mem_sets' :
+(countable_sInter_mem' :
   ∀ {S : set (set α)} (hSc : countable S) (hS : ∀ s ∈ S, s ∈ l), ⋂₀ S ∈ l)
 
 variables {l : filter α} [countable_Inter_filter l]
 
-lemma countable_sInter_mem_sets {S : set (set α)} (hSc : countable S) :
+lemma countable_sInter_mem {S : set (set α)} (hSc : countable S) :
   ⋂₀ S ∈ l ↔ ∀ s ∈ S, s ∈ l :=
 ⟨λ hS s hs, mem_of_superset hS (sInter_subset_of_mem hs),
-  countable_Inter_filter.countable_sInter_mem_sets' hSc⟩
+  countable_Inter_filter.countable_sInter_mem' hSc⟩
 
-lemma countable_Inter_mem_sets [encodable ι] {s : ι → set α} :
+lemma countable_Inter_mem [encodable ι] {s : ι → set α} :
   (⋂ i, s i) ∈ l ↔ ∀ i, s i ∈ l :=
-sInter_range s ▸ (countable_sInter_mem_sets (countable_range _)).trans forall_range_iff
+sInter_range s ▸ (countable_sInter_mem (countable_range _)).trans forall_range_iff
 
 lemma countable_bInter_mem {S : set ι} (hS : countable S) {s : Π i ∈ S, set α} :
   (⋂ i ∈ S, s i ‹_›) ∈ l ↔  ∀ i ∈ S, s i ‹_› ∈ l :=
 begin
   rw [bInter_eq_Inter],
   haveI := hS.to_encodable,
-  exact countable_Inter_mem_sets.trans subtype.forall
+  exact countable_Inter_mem.trans subtype.forall
 end
 
 lemma eventually_countable_forall [encodable ι] {p : α → ι → Prop} :
   (∀ᶠ x in l, ∀ i, p x i) ↔ ∀ i, ∀ᶠ x in l, p x i :=
 by simpa only [filter.eventually, set_of_forall]
-  using @countable_Inter_mem_sets _ _ l _ _ (λ i, {x | p x i})
+  using @countable_Inter_mem _ _ l _ _ (λ i, {x | p x i})
 
 lemma eventually_countable_ball {S : set ι} (hS : countable S) {p : Π (x : α) (i ∈ S), Prop} :
   (∀ᶠ x in l, ∀ i ∈ S, p x i ‹_›) ↔ ∀ i ∈ S, ∀ᶠ x in l, p x i ‹_› :=
@@ -101,6 +109,29 @@ lemma eventually_eq.countable_bInter {S : set ι} (hS : countable S) {s t : Π i
 (eventually_le.countable_bInter hS (λ i hi, (h i hi).le)).antisymm
   (eventually_le.countable_bInter hS (λ i hi, (h i hi).symm.le))
 
+/-- Construct a filter with countable intersection property. This constructor deduces
+`filter.univ_sets` and `filter.inter_sets` from the countable intersection property. -/
+def filter.of_countable_Inter (l : set (set α))
+  (hp : ∀ S : set (set α), countable S → S ⊆ l → (⋂₀ S) ∈ l)
+  (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) :
+  filter α :=
+{ sets := l,
+  univ_sets := @sInter_empty α ▸ hp _ countable_empty (empty_subset _),
+  sets_of_superset := h_mono,
+  inter_sets := λ s t hs ht, sInter_pair s t ▸
+    hp _ ((countable_singleton _).insert _) (insert_subset.2 ⟨hs, singleton_subset_iff.2 ht⟩) }
+
+instance filter.countable_Inter_of_countable_Inter (l : set (set α))
+  (hp : ∀ S : set (set α), countable S → S ⊆ l → (⋂₀ S) ∈ l)
+  (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) :
+  countable_Inter_filter (filter.of_countable_Inter l hp h_mono) := ⟨hp⟩
+
+@[simp] lemma filter.mem_of_countable_Inter {l : set (set α)}
+  (hp : ∀ S : set (set α), countable S → S ⊆ l → (⋂₀ S) ∈ l)
+  (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) {s : set α} :
+  s ∈ filter.of_countable_Inter l hp h_mono ↔ s ∈ l :=
+iff.rfl
+
 instance countable_Inter_filter_principal (s : set α) : countable_Inter_filter (𝓟 s) :=
 ⟨λ S hSc hS, subset_sInter hS⟩
 
@@ -110,6 +141,24 @@ by { rw ← principal_empty, apply countable_Inter_filter_principal }
 instance countable_Inter_filter_top : countable_Inter_filter (⊤ : filter α) :=
 by { rw ← principal_univ, apply countable_Inter_filter_principal }
 
+instance (l : filter β) [countable_Inter_filter l] (f : α → β) :
+  countable_Inter_filter (comap f l) :=
+begin
+  refine ⟨λ S hSc hS, _⟩,
+  choose! t htl ht using hS,
+  have : (⋂ s ∈ S, t s) ∈ l, from (countable_bInter_mem hSc).2 htl,
+  refine ⟨_, this, _⟩,
+  simpa [preimage_Inter] using (Inter₂_mono ht)
+end
+
+instance (l : filter α) [countable_Inter_filter l] (f : α → β) :
+  countable_Inter_filter (map f l) :=
+begin
+  constructor, intros S hSc hS,
+  simp only [mem_map, sInter_eq_bInter, preimage_Inter₂] at hS ⊢,
+  exact (countable_bInter_mem hSc).2 hS
+end
+
 /-- Infimum of two `countable_Inter_filter`s is a `countable_Inter_filter`. This is useful, e.g.,
 to automatically get an instance for `residual α ⊓ 𝓟 s`. -/
 instance countable_Inter_filter_inf (l₁ l₂ : filter α) [countable_Inter_filter l₁]
@@ -130,6 +179,6 @@ instance countable_Inter_filter_sup (l₁ l₂ : filter α) [countable_Inter_fil
   [countable_Inter_filter l₂] :
   countable_Inter_filter (l₁ ⊔ l₂) :=
 begin
-  refine ⟨λ S hSc hS, ⟨_, _⟩⟩; refine (countable_sInter_mem_sets hSc).2 (λ s hs, _),
+  refine ⟨λ S hSc hS, ⟨_, _⟩⟩; refine (countable_sInter_mem hSc).2 (λ s hs, _),
   exacts [(hS s hs).1, (hS s hs).2]
 end