ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I J✝ : Box ι
π✝ : TaggedPrepartition I
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
J : Box ι
hJ : J ∈ π.boxes
J' : Box ι
hJ' : J' ∈ (πi J).boxes
⊢ ↑(↑vol J') (f (tag (Prepartition.biUnionTagged π πi) J')) = ↑(↑vol J') (f (tag (πi J) J'))
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I J : Box ι
π✝ : TaggedPrepartition I
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ integralSum f vol (Prepartition.biUnionTagged π πi) = ∑ J in π.boxes, integralSum f vol (πi J)
refine (π.sum_biUnion_boxes _ _).trans <| sum_congr rfl fun J hJ => sum_congr rfl fun J' hJ' => ?_
no goals
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I J✝ : Box ι
π✝ : TaggedPrepartition I
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
J : Box ι
hJ : J ∈ π.boxes
J' : Box ι
hJ' : J' ∈ (πi J).boxes
⊢ ↑(↑vol J') (f (tag (Prepartition.biUnionTagged π πi) J')) = ↑(↑vol J') (f (tag (πi J) J'))
rw [π.tag_biUnionTagged hJ hJ']