English
If f and g are continuous on their respective regions defined by s and its complement, and they agree along the frontier of t, then the restricted piecewise is continuous on the domain s ∩ t ∪ s' ∩ tᶜ.
Русский
Если f и g непрерывны на своих областях, определённых через s и дополнение, и согласованы на границе frontier t, тогда непрерывность сохраняется для piecewise на соответствующем домене.
LaTeX
$$$\text{ContinuousOn}(\mathrm{piecewise}\ t\ f\ g)\ (t\mathrm{.ite}\ s\ s').$$$
Lean4
theorem continuous_piecewise [∀ a, Decidable (a ∈ s)] (hs : ∀ a ∈ frontier s, f a = g a)
(hf : ContinuousOn f (closure s)) (hg : ContinuousOn g (closure sᶜ)) : Continuous (piecewise s f g) :=
continuous_if hs hf hg
