Theorem: Average.sub (Ray/Misc/Measure.lean)

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f g : X → E
s : Set X
fi : IntegrableOn f s volume
gi : IntegrableOn g s volume
⊢ ⨍ (z : X) in s, f z - g z = (⨍ (z : X) in s, f z) - ⨍ (z : X) in s, g z
Tactic:
simp_rw [average_eq, integral_sub fi gi, smul_sub]
State after:
no goals