[Merged by Bors] - chore: rename some lemmas involving "of_closed"

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.

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)

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)))

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,19 +394,19 @@ 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) :
     IsConnected (f ⁻¹' s) :=
   ⟨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

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]

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],

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

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
 

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_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

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'