α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.265062
G : Type ?u.265065
𝕜 : Type ?u.265068
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 g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
hp_pair : Integrable ↑(pair f g)
⊢ 0.fst + 0.snd = 0
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.265062
G : Type ?u.265065
𝕜 : Type ?u.265068
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 g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
hp_pair : Integrable ↑(pair f g)
⊢ setToSimpleFunc T (f + g) = ∑ x in SimpleFunc.range (pair f g), ↑(T (↑(pair f g) ⁻¹' {x})) (x.fst + x.snd)
rw [add_eq_map₂, map_setToSimpleFunc T h_add hp_pair]
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.265062
G : Type ?u.265065
𝕜 : Type ?u.265068
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 g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
hp_pair : Integrable ↑(pair f g)
⊢ 0.fst + 0.snd = 0
simp
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.265062
G : Type ?u.265065
𝕜 : Type ?u.265068
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 g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
hp_pair : Integrable ↑(pair f g)
⊢ ∑ x in SimpleFunc.range (pair f g), (↑(T (↑(pair f g) ⁻¹' {x})) x.fst + ↑(T (↑(pair f g) ⁻¹' {x})) x.snd) =
    ∑ x in SimpleFunc.range (pair f g), ↑(T (↑(pair f g) ⁻¹' {x})) x.fst +
      ∑ x in SimpleFunc.range (pair f g), ↑(T (↑(pair f g) ⁻¹' {x})) x.snd
rw [Finset.sum_add_distrib]
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.265062
G : Type ?u.265065
𝕜 : Type ?u.265068
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 g : α →ₛ E
hf : Integrable ↑f
hg : Integrable ↑g
hp_pair : Integrable ↑(pair f g)
⊢ ∑ x in SimpleFunc.range (pair f g), ↑(T (↑(pair f g) ⁻¹' {x})) x.fst +
      ∑ x in SimpleFunc.range (pair f g), ↑(T (↑(pair f g) ⁻¹' {x})) x.snd =
    setToSimpleFunc T (map Prod.fst (pair f g)) + setToSimpleFunc T (map Prod.snd (pair f g))
rw [map_setToSimpleFunc T h_add hp_pair Prod.snd_zero,
  map_setToSimpleFunc T h_add hp_pair Prod.fst_zero]