α : Type u_1
E : Type u_2
F : Type ?u.817811
𝕜 : Type ?u.817814
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
f : { x // x ∈ Lp E 1 }
⊢ ↑integralCLM f = setToFun μ (weightedSMul μ) (_ : DominatedFinMeasAdditive μ (weightedSMul μ) 1) fun a => ↑↑f a
α : Type u_1
E : Type u_2
F : Type ?u.817811
𝕜 : Type ?u.817814
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
f : { x // x ∈ Lp E 1 }
⊢ integral f = ∫ (a : α), ↑↑f a ∂μ
simp only [integral, L1.integral, integral_eq_setToFun]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.817811
𝕜 : Type ?u.817814
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
f : { x // x ∈ Lp E 1 }
⊢ ↑integralCLM f = setToFun μ (weightedSMul μ) (_ : DominatedFinMeasAdditive μ (weightedSMul μ) 1) fun a => ↑↑f a
exact (L1.setToFun_eq_setToL1 (dominatedFinMeasAdditive_weightedSMul μ) f).symm