(𝕜 : Type u_4) →
  [inst : NontriviallyNormedField 𝕜] →
    {M : Type u_5} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : TopologicalSpace M] →
          [inst_3 : Module 𝕜 M] →
            {S : Type u_6} → [inst_4 : SetLike S M] → [SMulMemClass S 𝕜 M] → S → Submodule 𝕜 (StrongDual 𝕜 M)