α : Type u_1
E : Type ?u.162681
F : Type u_2
F' : Type u_3
G : Type ?u.162690
𝕜 : Type ?u.162693
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 α
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ↑(T (↑f ⁻¹' {x})) x = setToSimpleFunc T f
α : Type u_1
E : Type ?u.162681
F : Type u_2
F' : Type u_3
G : Type ?u.162690
𝕜 : Type ?u.162693
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 α
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ setToSimpleFunc T f = ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ↑(T (↑f ⁻¹' {x})) x
symm
α : Type u_1
E : Type ?u.162681
F : Type u_2
F' : Type u_3
G : Type ?u.162690
𝕜 : Type ?u.162693
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 α
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
x : F
x✝ : x ∈ SimpleFunc.range f
hx0 : x = 0
⊢ ↑(T (↑f ⁻¹' {x})) x = 0
α : Type u_1
E : Type ?u.162681
F : Type u_2
F' : Type u_3
G : Type ?u.162690
𝕜 : Type ?u.162693
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 α
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ↑(T (↑f ⁻¹' {x})) x = setToSimpleFunc T f
refine' sum_filter_of_ne fun x _ => mt fun hx0 => _
α : Type u_1
E : Type ?u.162681
F : Type u_2
F' : Type u_3
G : Type ?u.162690
𝕜 : Type ?u.162693
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 α
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
x : F
x✝ : x ∈ SimpleFunc.range f
hx0 : x = 0
⊢ ↑(T (↑f ⁻¹' {0})) 0 = 0
α : Type u_1
E : Type ?u.162681
F : Type u_2
F' : Type u_3
G : Type ?u.162690
𝕜 : Type ?u.162693
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 α
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
x : F
x✝ : x ∈ SimpleFunc.range f
hx0 : x = 0
⊢ ↑(T (↑f ⁻¹' {x})) x = 0
rw [hx0]
no goals
α : Type u_1
E : Type ?u.162681
F : Type u_2
F' : Type u_3
G : Type ?u.162690
𝕜 : Type ?u.162693
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 α
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
x : F
x✝ : x ∈ SimpleFunc.range f
hx0 : x = 0
⊢ ↑(T (↑f ⁻¹' {0})) 0 = 0
exact ContinuousLinearMap.map_zero _