∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {p : α → Prop}
  [inst_2 : (a : α) → Decidable (p a)],
  (∀ a ∈ frontier {x | p x}, f a = g a) →
    ContinuousOn f (closure {x | p x}) →
      ContinuousOn g (closure {x | ¬p x}) → Continuous fun a => if p a then f a else g a