no goals
M : Type ?u.43779
α : Type u_2
β : Type u_1
G : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : ContinuousConstSMul G α
inst✝ : TopologicalSpace β
f : β → α
b : β
s : Set β
c : G
⊢ (Continuous fun x => c • f x) ↔ Continuous f
simp only [continuous_iff_continuousAt, continuousAt_const_smul_iff]