∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {β : Type u_2} [inst_1 : One β] [inst_2 : TopologicalSpace β] (f : α → β)
  (E : Set α),
  Filter.Tendsto (fun δ => (Metric.cthickening δ E).mulIndicator f) (nhds 0) (nhds ((closure E).mulIndicator f))