From 74e301d4944443800daa74ba4e61aaeacad0d3af Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 18 Nov 2023 14:39:04 +0100 Subject: [PATCH 1/3] Urysohn's lemma: exists_continuous_zero_one_of_closed -> isClosed. --- Mathlib/MeasureTheory/Function/ContinuousMapDense.lean | 2 +- Mathlib/Topology/Category/CompHaus/Basic.lean | 2 +- Mathlib/Topology/CompletelyRegular.lean | 2 +- Mathlib/Topology/ContinuousFunction/Ideals.lean | 4 ++-- Mathlib/Topology/Metrizable/Urysohn.lean | 2 +- Mathlib/Topology/PartitionOfUnity.lean | 2 +- Mathlib/Topology/UrysohnsBounded.lean | 4 ++-- Mathlib/Topology/UrysohnsLemma.lean | 6 +++--- docs/overview.yaml | 2 +- 9 files changed, 13 insertions(+), 13 deletions(-) diff --git a/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean b/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean index f31e525030db7..697563e5e04fd 100644 --- a/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean +++ b/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean @@ -93,7 +93,7 @@ theorem exists_continuous_snorm_sub_le_of_closed [μ.OuterRegular] (hp : p ≠ have hsv : s ⊆ v := subset_inter hsu sV have hμv : μ v < ∞ := (measure_mono (inter_subset_right _ _)).trans_lt h'V obtain ⟨g, hgv, hgs, hg_range⟩ := - exists_continuous_zero_one_of_closed (u_open.inter V_open).isClosed_compl s_closed + exists_continuous_zero_one_of_isClosed (u_open.inter V_open).isClosed_compl s_closed (disjoint_compl_left_iff.2 hsv) -- Multiply this by `c` to get a continuous approximation to the function `f`; the key point is -- that this is pointwise bounded by the indicator of the set `v \ s`, which has small measure. diff --git a/Mathlib/Topology/Category/CompHaus/Basic.lean b/Mathlib/Topology/Category/CompHaus/Basic.lean index 5469cc845c5e2..621e39f4946ae 100644 --- a/Mathlib/Topology/Category/CompHaus/Basic.lean +++ b/Mathlib/Topology/Category/CompHaus/Basic.lean @@ -340,7 +340,7 @@ theorem epi_iff_surjective {X Y : CompHaus.{u}} (f : X ⟶ Y) : Epi f ↔ Functi rw [Set.disjoint_singleton_right] rintro ⟨y', hy'⟩ exact hy y' hy' - obtain ⟨φ, hφ0, hφ1, hφ01⟩ := exists_continuous_zero_one_of_closed hC hD hCD + obtain ⟨φ, hφ0, hφ1, hφ01⟩ := exists_continuous_zero_one_of_isClosed hC hD hCD haveI : CompactSpace (ULift.{u} <| Set.Icc (0 : ℝ) 1) := Homeomorph.ulift.symm.compactSpace haveI : T2Space (ULift.{u} <| Set.Icc (0 : ℝ) 1) := Homeomorph.ulift.symm.t2Space let Z := of (ULift.{u} <| Set.Icc (0 : ℝ) 1) diff --git a/Mathlib/Topology/CompletelyRegular.lean b/Mathlib/Topology/CompletelyRegular.lean index 653f17818480f..910224c0ffddb 100644 --- a/Mathlib/Topology/CompletelyRegular.lean +++ b/Mathlib/Topology/CompletelyRegular.lean @@ -75,7 +75,7 @@ instance NormalSpace.completelyRegularSpace [NormalSpace X] : CompletelyRegularS intro x K hK hx have cx : IsClosed {x} := by apply T1Space.t1 have d : Disjoint {x} K := by rwa [Set.disjoint_iff, subset_empty_iff, singleton_inter_eq_empty] - let ⟨⟨f, cf⟩, hfx, hfK, hficc⟩ := exists_continuous_zero_one_of_closed cx hK d + let ⟨⟨f, cf⟩, hfx, hfK, hficc⟩ := exists_continuous_zero_one_of_isClosed cx hK d let g : X → I := fun x => ⟨f x, hficc x⟩ have cg : Continuous g := cf.subtype_mk hficc have hgx : g x = 0 := Subtype.ext (hfx (mem_singleton_iff.mpr (Eq.refl x))) diff --git a/Mathlib/Topology/ContinuousFunction/Ideals.lean b/Mathlib/Topology/ContinuousFunction/Ideals.lean index c4eb7169d16c2..7340945618b49 100644 --- a/Mathlib/Topology/ContinuousFunction/Ideals.lean +++ b/Mathlib/Topology/ContinuousFunction/Ideals.lean @@ -324,7 +324,7 @@ theorem setOfIdeal_ofSet_eq_interior (s : Set X) : setOfIdeal (idealOfSet 𝕜 s /- Apply Urysohn's lemma to get `g : C(X, ℝ)` which is zero on `sᶜ` and `g x ≠ 0`, then compose with the natural embedding `ℝ ↪ 𝕜` to produce the desired `f`. -/ obtain ⟨g, hgs, hgx : Set.EqOn g 1 {x}, -⟩ := - exists_continuous_zero_one_of_closed isClosed_closure isClosed_singleton + exists_continuous_zero_one_of_isClosed isClosed_closure isClosed_singleton (Set.disjoint_singleton_right.mpr hx) exact ⟨⟨fun x => g x, continuous_ofReal.comp (map_continuous g)⟩, by @@ -435,7 +435,7 @@ variable [CompactSpace X] [T2Space X] [IsROrC 𝕜] theorem continuousMapEval_bijective : Bijective (continuousMapEval X 𝕜) := by refine' ⟨fun x y hxy => _, fun φ => _⟩ · contrapose! hxy - rcases exists_continuous_zero_one_of_closed (isClosed_singleton : _root_.IsClosed {x}) + rcases exists_continuous_zero_one_of_isClosed (isClosed_singleton : _root_.IsClosed {x}) (isClosed_singleton : _root_.IsClosed {y}) (Set.disjoint_singleton.mpr hxy) with ⟨f, fx, fy, -⟩ rw [FunLike.ne_iff] diff --git a/Mathlib/Topology/Metrizable/Urysohn.lean b/Mathlib/Topology/Metrizable/Urysohn.lean index e80219edb5447..a845af699534a 100644 --- a/Mathlib/Topology/Metrizable/Urysohn.lean +++ b/Mathlib/Topology/Metrizable/Urysohn.lean @@ -62,7 +62,7 @@ theorem exists_inducing_l_infty : ∃ f : X → ℕ →ᵇ ℝ, Inducing f := by have : ∀ UV : s, ∃ f : C(X, ℝ), EqOn f 0 UV.1.1 ∧ EqOn f (fun _ => ε UV) UV.1.2ᶜ ∧ ∀ x, f x ∈ Icc 0 (ε UV) := by intro UV - rcases exists_continuous_zero_one_of_closed isClosed_closure + rcases exists_continuous_zero_one_of_isClosed isClosed_closure (hB.isOpen UV.2.1.2).isClosed_compl (hd UV) with ⟨f, hf₀, hf₁, hf01⟩ exact ⟨ε UV • f, fun x hx => by simp [hf₀ (subset_closure hx)], fun x hx => by simp [hf₁ hx], diff --git a/Mathlib/Topology/PartitionOfUnity.lean b/Mathlib/Topology/PartitionOfUnity.lean index 02bcfe1bbc1fb..8a3267b212c00 100644 --- a/Mathlib/Topology/PartitionOfUnity.lean +++ b/Mathlib/Topology/PartitionOfUnity.lean @@ -321,7 +321,7 @@ theorem exists_isSubordinate_of_locallyFinite [NormalSpace X] (hs : IsClosed s) let ⟨f, _, hfU⟩ := exists_isSubordinate_of_locallyFinite_of_prop (fun _ => True) (fun _ _ hs ht hd => - (exists_continuous_zero_one_of_closed hs ht hd).imp fun _ hf => ⟨trivial, hf⟩) + (exists_continuous_zero_one_of_isClosed hs ht hd).imp fun _ hf => ⟨trivial, hf⟩) hs U ho hf hU ⟨f, hfU⟩ #align bump_covering.exists_is_subordinate_of_locally_finite BumpCovering.exists_isSubordinate_of_locallyFinite diff --git a/Mathlib/Topology/UrysohnsBounded.lean b/Mathlib/Topology/UrysohnsBounded.lean index 991dfca1f6069..2309ce0f181c4 100644 --- a/Mathlib/Topology/UrysohnsBounded.lean +++ b/Mathlib/Topology/UrysohnsBounded.lean @@ -11,7 +11,7 @@ import Mathlib.Topology.ContinuousFunction.Bounded /-! # Urysohn's lemma for bounded continuous functions -In this file we reformulate Urysohn's lemma `exists_continuous_zero_one_of_closed` in terms of +In this file we reformulate Urysohn's lemma `exists_continuous_zero_one_of_isClosed` in terms of bounded continuous functions `X →ᵇ ℝ`. These lemmas live in a separate file because `Topology.ContinuousFunction.Bounded` imports too many other files. @@ -35,7 +35,7 @@ then there exists a continuous function `f : X → ℝ` such that theorem exists_bounded_zero_one_of_closed {X : Type*} [TopologicalSpace X] [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) : ∃ f : X →ᵇ ℝ, EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 := - let ⟨f, hfs, hft, hf⟩ := exists_continuous_zero_one_of_closed hs ht hd + let ⟨f, hfs, hft, hf⟩ := exists_continuous_zero_one_of_isClosed hs ht hd ⟨⟨f, 1, fun _ _ => Real.dist_le_of_mem_Icc_01 (hf _) (hf _)⟩, hfs, hft, hf⟩ #align exists_bounded_zero_one_of_closed exists_bounded_zero_one_of_closed diff --git a/Mathlib/Topology/UrysohnsLemma.lean b/Mathlib/Topology/UrysohnsLemma.lean index 24ac35cef721e..c699350165bc7 100644 --- a/Mathlib/Topology/UrysohnsLemma.lean +++ b/Mathlib/Topology/UrysohnsLemma.lean @@ -12,7 +12,7 @@ import Mathlib.Topology.ContinuousFunction.Basic /-! # Urysohn's lemma -In this file we prove Urysohn's lemma `exists_continuous_zero_one_of_closed`: for any two disjoint +In this file we prove Urysohn's lemma `exists_continuous_zero_one_of_isClosed`: for any two disjoint closed sets `s` and `t` in a normal topological space `X` there exists a continuous function `f : X → ℝ` such that @@ -320,7 +320,7 @@ then there exists a continuous function `f : X → ℝ` such that * `f` equals one on `t`; * `0 ≤ f x ≤ 1` for all `x`. -/ -theorem exists_continuous_zero_one_of_closed [NormalSpace X] +theorem exists_continuous_zero_one_of_isClosed [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) : ∃ f : C(X, ℝ), EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 := by -- The actual proof is in the code above. Here we just repack it into the expected format. @@ -338,7 +338,7 @@ theorem exists_continuous_zero_one_of_closed [NormalSpace X] exact ⟨v, v_open, cv, hv, trivial⟩ } exact ⟨⟨c.lim, c.continuous_lim⟩, c.lim_of_mem_C, fun x hx => c.lim_of_nmem_U _ fun h => h hx, c.lim_mem_Icc⟩ -#align exists_continuous_zero_one_of_closed exists_continuous_zero_one_of_closed +#align exists_continuous_zero_one_of_isClosed exists_continuous_zero_one_of_isClosed /-- Urysohn's lemma: if `s` and `t` are two disjoint sets in a regular locally compact topological space `X`, with `s` compact and `t` closed, then there exists a continuous diff --git a/docs/overview.yaml b/docs/overview.yaml index cf8e008e6ad3a..b87559d193664 100644 --- a/docs/overview.yaml +++ b/docs/overview.yaml @@ -217,7 +217,7 @@ Topology: Stone-Cech compactification: 'StoneCech' topological fiber bundle: 'FiberBundle' topological vector bundle: 'VectorBundle' - Urysohn's lemma: 'exists_continuous_zero_one_of_closed' + Urysohn's lemma: 'exists_continuous_zero_one_of_isClosed' Stone-Weierstrass theorem: 'ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints' Uniform notions: uniform space: 'UniformSpace' From 247ce2eee8e3d0dbab94f1b289e0cf2f04d83a58 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 18 Nov 2023 14:41:43 +0100 Subject: [PATCH 2/3] of_closed_map, of_closed_map -> _of_isClosedMap --- Mathlib/Topology/Connected/Basic.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/Topology/Connected/Basic.lean b/Mathlib/Topology/Connected/Basic.lean index a90006f21a6ad..21a19c11f40ba 100644 --- a/Mathlib/Topology/Connected/Basic.lean +++ b/Mathlib/Topology/Connected/Basic.lean @@ -383,7 +383,7 @@ theorem IsPreconnected.preimage_of_open_map [TopologicalSpace β] {s : Set β} ( · exact ⟨a, has, hau, hinj.mem_set_image.1 hav⟩ #align is_preconnected.preimage_of_open_map IsPreconnected.preimage_of_open_map -theorem IsPreconnected.preimage_of_closed_map [TopologicalSpace β] {s : Set β} +theorem IsPreconnected.preimage_of_isClosedMap [TopologicalSpace β] {s : Set β} (hs : IsPreconnected s) {f : α → β} (hinj : Function.Injective f) (hf : IsClosedMap f) (hsf : s ⊆ range f) : IsPreconnected (f ⁻¹' s) := isPreconnected_closed_iff.2 fun u v hu hv hsuv hsu hsv => by @@ -394,7 +394,7 @@ theorem IsPreconnected.preimage_of_closed_map [TopologicalSpace β] {s : Set β} · simpa only [image_preimage_inter] using hsu.image f · simpa only [image_preimage_inter] using hsv.image f · exact ⟨a, has, hau, hinj.mem_set_image.1 hav⟩ -#align is_preconnected.preimage_of_closed_map IsPreconnected.preimage_of_closed_map +#align is_preconnected.preimage_of_closed_map IsPreconnected.preimage_of_isClosedMap theorem IsConnected.preimage_of_openMap [TopologicalSpace β] {s : Set β} (hs : IsConnected s) {f : α → β} (hinj : Function.Injective f) (hf : IsOpenMap f) (hsf : s ⊆ range f) : @@ -402,11 +402,11 @@ theorem IsConnected.preimage_of_openMap [TopologicalSpace β] {s : Set β} (hs : ⟨hs.nonempty.preimage' hsf, hs.isPreconnected.preimage_of_open_map hinj hf hsf⟩ #align is_connected.preimage_of_open_map IsConnected.preimage_of_openMap -theorem IsConnected.preimage_of_closedMap [TopologicalSpace β] {s : Set β} (hs : IsConnected s) +theorem IsConnected.preimage_of_isClosedMap [TopologicalSpace β] {s : Set β} (hs : IsConnected s) {f : α → β} (hinj : Function.Injective f) (hf : IsClosedMap f) (hsf : s ⊆ range f) : IsConnected (f ⁻¹' s) := - ⟨hs.nonempty.preimage' hsf, hs.isPreconnected.preimage_of_closed_map hinj hf hsf⟩ -#align is_connected.preimage_of_closed_map IsConnected.preimage_of_closedMap + ⟨hs.nonempty.preimage' hsf, hs.isPreconnected.preimage_of_isClosedMap hinj hf hsf⟩ +#align is_connected.preimage_of_closed_map IsConnected.preimage_of_isClosedMap theorem IsPreconnected.subset_or_subset (hu : IsOpen u) (hv : IsOpen v) (huv : Disjoint u v) (hsuv : s ⊆ u ∪ v) (hs : IsPreconnected s) : s ⊆ u ∨ s ⊆ v := by From 7bb1b882fd55718cc7e48734c96cc5f1ef67b637 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 29 Nov 2023 14:33:06 +0100 Subject: [PATCH 3/3] Fixup. --- Mathlib/Topology/UrysohnsLemma.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/UrysohnsLemma.lean b/Mathlib/Topology/UrysohnsLemma.lean index c699350165bc7..928f36b630709 100644 --- a/Mathlib/Topology/UrysohnsLemma.lean +++ b/Mathlib/Topology/UrysohnsLemma.lean @@ -338,7 +338,7 @@ theorem exists_continuous_zero_one_of_isClosed [NormalSpace X] exact ⟨v, v_open, cv, hv, trivial⟩ } exact ⟨⟨c.lim, c.continuous_lim⟩, c.lim_of_mem_C, fun x hx => c.lim_of_nmem_U _ fun h => h hx, c.lim_mem_Icc⟩ -#align exists_continuous_zero_one_of_isClosed exists_continuous_zero_one_of_isClosed +#align exists_continuous_zero_one_of_closed exists_continuous_zero_one_of_isClosed /-- Urysohn's lemma: if `s` and `t` are two disjoint sets in a regular locally compact topological space `X`, with `s` compact and `t` closed, then there exists a continuous