Convergence in probability

theorem MeasureTheory.TendstoInMeasure.add {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {ι : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {f g : ι → Ω → E} {l₁ l₂ : Ω → E} {u : Filter ι} (hf : TendstoInMeasure μ f u l₁) (hg : TendstoInMeasure μ g u l₂) : TendstoInMeasure μ (fun (n : ι) (ω : Ω) => f n ω + g n ω) u fun (ω : Ω) => l₁ ω + l₂ ω