English
If two functions f and g are continuous on overlaps, and agree on the boundary between their domains, then the piecewise function piecewise t f g is continuous on s.
Русский
Если функции f и g непрерывны на перекрытии и согласованы на границе раздела, то piecewise t f g непрерывна на s.
LaTeX
$$$\\forall a\\in s,\\; a\\in\\text{frontier}(t) \\Rightarrow f(a)=g(a)\\;\\Rightarrow\\; \\mathrm{ContinuousOn}(\\text{piecewise } t\\; f\\; g)\,\\text{on } s.$$$
Lean4
theorem piecewise [∀ a, Decidable (a ∈ t)] (ht : ∀ a ∈ s ∩ frontier t, f a = g a) (hf : ContinuousOn f <| s ∩ closure t)
(hg : ContinuousOn g <| s ∩ closure tᶜ) : ContinuousOn (piecewise t f g) s :=
hf.if ht hg
