[Merged by Bors] - feat: LocallyConstant.piecewise'

Mathlib/Topology/LocallyConstant/Basic.lean

@@ -610,10 +610,12 @@ section Piecewise
 
 /-- Given two closed sets covering a topological space, and locally constant maps on these two sets,
     then if these two locally constant maps agree on the intersection, we get a piecewise defined
-    locally constant map on the whole space. -/
+    locally constant map on the whole space.
+
+TODO: Generalise this construction to `ContinuousMap`. -/
 def piecewise {C₁ C₂ : Set X} (h₁ : IsClosed C₁) (h₂ : IsClosed C₂) (h : C₁ ∪ C₂ = Set.univ)
     (f : LocallyConstant C₁ Z) (g : LocallyConstant C₂ Z)
-    (hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f.toFun ⟨x, hx.1⟩ = g.toFun ⟨x, hx.2⟩)
+    (hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, hx.1⟩ = g ⟨x, hx.2⟩)
     [∀ j, Decidable (j ∈ C₁)] : LocallyConstant X Z where
   toFun i := if hi : i ∈ C₁ then f ⟨i, hi⟩ else g ⟨i, (Set.compl_subset_iff_union.mpr h) hi⟩
   isLocallyConstant := by
@@ -634,6 +636,32 @@ def piecewise {C₁ C₂ : Set X} (h₁ : IsClosed C₁) (h₂ : IsClosed C₂)
       · simp only [cond_true, restrict_dite, Subtype.coe_eta]
         exact hf
 
+/-- A variant of `LocallyConstant.piecewise` where the two closed sets cover a subset.
+
+TODO: Generalise this construction to `ContinuousMap`. -/
+noncomputable def piecewise' {C₀ C₁ C₂ : Set X} (h₀ : C₀ ⊆ C₁ ∪ C₂) (h₁ : IsClosed C₁)
+    (h₂ : IsClosed C₂) (f₁ : LocallyConstant C₁ Z) (f₂ : LocallyConstant C₂ Z)
+    [DecidablePred (· ∈ C₁)] (hf : ∀ x (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, hx.1⟩ = f₂ ⟨x, hx.2⟩) :
+    LocallyConstant C₀ Z :=
+  letI : ∀ j : C₀, Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j ↦ decidable_of_iff (↑j ∈ C₁) Iff.rfl
+  piecewise (h₁.preimage continuous_subtype_val) (h₂.preimage continuous_subtype_val)
+    (by simpa [Set.eq_univ_iff_forall] using h₀)
+    (f₁.comap (Set.restrictPreimage C₁ ((↑) : C₀ → X)))
+    (f₂.comap (Set.restrictPreimage C₂ ((↑) : C₀ → X))) <| by
+      rintro ⟨x, hx₀⟩ ⟨hx₁ : x ∈ C₁, hx₂ : x ∈ C₂⟩
+      simp_rw [coe_comap_apply _ _ continuous_subtype_val.restrictPreimage]
+      exact hf x ⟨hx₁, hx₂⟩
+
+@[simp]
+lemma piecewise'_apply {C₀ C₁ C₂ : Set X} (h₀ : C₀ ⊆ C₁ ∪ C₂) (h₁ : IsClosed C₁)
+    (h₂ : IsClosed C₂) (f₁ : LocallyConstant C₁ Z) (f₂ : LocallyConstant C₂ Z)
+    [DecidablePred (· ∈ C₁)] (hf : ∀ x (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, hx.1⟩ = f₂ ⟨x, hx.2⟩) (x : C₀) :
+    piecewise' h₀ h₁ h₂ f₁ f₂ hf x = if hx : x.val ∈ C₁ then f₁ ⟨x.val, hx⟩ else
+      f₂ ⟨x.val, (or_iff_not_imp_left.mp (h₀ x.prop)) hx⟩ := by
+  simp only [piecewise', piecewise, Set.mem_preimage, continuous_subtype_val.restrictPreimage,
+    coe_comap, Function.comp_apply]
+  rfl
+
 end Piecewise
 
 end LocallyConstant