Theorems · Theorem · real analysis

ENNReal.iInf_sum

∀ {ι : Type u_3} {α : Type u_4} {f : ι → α → ENNReal} {s : Finset α} [Nonempty ι],
  (∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a) → ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a

Defined in

Mathlib.Data.ENNReal.BigOperators

Cited by

0 results in Mathlib

Foundations

Depth 129 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Nonempty