no goals
α : Type u
α' : Type ?u.55194
β : Type v
β' : Type ?u.55199
γ : Type ?u.55202
φ : Type ?u.55205
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
p : Prop
hp : Decidable p
f g : α → β
hf : Continuous' f
hg : Continuous' g
⊢ Continuous' fun x => if p then f x else g x
split_ifs <;> simp [*]