Theorems · Theorem · functional analysis

Real.iSup_prod_eq_prod_iSup_of_nonneg

∀ {α : Type u_5} [inst : Fintype α] {ι : α → Type u} [∀ (a : α), Finite (ι a)] {f : (a : α) → ι a → ℝ},
  (∀ (a : α) (i : ι a), 0 ≤ f a i) → ⨆ i, ∏ a, f a (i a) = ∏ a, ⨆ i, f a i

Defined in

Mathlib.Analysis.Normed.Ring.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeFinite