∀ {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [ContinuousConstSMul M α] {c : M}, IsUnit c → ∀ {s : Set α} {a : α}, c • s ∈ nhds (c • a) ↔ s ∈ nhds a