English
If f and g are continuous on their respective regions, and frontier relations hold with equality on the intersected boundary, then the piecewise function t.piecewise f g is continuous on t.ite s s'.
Русский
Если f и g непрерывны на соответствующих областях, и границы согласованы, то t.piecewise f g непрерывна на t.ite s s'.
LaTeX
$$$\text{ContinuousOn}(t.\text{piecewise} f g)\ (t.\text{ite } s s').$$$
Lean4
theorem continuousOn_piecewise_ite' [∀ x, Decidable (x ∈ t)] (h : ContinuousOn f (s ∩ closure t))
(h' : ContinuousOn g (s' ∩ closure tᶜ)) (H : s ∩ frontier t = s' ∩ frontier t) (Heq : EqOn f g (s ∩ frontier t)) :
ContinuousOn (t.piecewise f g) (t.ite s s') :=
by
apply ContinuousOn.piecewise
· rwa [ite_inter_of_inter_eq _ H]
· rwa [ite_inter_closure_eq_of_inter_frontier_eq H]
· rwa [ite_inter_closure_compl_eq_of_inter_frontier_eq H]
