English
If f and g agree on t ∩ s and f' and g agree on t' ∩ sᶜ, then the piecewise function s.piecewise f f' agrees with g on s.ite t t'.
Русский
Если f и g согласны на t ∩ s, а f' и g — на t' ∩ sᶜ, то функция s.piecewise f f' совпадает с g на s.ite t t'.
LaTeX
$$$EqOn f g (t \\cap s) \\land EqOn f' g (t' \\cap s^{c}) \\Rightarrow EqOn (s.piecewise f f') g (s.ite t t')$$$
Lean4
theorem piecewise_ite' {f f' g : α → β} {t t'} (h : EqOn f g (t ∩ s)) (h' : EqOn f' g (t' ∩ sᶜ)) :
EqOn (s.piecewise f f') g (s.ite t t') := by simp [eqOn_piecewise, *]