Theorems · Theorem · real analysis

BoxIntegral.integralSum_congr

∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι}
  {π : BoxIntegral.TaggedPrepartition I} {f₁ f₂ : (ι → ℝ) → E} {vol₁ vol₂ : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
  Set.EqOn f₁ f₂ (BoxIntegral.Box.Icc I) →
    Set.EqOn ⇑vol₁ ⇑vol₂ ↑π.boxes → BoxIntegral.integralSum f₁ vol₁ π = BoxIntegral.integralSum f₂ vol₂ π

Defined in

Mathlib.Analysis.BoxIntegral.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace