Theorems · Theorem · real analysis

BoxIntegral.Prepartition.sum_ofWithBot

∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {M : Type u_2} [inst : AddCommMonoid M]
  (boxes : Finset (WithBot (BoxIntegral.Box ι))) (le_of_mem : ∀ J ∈ boxes, J ≤ ↑I)
  (pairwise_disjoint : (↑boxes).Pairwise Disjoint) (f : BoxIntegral.Box ι → M),
  ∑ J ∈ (BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint).boxes, f J =
    ∑ J ∈ boxes, Option.elim' 0 f J

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoid