∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : SeminormedAddGroup E]
  {ι : Type u_3} [Nonempty ι] [inst_2 : LinearOrder ι] {f : ι → α → E} {p : ℝ} {f_lim : α → E},
  (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (f_lim x))) →
    MeasureTheory.eLpNorm' f_lim p μ = (∫⁻ (a : α), Filter.liminf (fun x => ‖f x a‖ₑ ^ p) Filter.atTop ∂μ) ^ (1 / p)