English
If f1 and f2 map appropriate intersections correctly, then the piecewise function s.piecewise f1 f2 maps the corresponding unions as stated.
Русский
Если f1 и f2 сопоставляют корректно пересечения множеств, тогда функция piecewise корректно переводит на соответствующие объединения.
LaTeX
$$MapsTo (s.piecewise f1 f2) (s.ite s1 s2) (t.ite t1 t2)$$
Lean4
theorem piecewise_ite {s s₁ s₂ : Set α} {t t₁ t₂ : Set β} {f₁ f₂ : α → β} [∀ i, Decidable (i ∈ s)]
(h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)) (h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)) :
MapsTo (s.piecewise f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂) :=
by
refine (h₁.congr ?_).union_union (h₂.congr ?_)
exacts [(piecewise_eqOn s f₁ f₂).symm.mono inter_subset_right,
(piecewise_eqOn_compl s f₁ f₂).symm.mono inter_subset_right]
