English
Let h be a transform that for each i maps δ i to δ' i. Then for any x, h x applied to s.piecewise f g at x equals the piecewise of h x applied to f and g at x.
Русский
Пусть h составляет отображение для каждого i: δ i → δ' i. Тогда для любого x выполняется: h x применяемое к s.piecewise f g на x равно кусочно-заданному отображению h x (f x) и h x (g x) на x.
LaTeX
$$$h\ x\ (s.piecewise f g\ x) = s.piecewise (\\lambda x. h\ x\ (f\ x)) (\\lambda x. h\ x\ (g\ x))\\ x$$$
Lean4
theorem apply_piecewise {δ' : α → Sort*} (h : ∀ i, δ i → δ' i) {x : α} :
h x (s.piecewise f g x) = s.piecewise (fun x => h x (f x)) (fun x => h x (g x)) x := by
by_cases hx : x ∈ s <;> simp [hx]
