α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.281574
G : Type ?u.281577
𝕜 : Type ?u.281580
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f : α →ₛ E
hf : Integrable ↑f
⊢ ∑ x in SimpleFunc.range f, ↑(T (↑f ⁻¹' {x})) (-x) = ∑ x in SimpleFunc.range f, -↑(T (↑f ⁻¹' {x})) x
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.281574
G : Type ?u.281577
𝕜 : Type ?u.281580
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f : α →ₛ E
hf : Integrable ↑f
⊢ setToSimpleFunc T (map Neg.neg f) = -setToSimpleFunc T f
rw [map_setToSimpleFunc T h_add hf neg_zero, setToSimpleFunc, ← sum_neg_distrib]
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.281574
G : Type ?u.281577
𝕜 : Type ?u.281580
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f : α →ₛ E
hf : Integrable ↑f
⊢ ∑ x in SimpleFunc.range f, ↑(T (↑f ⁻¹' {x})) (-x) = ∑ x in SimpleFunc.range f, -↑(T (↑f ⁻¹' {x})) x
exact Finset.sum_congr rfl fun x _ => ContinuousLinearMap.map_neg _ _