English
Let s be a subset of α and f, f', g : α → β. For any t ⊆ α, the equality-on-t of the piecewise function s.piecewise f f' with g is equivalent to f agreeing with g on t ∩ s and f' agreeing with g on t ∩ sᶜ.
Русский
Пусть s ⊆ α и f, f', g : α → β. Тогда равенство по t для кусочно-заданной функции s.piecewise f f' с g эквивалентно тому, что f совпадает с g на t ∩ s, и f' совпадает с g на t ∩ sᶜ.
LaTeX
$$$EqOn (s.piecewise f f')\\, g\\, t \\iff \\bigl(EqOn f\\, g\\,(t \\cap s) \\land EqOn f'\\, g\\,(t \\cap s^{c})\\bigr)$$$
Lean4
theorem eqOn_piecewise {f f' g : α → β} {t} : EqOn (s.piecewise f f') g t ↔ EqOn f g (t ∩ s) ∧ EqOn f' g (t ∩ sᶜ) :=
by
simp only [EqOn, ← forall_and]
refine forall_congr' fun a => ?_; by_cases a ∈ s <;> simp [*]
