∀ {α : Type u_2} {β : Type u_3} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀]
  [inst_2 : MulAction G₀ α] [ContinuousConstSMul G₀ α] [inst_4 : TopologicalSpace β] {f : β → α} {b : β} {c : G₀}
  {s : Set β}, c ≠ 0 → (ContinuousWithinAt (fun x => c • f x) s b ↔ ContinuousWithinAt f s b)