Theorems · Theorem · real analysis

ENNReal.finsetSum_iSup

∀ {ι : Type u_1} {α : Type u_2} {s : Finset α} {f : α → ι → ENNReal},
  (∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k) → ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i

Defined in

Mathlib.Data.ENNReal.BigOperators

Cited by

2 results in Mathlib

Foundations

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