feat(Order/Filter) : add 2 constructors (#9200)

Add two constructors to create filters from a property on sets:
- `Filter.comk` if the property is stable under finite unions and set shrinking.
- `Filter.ofCountableUnion` if the property is stable under countable unions and set shrinking

`Filter.comk` is the key ingredient in `IsCompact.induction_on` but may be convenient to have as individual building block.
A `Filter` generated by `Filter.ofCountableUnion` is a `CountableInterFilter`, which is given by the instance `Filter.countableInter_ofCountableUnion`. 

### Other changes

- Use `Filter.comk` for `Filter.cofinite`, `Bornology.ofBounded` and `MeasureTheory.Measure.cofinite`.
- Use `Filter.ofCountableUnion` for `MeasureTheory.Measure.ae`.
- Use `{_ : Bornology _}` instead of `[Bornology _]` in some lemmas so that `rw/simp` work with non-instance bornologies.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: JADekker

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

@@ -1878,15 +1878,9 @@ end Pointwise
 /-! ### The `cofinite` filter -/
 
 /-- The filter of sets `s` such that `sᶜ` has finite measure. -/
-def cofinite {m0 : MeasurableSpace α} (μ : Measure α) : Filter α where
-  sets := { s | μ sᶜ < ∞ }
-  univ_sets := by simp
-  inter_sets {s t} hs ht := by
-    simp only [compl_inter, mem_setOf_eq]
-    calc
-      μ (sᶜ ∪ tᶜ) ≤ μ sᶜ + μ tᶜ := measure_union_le _ _
-      _ < ∞ := ENNReal.add_lt_top.2 ⟨hs, ht⟩
-  sets_of_superset {s t} hs hst := lt_of_le_of_lt (measure_mono <| compl_subset_compl.2 hst) hs
+def cofinite {m0 : MeasurableSpace α} (μ : Measure α) : Filter α :=
+  comk (μ · < ∞) (by simp) (fun t ht s hs ↦ (measure_mono hs).trans_lt ht) fun s hs t ht ↦
+    (measure_union_le s t).trans_lt <| ENNReal.add_lt_top.2 ⟨hs, ht⟩
 #align measure_theory.measure.cofinite MeasureTheory.Measure.cofinite
 
 theorem mem_cofinite : s ∈ μ.cofinite ↔ μ sᶜ < ∞ :=

Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

@@ -363,13 +363,10 @@ theorem measure_inter_null_of_null_left {S : Set α} (T : Set α) (h : μ S = 0)
 
 /-! ### The almost everywhere filter -/
 
-
 /-- The “almost everywhere” filter of co-null sets. -/
-def Measure.ae {α} {m : MeasurableSpace α} (μ : Measure α) : Filter α where
-  sets := { s | μ sᶜ = 0 }
-  univ_sets := by simp
-  inter_sets hs ht := by simp only [compl_inter, mem_setOf_eq]; exact measure_union_null hs ht
-  sets_of_superset hs hst := measure_mono_null (Set.compl_subset_compl.2 hst) hs
+def Measure.ae {α : Type*} {_m : MeasurableSpace α} (μ : Measure α) : Filter α :=
+  ofCountableUnion (μ · = 0) (fun _S hSc ↦ (measure_sUnion_null_iff hSc).2) fun _t ht _s hs ↦
+    measure_mono_null hs ht
 #align measure_theory.measure.ae MeasureTheory.Measure.ae
 
 -- mathport name: «expr∀ᵐ ∂ , »
@@ -415,11 +412,8 @@ theorem ae_of_all {p : α → Prop} (μ : Measure α) : (∀ a, p a) → ∀ᵐ
 -- ⟨fun s hs => let ⟨t, hst, htm, htμ⟩ := exists_measurable_superset_of_null hs;
 --   ⟨tᶜ, compl_mem_ae_iff.2 htμ, htm.compl, compl_subset_comm.1 hst⟩⟩
 
-instance instCountableInterFilter : CountableInterFilter μ.ae :=
-  ⟨by
-    intro S hSc hS
-    rw [mem_ae_iff, compl_sInter, sUnion_image]
-    exact (measure_biUnion_null_iff hSc).2 hS⟩
+instance instCountableInterFilter : CountableInterFilter μ.ae := by
+  unfold Measure.ae; infer_instance
 #align measure_theory.measure.ae.countable_Inter_filter MeasureTheory.instCountableInterFilter
 
 theorem ae_all_iff {ι : Sort*} [Countable ι] {p : α → ι → Prop} :

Mathlib/Order/Filter/Basic.lean

@@ -3325,3 +3325,26 @@ theorem Set.MapsTo.tendsto {α β} {s : Set α} {t : Set β} {f : α → β} (h
     Filter.Tendsto f (𝓟 s) (𝓟 t) :=
   Filter.tendsto_principal_principal.2 h
 #align set.maps_to.tendsto Set.MapsTo.tendsto
+
+namespace Filter
+
+/-- Construct a filter from a property that is stable under finite unions.
+A set `s` belongs to `Filter.comk p _ _ _` iff its complement satisfies the predicate `p`.
+This constructor is useful to define filters like `Filter.cofinite`. -/
+def comk (p : Set α → Prop) (he : p ∅) (hmono : ∀ t, p t → ∀ s ⊆ t, p s)
+    (hunion : ∀ s, p s → ∀ t, p t → p (s ∪ t)) : Filter α where
+  sets := {t | p tᶜ}
+  univ_sets := by simpa
+  sets_of_superset := fun ht₁ ht => hmono _ ht₁ _ (compl_subset_compl.2 ht)
+  inter_sets := fun ht₁ ht₂ => by simp [compl_inter, hunion _ ht₁ _ ht₂]
+
+@[simp]
+lemma mem_comk {p : Set α → Prop} {he hmono hunion s} :
+    s ∈ comk p he hmono hunion ↔ p sᶜ :=
+  .rfl
+
+lemma compl_mem_comk {p : Set α → Prop} {he hmono hunion s} :
+    sᶜ ∈ comk p he hmono hunion ↔ p s := by
+  simp
+
+end Filter

Mathlib/Order/Filter/Cofinite.lean

@@ -29,11 +29,8 @@ variable {ι α β : Type*} {l : Filter α}
 namespace Filter
 
 /-- The cofinite filter is the filter of subsets whose complements are finite. -/
-def cofinite : Filter α where
-  sets := { s | sᶜ.Finite }
-  univ_sets := by simp only [compl_univ, finite_empty, mem_setOf_eq]
-  sets_of_superset hs st := hs.subset <| compl_subset_compl.2 st
-  inter_sets hs ht := by simpa only [compl_inter, mem_setOf_eq] using hs.union ht
+def cofinite : Filter α :=
+  comk Set.Finite finite_empty (fun _t ht _s hsub ↦ ht.subset hsub) fun _ h _ ↦ h.union
 #align filter.cofinite Filter.cofinite
 
 @[simp]

Mathlib/Order/Filter/CountableInter.lean

@@ -150,6 +150,31 @@ theorem Filter.mem_ofCountableInter {l : Set (Set α)}
   Iff.rfl
 #align filter.mem_of_countable_Inter Filter.mem_ofCountableInter
 
+/-- Construct a filter with countable intersection property.
+Similarly to `Filter.comk`, a set belongs to this filter if its complement satisfies the property.
+Similarly to `Filter.ofCountableInter`,
+this constructor deduces some properties from the countable intersection property
+which becomes the countable union property because we take complements of all sets.
+
+Another small difference from `Filter.ofCountableInter`
+is that this definition takes `p : Set α → Prop` instead of `Set (Set α)`. -/
+def Filter.ofCountableUnion (p : Set α → Prop)
+    (hUnion : ∀ S : Set (Set α), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S))
+    (hmono : ∀ t, p t → ∀ s ⊆ t, p s) : Filter α := by
+  refine .ofCountableInter {s | p sᶜ} (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ ?_
+  · rw [mem_setOf_eq, compl_sInter]
+    exact hUnion _ (hSc.image _) (ball_image_iff.2 hSp)
+  · exact hmono _ ht _ (compl_subset_compl.2 hsub)
+
+instance Filter.countableInter_ofCountableUnion (p : Set α → Prop) (h₁ h₂) :
+    CountableInterFilter (Filter.ofCountableUnion p h₁ h₂) :=
+  countableInter_ofCountableInter ..
+
+@[simp]
+theorem Filter.mem_ofCountableUnion {p : Set α → Prop} {hunion hmono s} :
+    s ∈ ofCountableUnion p hunion hmono ↔ p sᶜ :=
+  Iff.rfl
+
 instance countableInterFilter_principal (s : Set α) : CountableInterFilter (𝓟 s) :=
   ⟨fun _ _ hS => subset_sInter hS⟩
 #align countable_Inter_filter_principal countableInterFilter_principal

Mathlib/Topology/Bornology/Basic.lean

@@ -94,23 +94,14 @@ def Bornology.ofBounded {α : Type*} (B : Set (Set α))
     (subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B)
     (union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B)
     (singleton_mem : ∀ x, {x} ∈ B) : Bornology α where
-  cobounded' :=
-    { sets := { s : Set α | sᶜ ∈ B }
-      univ_sets := by rwa [← compl_univ] at empty_mem
-      sets_of_superset := fun hx hy => subset_mem _ hx _ (compl_subset_compl.mpr hy)
-      inter_sets := fun hx hy => by simpa [compl_inter] using union_mem _ hx _ hy }
-  le_cofinite' := by
-    rw [le_cofinite_iff_compl_singleton_mem]
-    intro x
-    change {x}ᶜᶜ ∈ B
-    rw [compl_compl]
-    exact singleton_mem x
+  cobounded' := comk (· ∈ B) empty_mem subset_mem union_mem
+  le_cofinite' := by simpa [le_cofinite_iff_compl_singleton_mem]
 #align bornology.of_bounded Bornology.ofBounded
-#align bornology.of_bounded_cobounded_sets Bornology.ofBounded_cobounded_sets
+#align bornology.of_bounded_cobounded_sets Bornology.ofBounded_cobounded
 
 /-- A constructor for bornologies by specifying the bounded sets,
 and showing that they satisfy the appropriate conditions. -/
-@[simps!]
+@[simps! cobounded]
 def Bornology.ofBounded' {α : Type*} (B : Set (Set α))
     (empty_mem : ∅ ∈ B)
     (subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B)
@@ -122,24 +113,24 @@ def Bornology.ofBounded' {α : Type*} (B : Set (Set α))
     rcases sUnion_univ x with ⟨s, hs, hxs⟩
     exact subset_mem s hs {x} (singleton_subset_iff.mpr hxs)
 #align bornology.of_bounded' Bornology.ofBounded'
-#align bornology.of_bounded'_cobounded_sets Bornology.ofBounded'_cobounded_sets
+#align bornology.of_bounded'_cobounded_sets Bornology.ofBounded'_cobounded
 namespace Bornology
 
 section
 
-variable [Bornology α] {s t : Set α} {x : α}
-
 /-- `IsCobounded` is the predicate that `s` is in the filter of cobounded sets in the ambient
 bornology on `α` -/
-def IsCobounded (s : Set α) : Prop :=
+def IsCobounded [Bornology α] (s : Set α) : Prop :=
   s ∈ cobounded α
 #align bornology.is_cobounded Bornology.IsCobounded
 
 /-- `IsBounded` is the predicate that `s` is bounded relative to the ambient bornology on `α`. -/
-def IsBounded (s : Set α) : Prop :=
+def IsBounded [Bornology α] (s : Set α) : Prop :=
   IsCobounded sᶜ
 #align bornology.is_bounded Bornology.IsBounded
 
+variable {_ : Bornology α} {s t : Set α} {x : α}
+
 theorem isCobounded_def {s : Set α} : IsCobounded s ↔ s ∈ cobounded α :=
   Iff.rfl
 #align bornology.is_cobounded_def Bornology.isCobounded_def
@@ -263,9 +254,7 @@ theorem isCobounded_ofBounded_iff (B : Set (Set α)) {empty_mem subset_mem union
 
 theorem isBounded_ofBounded_iff (B : Set (Set α)) {empty_mem subset_mem union_mem sUnion_univ} :
     @IsBounded _ (ofBounded B empty_mem subset_mem union_mem sUnion_univ) s ↔ s ∈ B := by
-  rw [@isBounded_def _ (ofBounded B empty_mem subset_mem union_mem sUnion_univ), ← Filter.mem_sets,
-   ofBounded_cobounded_sets, Set.mem_setOf_eq, compl_compl]
--- porting note: again had to use `@isBounded_def _` and feed Lean the instance
+  rw [isBounded_def, ofBounded_cobounded, compl_mem_comk]
 #align bornology.is_bounded_of_bounded_iff Bornology.isBounded_ofBounded_iff
 
 variable [Bornology α]

Mathlib/Topology/Compactness/Compact.lean

@@ -3,6 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
 -/
+import Mathlib.Order.Filter.Basic
 import Mathlib.Topology.Bases
 import Mathlib.Data.Set.Accumulate
 import Mathlib.Topology.Bornology.Basic
@@ -69,11 +70,7 @@ theorem IsCompact.compl_mem_sets_of_nhdsWithin (hs : IsCompact s) {f : Filter X}
 theorem IsCompact.induction_on (hs : IsCompact s) {p : Set X → Prop} (he : p ∅)
     (hmono : ∀ ⦃s t⦄, s ⊆ t → p t → p s) (hunion : ∀ ⦃s t⦄, p s → p t → p (s ∪ t))
     (hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t) : p s := by
-  let f : Filter X :=
-    { sets := { t | p tᶜ }
-      univ_sets := by simpa
-      sets_of_superset := fun ht₁ ht => hmono (compl_subset_compl.2 ht) ht₁
-      inter_sets := fun ht₁ ht₂ => by simp [compl_inter, hunion ht₁ ht₂] }
+  let f : Filter X := comk p he (fun _t ht _s hsub ↦ hmono hsub ht) (fun _s hs _t ht ↦ hunion hs ht)
   have : sᶜ ∈ f := hs.compl_mem_sets_of_nhdsWithin (by simpa using hnhds)
   rwa [← compl_compl s]
 #align is_compact.induction_on IsCompact.induction_on