α : Type u_2
inst✝ : MeasurableSpace α
m✝ : OuterMeasure α
ι : Type u_1
m : ι → OuterMeasure α
s : Set α
⊢ ∀ (i : Set α),
    s ⊆ i →
      MeasurableSet i →
        (∑' (i : ι), ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑(m i) t) ≤ ∑' (i_3 : ι), ↑(m i_3) i
α : Type u_2
inst✝ : MeasurableSpace α
m✝ : OuterMeasure α
ι : Type u_1
m : ι → OuterMeasure α
s : Set α
⊢ ↑(sum fun i => trim (m i)) s ≤ ↑(trim (sum m)) s
simp [trim_eq_iInf]
no goals
α : Type u_2
inst✝ : MeasurableSpace α
m✝ : OuterMeasure α
ι : Type u_1
m : ι → OuterMeasure α
s : Set α
⊢ ∀ (i : Set α),
    s ⊆ i →
      MeasurableSet i →
        (∑' (i : ι), ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑(m i) t) ≤ ∑' (i_3 : ι), ↑(m i_3) i
exact fun t st ht =>
  ENNReal.tsum_le_tsum fun i => iInf_le_of_le t <| iInf_le_of_le st <| iInf_le _ ht