Theorems · Theorem · real analysis

BoxIntegral.Prepartition.sum_split_boxes

∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (I : BoxIntegral.Box ι) (i : ι) (x : ℝ)
  (f : BoxIntegral.Box ι → M),
  ∑ J ∈ (BoxIntegral.Prepartition.split I i x).boxes, f J =
    Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)

Defined in: Mathlib.Analysis.BoxIntegral.Partition.Split
Cited by: 1 results in Mathlib
Foundations: Depth 133 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddCommMonoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
AddCommMonoidstatement and proof · cited by 12,281
Finset.sumstatement and proof · cited by 5,195
BoxIntegral.Boxstatement and proof · cited by 464
BoxIntegral.Prepartitionproof · cited by 199
BoxIntegral.Prepartition.boxesstatement and proof · cited by 77
Option.elim'statement and proof · cited by 30
BoxIntegral.Prepartition.splitstatement · cited by 14
BoxIntegral.Box.splitLowerstatement and proof · cited by 11
BoxIntegral.Box.splitUpperstatement and proof · cited by 11
Finset.sum_pairproof · cited by 11
BoxIntegral.Prepartition.sum_ofWithBotproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

BoxIntegral.BoxAdditiveMap.map_split_addproof · cited by 0