∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {p : α → Prop}
  {f g : α → β} [inst_2 : (a : α) → Decidable (p a)],
  (∀ a ∈ s ∩ frontier {a | p a}, Filter.Tendsto f (nhdsWithin a (s ∩ {a | p a})) (nhds (if p a then f a else g a))) →
    (∀ a ∈ s ∩ frontier {a | p a}, Filter.Tendsto g (nhdsWithin a (s ∩ {a | ¬p a})) (nhds (if p a then f a else g a))) →
      ContinuousOn f (s ∩ {a | p a}) →
        ContinuousOn g (s ∩ {a | ¬p a}) → ContinuousOn (fun a => if p a then f a else g a) s