English
Under assumptions, evaluating piecewise' on an element from C0 with condition in C1 yields f1 at that element.
Русский
При данных условиях вычисление piecewise' на элементе из C0 с условием в C1 дает f1 в этом элементе.
LaTeX
$$$(piecewise'\\ h_0\\ h_1\\ h_2\\ f_1\\ f_2\\ hf)\\ x = f_1\\ ⟨x, \\cdots⟩$$$
Lean4
@[simp]
theorem piecewise'_apply_left {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₀) (hx : x.val ∈ C₁) :
piecewise' h₀ h₁ h₂ f₁ f₂ hf x = f₁ ⟨x.val, hx⟩ :=
by
letI : ∀ j : C₀, Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j ↦ decidable_of_iff (↑j ∈ C₁) Iff.rfl
rw [piecewise',
piecewise_apply_left (f :=
(f₁.comap ⟨(restrictPreimage C₁ ((↑) : C₀ → X)), continuous_subtype_val.restrictPreimage⟩)) (hx := hx)]
rfl
