∀ {ι : Type u} (s : Finset ι) {f g : ι → ℝ} {p : ℝ},
  1 ≤ p →
    (∀ i ∈ s, 0 ≤ f i) →
      (∀ i ∈ s, 0 ≤ g i) →
        (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)