feat(Topology/Separation): define R₁ spaces, review API (#10085)

### Main API changes

- Define `R1Space`, a.k.a. preregular space.
- Drop `T2OrLocallyCompactRegularSpace`.
- Generalize all existing theorems
  about `T2OrLocallyCompactRegularSpace` to `R1Space`.
- Drop the `[T2OrLocallyCompactRegularSpace _]` assumption
  if the space is known to be regular for other reason
  (e.g., because it's a topological group).

### New theorems

- `Specializes.not_disjoint`:
  if `x ⤳ y`, then `𝓝 x` and `𝓝 y` aren't disjoint;
- `specializes_iff_not_disjoint`, `Specializes.inseparable`,
  `disjoint_nhds_nhds_iff_not_inseparable`,
  `r1Space_iff_inseparable_or_disjoint_nhds`: basic API about `R1Space`s;
- `Inducing.r1Space`, `R1Space.induced`, `R1Space.sInf`, `R1Space.iInf`,
  `R1Space.inf`, instances for `Subtype _`, `X × Y`, and `∀ i, X i`:
  basic instances for `R1Space`;
- `IsCompact.mem_closure_iff_exists_inseparable`,
  `IsCompact.closure_eq_biUnion_inseparable`:
  characterizations of the closure of a compact set in a preregular space;
- `Inseparable.mem_measurableSet_iff`: topologically inseparable points
  can't be separated by a Borel measurable set;
- `IsCompact.closure_subset_measurableSet`, `IsCompact.measure_closure`:
  in a preregular space, a measurable superset of a compact set
  includes its closure as well;
  as a corollary, `closure K` has the same measure as `K`.
- `exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds`:
  an auxiliary lemma extracted from a `LocallyCompactPair` instance;
- `IsCompact.isCompact_isClosed_basis_nhds`:
  if `x` admits a compact neighborhood,
  then it admits a basis of compact closed neighborhoods;
  in particular, a weakly locally compact preregular space
  is a locally compact regular space;
- `isCompact_isClosed_basis_nhds`: a version of the previous theorem
  for weakly locally compact spaces;
- `exists_mem_nhds_isCompact_isClosed`: in a locally compact regular space,
  each point admits a compact closed neighborhood.

### Deprecated theorems

Some theorems about topological groups are true for any (pre)regular space,
so we deprecate the special cases.

- `exists_isCompact_isClosed_subset_isCompact_nhds_one`:
  use new `IsCompact.isCompact_isClosed_basis_nhds` instead;
- `instLocallyCompactSpaceOfWeaklyOfGroup`,
  `instLocallyCompactSpaceOfWeaklyOfAddGroup`:
  are now implied by `WeaklyLocallyCompactSpace.locallyCompactSpace`;
- `local_isCompact_isClosed_nhds_of_group`,
  `local_isCompact_isClosed_nhds_of_addGroup`:
  use `isCompact_isClosed_basis_nhds` instead;
- `exists_isCompact_isClosed_nhds_one`, `exists_isCompact_isClosed_nhds_zero`:
  use `exists_mem_nhds_isCompact_isClosed` instead.

### Renamed/moved theorems

For each renamed theorem, the old theorem is redefined as a deprecated alias.

- `isOpen_setOf_disjoint_nhds_nhds`: moved to `Constructions`;
- `isCompact_closure_of_subset_compact` -> `IsCompact.closure_of_subset`;
- `IsCompact.measure_eq_infi_isOpen` -> `IsCompact.measure_eq_iInf_isOpen`;
- `exists_compact_superset_iff` -> `exists_isCompact_superset_iff`;
- `separatedNhds_of_isCompact_isCompact_isClosed` -> `SeparatedNhds.of_isCompact_isCompact_isClosed`;
- `separatedNhds_of_isCompact_isCompact` -> `SeparatedNhds.of_isCompact_isCompact`;
- `separatedNhds_of_finset_finset` -> `SeparatedNhds.of_finset_finset`;
- `point_disjoint_finset_opens_of_t2` -> `SeparatedNhds.of_singleton_finset`;
- `separatedNhds_of_isCompact_isClosed` -> `SeparatedNhds.of_isCompact_isClosed`;
- `exists_open_superset_and_isCompact_closure` -> `exists_isOpen_superset_and_isCompact_closure`;
- `exists_open_with_compact_closure` -> `exists_isOpen_mem_isCompact_closure`;

Mathlib/Analysis/NormedSpace/CompactOperator.lean

@@ -85,7 +85,7 @@ theorem isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image [T2Space M
     IsCompactOperator f ↔ ∃ V ∈ (𝓝 0 : Filter M₁), IsCompact (closure <| f '' V) := by
   rw [isCompactOperator_iff_exists_mem_nhds_image_subset_compact]
   exact
-    ⟨fun ⟨V, hV, K, hK, hKV⟩ => ⟨V, hV, isCompact_closure_of_subset_compact hK hKV⟩,
+    ⟨fun ⟨V, hV, K, hK, hKV⟩ => ⟨V, hV, hK.closure_of_subset hKV⟩,
       fun ⟨V, hV, hVc⟩ => ⟨V, hV, closure (f '' V), hVc, subset_closure⟩⟩
 #align is_compact_operator_iff_exists_mem_nhds_is_compact_closure_image isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image
 
@@ -113,7 +113,7 @@ theorem IsCompactOperator.isCompact_closure_image_of_isVonNBounded [T2Space M₂
     (hf : IsCompactOperator f) {S : Set M₁} (hS : IsVonNBounded 𝕜₁ S) :
     IsCompact (closure <| f '' S) :=
   let ⟨_, hK, hKf⟩ := hf.image_subset_compact_of_isVonNBounded hS
-  isCompact_closure_of_subset_compact hK hKf
+  hK.closure_of_subset hKf
 set_option linter.uppercaseLean3 false in
 #align is_compact_operator.is_compact_closure_image_of_vonN_bounded IsCompactOperator.isCompact_closure_image_of_isVonNBounded
 

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

@@ -1550,7 +1550,7 @@ theorem isCompact_closure_image_coe_of_bounded [ProperSpace F] {s : Set (E' →S
     (hb : IsBounded s) : IsCompact (closure (((↑) : (E' →SL[σ₁₂] F) → E' → F) '' s)) :=
   have : ∀ x, IsCompact (closure (apply' F σ₁₂ x '' s)) := fun x =>
     ((apply' F σ₁₂ x).lipschitz.isBounded_image hb).isCompact_closure
-  isCompact_closure_of_subset_compact (isCompact_pi_infinite this)
+  (isCompact_pi_infinite this).closure_of_subset
     (image_subset_iff.2 fun _ hg _ => subset_closure <| mem_image_of_mem _ hg)
 #align continuous_linear_map.is_compact_closure_image_coe_of_bounded ContinuousLinearMap.isCompact_closure_image_coe_of_bounded
 

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -362,6 +362,34 @@ theorem IsCompact.measurableSet [T2Space α] (h : IsCompact s) : MeasurableSet s
   h.isClosed.measurableSet
 #align is_compact.measurable_set IsCompact.measurableSet
 
+/-- If two points are topologically inseparable,
+then they can't be separated by a Borel measurable set. -/
+theorem Inseparable.mem_measurableSet_iff {x y : γ} (h : Inseparable x y) {s : Set γ}
+    (hs : MeasurableSet s) : x ∈ s ↔ y ∈ s :=
+  hs.induction_on_open (C := fun s ↦ (x ∈ s ↔ y ∈ s)) (fun _ ↦ h.mem_open_iff) (fun s _ hs ↦ hs.not)
+    fun _ _ _ h ↦ by simp [h]
+
+/-- If `K` is a compact set in an R₁ space and `s ⊇ K` is a Borel measurable superset,
+then `s` includes the closure of `K` as well. -/
+theorem IsCompact.closure_subset_measurableSet [R1Space γ] {K s : Set γ} (hK : IsCompact K)
+    (hs : MeasurableSet s) (hKs : K ⊆ s) : closure K ⊆ s := by
+  rw [hK.closure_eq_biUnion_inseparable, iUnion₂_subset_iff]
+  exact fun x hx y hy ↦ (hy.mem_measurableSet_iff hs).1 (hKs hx)
+
+/-- In an R₁ topological space with Borel measure `μ`,
+the measure of the closure of a compact set `K` is equal to the measure of `K`.
+
+See also `MeasureTheory.Measure.OuterRegular.measure_closure_eq_of_isCompact`
+for a version that assumes `μ` to be outer regular
+but does not assume the `σ`-algebra to be Borel.  -/
+theorem IsCompact.measure_closure [R1Space γ] {K : Set γ} (hK : IsCompact K) (μ : Measure γ) :
+    μ (closure K) = μ K := by
+  refine le_antisymm ?_ (measure_mono subset_closure)
+  calc
+    μ (closure K) ≤ μ (toMeasurable μ K) := measure_mono <|
+      hK.closure_subset_measurableSet (measurableSet_toMeasurable ..) (subset_toMeasurable ..)
+    _ = μ K := measure_toMeasurable ..
+
 @[measurability]
 theorem measurableSet_closure : MeasurableSet (closure s) :=
   isClosed_closure.measurableSet

Mathlib/MeasureTheory/Group/Measure.lean

@@ -709,9 +709,9 @@ theorem measure_univ_of_isMulLeftInvariant [WeaklyLocallyCompactSpace G] [Noncom
     find `g = g (L)` such that `L` is disjoint from `g • K`. Iterating this, one finds
     infinitely many translates of `K` which are disjoint from each other. As they all have the
     same positive mass, it follows that the space has infinite measure. -/
-  obtain ⟨K, hK, Kclosed, K1⟩ : ∃ K : Set G, IsCompact K ∧ IsClosed K ∧ K ∈ 𝓝 1 :=
-    exists_isCompact_isClosed_nhds_one G
-  have K_pos : 0 < μ K := measure_pos_of_nonempty_interior _ ⟨_, mem_interior_iff_mem_nhds.2 K1⟩
+  obtain ⟨K, K1, hK, Kclosed⟩ : ∃ K ∈ 𝓝 (1 : G), IsCompact K ∧ IsClosed K :=
+    exists_mem_nhds_isCompact_isClosed 1
+  have K_pos : 0 < μ K := measure_pos_of_mem_nhds μ K1
   have A : ∀ L : Set G, IsCompact L → ∃ g : G, Disjoint L (g • K) := fun L hL =>
     exists_disjoint_smul_of_isCompact hL hK
   choose! g hg using A
@@ -760,11 +760,10 @@ lemma _root_.MeasurableSet.mul_closure_one_eq {s : Set G} (hs : MeasurableSet s)
     simp only [iUnion_smul, h''f]
 
 /-- If a compact set is included in a measurable set, then so is its closure. -/
-@[to_additive]
+@[to_additive (attr := deprecated IsCompact.closure_subset_measurableSet)] -- Since 28 Jan 2024
 lemma _root_.IsCompact.closure_subset_of_measurableSet_of_group {k s : Set G}
-    (hk : IsCompact k) (hs : MeasurableSet s) (h : k ⊆ s) : closure k ⊆ s := by
-  rw [← hk.mul_closure_one_eq_closure, ← hs.mul_closure_one_eq]
-  exact mul_subset_mul_right h
+    (hk : IsCompact k) (hs : MeasurableSet s) (h : k ⊆ s) : closure k ⊆ s :=
+  hk.closure_subset_measurableSet hs h
 
 @[to_additive (attr := simp)]
 lemma measure_mul_closure_one (s : Set G) (μ : Measure G) :
@@ -777,20 +776,19 @@ lemma measure_mul_closure_one (s : Set G) (μ : Measure G) :
   rw [← t_meas.mul_closure_one_eq]
   exact smul_subset_smul_right kt
 
-@[to_additive]
+@[to_additive (attr := deprecated IsCompact.measure_closure)] -- Since 28 Jan 2024
 lemma _root_.IsCompact.measure_closure_eq_of_group {k : Set G} (hk : IsCompact k) (μ : Measure G) :
-    μ (closure k) = μ k := by
-  rw [← hk.mul_closure_one_eq_closure, measure_mul_closure_one]
+    μ (closure k) = μ k :=
+  hk.measure_closure μ
 
 @[to_additive]
-lemma innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group [LocallyCompactSpace G]
-    [h : InnerRegularCompactLTTop μ] :
+lemma innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group [h : InnerRegularCompactLTTop μ] :
     InnerRegularWRT μ (fun s ↦ IsCompact s ∧ IsClosed s) (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞) := by
   intro s ⟨s_meas, μs⟩ r hr
   rcases h.innerRegular ⟨s_meas, μs⟩ r hr with ⟨K, Ks, K_comp, hK⟩
   refine ⟨closure K, ?_, ⟨K_comp.closure, isClosed_closure⟩, ?_⟩
-  · exact IsCompact.closure_subset_of_measurableSet_of_group K_comp s_meas Ks
-  · rwa [K_comp.measure_closure_eq_of_group]
+  · exact IsCompact.closure_subset_measurableSet K_comp s_meas Ks
+  · rwa [K_comp.measure_closure]
 
 end TopologicalGroup
 

Mathlib/MeasureTheory/Measure/Content.lean

@@ -41,9 +41,9 @@ For `μ : Content G`, we define
 * `μ.outerMeasure` : the outer measure associated to `μ`.
 * `μ.measure`      : the Borel measure associated to `μ`.
 
-These definitions are given for spaces which are either T2, or locally compact and regular (which
-covers possibly non-Hausdorff locally compact groups). The resulting measure `μ.measure` is always
-outer regular by design. When the space is locally compact, `μ.measure` is also regular.
+These definitions are given for spaces which are R₁.
+The resulting measure `μ.measure` is always outer regular by design.
+When the space is locally compact, `μ.measure` is also regular.
 
 ## References
 
@@ -171,7 +171,7 @@ theorem innerContent_exists_compact {U : Opens G} (hU : μ.innerContent U ≠ 
 #align measure_theory.content.inner_content_exists_compact MeasureTheory.Content.innerContent_exists_compact
 
 /-- The inner content of a supremum of opens is at most the sum of the individual inner contents. -/
-theorem innerContent_iSup_nat [T2OrLocallyCompactRegularSpace G] (U : ℕ → Opens G) :
+theorem innerContent_iSup_nat [R1Space G] (U : ℕ → Opens G) :
     μ.innerContent (⨆ i : ℕ, U i) ≤ ∑' i : ℕ, μ.innerContent (U i) := by
   have h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ t.sum fun i => μ (K i) := by
     intro t K
@@ -200,7 +200,7 @@ theorem innerContent_iSup_nat [T2OrLocallyCompactRegularSpace G] (U : ℕ → Op
 /-- The inner content of a union of sets is at most the sum of the individual inner contents.
   This is the "unbundled" version of `innerContent_iSup_nat`.
   It is required for the API of `inducedOuterMeasure`. -/
-theorem innerContent_iUnion_nat [T2OrLocallyCompactRegularSpace G] ⦃U : ℕ → Set G⦄
+theorem innerContent_iUnion_nat [R1Space G] ⦃U : ℕ → Set G⦄
     (hU : ∀ i : ℕ, IsOpen (U i)) :
     μ.innerContent ⟨⋃ i : ℕ, U i, isOpen_iUnion hU⟩ ≤ ∑' i : ℕ, μ.innerContent ⟨U i, hU i⟩ := by
   have := μ.innerContent_iSup_nat fun i => ⟨U i, hU i⟩
@@ -225,8 +225,7 @@ theorem is_mul_left_invariant_innerContent [Group G] [TopologicalGroup G]
 #align measure_theory.content.is_add_left_invariant_inner_content MeasureTheory.Content.is_add_left_invariant_innerContent
 
 @[to_additive]
-theorem innerContent_pos_of_is_mul_left_invariant [T2OrLocallyCompactRegularSpace G] [Group G]
-    [TopologicalGroup G]
+theorem innerContent_pos_of_is_mul_left_invariant [Group G] [TopologicalGroup G]
     (h3 : ∀ (g : G) {K : Compacts G}, μ (K.map _ <| continuous_mul_left g) = μ K) (K : Compacts G)
     (hK : μ K ≠ 0) (U : Opens G) (hU : (U : Set G).Nonempty) : 0 < μ.innerContent U := by
   have : (interior (U : Set G)).Nonempty
@@ -255,7 +254,7 @@ protected def outerMeasure : OuterMeasure G :=
   inducedOuterMeasure (fun U hU => μ.innerContent ⟨U, hU⟩) isOpen_empty μ.innerContent_bot
 #align measure_theory.content.outer_measure MeasureTheory.Content.outerMeasure
 
-variable [T2OrLocallyCompactRegularSpace G]
+variable [R1Space G]
 
 theorem outerMeasure_opens (U : Opens G) : μ.outerMeasure U = μ.innerContent U :=
   inducedOuterMeasure_eq' (fun _ => isOpen_iUnion) μ.innerContent_iUnion_nat μ.innerContent_mono U.2
@@ -450,7 +449,7 @@ theorem contentRegular_exists_compact (H : ContentRegular μ) (K : TopologicalSp
     (ENNReal.lt_add_right (ne_top_of_lt (μ.lt_top K)) (ENNReal.coe_ne_zero.mpr hε)))
 #align measure_theory.content.content_regular_exists_compact MeasureTheory.Content.contentRegular_exists_compact
 
-variable [MeasurableSpace G] [T2OrLocallyCompactRegularSpace G] [BorelSpace G]
+variable [MeasurableSpace G] [R1Space G] [BorelSpace G]
 
 /-- If `μ` is a regular content, then the measure induced by `μ` will agree with `μ`
   on compact sets. -/

Mathlib/MeasureTheory/Measure/Haar/Basic.lean

@@ -484,8 +484,7 @@ theorem chaar_sup_le {K₀ : PositiveCompacts G} (K₁ K₂ : Compacts G) :
 theorem chaar_sup_eq {K₀ : PositiveCompacts G}
     {K₁ K₂ : Compacts G} (h : Disjoint K₁.1 K₂.1) (h₂ : IsClosed K₂.1) :
     chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂ := by
-  have : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group
-  rcases separatedNhds_of_isCompact_isCompact_isClosed K₁.2 K₂.2 h₂ h
+  rcases SeparatedNhds.of_isCompact_isCompact_isClosed K₁.2 K₂.2 h₂ h
     with ⟨U₁, U₂, h1U₁, h1U₂, h2U₁, h2U₂, hU⟩
   rcases compact_open_separated_mul_right K₁.2 h1U₁ h2U₁ with ⟨L₁, h1L₁, h2L₁⟩
   rcases mem_nhds_iff.mp h1L₁ with ⟨V₁, h1V₁, h2V₁, h3V₁⟩
@@ -577,7 +576,6 @@ theorem is_left_invariant_haarContent {K₀ : PositiveCompacts G} (g : G) (K : C
 @[to_additive]
 theorem haarContent_outerMeasure_self_pos (K₀ : PositiveCompacts G) :
     0 < (haarContent K₀).outerMeasure K₀ := by
-  have : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group
   refine' zero_lt_one.trans_le _
   rw [Content.outerMeasure_eq_iInf]
   refine' le_iInf₂ fun U hU => le_iInf fun hK₀ => le_trans _ <| le_iSup₂ K₀.toCompacts hK₀
@@ -610,14 +608,12 @@ variable [TopologicalSpace G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpa
 "The Haar measure on the locally compact additive group `G`, scaled so that
 `addHaarMeasure K₀ K₀ = 1`."]
 noncomputable def haarMeasure (K₀ : PositiveCompacts G) : Measure G :=
-  have : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group
   ((haarContent K₀).measure K₀)⁻¹ • (haarContent K₀).measure
 #align measure_theory.measure.haar_measure MeasureTheory.Measure.haarMeasure
 #align measure_theory.measure.add_haar_measure MeasureTheory.Measure.addHaarMeasure
 
 @[to_additive]
-theorem haarMeasure_apply [LocallyCompactSpace G]
-    {K₀ : PositiveCompacts G} {s : Set G} (hs : MeasurableSet s) :
+theorem haarMeasure_apply {K₀ : PositiveCompacts G} {s : Set G} (hs : MeasurableSet s) :
     haarMeasure K₀ s = (haarContent K₀).outerMeasure s / (haarContent K₀).measure K₀ := by
   change ((haarContent K₀).measure K₀)⁻¹ * (haarContent K₀).measure s = _
   simp only [hs, div_eq_mul_inv, mul_comm, Content.measure_apply]
@@ -627,7 +623,6 @@ theorem haarMeasure_apply [LocallyCompactSpace G]
 @[to_additive]
 instance isMulLeftInvariant_haarMeasure (K₀ : PositiveCompacts G) :
     IsMulLeftInvariant (haarMeasure K₀) := by
-  have : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group
   rw [← forall_measure_preimage_mul_iff]
   intro g A hA
   rw [haarMeasure_apply hA, haarMeasure_apply (measurable_const_mul g hA)]
@@ -663,7 +658,7 @@ instance regular_haarMeasure {K₀ : PositiveCompacts G} : (haarMeasure K₀).Re
 
 @[to_additive]
 theorem haarMeasure_closure_self {K₀ : PositiveCompacts G} : haarMeasure K₀ (closure K₀) = 1 := by
-  rw [IsCompact.measure_closure_eq_of_group K₀.isCompact, haarMeasure_self]
+  rw [K₀.isCompact.measure_closure, haarMeasure_self]
 
 /-- The Haar measure is sigma-finite in a second countable group. -/
 @[to_additive "The additive Haar measure is sigma-finite in a second countable group."]
@@ -722,7 +717,7 @@ theorem div_mem_nhds_one_of_haar_pos (μ : Measure G) [IsHaarMeasure μ] [Locall
       ∃ (K : Set G), K ⊆ E ∧ IsCompact K ∧ IsClosed K ∧ 0 < μ K := by
     rcases MeasurableSet.exists_lt_isCompact hE hEpos with ⟨K, KE, K_comp, K_meas⟩
     refine ⟨closure K, ?_, K_comp.closure, isClosed_closure, ?_⟩
-    · exact IsCompact.closure_subset_of_measurableSet_of_group K_comp hE KE
+    · exact K_comp.closure_subset_measurableSet hE KE
     · rwa [K_comp.measure_closure_eq_of_group]
   obtain ⟨V, hV1, hV⟩ : ∃ V ∈ 𝓝 (1 : G), ∀ g ∈ V, μ (g • K \ K) < μ K :=
     exists_nhds_measure_smul_diff_lt hK K_closed hKpos.ne'
@@ -767,13 +762,11 @@ variable [SecondCountableTopology G]
   See also `isAddHaarMeasure_eq_smul_of_regular` for a statement not assuming second-countability."]
 theorem haarMeasure_unique (μ : Measure G) [SigmaFinite μ] [IsMulLeftInvariant μ]
     (K₀ : PositiveCompacts G) : μ = μ K₀ • haarMeasure K₀ := by
-  have : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group
   have A : Set.Nonempty (interior (closure (K₀ : Set G))) :=
     K₀.interior_nonempty.mono (interior_mono subset_closure)
   have := measure_eq_div_smul μ (haarMeasure K₀) (isClosed_closure (s := K₀)).measurableSet
     (measure_pos_of_nonempty_interior _ A).ne' K₀.isCompact.closure.measure_lt_top.ne
-  rwa [haarMeasure_closure_self, div_one, IsCompact.measure_closure_eq_of_group K₀.isCompact]
-    at this
+  rwa [haarMeasure_closure_self, div_one, K₀.isCompact.measure_closure] at this
 #align measure_theory.measure.haar_measure_unique MeasureTheory.Measure.haarMeasure_unique
 #align measure_theory.measure.add_haar_measure_unique MeasureTheory.Measure.addHaarMeasure_unique