English
If on the boundary of t, the values of f and g coincide in a suitable sense and f,g have continuity on the respective regions, then the piecewise function piecewise t f g is continuous on the corresponding split of the domain.
Русский
Если на границе множества t значения функций f и g согласованы в надлежащем смысле и f,g непрерывны на соответствующих областях, тогда функция (t.piecewise f g) непрерывна на разбиении области.
LaTeX
$$$\text{ContinuousOn}(\mathrm{piecewise}\ t\ f\ g)\ (t\mathrm{.ite}\ s\ s')$ under the stated hypotheses (hpf, hpg, hf, hg).$$
Lean4
theorem piecewise' [∀ a, Decidable (a ∈ t)] (hpf : ∀ a ∈ s ∩ frontier t, Tendsto f (𝓝[s ∩ t] a) (𝓝 (piecewise t f g a)))
(hpg : ∀ a ∈ s ∩ frontier t, Tendsto g (𝓝[s ∩ tᶜ] a) (𝓝 (piecewise t f g a))) (hf : ContinuousOn f <| s ∩ t)
(hg : ContinuousOn g <| s ∩ tᶜ) : ContinuousOn (piecewise t f g) s :=
hf.if' hpf hpg hg
