English
If h is a pointwise transform, then applying h to the pair of functions inside a piecewise expression is the same as applying h to the result of the piecewise and then feeding that into h.
Русский
Если есть отображение h, применимое по точкам, то применение h к s.piecewise f g равняется вертикально тому, как мы применяем h к f и g по отдельности внутри piecewise и затем полученное значение подаем в h.
LaTeX
$$$s\\text{.piecewise} (\\lambda x. h\ x\ (f\ x)) (\\lambda x. h\ x\ (g\ x)) = \\lambda x. h\\ x\\ (s\\text{.piecewise } f g\ x)$$$
Lean4
theorem piecewise_op {δ' : α → Sort*} (h : ∀ i, δ i → δ' i) :
(s.piecewise (fun x => h x (f x)) fun x => h x (g x)) = fun x => h x (s.piecewise f g x) :=
funext fun _ => (apply_piecewise _ _ _ _).symm
