feat(MeasureTheory): add CountablySeparated (#12433)

add a typeclass `CountablySeparated _` abbreviating `HasCountableSeparatingOn _ MeasurableSet univ`. This is a common assumption is measure theory and is already used often in the library. 

Additionally, mathlib was previously not consistent in choosing between the equivalent spellings `HasCountableSeparatingOn X MeasurableSet s` and `HasCountableSeparatingOn s MeasurableSet univ` for X a measurable space and `s : Set X`. (In the latter spelling, `s` is being coerced to the subtype of `X`.) Lemmas and instances are added to help unify the situation.  This is now spelled `CountablySeparated s`. 



Co-authored-by: Felix-Weilacher <112423742+Felix-Weilacher@users.noreply.github.com>

Mathlib/Dynamics/Ergodic/Function.lean

@@ -25,7 +25,7 @@ from `α` to a nonempty space with a countable family of measurable sets
 separating points of a set `s` such that `f x ∈ s` for a.e. `x`.
 If `g` that is a.e.-invariant under `f`, then `g` is a.e. constant. -/
 theorem QuasiErgodic.ae_eq_const_of_ae_eq_comp_of_ae_range₀ [Nonempty X] [MeasurableSpace X]
-    {s : Set X} [HasCountableSeparatingOn X MeasurableSet s] {f : α → α} {g : α → X}
+    {s : Set X} [MeasurableSpace.CountablySeparated s] {f : α → α} {g : α → X}
     (h : QuasiErgodic f μ) (hs : ∀ᵐ x ∂μ, g x ∈ s) (hgm : NullMeasurable g μ)
     (hg_eq : g ∘ f =ᵐ[μ] g) :
     ∃ c, g =ᵐ[μ] const α c := by
@@ -36,7 +36,7 @@ theorem QuasiErgodic.ae_eq_const_of_ae_eq_comp_of_ae_range₀ [Nonempty X] [Meas
 
 section CountableSeparatingOnUniv
 
-variable [Nonempty X] [MeasurableSpace X] [HasCountableSeparatingOn X MeasurableSet univ]
+variable [Nonempty X] [MeasurableSpace X] [MeasurableSpace.CountablySeparated X]
   {f : α → α} {g : α → X}
 
 /-- Let `f : α → α` be a (pre)ergodic map.

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -320,9 +320,10 @@ theorem IsOpen.measurableSet (h : IsOpen s) : MeasurableSet s :=
   OpensMeasurableSpace.borel_le _ <| GenerateMeasurable.basic _ h
 #align is_open.measurable_set IsOpen.measurableSet
 
-instance (priority := 500) {s : Set α} [HasCountableSeparatingOn α IsOpen s] :
-    HasCountableSeparatingOn α MeasurableSet s :=
-  .mono (fun _ ↦ IsOpen.measurableSet) Subset.rfl
+instance (priority := 1000) {s : Set α} [h : HasCountableSeparatingOn α IsOpen s] :
+    CountablySeparated s := by
+    rw [CountablySeparated.subtype_iff]
+    exact .mono (fun _ ↦ IsOpen.measurableSet) Subset.rfl
 
 @[measurability]
 theorem measurableSet_interior : MeasurableSet (interior s) :=
@@ -1917,10 +1918,10 @@ theorem exists_borelSpace_of_countablyGenerated_of_separatesPoints (α : Type*)
 /-- If a measurable space on `α` is countably generated and separates points, there is some
 second countable t4 topology on `α` (i.e. a separable metrizable one) for which every
 open set is measurable. -/
-theorem exists_opensMeasurableSpace_of_hasCountableSeparatingOn (α : Type*)
-    [m : MeasurableSpace α] [HasCountableSeparatingOn α MeasurableSet univ] :
+theorem exists_opensMeasurableSpace_of_countablySeparated (α : Type*)
+    [m : MeasurableSpace α] [CountablySeparated α] :
     ∃ τ : TopologicalSpace α, SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α := by
-  rcases exists_countablyGenerated_le_of_hasCountableSeparatingOn α with ⟨m', _, _, m'le⟩
+  rcases exists_countablyGenerated_le_of_countablySeparated α with ⟨m', _, _, m'le⟩
   rcases exists_borelSpace_of_countablyGenerated_of_separatesPoints (m := m') with ⟨τ, _, _, τm'⟩
   exact ⟨τ, ‹_›, ‹_›, @OpensMeasurableSpace.mk _ _ m (τm'.measurable_eq.symm.le.trans m'le)⟩
 

Mathlib/MeasureTheory/Constructions/Polish.lean

@@ -535,6 +535,8 @@ end MeasureTheory
 
 namespace Measurable
 
+open MeasurableSpace
+
 variable {X Y Z β : Type*} [MeasurableSpace X] [StandardBorelSpace X]
   [TopologicalSpace Y] [T0Space Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] [MeasurableSpace β]
   [MeasurableSpace Z]
@@ -544,19 +546,19 @@ to a countably separated measurable space, then the preimage of a set `s`
 is measurable if and only if the set is measurable.
 One implication is the definition of measurability, the other one heavily relies on `X` being a
 standard Borel space. -/
-theorem measurableSet_preimage_iff_of_surjective [HasCountableSeparatingOn Z MeasurableSet univ]
+theorem measurableSet_preimage_iff_of_surjective [CountablySeparated Z]
     {f : X → Z} (hf : Measurable f) (hsurj : Surjective f) {s : Set Z} :
     MeasurableSet (f ⁻¹' s) ↔ MeasurableSet s := by
   refine ⟨fun h => ?_, fun h => hf h⟩
-  rcases exists_opensMeasurableSpace_of_hasCountableSeparatingOn Z with ⟨τ, _, _, _⟩
+  rcases exists_opensMeasurableSpace_of_countablySeparated Z with ⟨τ, _, _, _⟩
   apply AnalyticSet.measurableSet_of_compl
   · rw [← image_preimage_eq s hsurj]
     exact h.analyticSet_image hf
   · rw [← image_preimage_eq sᶜ hsurj]
     exact h.compl.analyticSet_image hf
 #align measurable.measurable_set_preimage_iff_of_surjective Measurable.measurableSet_preimage_iff_of_surjective
 
-theorem map_measurableSpace_eq  [HasCountableSeparatingOn Z MeasurableSet univ]
+theorem map_measurableSpace_eq  [CountablySeparated Z]
     {f : X → Z} (hf : Measurable f)
     (hsurj : Surjective f) : MeasurableSpace.map f ‹MeasurableSpace X› = ‹MeasurableSpace Z› :=
   MeasurableSpace.ext fun _ => hf.measurableSet_preimage_iff_of_surjective hsurj
@@ -577,8 +579,7 @@ theorem borelSpace_codomain [SecondCountableTopology Y] {f : X → Y} (hf : Meas
 /-- If `f : X → Z` is a Borel measurable map from a standard Borel space to a
 countably separated measurable space then the preimage of a set `s` is measurable
 if and only if the set is measurable in `Set.range f`. -/
-theorem measurableSet_preimage_iff_preimage_val {f : X → Z}
-    [HasCountableSeparatingOn (range f) MeasurableSet univ]
+theorem measurableSet_preimage_iff_preimage_val {f : X → Z} [CountablySeparated (range f)]
     (hf : Measurable f) {s : Set Z} :
     MeasurableSet (f ⁻¹' s) ↔ MeasurableSet ((↑) ⁻¹' s : Set (range f)) :=
   have hf' : Measurable (rangeFactorization f) := hf.subtype_mk
@@ -589,8 +590,7 @@ theorem measurableSet_preimage_iff_preimage_val {f : X → Z}
 countably separated measurable space and the range of `f` is measurable,
 then the preimage of a set `s` is measurable
 if and only if the intesection with `Set.range f` is measurable. -/
-theorem measurableSet_preimage_iff_inter_range {f : X → Z}
-    [HasCountableSeparatingOn (range f) MeasurableSet univ]
+theorem measurableSet_preimage_iff_inter_range {f : X → Z} [CountablySeparated (range f)]
     (hf : Measurable f) (hr : MeasurableSet (range f)) {s : Set Z} :
     MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f) := by
   rw [hf.measurableSet_preimage_iff_preimage_val, inter_comm,
@@ -602,7 +602,7 @@ to a countably separated measurable space,
 then for any measurable space `β` and `g : Z → β`, the composition `g ∘ f` is
 measurable if and only if the restriction of `g` to the range of `f` is measurable. -/
 theorem measurable_comp_iff_restrict {f : X → Z}
-    [HasCountableSeparatingOn (range f) MeasurableSet univ]
+    [CountablySeparated (range f)]
     (hf : Measurable f) {g : Z → β} : Measurable (g ∘ f) ↔ Measurable (restrict (range f) g) :=
   forall₂_congr fun s _ => measurableSet_preimage_iff_preimage_val hf (s := g ⁻¹' s)
 #align measurable.measurable_comp_iff_restrict Measurable.measurable_comp_iff_restrict
@@ -611,7 +611,7 @@ theorem measurable_comp_iff_restrict {f : X → Z}
 to a countably separated measurable space,
 then for any measurable space `α` and `g : Z → α`, the composition
 `g ∘ f` is measurable if and only if `g` is measurable. -/
-theorem measurable_comp_iff_of_surjective [HasCountableSeparatingOn Z MeasurableSet univ]
+theorem measurable_comp_iff_of_surjective [CountablySeparated Z]
     {f : X → Z} (hf : Measurable f) (hsurj : Surjective f)
     {g : Z → β} : Measurable (g ∘ f) ↔ Measurable g :=
   forall₂_congr fun s _ => measurableSet_preimage_iff_of_surjective hf hsurj (s := g ⁻¹' s)
@@ -853,13 +853,13 @@ theorem _root_.MeasurableSet.image_of_continuousOn_injOn [OpensMeasurableSpace 
 then its image under a measurable injective map taking values in a
 countably separate measurable space is also Borel-measurable. -/
 theorem _root_.MeasurableSet.image_of_measurable_injOn {f : γ → α}
-    [HasCountableSeparatingOn α MeasurableSet univ]
+    [MeasurableSpace.CountablySeparated α]
     [MeasurableSpace γ] [StandardBorelSpace γ]
     (hs : MeasurableSet s) (f_meas : Measurable f) (f_inj : InjOn f s) :
     MeasurableSet (f '' s) := by
   letI := upgradeStandardBorel γ
   let tγ : TopologicalSpace γ := inferInstance
-  rcases exists_opensMeasurableSpace_of_hasCountableSeparatingOn α with ⟨τ, _, _, _⟩
+  rcases exists_opensMeasurableSpace_of_countablySeparated α with ⟨τ, _, _, _⟩
   -- for a finer Polish topology, `f` is continuous. Therefore, one may apply the corresponding
   -- result for continuous maps.
   obtain ⟨t', t't, f_cont, t'_polish⟩ :
@@ -907,7 +907,7 @@ theorem _root_.ContinuousOn.measurableEmbedding [BorelSpace β]
 /-- An injective measurable function from a standard Borel space to a
 countably separated measurable space is a measurable embedding. -/
 theorem _root_.Measurable.measurableEmbedding {f : γ → α}
-    [HasCountableSeparatingOn α MeasurableSet univ]
+    [MeasurableSpace.CountablySeparated α]
     [MeasurableSpace γ] [StandardBorelSpace γ]
     (f_meas : Measurable f) (f_inj : Injective f) : MeasurableEmbedding f :=
   { injective := f_inj
@@ -1031,7 +1031,7 @@ noncomputable def measurableEquivNatBoolOfNotCountable (h : ¬Countable α) : α
     isClosed_univ.exists_nat_bool_injection_of_not_countable
       (by rwa [← countable_coe_iff, (Equiv.Set.univ _).countable_iff])
   obtain ⟨g, gmeas, ginj⟩ :=
-    MeasurableSpace.measurable_injection_nat_bool_of_hasCountableSeparatingOn α
+    MeasurableSpace.measurable_injection_nat_bool_of_countablySeparated α
   exact ⟨borelSchroederBernstein gmeas ginj fcts.measurable finj⟩
 #align polish_space.measurable_equiv_nat_bool_of_not_countable PolishSpace.measurableEquivNatBoolOfNotCountable
 

Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean

@@ -148,9 +148,9 @@ theorem exists_measurableSet_of_ne [MeasurableSpace α] [SeparatesPoints α] {x
 
 theorem separatesPoints_iff [MeasurableSpace α] : SeparatesPoints α ↔
     ∀ x y : α, (∀ s, MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y :=
-  ⟨fun h => fun _ _ hxy => h.separates _ _ fun _ hs xs => (hxy _ hs).mp xs,
-    fun h => ⟨fun _ _ hxy => h _ _ fun _ hs =>
-    ⟨fun xs => hxy _ hs xs, not_imp_not.mp fun xs => hxy _ hs.compl xs⟩⟩⟩
+  ⟨fun h ↦ fun _ _ hxy ↦ h.separates _ _ fun _ hs xs ↦ (hxy _ hs).mp xs,
+    fun h ↦ ⟨fun _ _ hxy ↦ h _ _ fun _ hs ↦
+    ⟨fun xs ↦ hxy _ hs xs, not_imp_not.mp fun xs ↦ hxy _ hs.compl xs⟩⟩⟩
 
 /-- If the measurable space generated by `S` separates points,
 then this is witnessed by sets in `S`. -/
@@ -160,45 +160,83 @@ theorem separating_of_generateFrom (S : Set (Set α))
   letI := generateFrom S
   intros x y hxy
   rw [← forall_generateFrom_mem_iff_mem_iff] at hxy
-  exact separatesPoints_def $ fun _ hs => (hxy _ hs).mp
+  exact separatesPoints_def $ fun _ hs ↦ (hxy _ hs).mp
 
 theorem SeparatesPoints.mono {m m' : MeasurableSpace α} [hsep : @SeparatesPoints _ m] (h : m ≤ m') :
     @SeparatesPoints _ m' := @SeparatesPoints.mk _ m' fun _ _ hxy ↦
     @SeparatesPoints.separates _ m hsep _ _ fun _ hs ↦ hxy _ (h _ hs)
 
+/-- We say that a measurable space is countably separated if there is a
+countable sequence of measurable sets separating points. -/
+class CountablySeparated (α : Type*) [MeasurableSpace α] : Prop where
+  countably_separated : HasCountableSeparatingOn α MeasurableSet univ
+
+instance countablySeparated_of_hasCountableSeparatingOn [MeasurableSpace α]
+    [h : HasCountableSeparatingOn α MeasurableSet univ] : CountablySeparated α := ⟨h⟩
+
+instance hasCountableSeparatingOn_of_countablySeparated [MeasurableSpace α]
+    [h : CountablySeparated α] : HasCountableSeparatingOn α MeasurableSet univ :=
+  h.countably_separated
+
+theorem countablySeparated_def [MeasurableSpace α] :
+    CountablySeparated α ↔ HasCountableSeparatingOn α MeasurableSet univ :=
+  ⟨fun h ↦ h.countably_separated, fun h ↦ ⟨h⟩⟩
+
+theorem CountablySeparated.mono {m m' : MeasurableSpace α} [hsep : @CountablySeparated _ m]
+    (h : m ≤ m') : @CountablySeparated _ m' := by
+  simp_rw [countablySeparated_def] at *
+  rcases hsep with ⟨S, Sct, Smeas, hS⟩
+  use S, Sct, (fun s hs ↦ h _ <| Smeas _ hs), hS
+
+theorem CountablySeparated.subtype_iff [MeasurableSpace α] {s : Set α} :
+    CountablySeparated s ↔ HasCountableSeparatingOn α MeasurableSet s := by
+  rw [countablySeparated_def]
+  exact HasCountableSeparatingOn.subtype_iff
+
 instance (priority := 100) Subtype.separatesPoints [MeasurableSpace α] [h : SeparatesPoints α]
     {s : Set α} : SeparatesPoints s :=
   ⟨fun _ _ hxy ↦ Subtype.val_injective $ h.1 _ _ fun _ ht ↦ hxy _ $ measurable_subtype_coe ht⟩
 
+instance (priority := 100) Subtype.countablySeparated [MeasurableSpace α]
+    [h : CountablySeparated α] {s : Set α} : CountablySeparated s := by
+  rw [CountablySeparated.subtype_iff]
+  exact h.countably_separated.mono (fun s ↦ id) $ subset_univ _
+
 instance (priority := 100) separatesPoints_of_measurableSingletonClass [MeasurableSpace α]
     [MeasurableSingletonClass α] : SeparatesPoints α := by
   refine ⟨fun x y h ↦ ?_⟩
   specialize h _ (MeasurableSet.singleton x)
   simp_rw [mem_singleton_iff, forall_true_left] at h
   exact h.symm
 
-instance (priority := 100) [MeasurableSpace α] {s : Set α}
-    [h : CountablyGenerated s] [SeparatesPoints s] :
-    HasCountableSeparatingOn α MeasurableSet s := by
-  suffices HasCountableSeparatingOn s MeasurableSet univ from this.of_subtype fun _ ↦ id
-  rcases h.1 with ⟨b, hbc, hb⟩
+instance hasCountableSeparatingOn_of_countablySeparated_subtype
+    [MeasurableSpace α] {s : Set α} [h : CountablySeparated s] :
+    HasCountableSeparatingOn _ MeasurableSet s := CountablySeparated.subtype_iff.mp h
+
+instance countablySeparated_subtype_of_hasCountableSeparatingOn
+    [MeasurableSpace α] {s : Set α} [h : HasCountableSeparatingOn _ MeasurableSet s] :
+    CountablySeparated s := CountablySeparated.subtype_iff.mpr h
+
+instance countablySeparated_of_separatesPoints [MeasurableSpace α]
+    [h : CountablyGenerated α] [SeparatesPoints α] : CountablySeparated α := by
+  rcases h with ⟨b, hbc, hb⟩
   refine ⟨⟨b, hbc, fun t ht ↦ hb.symm ▸ .basic t ht, ?_⟩⟩
-  rw [hb] at ‹SeparatesPoints s›
+  rw [hb] at ‹SeparatesPoints _›
   convert separating_of_generateFrom b
   simp
 
 variable (α)
 
 /-- If a measurable space admits a countable separating family of measurable sets,
 there is a countably generated coarser space which still separates points. -/
-theorem exists_countablyGenerated_le_of_hasCountableSeparatingOn [m : MeasurableSpace α]
-    [h : HasCountableSeparatingOn α MeasurableSet univ] :
+theorem exists_countablyGenerated_le_of_countablySeparated [m : MeasurableSpace α]
+    [h : CountablySeparated α] :
     ∃ m' : MeasurableSpace α, @CountablyGenerated _ m' ∧ @SeparatesPoints _ m' ∧ m' ≤ m := by
-  rcases h.1 with ⟨b, bct, hbm, hb⟩
+  rcases h with ⟨b, bct, hbm, hb⟩
   refine ⟨generateFrom b, ?_, ?_, generateFrom_le hbm⟩
   · use b
   rw [@separatesPoints_iff]
-  exact fun x y hxy => hb _ trivial _ trivial fun _ hs => hxy _ $ measurableSet_generateFrom hs
+  exact fun x y hxy ↦ hb _ trivial _ trivial fun _ hs ↦ hxy _ $ measurableSet_generateFrom hs
 
 open scoped Classical
 
@@ -248,34 +286,25 @@ theorem measurableEquiv_nat_bool_of_countablyGenerated [MeasurableSpace α]
 /-- If a measurable space admits a countable sequence of measurable sets separating points,
 it admits a measurable injection into the Cantor space `ℕ → Bool`
 (equipped with the product sigma algebra). -/
-theorem measurable_injection_nat_bool_of_hasCountableSeparatingOn [MeasurableSpace α]
-    [HasCountableSeparatingOn α MeasurableSet univ] :
-    ∃ f : α → ℕ → Bool, Measurable f ∧ Injective f := by
-  rcases exists_countablyGenerated_le_of_hasCountableSeparatingOn α with ⟨m', _, _, m'le⟩
+theorem measurable_injection_nat_bool_of_countablySeparated [MeasurableSpace α]
+    [CountablySeparated α] : ∃ f : α → ℕ → Bool, Measurable f ∧ Injective f := by
+  rcases exists_countablyGenerated_le_of_countablySeparated α with ⟨m', _, _, m'le⟩
   refine ⟨mapNatBool α, ?_, injective_mapNatBool _⟩
   exact (measurable_mapNatBool _).mono m'le le_rfl
 
 variable {α}
 
 --TODO: Make this an instance
-theorem measurableSingletonClass_of_hasCountableSeparatingOn
-    [MeasurableSpace α] [HasCountableSeparatingOn α MeasurableSet univ] :
+theorem measurableSingletonClass_of_countablySeparated
+    [MeasurableSpace α] [CountablySeparated α] :
     MeasurableSingletonClass α := by
-  rcases measurable_injection_nat_bool_of_hasCountableSeparatingOn α with ⟨f, fmeas, finj⟩
+  rcases measurable_injection_nat_bool_of_countablySeparated α with ⟨f, fmeas, finj⟩
   refine ⟨fun x ↦ ?_⟩
   rw [← finj.preimage_image {x}, image_singleton]
   exact fmeas $ MeasurableSet.singleton _
 
 end SeparatesPoints
 
-instance [MeasurableSpace α] {s : Set α} [h : CountablyGenerated s] [MeasurableSingletonClass s] :
-    HasCountableSeparatingOn α MeasurableSet s := by
-  suffices HasCountableSeparatingOn s MeasurableSet univ from this.of_subtype fun _ ↦ id
-  rcases h.1 with ⟨b, hbc, hb⟩
-  refine ⟨⟨b, hbc, fun t ht ↦ hb.symm ▸ .basic t ht, fun x _ y _ h ↦ ?_⟩⟩
-  rw [← forall_generateFrom_mem_iff_mem_iff, ← hb] at h
-  simpa using h {y}
-
 section MeasurableMemPartition
 
 lemma measurableSet_succ_memPartition (t : ℕ → Set α) (n : ℕ) {s : Set α}

Mathlib/Order/Filter/CountableSeparatingOn.lean

@@ -125,6 +125,19 @@ theorem HasCountableSeparatingOn.of_subtype {α : Type*} {p : Set α → Prop} {
   rw [← hV U hU]
   exact h _ (mem_image_of_mem _ hU)
 
+theorem HasCountableSeparatingOn.subtype_iff {α : Type*} {p : Set α → Prop} {t : Set α} :
+    HasCountableSeparatingOn t (fun u ↦ ∃ v, p v ∧ (↑) ⁻¹' v = u) univ ↔
+    HasCountableSeparatingOn α p t := by
+  constructor <;> intro h
+  · exact h.of_subtype $ fun s ↦ id
+  rcases h with ⟨S, Sct, Sp, hS⟩
+  use {Subtype.val ⁻¹' s | s ∈ S}, Sct.image _, ?_, ?_
+  · rintro u ⟨t, tS, rfl⟩
+    exact ⟨t, Sp _ tS, rfl⟩
+  rintro x - y - hxy
+  exact Subtype.val_injective $ hS _ (Subtype.coe_prop _) _ (Subtype.coe_prop _)
+    fun s hs ↦ hxy (Subtype.val ⁻¹' s) ⟨s, hs, rfl⟩
+
 namespace Filter
 
 variable {l : Filter α} [CountableInterFilter l] {f g : α → β}