Skip to content

Commit 7458f0e

Browse files
urkudurkud
committed
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`;
1 parent 7afbac6 commit 7458f0e

14 files changed

Lines changed: 481 additions & 352 deletions

File tree

‎Mathlib/Analysis/NormedSpace/CompactOperator.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -85,7 +85,7 @@ theorem isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image [T2Space M
8585
IsCompactOperator f ↔ ∃ V ∈ (𝓝 0 : Filter M₁), IsCompact (closure <| f '' V) := by
8686
rw [isCompactOperator_iff_exists_mem_nhds_image_subset_compact]
8787
exact
88-
⟨fun ⟨V, hV, K, hK, hKV⟩ => ⟨V, hV, isCompact_closure_of_subset_compact hK hKV⟩,
88+
⟨fun ⟨V, hV, K, hK, hKV⟩ => ⟨V, hV, hK.closure_of_subset hKV⟩,
8989
fun ⟨V, hV, hVc⟩ => ⟨V, hV, closure (f '' V), hVc, subset_closure⟩⟩
9090
#align is_compact_operator_iff_exists_mem_nhds_is_compact_closure_image isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image
9191

@@ -113,7 +113,7 @@ theorem IsCompactOperator.isCompact_closure_image_of_isVonNBounded [T2Space M₂
113113
(hf : IsCompactOperator f) {S : Set M₁} (hS : IsVonNBounded 𝕜₁ S) :
114114
IsCompact (closure <| f '' S) :=
115115
let ⟨_, hK, hKf⟩ := hf.image_subset_compact_of_isVonNBounded hS
116-
isCompact_closure_of_subset_compact hK hKf
116+
hK.closure_of_subset hKf
117117
set_option linter.uppercaseLean3 false in
118118
#align is_compact_operator.is_compact_closure_image_of_vonN_bounded IsCompactOperator.isCompact_closure_image_of_isVonNBounded
119119

‎Mathlib/Analysis/NormedSpace/OperatorNorm.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1550,7 +1550,7 @@ theorem isCompact_closure_image_coe_of_bounded [ProperSpace F] {s : Set (E' →S
15501550
(hb : IsBounded s) : IsCompact (closure (((↑) : (E' →SL[σ₁₂] F) → E' → F) '' s)) :=
15511551
have : ∀ x, IsCompact (closure (apply' F σ₁₂ x '' s)) := fun x =>
15521552
((apply' F σ₁₂ x).lipschitz.isBounded_image hb).isCompact_closure
1553-
isCompact_closure_of_subset_compact (isCompact_pi_infinite this)
1553+
(isCompact_pi_infinite this).closure_of_subset
15541554
(image_subset_iff.2 fun _ hg _ => subset_closure <| mem_image_of_mem _ hg)
15551555
#align continuous_linear_map.is_compact_closure_image_coe_of_bounded ContinuousLinearMap.isCompact_closure_image_coe_of_bounded
15561556

‎Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -362,6 +362,34 @@ theorem IsCompact.measurableSet [T2Space α] (h : IsCompact s) : MeasurableSet s
362362
h.isClosed.measurableSet
363363
#align is_compact.measurable_set IsCompact.measurableSet
364364

365+
/-- If two points are topologically inseparable,
366+
then they can't be separated by a Borel measurable set. -/
367+
theorem Inseparable.mem_measurableSet_iff {x y : γ} (h : Inseparable x y) {s : Set γ}
368+
(hs : MeasurableSet s) : x ∈ s ↔ y ∈ s :=
369+
hs.induction_on_open (C := fun s ↦ (x ∈ s ↔ y ∈ s)) (fun _ ↦ h.mem_open_iff) (fun s _ hs ↦ hs.not)
370+
fun _ _ _ h ↦ by simp [h]
371+
372+
/-- If `K` is a compact set in an R₁ space and `s ⊇ K` is a Borel measurable superset,
373+
then `s` includes the closure of `K` as well. -/
374+
theorem IsCompact.closure_subset_measurableSet [R1Space γ] {K s : Set γ} (hK : IsCompact K)
375+
(hs : MeasurableSet s) (hKs : K ⊆ s) : closure K ⊆ s := by
376+
rw [hK.closure_eq_biUnion_inseparable, iUnion₂_subset_iff]
377+
exact fun x hx y hy ↦ (hy.mem_measurableSet_iff hs).1 (hKs hx)
378+
379+
/-- In an R₁ topological space with Borel measure `μ`,
380+
the measure of the closure of a compact set `K` is equal to the measure of `K`.
381+
382+
See also `MeasureTheory.Measure.OuterRegular.measure_closure_eq_of_isCompact`
383+
for a version that assumes `μ` to be outer regular
384+
but does not assume the `σ`-algebra to be Borel. -/
385+
theorem IsCompact.measure_closure [R1Space γ] {K : Set γ} (hK : IsCompact K) (μ : Measure γ) :
386+
μ (closure K) = μ K := by
387+
refine le_antisymm ?_ (measure_mono subset_closure)
388+
calc
389+
μ (closure K) ≤ μ (toMeasurable μ K) := measure_mono <|
390+
hK.closure_subset_measurableSet (measurableSet_toMeasurable ..) (subset_toMeasurable ..)
391+
_ = μ K := measure_toMeasurable ..
392+
365393
@[measurability]
366394
theorem measurableSet_closure : MeasurableSet (closure s) :=
367395
isClosed_closure.measurableSet

‎Mathlib/MeasureTheory/Group/Measure.lean‎

Lines changed: 12 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -709,9 +709,9 @@ theorem measure_univ_of_isMulLeftInvariant [WeaklyLocallyCompactSpace G] [Noncom
709709
find `g = g (L)` such that `L` is disjoint from `g • K`. Iterating this, one finds
710710
infinitely many translates of `K` which are disjoint from each other. As they all have the
711711
same positive mass, it follows that the space has infinite measure. -/
712-
obtain ⟨K, hK, Kclosed, K1⟩ : ∃ K : Set G, IsCompact K ∧ IsClosed K ∧ K ∈ 𝓝 1 :=
713-
exists_isCompact_isClosed_nhds_one G
714-
have K_pos : 0 < μ K := measure_pos_of_nonempty_interior _ ⟨_, mem_interior_iff_mem_nhds.2 K1⟩
712+
obtain ⟨K, K1, hK, Kclosed⟩ : ∃ K ∈ 𝓝 (1 : G), IsCompact K ∧ IsClosed K :=
713+
exists_mem_nhds_isCompact_isClosed 1
714+
have K_pos : 0 < μ K := measure_pos_of_mem_nhds μ K1
715715
have A : ∀ L : Set G, IsCompact L → ∃ g : G, Disjoint L (g • K) := fun L hL =>
716716
exists_disjoint_smul_of_isCompact hL hK
717717
choose! g hg using A
@@ -760,11 +760,10 @@ lemma _root_.MeasurableSet.mul_closure_one_eq {s : Set G} (hs : MeasurableSet s)
760760
simp only [iUnion_smul, h''f]
761761

762762
/-- If a compact set is included in a measurable set, then so is its closure. -/
763-
@[to_additive]
763+
@[to_additive (attr := deprecated IsCompact.closure_subset_measurableSet)] -- Since 28 Jan 2024
764764
lemma _root_.IsCompact.closure_subset_of_measurableSet_of_group {k s : Set G}
765-
(hk : IsCompact k) (hs : MeasurableSet s) (h : k ⊆ s) : closure k ⊆ s := by
766-
rw [← hk.mul_closure_one_eq_closure, ← hs.mul_closure_one_eq]
767-
exact mul_subset_mul_right h
765+
(hk : IsCompact k) (hs : MeasurableSet s) (h : k ⊆ s) : closure k ⊆ s :=
766+
hk.closure_subset_measurableSet hs h
768767

769768
@[to_additive (attr := simp)]
770769
lemma measure_mul_closure_one (s : Set G) (μ : Measure G) :
@@ -777,20 +776,19 @@ lemma measure_mul_closure_one (s : Set G) (μ : Measure G) :
777776
rw [← t_meas.mul_closure_one_eq]
778777
exact smul_subset_smul_right kt
779778

780-
@[to_additive]
779+
@[to_additive (attr := deprecated IsCompact.measure_closure)] -- Since 28 Jan 2024
781780
lemma _root_.IsCompact.measure_closure_eq_of_group {k : Set G} (hk : IsCompact k) (μ : Measure G) :
782-
μ (closure k) = μ k := by
783-
rw [← hk.mul_closure_one_eq_closure, measure_mul_closure_one]
781+
μ (closure k) = μ k :=
782+
hk.measure_closure μ
784783

785784
@[to_additive]
786-
lemma innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group [LocallyCompactSpace G]
787-
[h : InnerRegularCompactLTTop μ] :
785+
lemma innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group [h : InnerRegularCompactLTTop μ] :
788786
InnerRegularWRT μ (fun s ↦ IsCompact s ∧ IsClosed s) (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞) := by
789787
intro s ⟨s_meas, μs⟩ r hr
790788
rcases h.innerRegular ⟨s_meas, μs⟩ r hr with ⟨K, Ks, K_comp, hK⟩
791789
refine ⟨closure K, ?_, ⟨K_comp.closure, isClosed_closure⟩, ?_⟩
792-
· exact IsCompact.closure_subset_of_measurableSet_of_group K_comp s_meas Ks
793-
· rwa [K_comp.measure_closure_eq_of_group]
790+
· exact IsCompact.closure_subset_measurableSet K_comp s_meas Ks
791+
· rwa [K_comp.measure_closure]
794792

795793
end TopologicalGroup
796794

‎Mathlib/MeasureTheory/Measure/Content.lean‎

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -41,9 +41,9 @@ For `μ : Content G`, we define
4141
* `μ.outerMeasure` : the outer measure associated to `μ`.
4242
* `μ.measure` : the Borel measure associated to `μ`.
4343
44-
These definitions are given for spaces which are either T2, or locally compact and regular (which
45-
covers possibly non-Hausdorff locally compact groups). The resulting measure `μ.measure` is always
46-
outer regular by design. When the space is locally compact, `μ.measure` is also regular.
44+
These definitions are given for spaces which are R₁.
45+
The resulting measure `μ.measure` is always outer regular by design.
46+
When the space is locally compact, `μ.measure` is also regular.
4747
4848
## References
4949
@@ -171,7 +171,7 @@ theorem innerContent_exists_compact {U : Opens G} (hU : μ.innerContent U ≠
171171
#align measure_theory.content.inner_content_exists_compact MeasureTheory.Content.innerContent_exists_compact
172172

173173
/-- The inner content of a supremum of opens is at most the sum of the individual inner contents. -/
174-
theorem innerContent_iSup_nat [T2OrLocallyCompactRegularSpace G] (U : ℕ → Opens G) :
174+
theorem innerContent_iSup_nat [R1Space G] (U : ℕ → Opens G) :
175175
μ.innerContent (⨆ i : ℕ, U i) ≤ ∑' i : ℕ, μ.innerContent (U i) := by
176176
have h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ t.sum fun i => μ (K i) := by
177177
intro t K
@@ -200,7 +200,7 @@ theorem innerContent_iSup_nat [T2OrLocallyCompactRegularSpace G] (U : ℕ → Op
200200
/-- The inner content of a union of sets is at most the sum of the individual inner contents.
201201
This is the "unbundled" version of `innerContent_iSup_nat`.
202202
It is required for the API of `inducedOuterMeasure`. -/
203-
theorem innerContent_iUnion_nat [T2OrLocallyCompactRegularSpace G] ⦃U : ℕ → Set G⦄
203+
theorem innerContent_iUnion_nat [R1Space G] ⦃U : ℕ → Set G⦄
204204
(hU : ∀ i : ℕ, IsOpen (U i)) :
205205
μ.innerContent ⟨⋃ i : ℕ, U i, isOpen_iUnion hU⟩ ≤ ∑' i : ℕ, μ.innerContent ⟨U i, hU i⟩ := by
206206
have := μ.innerContent_iSup_nat fun i => ⟨U i, hU i⟩
@@ -225,8 +225,7 @@ theorem is_mul_left_invariant_innerContent [Group G] [TopologicalGroup G]
225225
#align measure_theory.content.is_add_left_invariant_inner_content MeasureTheory.Content.is_add_left_invariant_innerContent
226226

227227
@[to_additive]
228-
theorem innerContent_pos_of_is_mul_left_invariant [T2OrLocallyCompactRegularSpace G] [Group G]
229-
[TopologicalGroup G]
228+
theorem innerContent_pos_of_is_mul_left_invariant [Group G] [TopologicalGroup G]
230229
(h3 : ∀ (g : G) {K : Compacts G}, μ (K.map _ <| continuous_mul_left g) = μ K) (K : Compacts G)
231230
(hK : μ K ≠ 0) (U : Opens G) (hU : (U : Set G).Nonempty) : 0 < μ.innerContent U := by
232231
have : (interior (U : Set G)).Nonempty
@@ -255,7 +254,7 @@ protected def outerMeasure : OuterMeasure G :=
255254
inducedOuterMeasure (fun U hU => μ.innerContent ⟨U, hU⟩) isOpen_empty μ.innerContent_bot
256255
#align measure_theory.content.outer_measure MeasureTheory.Content.outerMeasure
257256

258-
variable [T2OrLocallyCompactRegularSpace G]
257+
variable [R1Space G]
259258

260259
theorem outerMeasure_opens (U : Opens G) : μ.outerMeasure U = μ.innerContent U :=
261260
inducedOuterMeasure_eq' (fun _ => isOpen_iUnion) μ.innerContent_iUnion_nat μ.innerContent_mono U.2
@@ -450,7 +449,7 @@ theorem contentRegular_exists_compact (H : ContentRegular μ) (K : TopologicalSp
450449
(ENNReal.lt_add_right (ne_top_of_lt (μ.lt_top K)) (ENNReal.coe_ne_zero.mpr hε)))
451450
#align measure_theory.content.content_regular_exists_compact MeasureTheory.Content.contentRegular_exists_compact
452451

453-
variable [MeasurableSpace G] [T2OrLocallyCompactRegularSpace G] [BorelSpace G]
452+
variable [MeasurableSpace G] [R1Space G] [BorelSpace G]
454453

455454
/-- If `μ` is a regular content, then the measure induced by `μ` will agree with `μ`
456455
on compact sets. -/

‎Mathlib/MeasureTheory/Measure/Haar/Basic.lean‎

Lines changed: 5 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -484,8 +484,7 @@ theorem chaar_sup_le {K₀ : PositiveCompacts G} (K₁ K₂ : Compacts G) :
484484
theorem chaar_sup_eq {K₀ : PositiveCompacts G}
485485
{K₁ K₂ : Compacts G} (h : Disjoint K₁.1 K₂.1) (h₂ : IsClosed K₂.1) :
486486
chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂ := by
487-
have : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group
488-
rcases separatedNhds_of_isCompact_isCompact_isClosed K₁.2 K₂.2 h₂ h
487+
rcases SeparatedNhds.of_isCompact_isCompact_isClosed K₁.2 K₂.2 h₂ h
489488
with ⟨U₁, U₂, h1U₁, h1U₂, h2U₁, h2U₂, hU⟩
490489
rcases compact_open_separated_mul_right K₁.2 h1U₁ h2U₁ with ⟨L₁, h1L₁, h2L₁⟩
491490
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
577576
@[to_additive]
578577
theorem haarContent_outerMeasure_self_pos (K₀ : PositiveCompacts G) :
579578
0 < (haarContent K₀).outerMeasure K₀ := by
580-
have : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group
581579
refine' zero_lt_one.trans_le _
582580
rw [Content.outerMeasure_eq_iInf]
583581
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
610608
"The Haar measure on the locally compact additive group `G`, scaled so that
611609
`addHaarMeasure K₀ K₀ = 1`."]
612610
noncomputable def haarMeasure (K₀ : PositiveCompacts G) : Measure G :=
613-
have : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group
614611
((haarContent K₀).measure K₀)⁻¹ • (haarContent K₀).measure
615612
#align measure_theory.measure.haar_measure MeasureTheory.Measure.haarMeasure
616613
#align measure_theory.measure.add_haar_measure MeasureTheory.Measure.addHaarMeasure
617614

618615
@[to_additive]
619-
theorem haarMeasure_apply [LocallyCompactSpace G]
620-
{K₀ : PositiveCompacts G} {s : Set G} (hs : MeasurableSet s) :
616+
theorem haarMeasure_apply {K₀ : PositiveCompacts G} {s : Set G} (hs : MeasurableSet s) :
621617
haarMeasure K₀ s = (haarContent K₀).outerMeasure s / (haarContent K₀).measure K₀ := by
622618
change ((haarContent K₀).measure K₀)⁻¹ * (haarContent K₀).measure s = _
623619
simp only [hs, div_eq_mul_inv, mul_comm, Content.measure_apply]
@@ -627,7 +623,6 @@ theorem haarMeasure_apply [LocallyCompactSpace G]
627623
@[to_additive]
628624
instance isMulLeftInvariant_haarMeasure (K₀ : PositiveCompacts G) :
629625
IsMulLeftInvariant (haarMeasure K₀) := by
630-
have : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group
631626
rw [← forall_measure_preimage_mul_iff]
632627
intro g A hA
633628
rw [haarMeasure_apply hA, haarMeasure_apply (measurable_const_mul g hA)]
@@ -663,7 +658,7 @@ instance regular_haarMeasure {K₀ : PositiveCompacts G} : (haarMeasure K₀).Re
663658

664659
@[to_additive]
665660
theorem haarMeasure_closure_self {K₀ : PositiveCompacts G} : haarMeasure K₀ (closure K₀) = 1 := by
666-
rw [IsCompact.measure_closure_eq_of_group K₀.isCompact, haarMeasure_self]
661+
rw [K₀.isCompact.measure_closure, haarMeasure_self]
667662

668663
/-- The Haar measure is sigma-finite in a second countable group. -/
669664
@[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
722717
∃ (K : Set G), K ⊆ E ∧ IsCompact K ∧ IsClosed K ∧ 0 < μ K := by
723718
rcases MeasurableSet.exists_lt_isCompact hE hEpos with ⟨K, KE, K_comp, K_meas⟩
724719
refine ⟨closure K, ?_, K_comp.closure, isClosed_closure, ?_⟩
725-
· exact IsCompact.closure_subset_of_measurableSet_of_group K_comp hE KE
720+
· exact K_comp.closure_subset_measurableSet hE KE
726721
· rwa [K_comp.measure_closure_eq_of_group]
727722
obtain ⟨V, hV1, hV⟩ : ∃ V ∈ 𝓝 (1 : G), ∀ g ∈ V, μ (g • K \ K) < μ K :=
728723
exists_nhds_measure_smul_diff_lt hK K_closed hKpos.ne'
@@ -767,13 +762,11 @@ variable [SecondCountableTopology G]
767762
See also `isAddHaarMeasure_eq_smul_of_regular` for a statement not assuming second-countability."]
768763
theorem haarMeasure_unique (μ : Measure G) [SigmaFinite μ] [IsMulLeftInvariant μ]
769764
(K₀ : PositiveCompacts G) : μ = μ K₀ • haarMeasure K₀ := by
770-
have : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group
771765
have A : Set.Nonempty (interior (closure (K₀ : Set G))) :=
772766
K₀.interior_nonempty.mono (interior_mono subset_closure)
773767
have := measure_eq_div_smul μ (haarMeasure K₀) (isClosed_closure (s := K₀)).measurableSet
774768
(measure_pos_of_nonempty_interior _ A).ne' K₀.isCompact.closure.measure_lt_top.ne
775-
rwa [haarMeasure_closure_self, div_one, IsCompact.measure_closure_eq_of_group K₀.isCompact]
776-
at this
769+
rwa [haarMeasure_closure_self, div_one, K₀.isCompact.measure_closure] at this
777770
#align measure_theory.measure.haar_measure_unique MeasureTheory.Measure.haarMeasure_unique
778771
#align measure_theory.measure.add_haar_measure_unique MeasureTheory.Measure.addHaarMeasure_unique
779772

0 commit comments

Comments
 (0)