chore: rename most lemmas involving clopen to isClopen (#8720)

This PR renames the field Clopens.clopen' -> Clopens.isClopen', and the lemmas
* preimage_closed_of_closed -> ContinuousOn.preimage_isClosed_of_isClosed

as well as:
ClopenUpperSet.clopen -> ClopenUpperSet.isClopen
connectedComponent_eq_iInter_clopen -> connectedComponent_eq_iInter_isClopen
connectedComponent_subset_iInter_clopen -> connectedComponent_subset_iInter_isClopen
continuous_boolIndicator_iff_clopen -> continuous_boolIndicator_iff_isClopen
continuousOn_boolIndicator_iff_clopen -> continuousOn_boolIndicator_iff_isClopen
DiscreteQuotient.ofClopen -> DiscreteQuotient.ofIsClopen
disjoint_or_subset_of_clopen -> disjoint_or_subset_of_isClopen
exists_clopen_{lower,upper}_of_not_le -> exists_isClopen_{lower,upper}_of_not_le
exists_clopen_of_cofiltered -> exists_isClopen_of_cofiltered
exists_clopen_of_totally_separated -> exists_isClopen_of_totally_separated
exists_clopen_upper_or_lower_of_ne -> exists_isClopen_upper_or_lower_of_ne
IsPreconnected.subset_clopen -> IsPreconnected.subset_isClopen
isTotallyDisconnected_of_clopen_set -> isTotallyDisconnected_of_isClopen_set
LocallyConstant.ofClopen_fiber_one -> LocallyConstant.ofIsClopen_fiber_one
LocallyConstant.ofClopen_fiber_zero -> LocallyConstant.ofIsClopen_fiber_zero
LocallyConstant.ofClopen -> LocallyConstant.ofIsClopen
preimage_clopen_of_clopen -> preimage_isClopen_of_isClopen
TopologicalSpace.Clopens.clopen -> TopologicalSpace.Clopens.isClopen

Counterexamples/SorgenfreyLine.lean

@@ -179,8 +179,8 @@ theorem isClopen_Ico (a b : ℝₗ) : IsClopen (Ico a b) :=
 
 instance : TotallyDisconnectedSpace ℝₗ :=
   ⟨fun _ _ hs x hx y hy =>
-    le_antisymm (hs.subset_clopen (isClopen_Ici x) ⟨x, hx, left_mem_Ici⟩ hy)
-      (hs.subset_clopen (isClopen_Ici y) ⟨y, hy, left_mem_Ici⟩ hx)⟩
+    le_antisymm (hs.subset_isClopen (isClopen_Ici x) ⟨x, hx, left_mem_Ici⟩ hy)
+      (hs.subset_isClopen (isClopen_Ici y) ⟨y, hy, left_mem_Ici⟩ hx)⟩
 
 instance : FirstCountableTopology ℝₗ :=
   ⟨fun x => (nhds_basis_Ico_rat x).isCountablyGenerated⟩

Mathlib/Analysis/Calculus/MeanValue.lean

@@ -103,7 +103,7 @@ theorem image_le_of_liminf_slope_right_lt_deriv_boundary' {f f' : ℝ → ℝ} {
   have A : ContinuousOn (fun x => (f x, B x)) (Icc a b) := hf.prod hB
   have : IsClosed s := by
     simp only [inter_comm]
-    exact A.preimage_closed_of_closed isClosed_Icc OrderClosedTopology.isClosed_le'
+    exact A.preimage_isClosed_of_isClosed isClosed_Icc OrderClosedTopology.isClosed_le'
   apply this.Icc_subset_of_forall_exists_gt ha
   rintro x ⟨hxB : f x ≤ B x, xab⟩ y hy
   cases' hxB.lt_or_eq with hxB hxB

Mathlib/FieldTheory/KrullTopology.lean

@@ -260,7 +260,7 @@ section TotallyDisconnected
   totally disconnected. -/
 theorem krullTopology_totallyDisconnected {K L : Type*} [Field K] [Field L] [Algebra K L]
     (h_int : Algebra.IsIntegral K L) : IsTotallyDisconnected (Set.univ : Set (L ≃ₐ[K] L)) := by
-  apply isTotallyDisconnected_of_clopen_set
+  apply isTotallyDisconnected_of_isClopen_set
   intro σ τ h_diff
   have hστ : σ⁻¹ * τ ≠ 1 := by rwa [Ne.def, inv_mul_eq_one]
   rcases FunLike.exists_ne hστ with ⟨x, hx : (σ⁻¹ * τ) x ≠ x⟩

Mathlib/Geometry/Manifold/BumpFunction.lean

@@ -214,7 +214,7 @@ theorem nhdsWithin_range_basis :
 theorem isClosed_image_of_isClosed {s : Set M} (hsc : IsClosed s) (hs : s ⊆ support f) :
     IsClosed (extChartAt I c '' s) := by
   rw [f.image_eq_inter_preimage_of_subset_support hs]
-  refine' ContinuousOn.preimage_closed_of_closed
+  refine' ContinuousOn.preimage_isClosed_of_isClosed
     ((continuousOn_extChartAt_symm _ _).mono f.closedBall_subset) _ hsc
   exact IsClosed.inter isClosed_ball I.closed_range
 #align smooth_bump_function.is_closed_image_of_is_closed SmoothBumpFunction.isClosed_image_of_isClosed

Mathlib/MeasureTheory/Integral/FundThmCalculus.lean

@@ -1031,7 +1031,7 @@ theorem sub_le_integral_of_hasDeriv_right_of_le_Ico (hab : a ≤ b)
       rw [← uIcc_of_le hab] at G'int hcont ⊢
       exact (hcont.sub continuousOn_const).prod (continuousOn_primitive_interval G'int)
     simp only [inter_comm]
-    exact this.preimage_closed_of_closed isClosed_Icc OrderClosedTopology.isClosed_le'
+    exact this.preimage_isClosed_of_isClosed isClosed_Icc OrderClosedTopology.isClosed_le'
   have main : Icc a b ⊆ {t | g t - g a ≤ ∫ u in a..t, (G' u).toReal} := by
     -- to show that the set `s` is all `[a, b]`, it suffices to show that any point `t` in `s`
     -- with `t < b` admits another point in `s` slightly to its right
@@ -1129,7 +1129,7 @@ theorem sub_le_integral_of_hasDeriv_right_of_le (hab : a ≤ b) (hcont : Continu
       rw [← uIcc_of_le hab] at hcont φint ⊢
       exact (continuousOn_const.sub hcont).prod (continuousOn_primitive_interval_left φint)
     simp only [inter_comm]
-    exact this.preimage_closed_of_closed isClosed_Icc isClosed_le_prod
+    exact this.preimage_isClosed_of_isClosed isClosed_Icc isClosed_le_prod
   have A : closure (Ioc a b) ⊆ s := by
     apply s_closed.closure_subset_iff.2
     intro t ht

Mathlib/Topology/Category/Profinite/Basic.lean

@@ -382,20 +382,20 @@ theorem epi_iff_surjective {X Y : Profinite.{u}} (f : X ⟶ Y) : Epi f ↔ Funct
     obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_clopen.mem_nhds_iff.mp hUy
     classical
       let Z := of (ULift.{u} <| Fin 2)
-      let g : Y ⟶ Z := ⟨(LocallyConstant.ofClopen hV).map ULift.up, LocallyConstant.continuous _⟩
+      let g : Y ⟶ Z := ⟨(LocallyConstant.ofIsClopen hV).map ULift.up, LocallyConstant.continuous _⟩
       let h : Y ⟶ Z := ⟨fun _ => ⟨1⟩, continuous_const⟩
       have H : h = g := by
         rw [← cancel_epi f]
         ext x
         apply ULift.ext
-        dsimp [LocallyConstant.ofClopen]
+        dsimp [LocallyConstant.ofIsClopen]
         -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
         erw [comp_apply, ContinuousMap.coe_mk, comp_apply, ContinuousMap.coe_mk,
           Function.comp_apply, if_neg]
         refine' mt (fun α => hVU α) _
         simp only [Set.mem_range_self, not_true, not_false_iff, Set.mem_compl_iff]
       apply_fun fun e => (e y).down at H
-      dsimp [LocallyConstant.ofClopen] at H
+      dsimp [LocallyConstant.ofIsClopen] at H
       -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
       erw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Function.comp_apply, if_pos hyV] at H
       exact top_ne_bot H

Mathlib/Topology/Category/Profinite/CofilteredLimit.lean

@@ -18,7 +18,7 @@ This file contains some theorems about cofiltered limits of profinite sets.
 
 ## Main Results
 
-- `exists_clopen_of_cofiltered` shows that any clopen set in a cofiltered limit of profinite
+- `exists_isClopen_of_cofiltered` shows that any clopen set in a cofiltered limit of profinite
   sets is the pullback of a clopen set from one of the factors in the limit.
 - `exists_locally_constant` shows that any locally constant function from a cofiltered limit
   of profinite sets factors through one of the components.
@@ -47,7 +47,7 @@ instance preserves_smaller_limits_toTopCat :
 /-- If `X` is a cofiltered limit of profinite sets, then any clopen subset of `X` arises from
 a clopen set in one of the terms in the limit.
 -/
-theorem exists_clopen_of_cofiltered {U : Set C.pt} (hC : IsLimit C) (hU : IsClopen U) :
+theorem exists_isClopen_of_cofiltered {U : Set C.pt} (hC : IsLimit C) (hU : IsClopen U) :
     ∃ (j : J) (V : Set (F.obj j)) (_ : IsClopen V), U = C.π.app j ⁻¹' V := by
   have := preserves_smaller_limits_toTopCat.{u, v}
   -- First, we have the topological basis of the cofiltered limit obtained by pulling back
@@ -118,20 +118,20 @@ theorem exists_clopen_of_cofiltered {U : Set C.pt} (hC : IsLimit C) (hU : IsClop
       rw [(hV s).2]
       rwa [dif_pos hs, ← Set.preimage_comp, ← Profinite.coe_comp, ← Functor.map_comp, C.w] at hx
 set_option linter.uppercaseLean3 false in
-#align Profinite.exists_clopen_of_cofiltered Profinite.exists_clopen_of_cofiltered
+#align Profinite.exists_clopen_of_cofiltered Profinite.exists_isClopen_of_cofiltered
 
 theorem exists_locallyConstant_fin_two (hC : IsLimit C) (f : LocallyConstant C.pt (Fin 2)) :
     ∃ (j : J) (g : LocallyConstant (F.obj j) (Fin 2)), f = g.comap (C.π.app _) := by
   let U := f ⁻¹' {0}
   have hU : IsClopen U := f.isLocallyConstant.isClopen_fiber _
-  obtain ⟨j, V, hV, h⟩ := exists_clopen_of_cofiltered C hC hU
-  use j, LocallyConstant.ofClopen hV
+  obtain ⟨j, V, hV, h⟩ := exists_isClopen_of_cofiltered C hC hU
+  use j, LocallyConstant.ofIsClopen hV
   apply LocallyConstant.locallyConstant_eq_of_fiber_zero_eq
   -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
   erw [LocallyConstant.coe_comap _ _ (C.π.app j).continuous]
   conv_rhs => rw [Set.preimage_comp]
   -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-  erw [LocallyConstant.ofClopen_fiber_zero hV, ← h]
+  erw [LocallyConstant.ofIsClopen_fiber_zero hV, ← h]
 set_option linter.uppercaseLean3 false in
 #align Profinite.exists_locally_constant_fin_two Profinite.exists_locallyConstant_fin_two
 

Mathlib/Topology/Category/Profinite/Nobeling.lean

@@ -1814,7 +1814,7 @@ theorem Nobeling.embedding : ClosedEmbedding (Nobeling.ι S) := by
       simp only [Set.mem_preimage, Set.mem_singleton_iff, decide_eq_true_eq]
   · intro a b h
     by_contra hn
-    obtain ⟨C, hC, hh⟩ := exists_clopen_of_totally_separated hn
+    obtain ⟨C, hC, hh⟩ := exists_isClopen_of_totally_separated hn
     apply hh.2 ∘ of_decide_eq_true
     dsimp (config := { unfoldPartialApp := true }) [ι] at h
     rw [← congr_fun h ⟨C, hC⟩]

Mathlib/Topology/Category/Stonean/Basic.lean

@@ -194,7 +194,7 @@ lemma epi_iff_surjective {X Y : Stonean} (f : X ⟶ Y) :
   obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_clopen.mem_nhds_iff.mp hUy
   classical
   let g : Y ⟶ mkFinite (ULift (Fin 2)) :=
-    ⟨(LocallyConstant.ofClopen hV).map ULift.up, LocallyConstant.continuous _⟩
+    ⟨(LocallyConstant.ofIsClopen hV).map ULift.up, LocallyConstant.continuous _⟩
   let h : Y ⟶ mkFinite (ULift (Fin 2)) := ⟨fun _ => ⟨1⟩, continuous_const⟩
   have H : h = g := by
     rw [← cancel_epi f]

Mathlib/Topology/Clopen.lean

@@ -110,11 +110,11 @@ theorem IsClopen.preimage {s : Set Y} (h : IsClopen s) {f : X → Y} (hf : Conti
   ⟨h.1.preimage hf, h.2.preimage hf⟩
 #align is_clopen.preimage IsClopen.preimage
 
-theorem ContinuousOn.preimage_clopen_of_clopen {f : X → Y} {s : Set X} {t : Set Y}
+theorem ContinuousOn.preimage_isClopen_of_isClopen {f : X → Y} {s : Set X} {t : Set Y}
     (hf : ContinuousOn f s) (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ∩ f ⁻¹' t) :=
   ⟨ContinuousOn.preimage_open_of_open hf hs.1 ht.1,
-    ContinuousOn.preimage_closed_of_closed hf hs.2 ht.2⟩
-#align continuous_on.preimage_clopen_of_clopen ContinuousOn.preimage_clopen_of_clopen
+    ContinuousOn.preimage_isClosed_of_isClosed hf hs.2 ht.2⟩
+#align continuous_on.preimage_clopen_of_clopen ContinuousOn.preimage_isClopen_of_isClopen
 
 /-- The intersection of a disjoint covering by two open sets of a clopen set will be clopen. -/
 theorem isClopen_inter_of_disjoint_cover_clopen {s a b : Set X} (h : IsClopen s) (cover : s ⊆ a ∪ b)
@@ -150,7 +150,7 @@ protected theorem QuotientMap.isClopen_preimage {f : X → Y} (hf : QuotientMap
   and_congr hf.isOpen_preimage hf.isClosed_preimage
 #align quotient_map.is_clopen_preimage QuotientMap.isClopen_preimage
 
-theorem continuous_boolIndicator_iff_clopen (U : Set X) :
+theorem continuous_boolIndicator_iff_isClopen (U : Set X) :
     Continuous U.boolIndicator ↔ IsClopen U := by
   constructor
   · intro hc
@@ -159,12 +159,12 @@ theorem continuous_boolIndicator_iff_clopen (U : Set X) :
   · refine' fun hU => ⟨fun s _ => _⟩
     rcases U.preimage_boolIndicator s with (h | h | h | h) <;> rw [h]
     exacts [isOpen_univ, hU.1, hU.2.isOpen_compl, isOpen_empty]
-#align continuous_bool_indicator_iff_clopen continuous_boolIndicator_iff_clopen
+#align continuous_bool_indicator_iff_clopen continuous_boolIndicator_iff_isClopen
 
-theorem continuousOn_boolIndicator_iff_clopen (s U : Set X) :
+theorem continuousOn_boolIndicator_iff_isClopen (s U : Set X) :
     ContinuousOn U.boolIndicator s ↔ IsClopen (((↑) : s → X) ⁻¹' U) := by
-  rw [continuousOn_iff_continuous_restrict, ← continuous_boolIndicator_iff_clopen]
+  rw [continuousOn_iff_continuous_restrict, ← continuous_boolIndicator_iff_isClopen]
   rfl
-#align continuous_on_indicator_iff_clopen continuousOn_boolIndicator_iff_clopen
+#align continuous_on_indicator_iff_clopen continuousOn_boolIndicator_iff_isClopen
 
 end Clopen

Mathlib/Topology/Connected/Basic.lean

@@ -438,10 +438,10 @@ theorem IsPreconnected.subset_right_of_subset_union (hu : IsOpen u) (hv : IsOpen
 
 -- porting note: moved up
 /-- Preconnected sets are either contained in or disjoint to any given clopen set. -/
-theorem IsPreconnected.subset_clopen {s t : Set α} (hs : IsPreconnected s) (ht : IsClopen t)
+theorem IsPreconnected.subset_isClopen {s t : Set α} (hs : IsPreconnected s) (ht : IsClopen t)
     (hne : (s ∩ t).Nonempty) : s ⊆ t :=
   hs.subset_left_of_subset_union ht.isOpen ht.compl.isOpen disjoint_compl_right (by simp) hne
-#align is_preconnected.subset_clopen IsPreconnected.subset_clopen
+#align is_preconnected.subset_clopen IsPreconnected.subset_isClopen
 
 /-- If a preconnected set `s` intersects an open set `u`, and limit points of `u` inside `s` are
 contained in `u`, then the whole set `s` is contained in `u`. -/
@@ -511,7 +511,7 @@ theorem Sigma.isConnected_iff [∀ i, TopologicalSpace (π i)] {s : Set (Σi, π
   refine' ⟨fun hs => _, _⟩
   · obtain ⟨⟨i, x⟩, hx⟩ := hs.nonempty
     have : s ⊆ range (Sigma.mk i) :=
-      hs.isPreconnected.subset_clopen isClopen_range_sigmaMk ⟨⟨i, x⟩, hx, x, rfl⟩
+      hs.isPreconnected.subset_isClopen isClopen_range_sigmaMk ⟨⟨i, x⟩, hx, x, rfl⟩
     exact ⟨i, Sigma.mk i ⁻¹' s, hs.preimage_of_openMap sigma_mk_injective isOpenMap_sigmaMk this,
       (Set.image_preimage_eq_of_subset this).symm⟩
   · rintro ⟨i, t, ht, rfl⟩
@@ -535,12 +535,12 @@ theorem Sum.isConnected_iff [TopologicalSpace β] {s : Set (Sum α β)} :
   refine' ⟨fun hs => _, _⟩
   · obtain ⟨x | x, hx⟩ := hs.nonempty
     · have h : s ⊆ range Sum.inl :=
-        hs.isPreconnected.subset_clopen isClopen_range_inl ⟨.inl x, hx, x, rfl⟩
+        hs.isPreconnected.subset_isClopen isClopen_range_inl ⟨.inl x, hx, x, rfl⟩
       refine' Or.inl ⟨Sum.inl ⁻¹' s, _, _⟩
       · exact hs.preimage_of_openMap Sum.inl_injective isOpenMap_inl h
       · exact (image_preimage_eq_of_subset h).symm
     · have h : s ⊆ range Sum.inr :=
-        hs.isPreconnected.subset_clopen isClopen_range_inr ⟨.inr x, hx, x, rfl⟩
+        hs.isPreconnected.subset_isClopen isClopen_range_inr ⟨.inr x, hx, x, rfl⟩
       refine' Or.inr ⟨Sum.inr ⁻¹' s, _, _⟩
       · exact hs.preimage_of_openMap Sum.inr_injective isOpenMap_inr h
       · exact (image_preimage_eq_of_subset h).symm
@@ -1058,13 +1058,13 @@ theorem isConnected_iff_sUnion_disjoint_open {s : Set α} :
     simpa [*, or_imp, forall_and] using h {u, v}
 #align is_connected_iff_sUnion_disjoint_open isConnected_iff_sUnion_disjoint_open
 
--- porting note: `IsPreconnected.subset_clopen` moved up from here
+-- porting note: `IsPreconnected.subset_isClopen` moved up from here
 
 /-- Preconnected sets are either contained in or disjoint to any given clopen set. -/
-theorem disjoint_or_subset_of_clopen {s t : Set α} (hs : IsPreconnected s) (ht : IsClopen t) :
+theorem disjoint_or_subset_of_isClopen {s t : Set α} (hs : IsPreconnected s) (ht : IsClopen t) :
     Disjoint s t ∨ s ⊆ t :=
-  (disjoint_or_nonempty_inter s t).imp_right <| hs.subset_clopen ht
-#align disjoint_or_subset_of_clopen disjoint_or_subset_of_clopen
+  (disjoint_or_nonempty_inter s t).imp_right <| hs.subset_isClopen ht
+#align disjoint_or_subset_of_clopen disjoint_or_subset_of_isClopen
 
 /-- A set `s` is preconnected if and only if
 for every cover by two closed sets that are disjoint on `s`,
@@ -1115,15 +1115,15 @@ theorem isPreconnected_iff_subset_of_fully_disjoint_closed {s : Set α} (hs : Is
 
 theorem IsClopen.connectedComponent_subset {x} (hs : IsClopen s) (hx : x ∈ s) :
     connectedComponent x ⊆ s :=
-  isPreconnected_connectedComponent.subset_clopen hs ⟨x, mem_connectedComponent, hx⟩
+  isPreconnected_connectedComponent.subset_isClopen hs ⟨x, mem_connectedComponent, hx⟩
 #align is_clopen.connected_component_subset IsClopen.connectedComponent_subset
 
 /-- The connected component of a point is always a subset of the intersection of all its clopen
 neighbourhoods. -/
-theorem connectedComponent_subset_iInter_clopen {x : α} :
+theorem connectedComponent_subset_iInter_isClopen {x : α} :
     connectedComponent x ⊆ ⋂ Z : { Z : Set α // IsClopen Z ∧ x ∈ Z }, Z :=
   subset_iInter fun Z => Z.2.1.connectedComponent_subset Z.2.2
-#align connected_component_subset_Inter_clopen connectedComponent_subset_iInter_clopen
+#align connected_component_subset_Inter_clopen connectedComponent_subset_iInter_isClopen
 
 /-- A clopen set is the union of its connected components. -/
 theorem IsClopen.biUnion_connectedComponent_eq {Z : Set α} (h : IsClopen Z) :
@@ -1315,7 +1315,7 @@ theorem isPreconnected_of_forall_constant {s : Set α}
   rcases this with ⟨u, v, u_op, v_op, hsuv, ⟨x, x_in_s, x_in_u⟩, ⟨y, y_in_s, y_in_v⟩, H⟩
   have hy : y ∉ u := fun y_in_u => eq_empty_iff_forall_not_mem.mp H y ⟨y_in_s, ⟨y_in_u, y_in_v⟩⟩
   have : ContinuousOn u.boolIndicator s := by
-    apply (continuousOn_boolIndicator_iff_clopen _ _).mpr ⟨_, _⟩
+    apply (continuousOn_boolIndicator_iff_isClopen _ _).mpr ⟨_, _⟩
     · exact u_op.preimage continuous_subtype_val
     · rw [preimage_subtype_coe_eq_compl hsuv H]
       exact (v_op.preimage continuous_subtype_val).isClosed_compl

Mathlib/Topology/Connected/TotallyDisconnected.lean

@@ -90,19 +90,19 @@ instance [∀ i, TopologicalSpace (π i)] [∀ i, TotallyDisconnectedSpace (π i
 -- porting note: reformulated using `Pairwise`
 /-- Let `X` be a topological space, and suppose that for all distinct `x,y ∈ X`, there
   is some clopen set `U` such that `x ∈ U` and `y ∉ U`. Then `X` is totally disconnected. -/
-theorem isTotallyDisconnected_of_clopen_set {X : Type*} [TopologicalSpace X]
+theorem isTotallyDisconnected_of_isClopen_set {X : Type*} [TopologicalSpace X]
     (hX : Pairwise fun x y => ∃ (U : Set X), IsClopen U ∧ x ∈ U ∧ y ∉ U) :
     IsTotallyDisconnected (Set.univ : Set X) := by
   rintro S - hS
   unfold Set.Subsingleton
   by_contra' h_contra
   rcases h_contra with ⟨x, hx, y, hy, hxy⟩
-  obtain ⟨U, h_clopen, hxU, hyU⟩ := hX hxy
+  obtain ⟨U, hU, hxU, hyU⟩ := hX hxy
   specialize
-    hS U Uᶜ h_clopen.1 h_clopen.compl.1 (fun a _ => em (a ∈ U)) ⟨x, hx, hxU⟩ ⟨y, hy, hyU⟩
+    hS U Uᶜ hU.1 hU.compl.1 (fun a _ => em (a ∈ U)) ⟨x, hx, hxU⟩ ⟨y, hy, hyU⟩
   rw [inter_compl_self, Set.inter_empty] at hS
   exact Set.not_nonempty_empty hS
-#align is_totally_disconnected_of_clopen_set isTotallyDisconnected_of_clopen_set
+#align is_totally_disconnected_of_clopen_set isTotallyDisconnected_of_isClopen_set
 
 /-- A space is totally disconnected iff its connected components are subsingletons. -/
 theorem totallyDisconnectedSpace_iff_connectedComponent_subsingleton :
@@ -235,16 +235,16 @@ instance (priority := 100) TotallySeparatedSpace.of_discrete (α : Type*) [Topol
     (compl_union_self _).symm.subset, disjoint_compl_left⟩⟩
 #align totally_separated_space.of_discrete TotallySeparatedSpace.of_discrete
 
-theorem exists_clopen_of_totally_separated {α : Type*} [TopologicalSpace α]
+theorem exists_isClopen_of_totally_separated {α : Type*} [TopologicalSpace α]
     [TotallySeparatedSpace α] {x y : α} (hxy : x ≠ y) :
     ∃ U : Set α, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ := by
   obtain ⟨U, V, hU, hV, Ux, Vy, f, disj⟩ :=
     TotallySeparatedSpace.isTotallySeparated_univ x (Set.mem_univ x) y (Set.mem_univ y) hxy
-  have clopen_U := isClopen_inter_of_disjoint_cover_clopen isClopen_univ f hU hV disj
-  rw [univ_inter _] at clopen_U
+  have hU := isClopen_inter_of_disjoint_cover_clopen isClopen_univ f hU hV disj
+  rw [univ_inter _] at hU
   rw [← Set.subset_compl_iff_disjoint_right, subset_compl_comm] at disj
-  exact ⟨U, clopen_U, Ux, disj Vy⟩
-#align exists_clopen_of_totally_separated exists_clopen_of_totally_separated
+  exact ⟨U, hU, Ux, disj Vy⟩
+#align exists_clopen_of_totally_separated exists_isClopen_of_totally_separated
 
 end TotallySeparated
 

Mathlib/Topology/ContinuousOn.lean

@@ -1075,12 +1075,12 @@ theorem ContinuousOn.isOpen_preimage {f : α → β} {s : Set α} {t : Set β} (
   rw [inter_comm, inter_eq_self_of_subset_left hp]
 #align continuous_on.is_open_preimage ContinuousOn.isOpen_preimage
 
-theorem ContinuousOn.preimage_closed_of_closed {f : α → β} {s : Set α} {t : Set β}
+theorem ContinuousOn.preimage_isClosed_of_isClosed {f : α → β} {s : Set α} {t : Set β}
     (hf : ContinuousOn f s) (hs : IsClosed s) (ht : IsClosed t) : IsClosed (s ∩ f ⁻¹' t) := by
   rcases continuousOn_iff_isClosed.1 hf t ht with ⟨u, hu⟩
   rw [inter_comm, hu.2]
   apply IsClosed.inter hu.1 hs
-#align continuous_on.preimage_closed_of_closed ContinuousOn.preimage_closed_of_closed
+#align continuous_on.preimage_closed_of_closed ContinuousOn.preimage_isClosed_of_isClosed
 
 theorem ContinuousOn.preimage_interior_subset_interior_preimage {f : α → β} {s : Set α} {t : Set β}
     (hf : ContinuousOn f s) (hs : IsOpen s) : s ∩ f ⁻¹' interior t ⊆ s ∩ interior (f ⁻¹' t) :=