From 561e9afe588e73cfb54b17c88ada0180f15719f0 Mon Sep 17 00:00:00 2001 From: JADekker <114015169+JADekker@users.noreply.github.com> Date: Thu, 4 Jan 2024 18:16:26 +0000 Subject: [PATCH] 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 --- .../MeasureTheory/Measure/MeasureSpace.lean | 12 ++----- .../Measure/MeasureSpaceDef.lean | 16 +++------- Mathlib/Order/Filter/Basic.lean | 23 ++++++++++++++ Mathlib/Order/Filter/Cofinite.lean | 7 ++--- Mathlib/Order/Filter/CountableInter.lean | 25 +++++++++++++++ Mathlib/Topology/Bornology/Basic.lean | 31 ++++++------------- Mathlib/Topology/Compactness/Compact.lean | 7 ++--- 7 files changed, 70 insertions(+), 51 deletions(-) diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean index f6fd90533d436..e87733ebb9ebf 100644 --- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean +++ b/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ᶜ < ∞ := diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean b/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean index a68d762f3c371..dc80e03812b97 100644 --- a/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean +++ b/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} : diff --git a/Mathlib/Order/Filter/Basic.lean b/Mathlib/Order/Filter/Basic.lean index b9381a98c8117..41393120a5061 100644 --- a/Mathlib/Order/Filter/Basic.lean +++ b/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 diff --git a/Mathlib/Order/Filter/Cofinite.lean b/Mathlib/Order/Filter/Cofinite.lean index 2275cbf66e058..c145c66ebb9d2 100644 --- a/Mathlib/Order/Filter/Cofinite.lean +++ b/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] diff --git a/Mathlib/Order/Filter/CountableInter.lean b/Mathlib/Order/Filter/CountableInter.lean index e560005b7ed43..96d2f8bd148d2 100644 --- a/Mathlib/Order/Filter/CountableInter.lean +++ b/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 diff --git a/Mathlib/Topology/Bornology/Basic.lean b/Mathlib/Topology/Bornology/Basic.lean index c7d11d2ea4a4e..b45b72bc1b2fb 100644 --- a/Mathlib/Topology/Bornology/Basic.lean +++ b/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 α] diff --git a/Mathlib/Topology/Compactness/Compact.lean b/Mathlib/Topology/Compactness/Compact.lean index e98a426fc3409..54dc5979f52e9 100644 --- a/Mathlib/Topology/Compactness/Compact.lean +++ b/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