Misc lemmas about Specializes, Inseparable and path-connectedness (#7970

)

Generalizing one of the proofs introduced in #7878

Mathlib/Data/Set/Basic.lean

@@ -2350,6 +2350,16 @@ theorem subset_ite {t s s' u : Set α} : u ⊆ t.ite s s' ↔ u ∩ t ⊆ s ∧
   by_cases hx : x ∈ t <;> simp [*, Set.ite]
 #align set.subset_ite Set.subset_ite
 
+theorem ite_eq_of_subset_left (t : Set α) {s₁ s₂ : Set α} (h : s₁ ⊆ s₂) :
+    t.ite s₁ s₂ = s₁ ∪ (s₂ \ t) := by
+  ext x
+  by_cases hx : x ∈ t <;> simp [*, Set.ite, or_iff_right_of_imp (@h x)]
+
+theorem ite_eq_of_subset_right (t : Set α) {s₁ s₂ : Set α} (h : s₂ ⊆ s₁) :
+    t.ite s₁ s₂ = (s₁ ∩ t) ∪ s₂ := by
+  ext x
+  by_cases hx : x ∈ t <;> simp [*, Set.ite, or_iff_left_of_imp (@h x)]
+
 /-! ### Subsingleton -/
 
 

Mathlib/Topology/Basic.lean

@@ -1609,10 +1609,12 @@ theorem IsOpen.preimage {f : α → β} (hf : Continuous f) {s : Set β} (h : Is
   hf.isOpen_preimage s h
 #align is_open.preimage IsOpen.preimage
 
-theorem Continuous.congr {f g : α → β} (h : Continuous f) (h' : ∀ x, f x = g x) : Continuous g := by
-  convert h
-  ext
-  rw [h']
+theorem continuous_congr {f g : α → β} (h : ∀ x, f x = g x) :
+    Continuous f ↔ Continuous g :=
+  .of_eq <| congrArg _ <| funext h
+
+theorem Continuous.congr {f g : α → β} (h : Continuous f) (h' : ∀ x, f x = g x) : Continuous g :=
+  continuous_congr h' |>.mp h
 #align continuous.congr Continuous.congr
 
 /-- A function between topological spaces is continuous at a point `x₀`

Mathlib/Topology/Connected/PathConnected.lean

@@ -875,13 +875,8 @@ theorem JoinedIn.trans (hxy : JoinedIn F x y) (hyz : JoinedIn F y z) : JoinedIn
 
 theorem Specializes.joinedIn (h : x ⤳ y) (hx : x ∈ F) (hy : y ∈ F) : JoinedIn F x y := by
   refine ⟨⟨⟨Set.piecewise {1} (const I y) (const I x), ?_⟩, by simp, by simp⟩, fun t ↦ ?_⟩
-  · simp only [const, continuous_def, piecewise_preimage]
-    intro U hU
-    by_cases hy' : y ∈ U
-    · simp [hy', h.mem_open hU hy']
-    · by_cases hx' : x ∈ U
-      · simpa [hx', hy'] using isOpen_univ.sdiff isClosed_singleton
-      · simp [hx', hy']
+  · exact isClosed_singleton.continuous_piecewise_of_specializes continuous_const continuous_const
+      fun _ ↦ h
   · simp only [Path.coe_mk_mk, piecewise]
     split_ifs <;> assumption
 

Mathlib/Topology/Inseparable.lean

@@ -18,7 +18,7 @@ In this file we define
 * `Inseparable`: a relation saying that two points in a topological space have the same
   neighbourhoods; equivalently, they can't be separated by an open set;
 
-* `InseparableSetoid X`: same relation, as a `setoid`;
+* `InseparableSetoid X`: same relation, as a `Setoid`;
 
 * `SeparationQuotient X`: the quotient of `X` by its `InseparableSetoid`.
 
@@ -39,7 +39,7 @@ topological space, separation setoid
 open Set Filter Function Topology List
 
 variable {X Y Z α ι : Type*} {π : ι → Type*} [TopologicalSpace X] [TopologicalSpace Y]
-  [TopologicalSpace Z] [∀ i, TopologicalSpace (π i)] {x y z : X} {s : Set X} {f : X → Y}
+  [TopologicalSpace Z] [∀ i, TopologicalSpace (π i)] {x y z : X} {s : Set X} {f g : X → Y}
 
 /-!
 ### `Specializes` relation
@@ -228,6 +228,20 @@ theorem not_specializes_iff_exists_closed : ¬x ⤳ y ↔ ∃ S : Set X, IsClose
   rfl
 #align not_specializes_iff_exists_closed not_specializes_iff_exists_closed
 
+theorem IsOpen.continuous_piecewise_of_specializes [DecidablePred (· ∈ s)] (hs : IsOpen s)
+    (hf : Continuous f) (hg : Continuous g) (hspec : ∀ x, f x ⤳ g x) :
+    Continuous (s.piecewise f g) := by
+  have : ∀ U, IsOpen U → g ⁻¹' U ⊆ f ⁻¹' U := fun U hU x hx ↦ (hspec x).mem_open hU hx
+  rw [continuous_def]
+  intro U hU
+  rw [piecewise_preimage, ite_eq_of_subset_right _ (this U hU)]
+  exact hU.preimage hf |>.inter hs |>.union (hU.preimage hg)
+
+theorem IsClosed.continuous_piecewise_of_specializes [DecidablePred (· ∈ s)] (hs : IsClosed s)
+    (hf : Continuous f) (hg : Continuous g) (hspec : ∀ x, g x ⤳ f x) :
+    Continuous (s.piecewise f g) := by
+  simpa only [piecewise_compl] using hs.isOpen_compl.continuous_piecewise_of_specializes hg hf hspec
+
 variable (X)
 
 /-- Specialization forms a preorder on the topological space. -/
@@ -634,3 +648,8 @@ theorem continuous_lift₂ {f : X → Y → Z} {hf : ∀ a b c d, (a ~ᵢ c) →
 #align separation_quotient.continuous_lift₂ SeparationQuotient.continuous_lift₂
 
 end SeparationQuotient
+
+theorem continuous_congr_of_inseparable (h : ∀ x, f x ~ᵢ g x) :
+    Continuous f ↔ Continuous g := by
+  simp_rw [SeparationQuotient.inducing_mk.continuous_iff (β := Y)]
+  exact continuous_congr fun x ↦ SeparationQuotient.mk_eq_mk.mpr (h x)