α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.296683
G : Type ?u.296686
𝕜 : Type ?u.296689
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
c : ℝ
f : α →ₛ E
hf : Integrable ↑f
⊢ (fun x x_1 => x • x_1) c 0 = 0
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.296683
G : Type ?u.296686
𝕜 : Type ?u.296689
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
c : ℝ
f : α →ₛ E
hf : Integrable ↑f
⊢ setToSimpleFunc T (c • f) = ∑ x in SimpleFunc.range f, ↑(T (↑f ⁻¹' {x})) (c • x)
rw [smul_eq_map c f, map_setToSimpleFunc T h_add hf]
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.296683
G : Type ?u.296686
𝕜 : Type ?u.296689
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
c : ℝ
f : α →ₛ E
hf : Integrable ↑f
⊢ c • 0 = 0
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.296683
G : Type ?u.296686
𝕜 : Type ?u.296689
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
c : ℝ
f : α →ₛ E
hf : Integrable ↑f
⊢ (fun x x_1 => x • x_1) c 0 = 0
dsimp only
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.296683
G : Type ?u.296686
𝕜 : Type ?u.296689
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
c : ℝ
f : α →ₛ E
hf : Integrable ↑f
⊢ c • 0 = 0
rw [smul_zero]
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.296683
G : Type ?u.296686
𝕜 : Type ?u.296689
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
c : ℝ
f : α →ₛ E
hf : Integrable ↑f
b : E
x✝ : b ∈ SimpleFunc.range f
⊢ ↑(T (↑f ⁻¹' {b})) (c • b) = c • ↑(T (↑f ⁻¹' {b})) b
rw [ContinuousLinearMap.map_smul (T (f ⁻¹' {b})) c b]
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.296683
G : Type ?u.296686
𝕜 : Type ?u.296689
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
c : ℝ
f : α →ₛ E
hf : Integrable ↑f
⊢ ∑ x in SimpleFunc.range f, c • ↑(T (↑f ⁻¹' {x})) x = c • setToSimpleFunc T f
simp only [setToSimpleFunc, smul_sum, smul_smul, mul_comm]