English
A variant of piecewise defined on a subset C0 ⊆ C1 ∪ C2, producing LocallyConstant on C0 from data on C1 and C2.
Русский
Вариант piecewise', определяемый на подмножестве C0 ⊆ C1 ∪ C2, дающий локально константное отображение на C0 из данных на C1 и C2.
LaTeX
$$$\\text{piecewise'}\\ h_0\\ h_1\\ h_2\\ f_1\\ f_2\\ hf : LocallyConstant\\ C_0.Elem\\ Z$$$
Lean4
/-- A variant of `LocallyConstant.piecewise` where the two closed sets cover a subset.
TODO: Generalise this construction to `ContinuousMap`. -/
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 [eq_univ_iff_forall] using h₀)
(f₁.comap ⟨(restrictPreimage C₁ ((↑) : C₀ → X)), continuous_subtype_val.restrictPreimage⟩)
(f₂.comap ⟨(restrictPreimage C₂ ((↑) : C₀ → X)), continuous_subtype_val.restrictPreimage⟩) <|
by
rintro ⟨x, hx₀⟩ ⟨hx₁ : x ∈ C₁, hx₂ : x ∈ C₂⟩
simpa using hf x ⟨hx₁, hx₂⟩
