no goals
α : Type u_3
ι : Type u_2
E : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SeminormedAddCommGroup E
l : Filter ι
f : ι → α → E
g : α → E
⊢ TendstoInMeasure μ f l g ↔ ∀ (ε : ℝ), 0 < ε → Tendsto (fun i => ↑↑μ {x | ε ≤ ‖f i x - g x‖}) l (𝓝 0)
simp_rw [TendstoInMeasure, dist_eq_norm]