English
If p is a proposition and Decidable, the function a ↦ if p then f a else g a is continuous whenever f and g are continuous (independently of p).
Русский
Если p — предложение и Decidable, функция a ↦ если p тогда f a иначе g a непрерывна, когда f и g непрерывны отдельно.
LaTeX
$$$\forall p,\ \text{Decidable } p\Rightarrow (\mathrm{Continuous}\ f \Rightarrow \mathrm{Continuous}\ g)\Rightarrow \mathrm{Continuous}\ (a\mapsto \mathrm{ite}(p, f(a), g(a))).$$$
Lean4
theorem continuous_if_const (p : Prop) [Decidable p] (hf : p → Continuous f) (hg : ¬p → Continuous g) :
Continuous fun a => if p then f a else g a := by
split_ifs with h
exacts [hf h, hg h]