∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E}, s ∈ nhds 0 → IsClosed (DFunLike.coe '' StrongDual.polar 𝕜 s)