∀ {α : Type u_1} {E : Type u_2} (𝕜 : Type u_3) {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {t : Set E},
  TopologicalSpace.IsSeparable t →
    ∀ {f : α → E}, (∀ (c : StrongDual 𝕜 E), (fun x => c (f x)) =ᵐ[μ] 0) → (∀ᵐ (x : α) ∂μ, f x ∈ t) → f =ᵐ[μ] 0