English
Let p be a predicate, and suppose f and g are continuous and coincide on the frontier of the set where p holds; then the function a ↦ if p a then f a else g a is continuous on the whole space.
Русский
Пусть p — предикат, f и g непрерывны и совпадают на границе множества, где выполняется p; тогда функция a ↦ если p(a) тогда f(a) иначе g(a) непрерывна во всём пространстве.
LaTeX
$$$\forall p: \alpha \to \mathrm{Prop},\; (\forall a, \text{frontier}(\{x\mid p x\}) ) \Rightarrow \text{Continuous}\ (\lambda a. \text{ite}(p(a), f(a), g(a))).$$$
Lean4
theorem continuous_if {p : α → Prop} [∀ a, Decidable (p a)] (hp : ∀ a ∈ frontier {x | p x}, f a = g a)
(hf : ContinuousOn f (closure {x | p x})) (hg : ContinuousOn g (closure {x | ¬p x})) :
Continuous fun a => if p a then f a else g a :=
by
rw [← continuousOn_univ]
apply ContinuousOn.if <;> simpa
