∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace β]
  {s : Set α} {a : α} {f : α → β},
  ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Set.Iic a) a ∧ ContinuousWithinAt f (s ∩ Set.Ici a) a