∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f g h : α → E},
  MeasureTheory.MemLp f p μ →
    MeasureTheory.MemLp g p μ →
      1 ≤ p → MeasureTheory.lpNorm (f - h) p μ ≤ MeasureTheory.lpNorm (f - g) p μ + MeasureTheory.lpNorm (g - h) p μ