α : Type u_1
E : Type u_2
F : Type ?u.484290
𝕜 : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
c : 𝕜
f : { x // x ∈ Lp E 1 }
⊢ ↑integralCLM (c • f) = c • ↑integralCLM f
α : Type u_1
E : Type u_2
F : Type ?u.484290
𝕜 : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
c : 𝕜
f : { x // x ∈ Lp E 1 }
⊢ integral (c • f) = c • integral f
simp only [integral]
α : Type u_1
E : Type u_2
F : Type ?u.484290
𝕜 : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
c : 𝕜
f : { x // x ∈ Lp E 1 }
⊢ ↑(integralCLM' 𝕜) (c • f) = c • ↑(integralCLM' 𝕜) f
α : Type u_1
E : Type u_2
F : Type ?u.484290
𝕜 : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
c : 𝕜
f : { x // x ∈ Lp E 1 }
⊢ ↑integralCLM (c • f) = c • ↑integralCLM f
show (integralCLM' (E := E) 𝕜) (c • f) = c • (integralCLM' (E := E) 𝕜) f
no goals
α : Type u_1
E : Type u_2
F : Type ?u.484290
𝕜 : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
c : 𝕜
f : { x // x ∈ Lp E 1 }
⊢ ↑(integralCLM' 𝕜) (c • f) = c • ↑(integralCLM' 𝕜) f
exact map_smul (integralCLM' (E := E) 𝕜) c f