Theorems · Theorem · functional analysis

Real.iSup_prod_eq_prod_iSup_of_nonnegHomClass

∀ {α : Type u_5} {R : Type u_6} [inst : Fintype α] {ι : α → Type u} [∀ (a : α), Finite (ι a)] {F : Type u_7}
  [inst_2 : FunLike F R ℝ] [NonnegHomClass F R ℝ] (v : F) {x : (a : α) → ι a → R},
  ⨆ i, ∏ a, v (x a (i a)) = ∏ a, ⨆ i, v (x a i)

Defined in

Mathlib.Analysis.Normed.Ring.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeFiniteFunLikeNonnegHomClass