English
If f is continuous on s and g is continuous on s', and frontier intersections match, then the piecewise function t.piecewise f g is continuous on t.ite s s'.
Русский
Если f непрерывна на s, g — на s', и границы совпадают, то t.piecewise f g непрерывна на t.ite s s'.
LaTeX
$$$\text{ContinuousOn}(f,s) \to \text{ContinuousOn}(g,s') \to (s\cap frontier t = s'\cap frontier t) \to \text{ContinuousOn}(t\.piecewise f g)(t\.ite s s').$$$
Lean4
theorem continuousOn_piecewise_ite [∀ x, Decidable (x ∈ t)] (h : ContinuousOn f s) (h' : ContinuousOn g s')
(H : s ∩ frontier t = s' ∩ frontier t) (Heq : EqOn f g (s ∩ frontier t)) :
ContinuousOn (t.piecewise f g) (t.ite s s') :=
continuousOn_piecewise_ite' (h.mono inter_subset_left) (h'.mono inter_subset_left) H Heq
