From 948d3c95578f9d9adc716d1fdaf1df526a761295 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 28 Jan 2024 05:57:30 -0600 Subject: [PATCH 01/16] Snapshot --- .../Topology/Compactness/LocallyCompact.lean | 4 +- Mathlib/Topology/Constructions.lean | 8 + Mathlib/Topology/Inseparable.lean | 3 + Mathlib/Topology/Separation.lean | 477 +++++++++--------- Mathlib/Topology/Support.lean | 4 +- 5 files changed, 261 insertions(+), 235 deletions(-) diff --git a/Mathlib/Topology/Compactness/LocallyCompact.lean b/Mathlib/Topology/Compactness/LocallyCompact.lean index fcc3fa87302dd..c2ce357544663 100644 --- a/Mathlib/Topology/Compactness/LocallyCompact.lean +++ b/Mathlib/Topology/Compactness/LocallyCompact.lean @@ -161,9 +161,9 @@ most notably in `ContinuousMap.continuous_comp'` and `ContinuousMap.continuous_e It is satisfied in two cases: - if `X` is a locally compact topological space, for obvious reasons; -- if `X` is a weakly locally compact topological space and `Y` is a Hausdorff space; +- if `X` is a weakly locally compact topological space and `Y` is a preregular space; this fact is a simple generalization of the theorem - saying that a weakly locally compact Hausdorff topological space is locally compact. + saying that a weakly locally compact preregular topological space is locally compact. -/ class LocallyCompactPair (X Y : Type*) [TopologicalSpace X] [TopologicalSpace Y] : Prop where /-- If `f : X → Y` is a continuous map in a locally compact pair of topological spaces diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean index 9ccf472786302..29642a985f4f3 100644 --- a/Mathlib/Topology/Constructions.lean +++ b/Mathlib/Topology/Constructions.lean @@ -585,6 +585,14 @@ theorem prod_mem_nhds {s : Set X} {t : Set Y} {x : X} {y : Y} (hx : s ∈ 𝓝 x prod_mem_nhds_iff.2 ⟨hx, hy⟩ #align prod_mem_nhds prod_mem_nhds +theorem isOpen_setOf_disjoint_nhds_nhds : IsOpen { p : X × X | Disjoint (𝓝 p.1) (𝓝 p.2) } := by + simp only [isOpen_iff_mem_nhds, Prod.forall, mem_setOf_eq] + intro x y h + obtain ⟨U, hU, V, hV, hd⟩ := ((nhds_basis_opens x).disjoint_iff (nhds_basis_opens y)).mp h + exact mem_nhds_prod_iff'.mpr ⟨U, V, hU.2, hU.1, hV.2, hV.1, fun ⟨x', y'⟩ ⟨hx', hy'⟩ => + disjoint_of_disjoint_of_mem hd (hU.2.mem_nhds hx') (hV.2.mem_nhds hy')⟩ +#align is_open_set_of_disjoint_nhds_nhds isOpen_setOf_disjoint_nhds_nhds + theorem Filter.Eventually.prod_nhds {p : X → Prop} {q : Y → Prop} {x : X} {y : Y} (hx : ∀ᶠ x in 𝓝 x, p x) (hy : ∀ᶠ y in 𝓝 y, q y) : ∀ᶠ z : X × Y in 𝓝 (x, y), p z.1 ∧ q z.2 := prod_mem_nhds hx hy diff --git a/Mathlib/Topology/Inseparable.lean b/Mathlib/Topology/Inseparable.lean index 17facf148dccd..24c8f048dd2b5 100644 --- a/Mathlib/Topology/Inseparable.lean +++ b/Mathlib/Topology/Inseparable.lean @@ -98,6 +98,9 @@ theorem specializes_iff_nhds : x ⤳ y ↔ 𝓝 x ≤ 𝓝 y := Iff.rfl #align specializes_iff_nhds specializes_iff_nhds +theorem Specializes.not_disjoint (h : x ⤳ y) : ¬Disjoint (𝓝 x) (𝓝 y) := fun hd ↦ + absurd (hd.mono_right h) <| by simp [NeBot.ne'] + theorem specializes_iff_pure : x ⤳ y ↔ pure x ≤ 𝓝 y := (specializes_TFAE x y).out 0 1 #align specializes_iff_pure specializes_iff_pure diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index 92389bfba11cf..8d9594476d1e0 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -912,6 +912,208 @@ theorem TopologicalSpace.subset_trans {s t : Set X} (ts : t ⊆ s) : (embedding_inclusion ts).induced #align topological_space.subset_trans TopologicalSpace.subset_trans +/-! ### Preregular (R₁) spaces -/ + +section R1Space + +/-- A topological space is called a *preregular* (a.k.a. R₁) space, +if any two topologically distinguishable points have disjoint neighbourhoods. -/ +@[mk_iff r1Space_iff_specializes_or_disjoint_nhds] +class R1Space (X : Type*) [TopologicalSpace X] : Prop where + specializes_or_disjoint_nhds (x y : X) : Specializes x y ∨ Disjoint (𝓝 x) (𝓝 y) + +export R1Space (specializes_or_disjoint_nhds) + +variable [R1Space X] {x y : X} + +theorem disjoint_nhds_nhds_iff_not_specializes : Disjoint (𝓝 x) (𝓝 y) ↔ ¬x ⤳ y := + ⟨fun hd hspec ↦ hspec.not_disjoint hd, (specializes_or_disjoint_nhds _ _).resolve_left⟩ +#align disjoint_nhds_nhds_iff_not_specializes disjoint_nhds_nhds_iff_not_specializes + +theorem specializes_iff_not_disjoint : x ⤳ y ↔ ¬Disjoint (𝓝 x) (𝓝 y) := + disjoint_nhds_nhds_iff_not_specializes.not_left.symm + +/-- An R₁ space is an R₀ space: the `Specializes` relation is symmetric. -/ +theorem Specializes.symm (h : x ⤳ y) : y ⤳ x := by + simpa only [specializes_iff_not_disjoint, disjoint_comm] using h +#align specializes.symm Specializes.symm + +/-- An R₁ space is an R₀ space: the `Specializes` relation is symmetric. -/ +theorem specializes_comm : x ⤳ y ↔ y ⤳ x := ⟨Specializes.symm, Specializes.symm⟩ +#align specializes_comm specializes_comm + +theorem specializes_iff_inseparable : x ⤳ y ↔ Inseparable x y := + ⟨fun h ↦ h.antisymm h.symm, Inseparable.specializes⟩ +#align specializes_iff_inseparable specializes_iff_inseparable + +/-- An R₁ space is an R₀ space: if `x` specializes `y`, then they are inseparable. -/ +alias ⟨Specializes.inseparable, _⟩ := specializes_iff_inseparable + +theorem disjoint_nhds_nhds_iff_not_inseparable : Disjoint (𝓝 x) (𝓝 y) ↔ ¬Inseparable x y := by + rw [disjoint_nhds_nhds_iff_not_specializes, specializes_iff_inseparable] + +theorem r1Space_iff_inseparable_or_disjoint_nhds {X : Type*} [TopologicalSpace X]: + R1Space X ↔ ∀ x y : X, Inseparable x y ∨ Disjoint (𝓝 x) (𝓝 y) := + ⟨fun _h x y ↦ (specializes_or_disjoint_nhds x y).imp_left Specializes.inseparable, fun h ↦ + ⟨fun x y ↦ (h x y).imp_left Inseparable.specializes⟩⟩ + +theorem isClosed_setOf_specializes : IsClosed { p : X × X | p.1 ⤳ p.2 } := by + simp only [← isOpen_compl_iff, compl_setOf, ← disjoint_nhds_nhds_iff_not_specializes, + isOpen_setOf_disjoint_nhds_nhds] +#align is_closed_set_of_specializes isClosed_setOf_specializes + +theorem isClosed_setOf_inseparable : IsClosed { p : X × X | Inseparable p.1 p.2 } := by + simp only [← specializes_iff_inseparable, isClosed_setOf_specializes] +#align is_closed_set_of_inseparable isClosed_setOf_inseparable + +/-- In a preregular space, a point belongs to the closure of a compact set `K` +if and only if it is topologically inseparable from some point of `K`. -/ +theorem IsCompact.mem_closure_iff_exists_inseparable {K : Set X} (hK : IsCompact K) : + y ∈ closure K ↔ ∃ x ∈ K, Inseparable x y := by + refine ⟨fun hy ↦ ?_, fun ⟨x, hxK, hxy⟩ ↦ + (hxy.mem_closed_iff isClosed_closure).1 <| subset_closure hxK⟩ + contrapose! hy + have : Disjoint (𝓝 y) (𝓝ˢ K) := hK.disjoint_nhdsSet_right.2 fun x hx ↦ + (disjoint_nhds_nhds_iff_not_inseparable.2 (hy x hx)).symm + simpa only [disjoint_iff, not_mem_closure_iff_nhdsWithin_eq_bot] + using this.mono_right principal_le_nhdsSet + +theorem IsCompact.closure_eq_biUnion_inseparable {K : Set X} (hK : IsCompact K) : + closure K = ⋃ x ∈ K, {y | Inseparable x y} := by + ext; simp [hK.mem_closure_iff_exists_inseparable] + +/-- In a preregular space, if a compact set `K` is contained in an open set `U`, +then its closure is also contained in `U`. -/ +theorem IsCompact.closure_subset_of_isOpen {K : Set X} (hK : IsCompact K) + {U : Set X} (hU : IsOpen U) (hKU : K ⊆ U) : closure K ⊆ U := by + rw [hK.closure_eq_biUnion_inseparable, iUnion₂_subset_iff] + exact fun x hx y hxy ↦ (hxy.mem_open_iff hU).1 (hKU hx) + +/-- The closure of a compact set in a preregular space is a compact set. -/ +protected theorem IsCompact.closure {K : Set X} (hK : IsCompact K) : IsCompact (closure K) := by + refine isCompact_of_finite_subcover fun U hUo hKU ↦ ?_ + rcases hK.elim_finite_subcover U hUo (subset_closure.trans hKU) with ⟨t, ht⟩ + exact ⟨t, hK.closure_subset_of_isOpen (isOpen_biUnion fun _ _ ↦ hUo _) ht⟩ + +theorem IsCompact.closure_of_subset {s K : Set X} (hK : IsCompact K) (h : s ⊆ K) : + IsCompact (closure s) := + hK.closure.of_isClosed_subset isClosed_closure (closure_mono h) +#align is_compact_closure_of_subset_compact IsCompact.closure_of_subset + +@[simp] +theorem exists_compact_superset_iff {s : Set X} : + (∃ K, IsCompact K ∧ s ⊆ K) ↔ IsCompact (closure s) := + ⟨fun ⟨_K, hK, hsK⟩ => hK.closure_of_subset hsK, fun h => ⟨closure s, h, subset_closure⟩⟩ +#align exists_compact_superset_iff exists_compact_superset_iff + +/-- If `K` and `L` are a disjoint compact set in a preregular topological space +and `L` is also closed, then `K` and `L` have disjoint neighborhoods. -/ +theorem SeparatedNhds.of_isCompact_isCompact_isClosed {K L : Set X} (hK : IsCompact K) + (hL : IsCompact L) (h'L : IsClosed L) (hd : Disjoint K L) : SeparatedNhds K L := by + simp_rw [separatedNhds_iff_disjoint, hK.disjoint_nhdsSet_left, hL.disjoint_nhdsSet_right, + disjoint_nhds_nhds_iff_not_inseparable] + intro x hx y hy h + exact absurd ((h.mem_closed_iff h'L).2 hy) <| disjoint_left.1 hd hx + +/-- If a compact set is covered by two open sets, then we can cover it by two compact subsets. -/ +theorem IsCompact.binary_compact_cover {K U V : Set X} + (hK : IsCompact K) (hU : IsOpen U) (hV : IsOpen V) (h2K : K ⊆ U ∪ V) : + ∃ K₁ K₂ : Set X, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂ := by + have hK' : IsCompact (closure K) := hK.closure + have : SeparatedNhds (closure K \ U) (closure K \ V) := by + apply SeparatedNhds.of_isCompact_isCompact_isClosed (hK'.diff hU) (hK'.diff hV) + (isClosed_closure.sdiff hV) + rw [disjoint_iff_inter_eq_empty, diff_inter_diff, diff_eq_empty] + exact hK.closure_subset_of_isOpen (hU.union hV) h2K + have : SeparatedNhds (K \ U) (K \ V) := + this.mono (diff_subset_diff_left (subset_closure)) (diff_subset_diff_left (subset_closure)) + rcases this with ⟨O₁, O₂, h1O₁, h1O₂, h2O₁, h2O₂, hO⟩ + exact ⟨K \ O₁, K \ O₂, hK.diff h1O₁, hK.diff h1O₂, diff_subset_comm.mp h2O₁, + diff_subset_comm.mp h2O₂, by rw [← diff_inter, hO.inter_eq, diff_empty]⟩ +#align is_compact.binary_compact_cover IsCompact.binary_compact_cover + +/-- For every finite open cover `Uᵢ` of a compact set, there exists a compact cover `Kᵢ ⊆ Uᵢ`. -/ +theorem IsCompact.finite_compact_cover {s : Set X} (hs : IsCompact s) {ι : Type*} + (t : Finset ι) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i) : + ∃ K : ι → Set X, (∀ i, IsCompact (K i)) ∧ (∀ i, K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i := by + induction' t using Finset.induction with x t hx ih generalizing U s + · refine' ⟨fun _ => ∅, fun _ => isCompact_empty, fun i => empty_subset _, _⟩ + simpa only [subset_empty_iff, Finset.not_mem_empty, iUnion_false, iUnion_empty] using hsC + simp only [Finset.set_biUnion_insert] at hsC + simp only [Finset.forall_mem_insert] at hU + have hU' : ∀ i ∈ t, IsOpen (U i) := fun i hi => hU.2 i hi + rcases hs.binary_compact_cover hU.1 (isOpen_biUnion hU') hsC with + ⟨K₁, K₂, h1K₁, h1K₂, h2K₁, h2K₂, hK⟩ + rcases ih h1K₂ U hU' h2K₂ with ⟨K, h1K, h2K, h3K⟩ + refine' ⟨update K x K₁, _, _, _⟩ + · intro i + rcases eq_or_ne i x with rfl | hi + · simp only [update_same, h1K₁] + · simp only [update_noteq hi, h1K] + · intro i + rcases eq_or_ne i x with rfl | hi + · simp only [update_same, h2K₁] + · simp only [update_noteq hi, h2K] + · simp only [Finset.set_biUnion_insert_update _ hx, hK, h3K] +#align is_compact.finite_compact_cover IsCompact.finite_compact_cover + +instance (priority := 900) {X Y : Type*} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] + [TopologicalSpace Y] [R1Space Y] : + LocallyCompactPair X Y where + exists_mem_nhds_isCompact_mapsTo := by + intro f x s hf hs + rcases exists_compact_mem_nhds x with ⟨K, hKc, hKx⟩ + have hc : IsCompact (f '' K \ interior s) := (hKc.image hf).diff isOpen_interior + obtain ⟨U, V, Uo, Vo, hxU, hV, hd⟩ : SeparatedNhds {f x} (f '' K \ interior s) := by + simp_rw [separatedNhds_iff_disjoint, nhdsSet_singleton, hc.disjoint_nhdsSet_right, + disjoint_nhds_nhds_iff_not_inseparable] + rintro y ⟨-, hys⟩ hxy + refine hys <| (hxy.mem_open_iff isOpen_interior).1 ?_ + rwa [mem_interior_iff_mem_nhds] + refine ⟨K \ f ⁻¹' V, diff_mem hKx ?_, hKc.diff <| Vo.preimage hf, fun y hy ↦ ?_⟩ + · filter_upwards [hf.continuousAt <| Uo.mem_nhds (hxU rfl)] with x hx + using Set.disjoint_left.1 hd hx + · by_contra hys + exact hy.2 (hV ⟨mem_image_of_mem _ hy.1, not_mem_subset interior_subset hys⟩) + +variable [WeaklyLocallyCompactSpace X] + +-- see Note [lower instance priority] +/-- A weakly locally compact preregular space is locally compact. -/ +instance (priority := 80) WeaklyLocallyCompactSpace.locallyCompactSpace : + LocallyCompactSpace X where + local_compact_nhds _x _s hs := + let ⟨K, hKx, hKc, hKs⟩ := exists_mem_nhds_isCompact_mapsTo continuous_id hs + ⟨K, hKx, hKs, hKc⟩ +#align locally_compact_of_compact_nhds WeaklyLocallyCompactSpace.locallyCompactSpace + +/-- In a locally compact R₁ space, compact closed neighborhoods of a point `x` +form a basis of neighborhoods of `x`. -/ +theorem isCompact_isClosed_basis_nhds (x : X) : + (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsCompact s ∧ IsClosed s) (·) := + hasBasis_self.2 fun _U hU ↦ + let ⟨K, hxK, hKU, hKc⟩ := local_compact_nhds <| interior_mem_nhds.2 hU + ⟨closure K, mem_of_superset hxK subset_closure, ⟨hKc.closure, isClosed_closure⟩, + (hKc.closure_subset_of_isOpen isOpen_interior hKU).trans interior_subset⟩ + +/-- In a weakly locally compact space which is either T₂ or locally compact regular, +every compact set has an open neighborhood with compact closure. -/ +theorem exists_open_superset_and_isCompact_closure {K : Set X} (hK : IsCompact K) : + ∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V) := by + rcases exists_compact_superset hK with ⟨K', hK', hKK'⟩ + exact ⟨interior K', isOpen_interior, hKK', hK'.closure_of_subset interior_subset⟩ +#align exists_open_superset_and_is_compact_closure exists_open_superset_and_isCompact_closure + +/-- In a weakly locally compact which is either T₂ or locally compact regular, +every point has an open neighborhood with compact closure. -/ +theorem exists_open_with_compact_closure (x : X) : + ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U) := by + simpa only [singleton_subset_iff] + using exists_open_superset_and_isCompact_closure isCompact_singleton +#align exists_open_with_compact_closure exists_open_with_compact_closure + +end R1Space + /-- A T₂ space, also known as a Hausdorff space, is one in which for every `x ≠ y` there exists disjoint open sets around `x` and `y`. This is the most widely used of the separation axioms. -/ @@ -953,22 +1155,24 @@ theorem Set.Finite.t2_separation [T2Space X] {s : Set X} (hs : s.Finite) : s.pairwiseDisjoint_nhds.exists_mem_filter_basis hs nhds_basis_opens #align set.finite.t2_separation Set.Finite.t2_separation -theorem isOpen_setOf_disjoint_nhds_nhds : IsOpen { p : X × X | Disjoint (𝓝 p.1) (𝓝 p.2) } := by - simp only [isOpen_iff_mem_nhds, Prod.forall, mem_setOf_eq] - intro x y h - obtain ⟨U, hU, V, hV, hd⟩ := ((nhds_basis_opens x).disjoint_iff (nhds_basis_opens y)).mp h - exact - mem_nhds_prod_iff.mpr - ⟨U, hU.2.mem_nhds hU.1, V, hV.2.mem_nhds hV.1, fun ⟨x', y'⟩ ⟨hx', hy'⟩ => - disjoint_of_disjoint_of_mem hd (hU.2.mem_nhds hx') (hV.2.mem_nhds hy')⟩ -#align is_open_set_of_disjoint_nhds_nhds isOpen_setOf_disjoint_nhds_nhds - -- see Note [lower instance priority] instance (priority := 100) T2Space.t1Space [T2Space X] : T1Space X := t1Space_iff_disjoint_pure_nhds.mpr fun _ _ hne => (disjoint_nhds_nhds.2 hne).mono_left <| pure_le_nhds _ #align t2_space.t1_space T2Space.t1Space +-- see Note [lower instance priority] +instance (priority := 100) T2Space.r1Space [T2Space X] : R1Space X := + ⟨fun x y ↦ (eq_or_ne x y).imp specializes_of_eq disjoint_nhds_nhds.2⟩ + +theorem SeparationQuotient.t2Space_iff : T2Space (SeparationQuotient X) ↔ R1Space X := by + simp only [t2Space_iff_disjoint_nhds, Pairwise, surjective_mk.forall₂, ne_eq, mk_eq_mk, + r1Space_iff_inseparable_or_disjoint_nhds, ← disjoint_comap_iff surjective_mk, comap_mk_nhds_mk, + ← or_iff_not_imp_left] + +instance SeparationQuotient.t2Space [R1Space X] : T2Space (SeparationQuotient X) := + t2Space_iff.2 ‹_› + /-- A space is T₂ iff the neighbourhoods of distinct points generate the bottom filter. -/ theorem t2_iff_nhds : T2Space X ↔ ∀ {x y : X}, NeBot (𝓝 x ⊓ 𝓝 y) → x = y := by simp only [t2Space_iff_disjoint_nhds, disjoint_iff, neBot_iff, Ne.def, not_imp_comm, Pairwise] @@ -1197,7 +1401,6 @@ Hausdorff spaces: We use this lemma to prove that topological spaces defined using `coinduced` are Hausdorff spaces. -/ - -- see Note [lower instance priority] instance (priority := 100) DiscreteTopology.toT2Space [DiscreteTopology X] : T2Space X := @@ -1335,18 +1538,17 @@ theorem Function.LeftInverse.closedEmbedding [T2Space X] {f : X → Y} {g : Y ⟨h.embedding hf hg, h.closed_range hf hg⟩ #align function.left_inverse.closed_embedding Function.LeftInverse.closedEmbedding -theorem separatedNhds_of_isCompact_isCompact [T2Space X] {s t : Set X} (hs : IsCompact s) +theorem SeparatedNhds.of_isCompact_isCompact [T2Space X] {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) (hst : Disjoint s t) : SeparatedNhds s t := by simp only [SeparatedNhds, prod_subset_compl_diagonal_iff_disjoint.symm] at hst ⊢ exact generalized_tube_lemma hs ht isClosed_diagonal.isOpen_compl hst -#align is_compact_is_compact_separated separatedNhds_of_isCompact_isCompact +#align is_compact_is_compact_separated SeparatedNhds.of_isCompact_isCompact section SeparatedFinset theorem separatedNhds_of_finset_finset [T2Space X] (s t : Finset X) (h : Disjoint s t) : SeparatedNhds (s : Set X) t := - separatedNhds_of_isCompact_isCompact s.finite_toSet.isCompact t.finite_toSet.isCompact - <| mod_cast h + .of_isCompact_isCompact s.finite_toSet.isCompact t.finite_toSet.isCompact <| mod_cast h #align finset_disjoint_finset_opens_of_t2 separatedNhds_of_finset_finset theorem point_disjoint_finset_opens_of_t2 [T2Space X] {x : X} {s : Finset X} (h : x ∉ s) : @@ -1360,7 +1562,7 @@ end SeparatedFinset theorem IsCompact.isClosed [T2Space X] {s : Set X} (hs : IsCompact s) : IsClosed s := isOpen_compl_iff.1 <| isOpen_iff_forall_mem_open.mpr fun x hx => let ⟨u, v, _, vo, su, xv, uv⟩ := - separatedNhds_of_isCompact_isCompact hs isCompact_singleton (disjoint_singleton_right.2 hx) + SeparatedNhds.of_isCompact_isCompact hs isCompact_singleton (disjoint_singleton_right.2 hx) ⟨v, (uv.mono_left <| show s ≤ u from su).subset_compl_left, vo, by simpa using xv⟩ #align is_compact.is_closed IsCompact.isClosed @@ -1422,21 +1624,6 @@ theorem QuotientMap.of_surjective_continuous [CompactSpace X] [T2Space Y] {f : X hcont.isClosedMap.to_quotientMap hcont hsurj #align quotient_map.of_surjective_continuous QuotientMap.of_surjective_continuous -instance (priority := 900) [WeaklyLocallyCompactSpace X] [T2Space Y] : LocallyCompactPair X Y where - exists_mem_nhds_isCompact_mapsTo := by - intro f x s hf hs - rcases exists_compact_mem_nhds x with ⟨K, hKc, hKx⟩ - have hc : IsCompact (f '' K \ interior s) := (hKc.image hf).diff isOpen_interior - have hd : Disjoint {f x} (f '' K \ interior s) := disjoint_singleton_left.2 fun h ↦ - h.2 <| mem_interior_iff_mem_nhds.2 hs - rcases separatedNhds_of_isCompact_isCompact isCompact_singleton hc hd - with ⟨U, V, Uo, Vo, hxU, hV, hd⟩ - refine ⟨K \ f ⁻¹' V, diff_mem hKx ?_, hKc.diff <| Vo.preimage hf, fun y hy ↦ ?_⟩ - · filter_upwards [hf.continuousAt <| Uo.mem_nhds (hxU rfl)] with x hx - using Set.disjoint_left.1 hd hx - · by_contra hys - exact hy.2 (hV ⟨mem_image_of_mem _ hy.1, not_mem_subset interior_subset hys⟩) - theorem isPreirreducible_iff_subsingleton [T2Space X] {S : Set X} : IsPreirreducible S ↔ S.Subsingleton := by refine' ⟨fun h x hx y hy => _, Set.Subsingleton.isPreirreducible⟩ @@ -1525,11 +1712,9 @@ theorem RegularSpace.ofExistsMemNhdsIsClosedSubset Iff.mpr ((regularSpace_TFAE X).out 0 3) h #align regular_space.of_exists_mem_nhds_is_closed_subset RegularSpace.ofExistsMemNhdsIsClosedSubset -/-- A locally compact T2 space is regular. -/ -instance (priority := 100) [LocallyCompactSpace X] [T2Space X] : RegularSpace X := by - apply RegularSpace.ofExistsMemNhdsIsClosedSubset (fun x s hx ↦ ?_) - rcases local_compact_nhds hx with ⟨k, kx, ks, hk⟩ - exact ⟨k, kx, hk.isClosed, ks⟩ +/-- A weakly locally compact R₁ space is regular. -/ +instance (priority := 100) [WeaklyLocallyCompactSpace X] [R1Space X] : RegularSpace X := + .ofBasis isCompact_isClosed_basis_nhds fun _ _ ⟨_, _, h⟩ ↦ h variable [RegularSpace X] {x : X} {s : Set X} @@ -1542,6 +1727,11 @@ theorem disjoint_nhds_nhdsSet : Disjoint (𝓝 x) (𝓝ˢ s) ↔ x ∉ closure s disjoint_comm.trans disjoint_nhdsSet_nhds #align disjoint_nhds_nhds_set disjoint_nhds_nhdsSet +/-- A regular space is preregular. -/ +instance (priority := 100) : R1Space X where + specializes_or_disjoint_nhds _ _ := or_iff_not_imp_left.2 fun h ↦ by + rwa [← nhdsSet_singleton, disjoint_nhdsSet_nhds, ← specializes_iff_mem_closure] + theorem exists_mem_nhds_isClosed_subset {x : X} {s : Set X} (h : s ∈ 𝓝 x) : ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s := by have h' := (regularSpace_TFAE X).out 0 3 @@ -1581,30 +1771,6 @@ theorem TopologicalSpace.IsTopologicalBasis.exists_closure_subset {B : Set (Set simpa only [exists_prop, and_assoc] using hB.nhds_hasBasis.nhds_closure.mem_iff.mp h #align topological_space.is_topological_basis.exists_closure_subset TopologicalSpace.IsTopologicalBasis.exists_closure_subset -theorem disjoint_nhds_nhds_iff_not_specializes {a b : X} : Disjoint (𝓝 a) (𝓝 b) ↔ ¬a ⤳ b := by - rw [← nhdsSet_singleton, disjoint_nhdsSet_nhds, specializes_iff_mem_closure] -#align disjoint_nhds_nhds_iff_not_specializes disjoint_nhds_nhds_iff_not_specializes - -theorem specializes_comm {a b : X} : a ⤳ b ↔ b ⤳ a := by - simp only [← (disjoint_nhds_nhds_iff_not_specializes (X := X)).not_left, disjoint_comm] -#align specializes_comm specializes_comm - -alias ⟨Specializes.symm, _⟩ := specializes_comm -#align specializes.symm Specializes.symm - -theorem specializes_iff_inseparable {a b : X} : a ⤳ b ↔ Inseparable a b := - ⟨fun h => h.antisymm h.symm, le_of_eq⟩ -#align specializes_iff_inseparable specializes_iff_inseparable - -theorem isClosed_setOf_specializes : IsClosed { p : X × X | p.1 ⤳ p.2 } := by - simp only [← isOpen_compl_iff, compl_setOf, ← disjoint_nhds_nhds_iff_not_specializes, - isOpen_setOf_disjoint_nhds_nhds] -#align is_closed_set_of_specializes isClosed_setOf_specializes - -theorem isClosed_setOf_inseparable : IsClosed { p : X × X | Inseparable p.1 p.2 } := by - simp only [← specializes_iff_inseparable, isClosed_setOf_specializes] -#align is_closed_set_of_inseparable isClosed_setOf_inseparable - protected theorem Inducing.regularSpace [TopologicalSpace Y] {f : Y → X} (hf : Inducing f) : RegularSpace Y := RegularSpace.ofBasis @@ -1656,78 +1822,12 @@ instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, neighborhoods. -/ lemma separatedNhds_of_isCompact_isClosed [RegularSpace X] {s t : Set X} (hs : IsCompact s) (ht : IsClosed t) (hst : Disjoint s t) : SeparatedNhds s t := by - apply hs.induction_on (p := fun u ↦ SeparatedNhds u t) - · simp - · intro s u su hu - exact hu.mono su Subset.rfl - · intro u v hu hv - exact hu.union_left hv - · intro x hx - have : tᶜ ∈ 𝓝 x := ht.isOpen_compl.mem_nhds (disjoint_left.1 hst hx) - rcases exists_mem_nhds_isClosed_subset this with ⟨u, u_mem, u_closed, hu⟩ - refine ⟨interior u, mem_nhdsWithin_of_mem_nhds (interior_mem_nhds.2 u_mem), ?_⟩ - exact ⟨interior u, uᶜ, isOpen_interior, u_closed.isOpen_compl, Subset.rfl, - subset_compl_comm.mp hu, disjoint_compl_right.mono_left (interior_subset)⟩ + simpa only [separatedNhds_iff_disjoint, hs.disjoint_nhdsSet_left, disjoint_nhds_nhdsSet, + ht.closure_eq, disjoint_left] using hst end RegularSpace -section T2OrLocallyCompactRegularSpace - -/-- A topological space which is either T2 or locally compact regular. Equivalent to regularity -among locally compact spaces. These two classes share the properties that are needed to develop a -lot of measure theory, so it's worth defining a single class to avoid developing things twice. -/ -class T2OrLocallyCompactRegularSpace (X : Type*) [TopologicalSpace X] : Prop := - out : T2Space X ∨ (LocallyCompactSpace X ∧ RegularSpace X) - -instance (priority := 100) [h : T2Space X] : T2OrLocallyCompactRegularSpace X := ⟨Or.inl h⟩ -instance (priority := 100) [h : LocallyCompactSpace X] [h' : RegularSpace X] : - T2OrLocallyCompactRegularSpace X := ⟨Or.inr ⟨h, h'⟩⟩ - -/-- A locally compact space which is T2 or locally comapct regular is regular. Not an instance, as -one should instead assume `LocallyCompactSpace X` and `RegularSpace X`. -/ -theorem RegularSpace.ofT2SpaceOrRegularSpace - [LocallyCompactSpace X] [h : T2OrLocallyCompactRegularSpace X] : RegularSpace X := by - rcases h.out with h'|⟨-, h'⟩ <;> infer_instance - -/-- In a space which is T2 or locally compact regular, if a compact set `s` is contained in an -open set `u`, then its closure is also contained in `u`. -/ -theorem IsCompact.closure_subset_of_isOpen [hX : T2OrLocallyCompactRegularSpace X] - {s : Set X} (hs : IsCompact s) {u : Set X} (hu : IsOpen u) (h : s ⊆ u) : - closure s ⊆ u := by - rcases hX.out with h'|⟨-, h'⟩ - · rwa [hs.isClosed.closure_eq] - obtain ⟨F, sF, F_closed, Fu⟩ : ∃ F, s ⊆ F ∧ IsClosed F ∧ F ⊆ u := by - apply hs.induction_on (p := fun t ↦ ∃ F, t ⊆ F ∧ IsClosed F ∧ F ⊆ u) - · exact ⟨∅, by simp⟩ - · intro t' t ht't ⟨F, tF, F_closed, Fu⟩ - exact ⟨F, ht't.trans tF, F_closed, Fu⟩ - · intro t t' ⟨F, tF, F_closed, Fu⟩ ⟨F', t'F', F'_closed, F'u⟩ - exact ⟨F ∪ F', union_subset_union tF t'F', F_closed.union F'_closed, union_subset Fu F'u⟩ - · intro x hx - rcases exists_mem_nhds_isClosed_subset (hu.mem_nhds (h hx)) with ⟨F, F_mem, F_closed, Fu⟩ - exact ⟨F, nhdsWithin_le_nhds F_mem, F, Subset.rfl, F_closed, Fu⟩ - exact (closure_minimal sF F_closed).trans Fu - -theorem separatedNhds_of_isCompact_isCompact_isClosed [hX : T2OrLocallyCompactRegularSpace X] - {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) (h't : IsClosed t) - (hst : Disjoint s t) : SeparatedNhds s t := by - rcases hX.out with h'|⟨-, h'⟩ - · exact separatedNhds_of_isCompact_isCompact hs ht hst - · exact separatedNhds_of_isCompact_isClosed hs h't hst - -protected theorem IsCompact.closure [hX : T2OrLocallyCompactRegularSpace X] - {K : Set X} (hK : IsCompact K) : IsCompact (closure K) := by - rcases hX.out with h'|⟨h', -⟩ - · rwa [hK.isClosed.closure_eq] - rcases exists_compact_superset hK with ⟨L, L_comp, hL⟩ - exact L_comp.of_isClosed_subset isClosed_closure - ((hK.closure_subset_of_isOpen isOpen_interior hL).trans interior_subset) - -theorem isCompact_closure_of_subset_compact [T2OrLocallyCompactRegularSpace X] - {s t : Set X} (ht : IsCompact t) - (h : s ⊆ t) : IsCompact (closure s) := - ht.closure.of_isClosed_subset isClosed_closure (closure_mono h) -#align is_compact_closure_of_subset_compact isCompact_closure_of_subset_compact +section LocallyCompactRegularSpace /-- In a (possibly non-Hausdorff) locally compact regular space, for every containment `K ⊆ U` of a compact set `K` in an open set `U`, there is a compact closed neighborhood `L` @@ -1735,18 +1835,10 @@ theorem isCompact_closure_of_subset_compact [T2OrLocallyCompactRegularSpace X] that `K ⊆ interior L` and `L ⊆ U`. -/ theorem exists_compact_closed_between [LocallyCompactSpace X] [RegularSpace X] {K U : Set X} (hK : IsCompact K) (hU : IsOpen U) (h_KU : K ⊆ U) : - ∃ L, IsCompact L ∧ IsClosed L ∧ K ⊆ interior L ∧ L ⊆ U := by - rcases exists_compact_between hK hU h_KU with ⟨L, L_comp, KL, LU⟩ - rcases exists_compact_between hK isOpen_interior KL with ⟨M, M_comp, KM, ML⟩ - refine ⟨closure M, ?_, isClosed_closure, ?_, ?_⟩ - · have : closure M ∩ L = closure M := by - apply inter_eq_self_of_subset_left - exact (M_comp.closure_subset_of_isOpen isOpen_interior ML).trans interior_subset - rw [← this] - apply L_comp.inter_left isClosed_closure - · exact KM.trans (interior_mono subset_closure) - · apply M_comp.closure_subset_of_isOpen hU - exact ML.trans (interior_subset.trans LU) + ∃ L, IsCompact L ∧ IsClosed L ∧ K ⊆ interior L ∧ L ⊆ U := + let ⟨L, L_comp, KL, LU⟩ := exists_compact_between hK hU h_KU + ⟨closure L, L_comp.closure, isClosed_closure, KL.trans <| interior_mono subset_closure, + L_comp.closure_subset_of_isOpen hU LU⟩ /-- In a locally compact regular space, given a compact set `K` inside an open set `U`, we can find an open set `V` between these sets with compact closure: `K ⊆ V` and the closure of `V` is @@ -1758,99 +1850,16 @@ theorem exists_open_between_and_isCompact_closure [LocallyCompactSpace X] [Regul have A : closure (interior L) ⊆ L := by apply (closure_mono interior_subset).trans (le_of_eq L_closed.closure_eq) refine ⟨interior L, isOpen_interior, KL, A.trans LU, ?_⟩ - exact isCompact_closure_of_subset_compact L_compact interior_subset + exact L_compact.closure_of_subset interior_subset #align exists_open_between_and_is_compact_closure exists_open_between_and_isCompact_closure -@[simp] -theorem exists_compact_superset_iff [T2OrLocallyCompactRegularSpace X] {s : Set X} : - (∃ K, IsCompact K ∧ s ⊆ K) ↔ IsCompact (closure s) := - ⟨fun ⟨_K, hK, hsK⟩ => isCompact_closure_of_subset_compact hK hsK, fun h => - ⟨closure s, h, subset_closure⟩⟩ -#align exists_compact_superset_iff exists_compact_superset_iff - -/-- In a weakly locally compact space which is either T₂ or locally compact regular, -every compact set has an open neighborhood with compact closure. -/ -theorem exists_open_superset_and_isCompact_closure - [WeaklyLocallyCompactSpace X] [T2OrLocallyCompactRegularSpace X] - {K : Set X} (hK : IsCompact K) : ∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V) := by - rcases exists_compact_superset hK with ⟨K', hK', hKK'⟩ - exact ⟨interior K', isOpen_interior, hKK', - isCompact_closure_of_subset_compact hK' interior_subset⟩ -#align exists_open_superset_and_is_compact_closure exists_open_superset_and_isCompact_closure - -/-- In a weakly locally compact which is either T₂ or locally compact regular, -every point has an open neighborhood with compact closure. -/ -theorem exists_open_with_compact_closure - [WeaklyLocallyCompactSpace X] [T2OrLocallyCompactRegularSpace X] (x : X) : - ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U) := by - simpa only [singleton_subset_iff] - using exists_open_superset_and_isCompact_closure isCompact_singleton -#align exists_open_with_compact_closure exists_open_with_compact_closure - --- see Note [lower instance priority] -/-- A weakly locally compact Hausdorff space is locally compact. -/ -instance (priority := 80) WeaklyLocallyCompactSpace.locallyCompactSpace - [WeaklyLocallyCompactSpace X] [hX : T2OrLocallyCompactRegularSpace X] : - LocallyCompactSpace X := by - rcases hX.out with h'X|⟨h'X, -⟩ - · exact ⟨fun _ _ h => - let ⟨K, hKx, hKc, hKs⟩ := exists_mem_nhds_isCompact_mapsTo continuous_id h - ⟨K, hKx, hKs, hKc⟩⟩ - · exact h'X -#align locally_compact_of_compact_nhds WeaklyLocallyCompactSpace.locallyCompactSpace - -@[deprecated WeaklyLocallyCompactSpace.locallyCompactSpace] +@[deprecated WeaklyLocallyCompactSpace.locallyCompactSpace] -- 3 Sep 2023 theorem locally_compact_of_compact [T2Space X] [CompactSpace X] : LocallyCompactSpace X := inferInstance #align locally_compact_of_compact locally_compact_of_compact -/-- If a compact set is covered by two open sets, then we can cover it by two compact subsets. -/ -theorem IsCompact.binary_compact_cover [T2OrLocallyCompactRegularSpace X] {K U V : Set X} - (hK : IsCompact K) (hU : IsOpen U) (hV : IsOpen V) (h2K : K ⊆ U ∪ V) : - ∃ K₁ K₂ : Set X, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂ := by - have hK' : IsCompact (closure K) := hK.closure - have : SeparatedNhds (closure K \ U) (closure K \ V) := by - apply separatedNhds_of_isCompact_isCompact_isClosed (hK'.diff hU) (hK'.diff hV) - (isClosed_closure.sdiff hV) - rw [disjoint_iff_inter_eq_empty, diff_inter_diff, diff_eq_empty] - exact hK.closure_subset_of_isOpen (hU.union hV) h2K - have : SeparatedNhds (K \ U) (K \ V) := - this.mono (diff_subset_diff_left (subset_closure)) (diff_subset_diff_left (subset_closure)) - rcases this with ⟨O₁, O₂, h1O₁, h1O₂, h2O₁, h2O₂, hO⟩ - exact ⟨K \ O₁, K \ O₂, hK.diff h1O₁, hK.diff h1O₂, diff_subset_comm.mp h2O₁, - diff_subset_comm.mp h2O₂, by rw [← diff_inter, hO.inter_eq, diff_empty]⟩ -#align is_compact.binary_compact_cover IsCompact.binary_compact_cover - -open Finset Function - -/-- For every finite open cover `Uᵢ` of a compact set, there exists a compact cover `Kᵢ ⊆ Uᵢ`. -/ -theorem IsCompact.finite_compact_cover [T2OrLocallyCompactRegularSpace X] - {s : Set X} (hs : IsCompact s) {ι} - (t : Finset ι) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i) : - ∃ K : ι → Set X, (∀ i, IsCompact (K i)) ∧ (∀ i, K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i := by - induction' t using Finset.induction with x t hx ih generalizing U s - · refine' ⟨fun _ => ∅, fun _ => isCompact_empty, fun i => empty_subset _, _⟩ - simpa only [subset_empty_iff, Finset.not_mem_empty, iUnion_false, iUnion_empty] using hsC - simp only [Finset.set_biUnion_insert] at hsC - simp only [Finset.forall_mem_insert] at hU - have hU' : ∀ i ∈ t, IsOpen (U i) := fun i hi => hU.2 i hi - rcases hs.binary_compact_cover hU.1 (isOpen_biUnion hU') hsC with - ⟨K₁, K₂, h1K₁, h1K₂, h2K₁, h2K₂, hK⟩ - rcases ih h1K₂ U hU' h2K₂ with ⟨K, h1K, h2K, h3K⟩ - refine' ⟨update K x K₁, _, _, _⟩ - · intro i - rcases eq_or_ne i x with rfl | hi - · simp only [update_same, h1K₁] - · simp only [update_noteq hi, h1K] - · intro i - rcases eq_or_ne i x with rfl | hi - · simp only [update_same, h2K₁] - · simp only [update_noteq hi, h2K] - · simp only [set_biUnion_insert_update _ hx, hK, h3K] -#align is_compact.finite_compact_cover IsCompact.finite_compact_cover - -end T2OrLocallyCompactRegularSpace +end LocallyCompactRegularSpace section T3 @@ -1948,7 +1957,13 @@ protected theorem ClosedEmbedding.normalSpace [TopologicalSpace Y] [NormalSpace (disjoint_image_of_injective hf.inj hst) exact (H.preimage hf.continuous).mono (subset_preimage_image _ _) (subset_preimage_image _ _) -/-- A regular topological space with second countable topology is a normal space. -/ +instance (priority := 100) NormalSpace.of_compactSpace_r1Space [CompactSpace X] [R1Space X] : + NormalSpace X where + normal _s _t hs ht := .of_isCompact_isCompact_isClosed hs.isCompact ht.isCompact ht + +/-- A regular topological space with second countable topology is a normal space. + +TODO: The same is true for a regular Lindelöf space. -/ instance (priority := 100) NormalSpace.of_regularSpace_secondCountableTopology [RegularSpace X] [SecondCountableTopology X] : NormalSpace X := by have key : ∀ {s t : Set X}, IsClosed t → Disjoint s t → @@ -2009,9 +2024,9 @@ instance (priority := 100) T4Space.t3Space [T4Space X] : T3Space X where (disjoint_singleton_right.mpr hxs)).disjoint_nhdsSet #align normal_space.t3_space T4Space.t3Space -instance (priority := 100) T4Space.of_compactSpace_t2Space [CompactSpace X] [T2Space X] : - T4Space X where - normal _s _t hs ht := separatedNhds_of_isCompact_isCompact hs.isCompact ht.isCompact +@[deprecated inferInstance] +theorem T4Space.of_compactSpace_t2Space [CompactSpace X] [T2Space X] : + T4Space X := inferInstance #align normal_of_compact_t2 T4Space.of_compactSpace_t2Space /-- If the codomain of a closed embedding is a T₄ space, then so is the domain. -/ diff --git a/Mathlib/Topology/Support.lean b/Mathlib/Topology/Support.lean index 6d83396d49e83..7a014fdcf589b 100644 --- a/Mathlib/Topology/Support.lean +++ b/Mathlib/Topology/Support.lean @@ -189,9 +189,9 @@ theorem intro' {K : Set α} (hK : IsCompact K) (h'K : IsClosed K) exact IsCompact.of_isClosed_subset hK ( isClosed_mulTSupport f) this @[to_additive] -theorem of_mulSupport_subset_isCompact [T2Space α] {K : Set α} +theorem of_mulSupport_subset_isCompact [R1Space α] {K : Set α} (hK : IsCompact K) (h : mulSupport f ⊆ K) : HasCompactMulSupport f := - isCompact_closure_of_subset_compact hK h + hK.closure_of_subset h @[to_additive] theorem isCompact (hf : HasCompactMulSupport f) : IsCompact (mulTSupport f) := From 0338d0ec5cb6b2186c24c0cac35f7ce2e12df4d6 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 28 Jan 2024 08:59:12 -0600 Subject: [PATCH 02/16] Snapshot --- .../Analysis/NormedSpace/CompactOperator.lean | 4 +- .../Analysis/NormedSpace/OperatorNorm.lean | 2 +- .../Constructions/BorelSpace/Basic.lean | 24 ++++++++++ Mathlib/MeasureTheory/Group/Measure.lean | 5 +-- Mathlib/MeasureTheory/Measure/Content.lean | 11 +++-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean | 2 +- Mathlib/MeasureTheory/Measure/Regular.lean | 45 +++++++++---------- 7 files changed, 57 insertions(+), 36 deletions(-) diff --git a/Mathlib/Analysis/NormedSpace/CompactOperator.lean b/Mathlib/Analysis/NormedSpace/CompactOperator.lean index 29fe55bc5ab36..f22aac970f2dd 100644 --- a/Mathlib/Analysis/NormedSpace/CompactOperator.lean +++ b/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 diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm.lean index bd2947b2c63cc..e5f2b63d3bd03 100644 --- a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean +++ b/Mathlib/Analysis/NormedSpace/OperatorNorm.lean @@ -1576,7 +1576,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 diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean index 7431d3b04eeb5..d15ce51074598 100644 --- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean +++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean @@ -362,6 +362,30 @@ theorem IsCompact.measurableSet [T2Space α] (h : IsCompact s) : MeasurableSet s h.isClosed.measurableSet #align is_compact.measurable_set IsCompact.measurableSet +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] + +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 a preregular 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 diff --git a/Mathlib/MeasureTheory/Group/Measure.lean b/Mathlib/MeasureTheory/Group/Measure.lean index 7d9619a37a4e3..9b3fb862a70bc 100644 --- a/Mathlib/MeasureTheory/Group/Measure.lean +++ b/Mathlib/MeasureTheory/Group/Measure.lean @@ -762,9 +762,8 @@ lemma _root_.MeasurableSet.mul_closure_one_eq {s : Set G} (hs : MeasurableSet s) /-- If a compact set is included in a measurable set, then so is its closure. -/ @[to_additive] 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) : diff --git a/Mathlib/MeasureTheory/Measure/Content.lean b/Mathlib/MeasureTheory/Measure/Content.lean index 435c5b18afab4..532d2bcfada82 100644 --- a/Mathlib/MeasureTheory/Measure/Content.lean +++ b/Mathlib/MeasureTheory/Measure/Content.lean @@ -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. -/ diff --git a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean index 9cac921156f24..de2ad8a80a3d5 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean @@ -485,7 +485,7 @@ 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₁⟩ diff --git a/Mathlib/MeasureTheory/Measure/Regular.lean b/Mathlib/MeasureTheory/Measure/Regular.lean index 96d8e09144bdf..6c4beb19561e9 100644 --- a/Mathlib/MeasureTheory/Measure/Regular.lean +++ b/Mathlib/MeasureTheory/Measure/Regular.lean @@ -319,14 +319,13 @@ class InnerRegularCompactLTTop (μ : Measure α) : Prop where protected innerRegular : InnerRegularWRT μ IsCompact (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞) -- see Note [lower instance priority] -/-- A regular measure is weakly regular in a T2 space or in a regular space. -/ -instance (priority := 100) Regular.weaklyRegular [T2OrLocallyCompactRegularSpace α] [Regular μ] : - WeaklyRegular μ := by - constructor - intro U hU r hr - rcases Regular.innerRegular hU r hr with ⟨K, KU, K_comp, hK⟩ - exact ⟨closure K, K_comp.closure_subset_of_isOpen hU KU, isClosed_closure, - hK.trans_le (measure_mono subset_closure)⟩ +/-- A regular measure is weakly regular in a preregular space. -/ +instance (priority := 100) Regular.weaklyRegular [R1Space α] [Regular μ] : + WeaklyRegular μ where + innerRegular := fun _U hU r hr ↦ + let ⟨K, KU, K_comp, hK⟩ := Regular.innerRegular hU r hr + ⟨closure K, K_comp.closure_subset_of_isOpen hU KU, isClosed_closure, + hK.trans_le (measure_mono subset_closure)⟩ #align measure_theory.measure.regular.weakly_regular MeasureTheory.Measure.Regular.weaklyRegular namespace OuterRegular @@ -438,7 +437,9 @@ lemma of_restrict [OpensMeasurableSpace α] {μ : Measure α} {s : ℕ → Set _ = μ (⋃ n, A n) + ∑' n, δ n := (congr_arg₂ (· + ·) (measure_iUnion hAd hAm).symm rfl) _ < r := hδε -lemma measure_closure_eq_of_isCompact [T2OrLocallyCompactRegularSpace α] [OuterRegular μ] +/-- See also `IsCompact.measure_closure` for a version +that assumes the `σ`-algebra to be the Borel `σ`-algebra but makes no assumptions on `μ`. -/ +lemma measure_closure_eq_of_isCompact [R1Space α] [OuterRegular μ] {k : Set α} (hk : IsCompact k) : μ (closure k) = μ k := by apply le_antisymm ?_ (measure_mono subset_closure) simp only [measure_eq_iInf_isOpen k, le_iInf_iff] @@ -672,8 +673,8 @@ instance smul_nnreal [InnerRegular μ] (c : ℝ≥0) : InnerRegular (c • μ) : instance (priority := 100) [InnerRegular μ] : InnerRegularCompactLTTop μ := ⟨fun _s hs r hr ↦ InnerRegular.innerRegular hs.1 r hr⟩ -lemma innerRegularWRT_isClosed_isOpen [T2OrLocallyCompactRegularSpace α] [OpensMeasurableSpace α] - [h : InnerRegular μ] : InnerRegularWRT μ IsClosed IsOpen := by +lemma innerRegularWRT_isClosed_isOpen [R1Space α] [OpensMeasurableSpace α] [h : InnerRegular μ] : + InnerRegularWRT μ IsClosed IsOpen := by intro U hU r hr rcases h.innerRegular hU.measurableSet r hr with ⟨K, KU, K_comp, hK⟩ exact ⟨closure K, K_comp.closure_subset_of_isOpen hU KU, isClosed_closure, @@ -766,20 +767,18 @@ instance (priority := 50) [h : InnerRegularCompactLTTop μ] [IsFiniteMeasure μ] convert h.innerRegular with s simp [measure_ne_top μ s] -instance (priority := 50) [BorelSpace α] [T2OrLocallyCompactRegularSpace α] - [InnerRegularCompactLTTop μ] [IsFiniteMeasure μ] : WeaklyRegular μ := by - apply InnerRegularWRT.weaklyRegular_of_finite - exact InnerRegular.innerRegularWRT_isClosed_isOpen +instance (priority := 50) [BorelSpace α] [R1Space α] [InnerRegularCompactLTTop μ] + [IsFiniteMeasure μ] : WeaklyRegular μ := + InnerRegular.innerRegularWRT_isClosed_isOpen.weaklyRegular_of_finite _ -instance (priority := 50) [BorelSpace α] [T2OrLocallyCompactRegularSpace α] - [h : InnerRegularCompactLTTop μ] [IsFiniteMeasure μ] : Regular μ := by - constructor - apply InnerRegularWRT.trans h.innerRegular - exact InnerRegularWRT.of_imp (fun U hU ↦ ⟨hU.measurableSet, measure_ne_top μ U⟩) +instance (priority := 50) [BorelSpace α] [R1Space α] [h : InnerRegularCompactLTTop μ] + [IsFiniteMeasure μ] : Regular μ where + innerRegular := InnerRegularWRT.trans h.innerRegular <| + InnerRegularWRT.of_imp (fun U hU ↦ ⟨hU.measurableSet, measure_ne_top μ U⟩) /-- I`μ` is inner regular for finite measure sets with respect to compact sets in a regular locally compact space, then any compact set can be approximated from outside by open sets. -/ -protected lemma _root_.IsCompact.measure_eq_infi_isOpen [InnerRegularCompactLTTop μ] +protected lemma _root_.IsCompact.measure_eq_iInf_isOpen [InnerRegularCompactLTTop μ] [IsFiniteMeasureOnCompacts μ] [LocallyCompactSpace α] [RegularSpace α] [BorelSpace α] {K : Set α} (hK : IsCompact K) : μ K = ⨅ (U : Set α) (_ : K ⊆ U) (_ : IsOpen U), μ U := by @@ -804,7 +803,7 @@ protected lemma _root_.IsCompact.exists_isOpen_lt_of_lt [InnerRegularCompactLTTo [BorelSpace α] {K : Set α} (hK : IsCompact K) (r : ℝ≥0∞) (hr : μ K < r) : ∃ U, K ⊆ U ∧ IsOpen U ∧ μ U < r := by have : ⨅ (U : Set α) (_ : K ⊆ U) (_ : IsOpen U), μ U < r := by - rwa [hK.measure_eq_infi_isOpen] at hr + rwa [hK.measure_eq_iInf_isOpen] at hr simpa only [iInf_lt_iff, exists_prop, exists_and_left] protected theorem _root_.IsCompact.exists_isOpen_lt_add [InnerRegularCompactLTTop μ] @@ -1006,7 +1005,7 @@ protected theorem smul [Regular μ] {x : ℝ≥0∞} (hx : x ≠ ∞) : (x • instance smul_nnreal [Regular μ] (c : ℝ≥0) : Regular (c • μ) := Regular.smul coe_ne_top /-- The restriction of a regular measure to a set of finite measure is regular. -/ -theorem restrict_of_measure_ne_top [T2OrLocallyCompactRegularSpace α] [BorelSpace α] [Regular μ] +theorem restrict_of_measure_ne_top [R1Space α] [BorelSpace α] [Regular μ] {A : Set α} (h'A : μ A ≠ ∞) : Regular (μ.restrict A) := by have : WeaklyRegular (μ.restrict A) := WeaklyRegular.restrict_of_measure_ne_top h'A constructor From 6d40163e929cf29aedb248298d1317a6e4c72371 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 28 Jan 2024 13:49:12 -0600 Subject: [PATCH 03/16] Snapshot --- Mathlib/Topology/Algebra/Group/Basic.lean | 49 +++++------- Mathlib/Topology/Separation.lean | 94 ++++++++++++++--------- 2 files changed, 78 insertions(+), 65 deletions(-) diff --git a/Mathlib/Topology/Algebra/Group/Basic.lean b/Mathlib/Topology/Algebra/Group/Basic.lean index d41a1fac3218d..b4af765368c16 100644 --- a/Mathlib/Topology/Algebra/Group/Basic.lean +++ b/Mathlib/Topology/Algebra/Group/Basic.lean @@ -1771,35 +1771,31 @@ theorem exists_disjoint_smul_of_isCompact [NoncompactSpace G] {K L : Set G} (hK /-- A compact neighborhood of `1` in a topological group admits a closed compact subset that is a neighborhood of `1`. -/ -@[to_additive "A compact neighborhood of `0` in a topological additive group +@[to_additive (attr := deprecated IsCompact.isCompact_isClosed_basis_nhds) + "A compact neighborhood of `0` in a topological additive group admits a closed compact subset that is a neighborhood of `0`."] theorem exists_isCompact_isClosed_subset_isCompact_nhds_one {L : Set G} (Lcomp : IsCompact L) (L1 : L ∈ 𝓝 (1 : G)) : - ∃ K : Set G, IsCompact K ∧ IsClosed K ∧ K ⊆ L ∧ K ∈ 𝓝 (1 : G) := by - rcases exists_mem_nhds_isClosed_subset L1 with ⟨K, hK, K_closed, KL⟩ - exact ⟨K, Lcomp.of_isClosed_subset K_closed KL, K_closed, KL, hK⟩ + ∃ K : Set G, IsCompact K ∧ IsClosed K ∧ K ⊆ L ∧ K ∈ 𝓝 (1 : G) := + let ⟨K, ⟨hK, hK₁, hK₂⟩, hKL⟩ := (Lcomp.isCompact_isClosed_basis_nhds L1).mem_iff.1 L1 + ⟨K, hK₁, hK₂, hKL, hK⟩ /-- If a point in a topological group has a compact neighborhood, then the group is locally compact. -/ @[to_additive] theorem IsCompact.locallyCompactSpace_of_mem_nhds_of_group {K : Set G} (hK : IsCompact K) {x : G} (h : K ∈ 𝓝 x) : LocallyCompactSpace G := by - refine ⟨fun y n hn ↦ ?_⟩ - have A : (y * x⁻¹) • K ∈ 𝓝 y := by - rw [← preimage_smul_inv] + suffices WeaklyLocallyCompactSpace G from inferInstance + refine ⟨fun y ↦ ⟨(y * x⁻¹) • K, ?_, ?_⟩⟩ + · exact hK.smul _ + · rw [← preimage_smul_inv] exact (continuous_const_smul _).continuousAt.preimage_mem_nhds (by simpa using h) - rcases exists_mem_nhds_isClosed_subset (inter_mem A hn) with ⟨L, hL, L_closed, LK⟩ - refine ⟨L, hL, LK.trans (inter_subset_right _ _), ?_⟩ - exact (hK.smul (y * x⁻¹)).of_isClosed_subset L_closed (LK.trans (inter_subset_left _ _)) --- The next instance creates a loop between weakly locally compact space and locally compact space --- for topological groups. Hopefully, it shouldn't create problems. /-- A topological group which is weakly locally compact is automatically locally compact. -/ -@[to_additive] -instance (priority := 90) instLocallyCompactSpaceOfWeaklyOfGroup [WeaklyLocallyCompactSpace G] : - LocallyCompactSpace G := by - rcases exists_compact_mem_nhds (1 : G) with ⟨K, K_comp, hK⟩ - exact K_comp.locallyCompactSpace_of_mem_nhds_of_group hK +@[to_additive (attr := deprecated WeaklyLocallyCompactSpace.locallyCompactSpace)] +theorem instLocallyCompactSpaceOfWeaklyOfGroup [WeaklyLocallyCompactSpace G] : + LocallyCompactSpace G := + WeaklyLocallyCompactSpace.locallyCompactSpace /-- If a function defined on a topological group has a support contained in a compact set, then either the function is trivial or the group is locally compact. -/ @@ -1834,34 +1830,31 @@ theorem HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group /-- In a locally compact group, any neighborhood of the identity contains a compact closed neighborhood of the identity, even without separation assumptions on the space. -/ -@[to_additive +@[to_additive (attr := deprecated isCompact_isClosed_basis_nhds) "In a locally compact additive group, any neighborhood of the identity contains a compact closed neighborhood of the identity, even without separation assumptions on the space."] theorem local_isCompact_isClosed_nhds_of_group [LocallyCompactSpace G] {U : Set G} (hU : U ∈ 𝓝 (1 : G)) : - ∃ K : Set G, IsCompact K ∧ IsClosed K ∧ K ⊆ U ∧ (1 : G) ∈ interior K := by - obtain ⟨L, L1, LU, Lcomp⟩ : ∃ (L : Set G), L ∈ 𝓝 (1 : G) ∧ L ⊆ U ∧ IsCompact L := - local_compact_nhds hU - obtain ⟨K, Kcomp, Kcl, KL, K1⟩ := exists_isCompact_isClosed_subset_isCompact_nhds_one Lcomp L1 - exact ⟨K, Kcomp, Kcl, KL.trans LU, mem_interior_iff_mem_nhds.2 K1⟩ + ∃ K : Set G, IsCompact K ∧ IsClosed K ∧ K ⊆ U ∧ (1 : G) ∈ interior K := + let ⟨K, ⟨hK₁, hKco, hKcl⟩, hKU⟩ := (isCompact_isClosed_basis_nhds (1 : G)).mem_iff.1 hU + ⟨K, hKco, hKcl, hKU, mem_interior_iff_mem_nhds.2 hK₁⟩ #align local_is_compact_is_closed_nhds_of_group local_isCompact_isClosed_nhds_of_group #align local_is_compact_is_closed_nhds_of_add_group local_isCompact_isClosed_nhds_of_addGroup variable (G) -@[to_additive] +@[to_additive (attr := deprecated exists_mem_nhds_isCompact_isClosed)] theorem exists_isCompact_isClosed_nhds_one [WeaklyLocallyCompactSpace G] : ∃ K : Set G, IsCompact K ∧ IsClosed K ∧ K ∈ 𝓝 1 := - let ⟨_L, Lcomp, L1⟩ := exists_compact_mem_nhds (1 : G) - let ⟨K, Kcl, Kcomp, _, K1⟩ := exists_isCompact_isClosed_subset_isCompact_nhds_one Lcomp L1 - ⟨K, Kcl, Kcomp, K1⟩ + let ⟨K, hK₁, hKcomp, hKcl⟩ := exists_mem_nhds_isCompact_isClosed (1 : G) + ⟨K, hKcomp, hKcl, hK₁⟩ /-- A quotient of a locally compact group is locally compact. -/ @[to_additive] instance [LocallyCompactSpace G] (N : Subgroup G) : LocallyCompactSpace (G ⧸ N) := by refine ⟨fun x n hn ↦ ?_⟩ let π := ((↑) : G → G ⧸ N) - have C : Continuous π := continuous_coinduced_rng + have C : Continuous π := continuous_quotient_mk' obtain ⟨y, rfl⟩ : ∃ y, π y = x := Quot.exists_rep x have : π ⁻¹' n ∈ 𝓝 y := preimage_nhds_coinduced hn rcases local_compact_nhds this with ⟨s, s_mem, hs, s_comp⟩ diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index 8d9594476d1e0..e62e983fdb627 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -1057,60 +1057,80 @@ theorem IsCompact.finite_compact_cover {s : Set X} (hs : IsCompact s) {ι : Type · simp only [Finset.set_biUnion_insert_update _ hx, hK, h3K] #align is_compact.finite_compact_cover IsCompact.finite_compact_cover +theorem exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds + {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [R1Space Y] {f : X → Y} {x : X} + {K : Set X} {s : Set Y} (hf : Continuous f) (hs : s ∈ 𝓝 (f x)) (hKc : IsCompact K) + (hKx : K ∈ 𝓝 x) : ∃ K ∈ 𝓝 x, IsCompact K ∧ MapsTo f K s := by + have hc : IsCompact (f '' K \ interior s) := (hKc.image hf).diff isOpen_interior + obtain ⟨U, V, Uo, Vo, hxU, hV, hd⟩ : SeparatedNhds {f x} (f '' K \ interior s) := by + simp_rw [separatedNhds_iff_disjoint, nhdsSet_singleton, hc.disjoint_nhdsSet_right, + disjoint_nhds_nhds_iff_not_inseparable] + rintro y ⟨-, hys⟩ hxy + refine hys <| (hxy.mem_open_iff isOpen_interior).1 ?_ + rwa [mem_interior_iff_mem_nhds] + refine ⟨K \ f ⁻¹' V, diff_mem hKx ?_, hKc.diff <| Vo.preimage hf, fun y hy ↦ ?_⟩ + · filter_upwards [hf.continuousAt <| Uo.mem_nhds (hxU rfl)] with x hx + using Set.disjoint_left.1 hd hx + · by_contra hys + exact hy.2 (hV ⟨mem_image_of_mem _ hy.1, not_mem_subset interior_subset hys⟩) + instance (priority := 900) {X Y : Type*} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] - [TopologicalSpace Y] [R1Space Y] : - LocallyCompactPair X Y where - exists_mem_nhds_isCompact_mapsTo := by - intro f x s hf hs - rcases exists_compact_mem_nhds x with ⟨K, hKc, hKx⟩ - have hc : IsCompact (f '' K \ interior s) := (hKc.image hf).diff isOpen_interior - obtain ⟨U, V, Uo, Vo, hxU, hV, hd⟩ : SeparatedNhds {f x} (f '' K \ interior s) := by - simp_rw [separatedNhds_iff_disjoint, nhdsSet_singleton, hc.disjoint_nhdsSet_right, - disjoint_nhds_nhds_iff_not_inseparable] - rintro y ⟨-, hys⟩ hxy - refine hys <| (hxy.mem_open_iff isOpen_interior).1 ?_ - rwa [mem_interior_iff_mem_nhds] - refine ⟨K \ f ⁻¹' V, diff_mem hKx ?_, hKc.diff <| Vo.preimage hf, fun y hy ↦ ?_⟩ - · filter_upwards [hf.continuousAt <| Uo.mem_nhds (hxU rfl)] with x hx - using Set.disjoint_left.1 hd hx - · by_contra hys - exact hy.2 (hV ⟨mem_image_of_mem _ hy.1, not_mem_subset interior_subset hys⟩) + [TopologicalSpace Y] [R1Space Y] : LocallyCompactPair X Y where + exists_mem_nhds_isCompact_mapsTo hf hs := + let ⟨_K, hKc, hKx⟩ := exists_compact_mem_nhds _ + exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds hf hs hKc hKx + +/-- If a point in a preregular space has a compact neighborhood, +then it has a basis of compact closed neighborhoods. -/ +theorem IsCompact.isCompact_isClosed_basis_nhds {x : X} {L : Set X} (hLc : IsCompact L) + (hxL : L ∈ 𝓝 x) : (𝓝 x).HasBasis (fun K ↦ K ∈ 𝓝 x ∧ IsCompact K ∧ IsClosed K) (·) := + hasBasis_self.2 fun _U hU ↦ + let ⟨K, hKx, hKc, hKU⟩ := exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds + continuous_id (interior_mem_nhds.2 hU) hLc hxL + ⟨closure K, mem_of_superset hKx subset_closure, ⟨hKc.closure, isClosed_closure⟩, + (hKc.closure_subset_of_isOpen isOpen_interior hKU).trans interior_subset⟩ + +/-! +### Lemmas about a weakly locally compact preregular space + +In fact, a space with these properties is locally compact and regular. +Some lemmas are formulated in that assumptions below. +-/ variable [WeaklyLocallyCompactSpace X] +/-- In a (weakly) locally compact R₁ space, compact closed neighborhoods of a point `x` +form a basis of neighborhoods of `x`. -/ +theorem isCompact_isClosed_basis_nhds (x : X) : + (𝓝 x).HasBasis (fun K => K ∈ 𝓝 x ∧ IsCompact K ∧ IsClosed K) (·) := + let ⟨_L, hLc, hLx⟩ := exists_compact_mem_nhds x + hLc.isCompact_isClosed_basis_nhds hLx + +/-- In a (weakly) locally compact R₁ space, each point admints a compact closed neighborhood. -/ +theorem exists_mem_nhds_isCompact_isClosed (x : X) : ∃ K ∈ 𝓝 x, IsCompact K ∧ IsClosed K := + (isCompact_isClosed_basis_nhds x).ex_mem + -- see Note [lower instance priority] /-- A weakly locally compact preregular space is locally compact. -/ -instance (priority := 80) WeaklyLocallyCompactSpace.locallyCompactSpace : - LocallyCompactSpace X where - local_compact_nhds _x _s hs := - let ⟨K, hKx, hKc, hKs⟩ := exists_mem_nhds_isCompact_mapsTo continuous_id hs - ⟨K, hKx, hKs, hKc⟩ +instance (priority := 80) WeaklyLocallyCompactSpace.locallyCompactSpace : LocallyCompactSpace X := + .of_hasBasis isCompact_isClosed_basis_nhds fun _ _ ⟨_, h, _⟩ ↦ h #align locally_compact_of_compact_nhds WeaklyLocallyCompactSpace.locallyCompactSpace -/-- In a locally compact R₁ space, compact closed neighborhoods of a point `x` -form a basis of neighborhoods of `x`. -/ -theorem isCompact_isClosed_basis_nhds (x : X) : - (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsCompact s ∧ IsClosed s) (·) := - hasBasis_self.2 fun _U hU ↦ - let ⟨K, hxK, hKU, hKc⟩ := local_compact_nhds <| interior_mem_nhds.2 hU - ⟨closure K, mem_of_superset hxK subset_closure, ⟨hKc.closure, isClosed_closure⟩, - (hKc.closure_subset_of_isOpen isOpen_interior hKU).trans interior_subset⟩ - /-- In a weakly locally compact space which is either T₂ or locally compact regular, every compact set has an open neighborhood with compact closure. -/ -theorem exists_open_superset_and_isCompact_closure {K : Set X} (hK : IsCompact K) : +theorem exists_isOpen_superset_and_isCompact_closure {K : Set X} (hK : IsCompact K) : ∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V) := by rcases exists_compact_superset hK with ⟨K', hK', hKK'⟩ exact ⟨interior K', isOpen_interior, hKK', hK'.closure_of_subset interior_subset⟩ -#align exists_open_superset_and_is_compact_closure exists_open_superset_and_isCompact_closure +#align exists_open_superset_and_is_compact_closure exists_isOpen_superset_and_isCompact_closure /-- In a weakly locally compact which is either T₂ or locally compact regular, every point has an open neighborhood with compact closure. -/ -theorem exists_open_with_compact_closure (x : X) : +theorem exists_isOpen_mem_isCompact_closure (x : X) : ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U) := by simpa only [singleton_subset_iff] - using exists_open_superset_and_isCompact_closure isCompact_singleton -#align exists_open_with_compact_closure exists_open_with_compact_closure + using exists_isOpen_superset_and_isCompact_closure isCompact_singleton +#align exists_open_with_compact_closure exists_isOpen_mem_isCompact_closure end R1Space @@ -1820,7 +1840,7 @@ instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, /-- In a regular space, if a compact set and a closed set are disjoint, then they have disjoint neighborhoods. -/ -lemma separatedNhds_of_isCompact_isClosed [RegularSpace X] {s t : Set X} +lemma SeparatedNhds.of_isCompact_isClosed [RegularSpace X] {s t : Set X} (hs : IsCompact s) (ht : IsClosed t) (hst : Disjoint s t) : SeparatedNhds s t := by simpa only [separatedNhds_iff_disjoint, hs.disjoint_nhdsSet_left, disjoint_nhds_nhdsSet, ht.closure_eq, disjoint_left] using hst From 8dda5223701a019e8db45e54372f68b9d901a0d1 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 28 Jan 2024 13:52:45 -0600 Subject: [PATCH 04/16] Whitespace --- Mathlib/Analysis/NormedSpace/OperatorNorm.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm.lean index e5f2b63d3bd03..224e25b0eeb6c 100644 --- a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean +++ b/Mathlib/Analysis/NormedSpace/OperatorNorm.lean @@ -1576,7 +1576,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_pi_infinite this).closure_of_subset + (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 From dd1dcd45d2527aa2f6c3cf67dd184e6c773c9841 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 28 Jan 2024 14:07:15 -0600 Subject: [PATCH 05/16] Restore some old names (with `@[deprecated]`) --- Mathlib/MeasureTheory/Measure/Regular.lean | 5 ++- Mathlib/Topology/Separation.lean | 41 ++++++++++++++++++---- 2 files changed, 38 insertions(+), 8 deletions(-) diff --git a/Mathlib/MeasureTheory/Measure/Regular.lean b/Mathlib/MeasureTheory/Measure/Regular.lean index 6c4beb19561e9..40cec0824fff3 100644 --- a/Mathlib/MeasureTheory/Measure/Regular.lean +++ b/Mathlib/MeasureTheory/Measure/Regular.lean @@ -769,7 +769,7 @@ instance (priority := 50) [h : InnerRegularCompactLTTop μ] [IsFiniteMeasure μ] instance (priority := 50) [BorelSpace α] [R1Space α] [InnerRegularCompactLTTop μ] [IsFiniteMeasure μ] : WeaklyRegular μ := - InnerRegular.innerRegularWRT_isClosed_isOpen.weaklyRegular_of_finite _ + InnerRegular.innerRegularWRT_isClosed_isOpen.weaklyRegular_of_finite _ instance (priority := 50) [BorelSpace α] [R1Space α] [h : InnerRegularCompactLTTop μ] [IsFiniteMeasure μ] : Regular μ where @@ -798,6 +798,9 @@ protected lemma _root_.IsCompact.measure_eq_iInf_isOpen [InnerRegularCompactLTTo refine ⟨U ∩ interior L, subset_inter KU KL, U_open.inter isOpen_interior, ?_⟩ rwa [restrict_apply U_open.measurableSet] at hU +@[deprecated] -- Since 28 Jan 2024 +alias _root_.IsCompact.measure_eq_infi_isOpen := IsCompact.measure_eq_iInf_isOpen + protected lemma _root_.IsCompact.exists_isOpen_lt_of_lt [InnerRegularCompactLTTop μ] [IsFiniteMeasureOnCompacts μ] [LocallyCompactSpace α] [RegularSpace α] [BorelSpace α] {K : Set α} (hK : IsCompact K) (r : ℝ≥0∞) (hr : μ K < r) : diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index e62e983fdb627..40b5d5c706d01 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -1000,11 +1000,17 @@ theorem IsCompact.closure_of_subset {s K : Set X} (hK : IsCompact K) (h : s ⊆ hK.closure.of_isClosed_subset isClosed_closure (closure_mono h) #align is_compact_closure_of_subset_compact IsCompact.closure_of_subset +@[deprecated] -- Since 28 Jan 2024 +alias isCompact_closure_of_subset_compact := IsCompact.closure_of_subset + @[simp] -theorem exists_compact_superset_iff {s : Set X} : +theorem exists_isCompact_superset_iff {s : Set X} : (∃ K, IsCompact K ∧ s ⊆ K) ↔ IsCompact (closure s) := ⟨fun ⟨_K, hK, hsK⟩ => hK.closure_of_subset hsK, fun h => ⟨closure s, h, subset_closure⟩⟩ -#align exists_compact_superset_iff exists_compact_superset_iff +#align exists_compact_superset_iff exists_isCompact_superset_iff + +@[deprecated] -- Since 28 Jan 2024 +alias exists_compact_superset_iff := exists_isCompact_superset_iff /-- If `K` and `L` are a disjoint compact set in a preregular topological space and `L` is also closed, then `K` and `L` have disjoint neighborhoods. -/ @@ -1015,6 +1021,9 @@ theorem SeparatedNhds.of_isCompact_isCompact_isClosed {K L : Set X} (hK : IsComp intro x hx y hy h exact absurd ((h.mem_closed_iff h'L).2 hy) <| disjoint_left.1 hd hx +@[deprecated] -- Since 28 Jan 2024 +alias separatedNhds_of_isCompact_isCompact_isClosed := SeparatedNhds.of_isCompact_isCompact_isClosed + /-- If a compact set is covered by two open sets, then we can cover it by two compact subsets. -/ theorem IsCompact.binary_compact_cover {K U V : Set X} (hK : IsCompact K) (hU : IsOpen U) (hV : IsOpen V) (h2K : K ⊆ U ∪ V) : @@ -1124,6 +1133,9 @@ theorem exists_isOpen_superset_and_isCompact_closure {K : Set X} (hK : IsCompact exact ⟨interior K', isOpen_interior, hKK', hK'.closure_of_subset interior_subset⟩ #align exists_open_superset_and_is_compact_closure exists_isOpen_superset_and_isCompact_closure +@[deprecated] -- Since 28 Jan 2024 +alias exists_open_superset_and_isCompact_closure := exists_isOpen_superset_and_isCompact_closure + /-- In a weakly locally compact which is either T₂ or locally compact regular, every point has an open neighborhood with compact closure. -/ theorem exists_isOpen_mem_isCompact_closure (x : X) : @@ -1132,6 +1144,9 @@ theorem exists_isOpen_mem_isCompact_closure (x : X) : using exists_isOpen_superset_and_isCompact_closure isCompact_singleton #align exists_open_with_compact_closure exists_isOpen_mem_isCompact_closure +@[deprecated] -- Since 28 Jan 2024 +alias exists_open_with_compact_closure := exists_isOpen_mem_isCompact_closure + end R1Space /-- A T₂ space, also known as a Hausdorff space, is one in which for every @@ -1564,17 +1579,26 @@ theorem SeparatedNhds.of_isCompact_isCompact [T2Space X] {s t : Set X} (hs : IsC exact generalized_tube_lemma hs ht isClosed_diagonal.isOpen_compl hst #align is_compact_is_compact_separated SeparatedNhds.of_isCompact_isCompact +@[deprecated] -- Since 28 Jan 2024 +alias separatedNhds_of_isCompact_isCompact := SeparatedNhds.of_isCompact_isCompact + section SeparatedFinset -theorem separatedNhds_of_finset_finset [T2Space X] (s t : Finset X) (h : Disjoint s t) : +theorem SeparatedNhds.of_finset_finset [T2Space X] (s t : Finset X) (h : Disjoint s t) : SeparatedNhds (s : Set X) t := .of_isCompact_isCompact s.finite_toSet.isCompact t.finite_toSet.isCompact <| mod_cast h -#align finset_disjoint_finset_opens_of_t2 separatedNhds_of_finset_finset +#align finset_disjoint_finset_opens_of_t2 SeparatedNhds.of_finset_finset + +@[deprecated] -- Since 28 Jan 2024 +alias separatedNhds_of_finset_finset := SeparatedNhds.of_finset_finset -theorem point_disjoint_finset_opens_of_t2 [T2Space X] {x : X} {s : Finset X} (h : x ∉ s) : +theorem SeparatedNhds.of_singleton_finset [T2Space X] {x : X} {s : Finset X} (h : x ∉ s) : SeparatedNhds ({x} : Set X) s := - mod_cast separatedNhds_of_finset_finset {x} s (Finset.disjoint_singleton_left.mpr h) -#align point_disjoint_finset_opens_of_t2 point_disjoint_finset_opens_of_t2 + mod_cast .of_finset_finset {x} s (Finset.disjoint_singleton_left.mpr h) +#align point_disjoint_finset_opens_of_t2 SeparatedNhds.of_singleton_finset + +@[deprecated] +alias point_disjoint_finset_opens_of_t2 := SeparatedNhds.of_singleton_finset end SeparatedFinset @@ -1845,6 +1869,9 @@ lemma SeparatedNhds.of_isCompact_isClosed [RegularSpace X] {s t : Set X} simpa only [separatedNhds_iff_disjoint, hs.disjoint_nhdsSet_left, disjoint_nhds_nhdsSet, ht.closure_eq, disjoint_left] using hst +@[deprecated] -- Since 28 Jan 2024 +alias separatedNhds_of_isCompact_isClosed := SeparatedNhds.of_isCompact_isClosed + end RegularSpace section LocallyCompactRegularSpace From d08ef0b19bbcbea7ee28c14b0df5c8e8b6a2b78a Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 28 Jan 2024 15:16:51 -0600 Subject: [PATCH 06/16] Add instances --- Mathlib/Topology/Separation.lean | 54 ++++++++++++++++++++++++++------ 1 file changed, 45 insertions(+), 9 deletions(-) diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index 40b5d5c706d01..adfa5e7dc091c 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -1066,6 +1066,43 @@ theorem IsCompact.finite_compact_cover {s : Set X} (hs : IsCompact s) {ι : Type · simp only [Finset.set_biUnion_insert_update _ hx, hK, h3K] #align is_compact.finite_compact_cover IsCompact.finite_compact_cover +theorem Inducing.r1Space [TopologicalSpace Y] {f : Y → X} (hf : Inducing f) : R1Space Y where + specializes_or_disjoint_nhds _ _ := by + simpa only [← hf.specializes_iff, hf.nhds_eq_comap, or_iff_not_imp_left, + ← disjoint_nhds_nhds_iff_not_specializes] using Filter.disjoint_comap + +protected theorem R1Space.induced (f : Y → X) : @R1Space Y (.induced f ‹_›) := + @Inducing.r1Space _ _ _ _ (.induced f _) f (inducing_induced f) + +instance (p : X → Prop) : R1Space (Subtype p) := .induced _ + +protected theorem R1Space.sInf {X : Type*} {T : Set (TopologicalSpace X)} + (hT : ∀ t ∈ T, @R1Space X t) : @R1Space X (sInf T) := by + let _ := sInf T + refine ⟨fun x y ↦ ?_⟩ + simp only [Specializes, nhds_sInf] + rcases em (∃ t ∈ T, Disjoint (@nhds X t x) (@nhds X t y)) with ⟨t, htT, htd⟩ | hTd + · exact .inr <| htd.mono (iInf₂_le t htT) (iInf₂_le t htT) + · push_neg at hTd + exact .inl <| iInf₂_mono fun t ht ↦ ((hT t ht).1 x y).resolve_right (hTd t ht) + +protected theorem R1Space.iInf {ι X : Type*} {t : ι → TopologicalSpace X} + (ht : ∀ i, @R1Space X (t i)) : @R1Space X (iInf t) := + .sInf <| forall_range_iff.2 ht + +protected theorem R1Space.inf {X : Type*} {t₁ t₂ : TopologicalSpace X} + (h₁ : @R1Space X t₁) (h₂ : @R1Space X t₂) : @R1Space X (t₁ ⊓ t₂) := by + rw [inf_eq_iInf] + apply R1Space.iInf + simp [*] + +instance [TopologicalSpace Y] [R1Space Y] : R1Space (X × Y) := + .inf (.induced _) (.induced _) + +instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, R1Space (X i)] : + R1Space (∀ i, X i) := + .iInf fun _ ↦ .induced _ + theorem exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [R1Space Y] {f : X → Y} {x : X} {K : Set X} {s : Set Y} (hf : Continuous f) (hs : s ∈ 𝓝 (f x)) (hKc : IsCompact K) @@ -1208,6 +1245,10 @@ theorem SeparationQuotient.t2Space_iff : T2Space (SeparationQuotient X) ↔ R1Sp instance SeparationQuotient.t2Space [R1Space X] : T2Space (SeparationQuotient X) := t2Space_iff.2 ‹_› +instance (priority := 80) [R1Space X] [T0Space X] : T2Space X := + t2Space_iff_disjoint_nhds.2 fun _x _y hne ↦ disjoint_nhds_nhds_iff_not_inseparable.2 fun hxy ↦ + hne hxy.eq + /-- A space is T₂ iff the neighbourhoods of distinct points generate the bottom filter. -/ theorem t2_iff_nhds : T2Space X ↔ ∀ {x y : X}, NeBot (𝓝 x ⊓ 𝓝 y) → x = y := by simp only [t2Space_iff_disjoint_nhds, disjoint_iff, neBot_iff, Ne.def, not_imp_comm, Pairwise] @@ -1457,13 +1498,10 @@ theorem separated_by_openEmbedding [TopologicalSpace Y] [T2Space X] mem_image_of_mem _ yv, disjoint_image_of_injective hf.inj uv⟩ #align separated_by_open_embedding separated_by_openEmbedding -instance {p : X → Prop} [T2Space X] : T2Space (Subtype p) := - ⟨fun _ _ h => separated_by_continuous continuous_subtype_val (mt Subtype.eq h)⟩ +instance {p : X → Prop} [T2Space X] : T2Space (Subtype p) := inferInstance instance Prod.t2Space [T2Space X] [TopologicalSpace Y] [T2Space Y] : T2Space (X × Y) := - ⟨fun _ _ h => Or.elim (not_and_or.mp (mt Prod.ext_iff.mpr h)) - (fun h₁ => separated_by_continuous continuous_fst h₁) fun h₂ => - separated_by_continuous continuous_snd h₂⟩ + inferInstance /-- If the codomain of an injective continuous function is a Hausdorff space, then so is its domain. -/ @@ -1492,9 +1530,7 @@ instance [T2Space X] [TopologicalSpace Y] [T2Space Y] : instance Pi.t2Space {Y : X → Type v} [∀ a, TopologicalSpace (Y a)] [∀ a, T2Space (Y a)] : T2Space (∀ a, Y a) := - ⟨fun _ _ h => - let ⟨i, hi⟩ := not_forall.mp (mt funext h) - separated_by_continuous (continuous_apply i) hi⟩ + inferInstance #align Pi.t2_space Pi.t2Space instance Sigma.t2Space {ι} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ a, T2Space (X a)] : @@ -1824,7 +1860,7 @@ protected theorem Inducing.regularSpace [TopologicalSpace Y] {f : Y → X} (hf : theorem regularSpace_induced (f : Y → X) : @RegularSpace Y (induced f ‹_›) := letI := induced f ‹_› - Inducing.regularSpace ⟨rfl⟩ + (inducing_induced f).regularSpace #align regular_space_induced regularSpace_induced theorem regularSpace_sInf {X} {T : Set (TopologicalSpace X)} (h : ∀ t ∈ T, @RegularSpace X t) : From a45ad21fa1321a20f95c6f568e44c44b0a00f2b9 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 28 Jan 2024 15:49:51 -0600 Subject: [PATCH 07/16] Migrate from deprecated names --- Mathlib/MeasureTheory/Group/Measure.lean | 6 +++--- Mathlib/Topology/Support.lean | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/MeasureTheory/Group/Measure.lean b/Mathlib/MeasureTheory/Group/Measure.lean index 9b3fb862a70bc..e6ec7bfadcad4 100644 --- a/Mathlib/MeasureTheory/Group/Measure.lean +++ b/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 diff --git a/Mathlib/Topology/Support.lean b/Mathlib/Topology/Support.lean index 7a014fdcf589b..ee29d43e42b75 100644 --- a/Mathlib/Topology/Support.lean +++ b/Mathlib/Topology/Support.lean @@ -165,16 +165,16 @@ theorem hasCompactMulSupport_def : HasCompactMulSupport f ↔ IsCompact (closure #align has_compact_support_def hasCompactSupport_def @[to_additive] -theorem exists_compact_iff_hasCompactMulSupport [T2Space α] : +theorem exists_compact_iff_hasCompactMulSupport [R1Space α] : (∃ K : Set α, IsCompact K ∧ ∀ x, x ∉ K → f x = 1) ↔ HasCompactMulSupport f := by simp_rw [← nmem_mulSupport, ← mem_compl_iff, ← subset_def, compl_subset_compl, - hasCompactMulSupport_def, exists_compact_superset_iff] + hasCompactMulSupport_def, exists_isCompact_superset_iff] #align exists_compact_iff_has_compact_mul_support exists_compact_iff_hasCompactMulSupport #align exists_compact_iff_has_compact_support exists_compact_iff_hasCompactSupport namespace HasCompactMulSupport @[to_additive] -theorem intro [T2Space α] {K : Set α} (hK : IsCompact K) +theorem intro [R1Space α] {K : Set α} (hK : IsCompact K) (hfK : ∀ x, x ∉ K → f x = 1) : HasCompactMulSupport f := exists_compact_iff_hasCompactMulSupport.mp ⟨K, hK, hfK⟩ #align has_compact_mul_support.intro HasCompactMulSupport.intro From 981bf920bea128ccf64c560bfd5f45c96b62c438 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 28 Jan 2024 16:22:28 -0600 Subject: [PATCH 08/16] Fix typos, add to the module docstring --- Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean | 4 ++++ Mathlib/Topology/Separation.lean | 4 +++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean index d15ce51074598..601f518d214d2 100644 --- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean +++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean @@ -362,11 +362,15 @@ 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 is a preregular 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] diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index adfa5e7dc091c..9c9970302b407 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -24,6 +24,8 @@ This file defines the predicate `SeparatedNhds`, and common separation axioms * `T1Space`: A T₁/Fréchet space is a space where every singleton set is closed. This is equivalent to, for every pair `x ≠ y`, there existing an open set containing `x` but not `y` (`t1Space_iff_exists_open` shows that these conditions are equivalent.) +* `R1Space`: An R₁/preregular space is a space where any two topologically distinguishable points + have disjoint neighbourhoods; * `T2Space`: A T₂/Hausdorff space is a space where, for every two points `x ≠ y`, there is two disjoint open sets, one containing `x`, and the other `y`. * `T25Space`: A T₂.₅/Urysohn space is a space where, for every two points `x ≠ y`, @@ -1152,7 +1154,7 @@ theorem isCompact_isClosed_basis_nhds (x : X) : let ⟨_L, hLc, hLx⟩ := exists_compact_mem_nhds x hLc.isCompact_isClosed_basis_nhds hLx -/-- In a (weakly) locally compact R₁ space, each point admints a compact closed neighborhood. -/ +/-- In a (weakly) locally compact R₁ space, each point admits a compact closed neighborhood. -/ theorem exists_mem_nhds_isCompact_isClosed (x : X) : ∃ K ∈ 𝓝 x, IsCompact K ∧ IsClosed K := (isCompact_isClosed_basis_nhds x).ex_mem From 40f98b30c37d86eebd0426ec646e1df65334c92f Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 28 Jan 2024 17:38:02 -0600 Subject: [PATCH 09/16] Drop some unused `have`s and assumptions --- Mathlib/MeasureTheory/Group/Measure.lean | 3 +-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean | 8 +------- Mathlib/Topology/Algebra/Group/Compact.lean | 12 +++--------- 3 files changed, 5 insertions(+), 18 deletions(-) diff --git a/Mathlib/MeasureTheory/Group/Measure.lean b/Mathlib/MeasureTheory/Group/Measure.lean index e6ec7bfadcad4..e825c68788ac3 100644 --- a/Mathlib/MeasureTheory/Group/Measure.lean +++ b/Mathlib/MeasureTheory/Group/Measure.lean @@ -782,8 +782,7 @@ lemma _root_.IsCompact.measure_closure_eq_of_group {k : Set G} (hk : IsCompact k rw [← hk.mul_closure_one_eq_closure, measure_mul_closure_one] @[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⟩ diff --git a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean index de2ad8a80a3d5..8eebd03f98e54 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean @@ -484,7 +484,6 @@ 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 with ⟨U₁, U₂, h1U₁, h1U₂, h2U₁, h2U₂, hU⟩ rcases compact_open_separated_mul_right K₁.2 h1U₁ h2U₁ with ⟨L₁, h1L₁, h2L₁⟩ @@ -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)] @@ -767,7 +762,6 @@ 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 diff --git a/Mathlib/Topology/Algebra/Group/Compact.lean b/Mathlib/Topology/Algebra/Group/Compact.lean index fdcf07932650e..664782989368a 100644 --- a/Mathlib/Topology/Algebra/Group/Compact.lean +++ b/Mathlib/Topology/Algebra/Group/Compact.lean @@ -36,15 +36,9 @@ is locally compact. -/ "Every topological additive group in which there exists a compact set with nonempty interior is locally compact."] theorem TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group - (K : PositiveCompacts G) : LocallyCompactSpace G := by - have A : WeaklyLocallyCompactSpace G := - { exists_compact_mem_nhds := by - intro x - obtain ⟨y, hy⟩ := K.interior_nonempty - refine ⟨(x * y⁻¹) • (K : Set G), K.isCompact.smul _, ?_⟩ - rw [mem_interior_iff_mem_nhds] at hy - simpa using smul_mem_nhds (x * y⁻¹) hy } - infer_instance + (K : PositiveCompacts G) : LocallyCompactSpace G := + let ⟨_x, hx⟩ := K.interior_nonempty + K.isCompact.locallyCompactSpace_of_mem_nhds_of_group (mem_interior_iff_mem_nhds.1 hx) #align topological_space.positive_compacts.locally_compact_space_of_group TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group #align topological_space.positive_compacts.locally_compact_space_of_add_group TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_addGroup From 2e2860cb4eeb046e887291c27f1e808760111a0f Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Mon, 29 Jan 2024 07:56:09 -0600 Subject: [PATCH 10/16] Apply suggestions from code review Co-authored-by: sgouezel --- .../MeasureTheory/Constructions/BorelSpace/Basic.lean | 2 +- Mathlib/MeasureTheory/Group/Measure.lean | 2 +- Mathlib/Topology/Separation.lean | 10 +++++----- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean index f63355af18bde..3d059e74299b1 100644 --- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean +++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean @@ -369,7 +369,7 @@ theorem Inseparable.mem_measurableSet_iff {x y : γ} (h : Inseparable x 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 is a preregular space and `s ⊇ K` is a Borel measurable superset, +/-- If `K` is a compact set in a preregular 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 diff --git a/Mathlib/MeasureTheory/Group/Measure.lean b/Mathlib/MeasureTheory/Group/Measure.lean index e825c68788ac3..dc63ab4ad6a23 100644 --- a/Mathlib/MeasureTheory/Group/Measure.lean +++ b/Mathlib/MeasureTheory/Group/Measure.lean @@ -760,7 +760,7 @@ 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)] -- 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 := hk.closure_subset_measurableSet hs h diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index f8eec1c2bef8c..a90017ae7007e 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -935,7 +935,7 @@ theorem disjoint_nhds_nhds_iff_not_specializes : Disjoint (𝓝 x) (𝓝 y) ↔ theorem specializes_iff_not_disjoint : x ⤳ y ↔ ¬Disjoint (𝓝 x) (𝓝 y) := disjoint_nhds_nhds_iff_not_specializes.not_left.symm -/-- An R₁ space is an R₀ space: the `Specializes` relation is symmetric. -/ +/-- In an R₁ space, the `Specializes` relation is symmetric, i.e., an R₁ is an R₀ space. -/ theorem Specializes.symm (h : x ⤳ y) : y ⤳ x := by simpa only [specializes_iff_not_disjoint, disjoint_comm] using h #align specializes.symm Specializes.symm @@ -1014,7 +1014,7 @@ theorem exists_isCompact_superset_iff {s : Set X} : @[deprecated] -- Since 28 Jan 2024 alias exists_compact_superset_iff := exists_isCompact_superset_iff -/-- If `K` and `L` are a disjoint compact set in a preregular topological space +/-- If `K` and `L` are disjoint compact sets in a preregular topological space and `L` is also closed, then `K` and `L` have disjoint neighborhoods. -/ theorem SeparatedNhds.of_isCompact_isCompact_isClosed {K L : Set X} (hK : IsCompact K) (hL : IsCompact L) (h'L : IsClosed L) (hd : Disjoint K L) : SeparatedNhds K L := by @@ -1142,7 +1142,7 @@ theorem IsCompact.isCompact_isClosed_basis_nhds {x : X} {L : Set X} (hLc : IsCom ### Lemmas about a weakly locally compact preregular space In fact, a space with these properties is locally compact and regular. -Some lemmas are formulated in that assumptions below. +Some lemmas are formulated using the latter assumptions below. -/ variable [WeaklyLocallyCompactSpace X] @@ -1164,7 +1164,7 @@ instance (priority := 80) WeaklyLocallyCompactSpace.locallyCompactSpace : Locall .of_hasBasis isCompact_isClosed_basis_nhds fun _ _ ⟨_, h, _⟩ ↦ h #align locally_compact_of_compact_nhds WeaklyLocallyCompactSpace.locallyCompactSpace -/-- In a weakly locally compact space which is either T₂ or locally compact regular, +/-- In a weakly locally compact preregular space, every compact set has an open neighborhood with compact closure. -/ theorem exists_isOpen_superset_and_isCompact_closure {K : Set X} (hK : IsCompact K) : ∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V) := by @@ -2109,7 +2109,7 @@ instance (priority := 100) T4Space.t3Space [T4Space X] : T3Space X where (disjoint_singleton_right.mpr hxs)).disjoint_nhdsSet #align normal_space.t3_space T4Space.t3Space -@[deprecated inferInstance] +@[deprecated inferInstance] -- Since 28 Jan 2024 theorem T4Space.of_compactSpace_t2Space [CompactSpace X] [T2Space X] : T4Space X := inferInstance #align normal_of_compact_t2 T4Space.of_compactSpace_t2Space From d1258cb5bc551f69f1904eb7ee3e7796028f2ecb Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Mon, 29 Jan 2024 08:45:01 -0600 Subject: [PATCH 11/16] =?UTF-8?q?preregular=20->=20R=E2=82=81,=20add=20dep?= =?UTF-8?q?recation=20dates?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../Constructions/BorelSpace/Basic.lean | 4 ++-- Mathlib/MeasureTheory/Measure/Regular.lean | 2 +- Mathlib/Topology/Algebra/Group/Basic.lean | 8 +++---- .../Topology/Compactness/LocallyCompact.lean | 4 ++-- Mathlib/Topology/Separation.lean | 22 +++++++++---------- 5 files changed, 20 insertions(+), 20 deletions(-) diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean index 3d059e74299b1..9c608a348efd7 100644 --- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean +++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean @@ -369,14 +369,14 @@ theorem Inseparable.mem_measurableSet_iff {x y : γ} (h : Inseparable x 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 a preregular space and `s ⊇ K` is a Borel measurable superset, +/-- 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 a preregular topological space with Borel measure `μ`, +/-- 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` diff --git a/Mathlib/MeasureTheory/Measure/Regular.lean b/Mathlib/MeasureTheory/Measure/Regular.lean index 40cec0824fff3..2509f6f3b2088 100644 --- a/Mathlib/MeasureTheory/Measure/Regular.lean +++ b/Mathlib/MeasureTheory/Measure/Regular.lean @@ -319,7 +319,7 @@ class InnerRegularCompactLTTop (μ : Measure α) : Prop where protected innerRegular : InnerRegularWRT μ IsCompact (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞) -- see Note [lower instance priority] -/-- A regular measure is weakly regular in a preregular space. -/ +/-- A regular measure is weakly regular in an R₁ space. -/ instance (priority := 100) Regular.weaklyRegular [R1Space α] [Regular μ] : WeaklyRegular μ where innerRegular := fun _U hU r hr ↦ diff --git a/Mathlib/Topology/Algebra/Group/Basic.lean b/Mathlib/Topology/Algebra/Group/Basic.lean index b4af765368c16..357ffcb37b4ca 100644 --- a/Mathlib/Topology/Algebra/Group/Basic.lean +++ b/Mathlib/Topology/Algebra/Group/Basic.lean @@ -1771,7 +1771,7 @@ theorem exists_disjoint_smul_of_isCompact [NoncompactSpace G] {K L : Set G} (hK /-- A compact neighborhood of `1` in a topological group admits a closed compact subset that is a neighborhood of `1`. -/ -@[to_additive (attr := deprecated IsCompact.isCompact_isClosed_basis_nhds) +@[to_additive (attr := deprecated IsCompact.isCompact_isClosed_basis_nhds) -- Since 28 Jan 2024 "A compact neighborhood of `0` in a topological additive group admits a closed compact subset that is a neighborhood of `0`."] theorem exists_isCompact_isClosed_subset_isCompact_nhds_one @@ -1792,7 +1792,7 @@ theorem IsCompact.locallyCompactSpace_of_mem_nhds_of_group {K : Set G} (hK : IsC exact (continuous_const_smul _).continuousAt.preimage_mem_nhds (by simpa using h) /-- A topological group which is weakly locally compact is automatically locally compact. -/ -@[to_additive (attr := deprecated WeaklyLocallyCompactSpace.locallyCompactSpace)] +@[to_additive (attr := deprecated WeaklyLocallyCompactSpace.locallyCompactSpace)] -- 28 Jan 2024 theorem instLocallyCompactSpaceOfWeaklyOfGroup [WeaklyLocallyCompactSpace G] : LocallyCompactSpace G := WeaklyLocallyCompactSpace.locallyCompactSpace @@ -1830,7 +1830,7 @@ theorem HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group /-- In a locally compact group, any neighborhood of the identity contains a compact closed neighborhood of the identity, even without separation assumptions on the space. -/ -@[to_additive (attr := deprecated isCompact_isClosed_basis_nhds) +@[to_additive (attr := deprecated isCompact_isClosed_basis_nhds) -- Since 28 Jan 2024 "In a locally compact additive group, any neighborhood of the identity contains a compact closed neighborhood of the identity, even without separation assumptions on the space."] theorem local_isCompact_isClosed_nhds_of_group [LocallyCompactSpace G] {U : Set G} @@ -1843,7 +1843,7 @@ theorem local_isCompact_isClosed_nhds_of_group [LocallyCompactSpace G] {U : Set variable (G) -@[to_additive (attr := deprecated exists_mem_nhds_isCompact_isClosed)] +@[to_additive (attr := deprecated exists_mem_nhds_isCompact_isClosed)] -- Since 28 Jan 2024 theorem exists_isCompact_isClosed_nhds_one [WeaklyLocallyCompactSpace G] : ∃ K : Set G, IsCompact K ∧ IsClosed K ∧ K ∈ 𝓝 1 := let ⟨K, hK₁, hKcomp, hKcl⟩ := exists_mem_nhds_isCompact_isClosed (1 : G) diff --git a/Mathlib/Topology/Compactness/LocallyCompact.lean b/Mathlib/Topology/Compactness/LocallyCompact.lean index c2ce357544663..747b456253a5c 100644 --- a/Mathlib/Topology/Compactness/LocallyCompact.lean +++ b/Mathlib/Topology/Compactness/LocallyCompact.lean @@ -161,9 +161,9 @@ most notably in `ContinuousMap.continuous_comp'` and `ContinuousMap.continuous_e It is satisfied in two cases: - if `X` is a locally compact topological space, for obvious reasons; -- if `X` is a weakly locally compact topological space and `Y` is a preregular space; +- if `X` is a weakly locally compact topological space and `Y` is an R₁ space; this fact is a simple generalization of the theorem - saying that a weakly locally compact preregular topological space is locally compact. + saying that a weakly locally compact R₁ topological space is locally compact. -/ class LocallyCompactPair (X Y : Type*) [TopologicalSpace X] [TopologicalSpace Y] : Prop where /-- If `f : X → Y` is a continuous map in a locally compact pair of topological spaces diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index a90017ae7007e..f8e0e0487cb37 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -914,7 +914,7 @@ theorem TopologicalSpace.subset_trans {s t : Set X} (ts : t ⊆ s) : (embedding_inclusion ts).induced #align topological_space.subset_trans TopologicalSpace.subset_trans -/-! ### Preregular (R₁) spaces -/ +/-! ### R₁ (preregular) spaces -/ section R1Space @@ -968,7 +968,7 @@ theorem isClosed_setOf_inseparable : IsClosed { p : X × X | Inseparable p.1 p.2 simp only [← specializes_iff_inseparable, isClosed_setOf_specializes] #align is_closed_set_of_inseparable isClosed_setOf_inseparable -/-- In a preregular space, a point belongs to the closure of a compact set `K` +/-- In an R₁ space, a point belongs to the closure of a compact set `K` if and only if it is topologically inseparable from some point of `K`. -/ theorem IsCompact.mem_closure_iff_exists_inseparable {K : Set X} (hK : IsCompact K) : y ∈ closure K ↔ ∃ x ∈ K, Inseparable x y := by @@ -984,14 +984,14 @@ theorem IsCompact.closure_eq_biUnion_inseparable {K : Set X} (hK : IsCompact K) closure K = ⋃ x ∈ K, {y | Inseparable x y} := by ext; simp [hK.mem_closure_iff_exists_inseparable] -/-- In a preregular space, if a compact set `K` is contained in an open set `U`, +/-- In an R₁ space, if a compact set `K` is contained in an open set `U`, then its closure is also contained in `U`. -/ theorem IsCompact.closure_subset_of_isOpen {K : Set X} (hK : IsCompact K) {U : Set X} (hU : IsOpen U) (hKU : K ⊆ U) : closure K ⊆ U := by rw [hK.closure_eq_biUnion_inseparable, iUnion₂_subset_iff] exact fun x hx y hxy ↦ (hxy.mem_open_iff hU).1 (hKU hx) -/-- The closure of a compact set in a preregular space is a compact set. -/ +/-- The closure of a compact set in an R₁ space is a compact set. -/ protected theorem IsCompact.closure {K : Set X} (hK : IsCompact K) : IsCompact (closure K) := by refine isCompact_of_finite_subcover fun U hUo hKU ↦ ?_ rcases hK.elim_finite_subcover U hUo (subset_closure.trans hKU) with ⟨t, ht⟩ @@ -1014,7 +1014,7 @@ theorem exists_isCompact_superset_iff {s : Set X} : @[deprecated] -- Since 28 Jan 2024 alias exists_compact_superset_iff := exists_isCompact_superset_iff -/-- If `K` and `L` are disjoint compact sets in a preregular topological space +/-- If `K` and `L` are disjoint compact sets in an R₁ topological space and `L` is also closed, then `K` and `L` have disjoint neighborhoods. -/ theorem SeparatedNhds.of_isCompact_isCompact_isClosed {K L : Set X} (hK : IsCompact K) (hL : IsCompact L) (h'L : IsClosed L) (hd : Disjoint K L) : SeparatedNhds K L := by @@ -1128,7 +1128,7 @@ instance (priority := 900) {X Y : Type*} [TopologicalSpace X] [WeaklyLocallyComp let ⟨_K, hKc, hKx⟩ := exists_compact_mem_nhds _ exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds hf hs hKc hKx -/-- If a point in a preregular space has a compact neighborhood, +/-- If a point in an R₁ space has a compact neighborhood, then it has a basis of compact closed neighborhoods. -/ theorem IsCompact.isCompact_isClosed_basis_nhds {x : X} {L : Set X} (hLc : IsCompact L) (hxL : L ∈ 𝓝 x) : (𝓝 x).HasBasis (fun K ↦ K ∈ 𝓝 x ∧ IsCompact K ∧ IsClosed K) (·) := @@ -1139,7 +1139,7 @@ theorem IsCompact.isCompact_isClosed_basis_nhds {x : X} {L : Set X} (hLc : IsCom (hKc.closure_subset_of_isOpen isOpen_interior hKU).trans interior_subset⟩ /-! -### Lemmas about a weakly locally compact preregular space +### Lemmas about a weakly locally compact R₁ space In fact, a space with these properties is locally compact and regular. Some lemmas are formulated using the latter assumptions below. @@ -1159,12 +1159,12 @@ theorem exists_mem_nhds_isCompact_isClosed (x : X) : ∃ K ∈ 𝓝 x, IsCompact (isCompact_isClosed_basis_nhds x).ex_mem -- see Note [lower instance priority] -/-- A weakly locally compact preregular space is locally compact. -/ +/-- A weakly locally compact R₁ space is locally compact. -/ instance (priority := 80) WeaklyLocallyCompactSpace.locallyCompactSpace : LocallyCompactSpace X := .of_hasBasis isCompact_isClosed_basis_nhds fun _ _ ⟨_, h, _⟩ ↦ h #align locally_compact_of_compact_nhds WeaklyLocallyCompactSpace.locallyCompactSpace -/-- In a weakly locally compact preregular space, +/-- In a weakly locally compact R₁ space, every compact set has an open neighborhood with compact closure. -/ theorem exists_isOpen_superset_and_isCompact_closure {K : Set X} (hK : IsCompact K) : ∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V) := by @@ -1635,7 +1635,7 @@ theorem SeparatedNhds.of_singleton_finset [T2Space X] {x : X} {s : Finset X} (h mod_cast .of_finset_finset {x} s (Finset.disjoint_singleton_left.mpr h) #align point_disjoint_finset_opens_of_t2 SeparatedNhds.of_singleton_finset -@[deprecated] +@[deprecated] -- Since 28 Jan 2024 alias point_disjoint_finset_opens_of_t2 := SeparatedNhds.of_singleton_finset end SeparatedFinset @@ -1809,7 +1809,7 @@ theorem disjoint_nhds_nhdsSet : Disjoint (𝓝 x) (𝓝ˢ s) ↔ x ∉ closure s disjoint_comm.trans disjoint_nhdsSet_nhds #align disjoint_nhds_nhds_set disjoint_nhds_nhdsSet -/-- A regular space is preregular. -/ +/-- A regular space is R₁. -/ instance (priority := 100) : R1Space X where specializes_or_disjoint_nhds _ _ := or_iff_not_imp_left.2 fun h ↦ by rwa [← nhdsSet_singleton, disjoint_nhdsSet_nhds, ← specializes_iff_mem_closure] From 11fe8b19a8015c987eaa68dc5e21b497600d3176 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Mon, 29 Jan 2024 08:48:51 -0600 Subject: [PATCH 12/16] =?UTF-8?q?Search=20for=20`T[2=E2=82=82].*\`,?= =?UTF-8?q?=20edit?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/MeasureTheory/Measure/Content.lean | 6 +++--- Mathlib/Topology/Separation.lean | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/MeasureTheory/Measure/Content.lean b/Mathlib/MeasureTheory/Measure/Content.lean index 532d2bcfada82..f73023f30ecf7 100644 --- a/Mathlib/MeasureTheory/Measure/Content.lean +++ b/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 diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index f8e0e0487cb37..f831ed54030f6 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -1175,7 +1175,7 @@ theorem exists_isOpen_superset_and_isCompact_closure {K : Set X} (hK : IsCompact @[deprecated] -- Since 28 Jan 2024 alias exists_open_superset_and_isCompact_closure := exists_isOpen_superset_and_isCompact_closure -/-- In a weakly locally compact which is either T₂ or locally compact regular, +/-- In a weakly locally compact R₁ space, every point has an open neighborhood with compact closure. -/ theorem exists_isOpen_mem_isCompact_closure (x : X) : ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U) := by From 54294075c740beb2b713b257534c2f63bd08d2ba Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Mon, 29 Jan 2024 08:58:24 -0600 Subject: [PATCH 13/16] Fix docs, add a lemma --- Mathlib/Topology/Separation.lean | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index f831ed54030f6..76ce9a1b1d2af 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -935,20 +935,21 @@ theorem disjoint_nhds_nhds_iff_not_specializes : Disjoint (𝓝 x) (𝓝 y) ↔ theorem specializes_iff_not_disjoint : x ⤳ y ↔ ¬Disjoint (𝓝 x) (𝓝 y) := disjoint_nhds_nhds_iff_not_specializes.not_left.symm -/-- In an R₁ space, the `Specializes` relation is symmetric, i.e., an R₁ is an R₀ space. -/ +/-- In an R₁ space, the `Specializes` relation is symmetric, i.e., an R₁ is an R₀ space. -/ theorem Specializes.symm (h : x ⤳ y) : y ⤳ x := by simpa only [specializes_iff_not_disjoint, disjoint_comm] using h #align specializes.symm Specializes.symm -/-- An R₁ space is an R₀ space: the `Specializes` relation is symmetric. -/ +/-- In an R₁ space, the `Specializes` relation is symmetric, i.e., an R₁ is an R₀ space. -/ theorem specializes_comm : x ⤳ y ↔ y ⤳ x := ⟨Specializes.symm, Specializes.symm⟩ #align specializes_comm specializes_comm +/-- In an R₁ space, the `Specializes` is equivalent to `Inseparable`, i.e., an R₁ is an R₀ space. -/ theorem specializes_iff_inseparable : x ⤳ y ↔ Inseparable x y := ⟨fun h ↦ h.antisymm h.symm, Inseparable.specializes⟩ #align specializes_iff_inseparable specializes_iff_inseparable -/-- An R₁ space is an R₀ space: if `x` specializes `y`, then they are inseparable. -/ +/-- An R₁ space, if `x` specializes `y`, then they are inseparable, i.e., an R₁ is an R₀ space. -/ alias ⟨Specializes.inseparable, _⟩ := specializes_iff_inseparable theorem disjoint_nhds_nhds_iff_not_inseparable : Disjoint (𝓝 x) (𝓝 y) ↔ ¬Inseparable x y := by @@ -984,6 +985,12 @@ theorem IsCompact.closure_eq_biUnion_inseparable {K : Set X} (hK : IsCompact K) closure K = ⋃ x ∈ K, {y | Inseparable x y} := by ext; simp [hK.mem_closure_iff_exists_inseparable] +/-- In an R₁ space, the closure of a compact set is the union of the closures of its points. -/ +theorem IsCompact.closure_eq_biUnion_closure_singleton {K : Set X} (hK : IsCompact K) : + closure K = ⋃ x ∈ K, closure {x} := by + simp only [hK.closure_eq_biUnion_inseparable, ← specializes_iff_inseparable, + specializes_iff_mem_closure, setOf_mem_eq] + /-- In an R₁ space, if a compact set `K` is contained in an open set `U`, then its closure is also contained in `U`. -/ theorem IsCompact.closure_subset_of_isOpen {K : Set X} (hK : IsCompact K) From 2a0919453746d1481bb1fc0f55c23549943cb503 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Mon, 29 Jan 2024 09:11:30 -0600 Subject: [PATCH 14/16] "the", newlines --- Mathlib/Topology/Separation.lean | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index 76ce9a1b1d2af..86b800caf469a 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -935,21 +935,25 @@ theorem disjoint_nhds_nhds_iff_not_specializes : Disjoint (𝓝 x) (𝓝 y) ↔ theorem specializes_iff_not_disjoint : x ⤳ y ↔ ¬Disjoint (𝓝 x) (𝓝 y) := disjoint_nhds_nhds_iff_not_specializes.not_left.symm -/-- In an R₁ space, the `Specializes` relation is symmetric, i.e., an R₁ is an R₀ space. -/ +/-- In an R₁ space, the `Specializes` relation is symmetric, +i.e., an R₁ space is an R₀ space. -/ theorem Specializes.symm (h : x ⤳ y) : y ⤳ x := by simpa only [specializes_iff_not_disjoint, disjoint_comm] using h #align specializes.symm Specializes.symm -/-- In an R₁ space, the `Specializes` relation is symmetric, i.e., an R₁ is an R₀ space. -/ +/-- In an R₁ space, the `Specializes` relation is symmetric, +i.e., an R₁ space is an R₀ space. -/ theorem specializes_comm : x ⤳ y ↔ y ⤳ x := ⟨Specializes.symm, Specializes.symm⟩ #align specializes_comm specializes_comm -/-- In an R₁ space, the `Specializes` is equivalent to `Inseparable`, i.e., an R₁ is an R₀ space. -/ +/-- In an R₁ space, `Specializes` is equivalent to `Inseparable`, +i.e., an R₁ space is an R₀ space. -/ theorem specializes_iff_inseparable : x ⤳ y ↔ Inseparable x y := ⟨fun h ↦ h.antisymm h.symm, Inseparable.specializes⟩ #align specializes_iff_inseparable specializes_iff_inseparable -/-- An R₁ space, if `x` specializes `y`, then they are inseparable, i.e., an R₁ is an R₀ space. -/ +/-- An R₁ space, if `x` specializes `y`, then they are inseparable, +i.e., an R₁ space is an R₀ space. -/ alias ⟨Specializes.inseparable, _⟩ := specializes_iff_inseparable theorem disjoint_nhds_nhds_iff_not_inseparable : Disjoint (𝓝 x) (𝓝 y) ↔ ¬Inseparable x y := by From f57c526887e1e758d6ca30e0ee13c5eac9fa1cbc Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Mon, 29 Jan 2024 10:37:58 -0600 Subject: [PATCH 15/16] Migrate from deprecated lemmas --- Mathlib/MeasureTheory/Group/Measure.lean | 12 ++++++------ Mathlib/MeasureTheory/Measure/Haar/Basic.lean | 7 +++---- 2 files changed, 9 insertions(+), 10 deletions(-) diff --git a/Mathlib/MeasureTheory/Group/Measure.lean b/Mathlib/MeasureTheory/Group/Measure.lean index dc63ab4ad6a23..f4bcac50511fa 100644 --- a/Mathlib/MeasureTheory/Group/Measure.lean +++ b/Mathlib/MeasureTheory/Group/Measure.lean @@ -760,7 +760,7 @@ 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 (attr := deprecated)] -- Since 28 Jan 2024 +@[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 := hk.closure_subset_measurableSet hs h @@ -776,10 +776,10 @@ 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 [h : InnerRegularCompactLTTop μ] : @@ -787,8 +787,8 @@ lemma innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group [h : InnerRegul 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 diff --git a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean index 8eebd03f98e54..7ff491b64f82c 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean @@ -658,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."] @@ -717,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' @@ -766,8 +766,7 @@ theorem haarMeasure_unique (μ : Measure G) [SigmaFinite μ] [IsMulLeftInvariant 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 From 40b5aff5711e6b4f43f2b746a170a8a0dc7860a3 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Mon, 29 Jan 2024 12:03:35 -0600 Subject: [PATCH 16/16] Update Mathlib/Topology/Separation.lean Co-authored-by: Jeremy Tan Jie Rui --- Mathlib/Topology/Separation.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index 86b800caf469a..2b9eec5b511b7 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -952,7 +952,7 @@ theorem specializes_iff_inseparable : x ⤳ y ↔ Inseparable x y := ⟨fun h ↦ h.antisymm h.symm, Inseparable.specializes⟩ #align specializes_iff_inseparable specializes_iff_inseparable -/-- An R₁ space, if `x` specializes `y`, then they are inseparable, +/-- In an R₁ space, `Specializes` implies `Inseparable`, i.e., an R₁ space is an R₀ space. -/ alias ⟨Specializes.inseparable, _⟩ := specializes_iff_inseparable