English
Let s be a set and f,g on α→β. For t,t' subsets, if f and g agree appropriately on t∩s and t'∩sᶜ, then the two-argument map h preserves the piecewise composition as in the lemma piecewise_ite'.
Русский
Пусть s—множество, f,g: α→β. Для подмножеств t,t' и подходящих условий соглашения на t∩s и t'∩sᶜ, отображение h сохраняет кусочно заданное сочетание как в лемме piecewise_ite'.
LaTeX
$$$\\text{EqOn f g (t \\cap s)} \\land \\text{EqOn f' g (t' \\cap s^{c})} \\Rightarrow \\text{EqOn (s.piecewise f f') g (s.ite t t')} $$$
Lean4
theorem apply_piecewise₂ {δ' δ'' : α → Sort*} (f' g' : ∀ i, δ' i) (h : ∀ i, δ i → δ' i → δ'' i) {x : α} :
h x (s.piecewise f g x) (s.piecewise f' g' x) =
s.piecewise (fun x => h x (f x) (f' x)) (fun x => h x (g x) (g' x)) x :=
by by_cases hx : x ∈ s <;> simp [hx]
