∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : SeminormedAddGroup E] {l : Filter ι} {f : ι → α → E} {g : α → E},
  MeasureTheory.TendstoInMeasure μ f l g =
    ∀ (ε : ℝ), 0 < ε → Filter.Tendsto (fun i => μ {x | ε ≤ ‖f i x - g x‖}) l (nhds 0)