English
If you apply a two-argument transform h to the pair of piecewise values, you obtain the piecewise of h applied coordinatewise.
Русский
Если применять двухаргументное отображение h к парам значений s.piecewise f g и s.piecewise f' g', то это равно fine-образу: h применяется по каждому аргументу внутри соответствующих ветвей.
LaTeX
$$$s.piecewise (\\lambda x. h\\ x\\ (f\\ x) (f'\\ x)) (\\lambda x. h\\ x\\ (g\\ x) (g'\\ x)) = \\lambda x. h\\ x\\ (s.piecewise f g\\ x) (s.piecewise f' g'\\ x)$$$
Lean4
theorem piecewise_op₂ {δ' δ'' : α → Sort*} (f' g' : ∀ i, δ' i) (h : ∀ i, δ i → δ' i → δ'' i) :
(s.piecewise (fun x => h x (f x) (f' x)) fun x => h x (g x) (g' x)) = fun x =>
h x (s.piecewise f g x) (s.piecewise f' g' x) :=
funext fun _ => (apply_piecewise₂ _ _ _ _ _ _).symm
