∀ (R : Type u_1) {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] {ι : Sort u_4} {S : Type u_5} [inst_4 : SetLike S M] [SMulMemClass S R M]
  [AddSubmonoidClass S M] {p : ι → Prop} {s : ι → S}, ((nhds 0).HasBasis p fun i => ↑(s i)) → IsLinearTopology R M