α : Type u_1
E : Type u_2
F : Type ?u.419045
𝕜 : Type ?u.419048
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
f : { x // x ∈ Lp E 1 }
⊢ ↑integralCLM f = ↑(setToL1 (_ : DominatedFinMeasAdditive μ (weightedSMul μ) 1)) f
α : Type u_1
E : Type u_2
F : Type ?u.419045
𝕜 : Type ?u.419048
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
f : { x // x ∈ Lp E 1 }
⊢ integral f = ↑(setToL1 (_ : DominatedFinMeasAdditive μ (weightedSMul μ) 1)) f
simp only [integral]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.419045
𝕜 : Type ?u.419048
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
f : { x // x ∈ Lp E 1 }
⊢ ↑integralCLM f = ↑(setToL1 (_ : DominatedFinMeasAdditive μ (weightedSMul μ) 1)) f
rfl