∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} {μ : MeasureTheory.Measure E} [BorelSpace E] [FiniteDimensional ℝ E]
  [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] {ι : Type u_2} {φ : ι → ContDiffBump c} {l : Filter ι},
  Filter.Tendsto (fun i => (φ i).rOut) l (nhds 0) →
    Filter.Tendsto (fun i => Function.support fun x => (φ i).normed μ x) l (nhds c).smallSets