α : Type u_2
E : Type u_1
F : Type ?u.871391
𝕜 : Type ?u.871394
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 α
⊢ (if hf : Integrable fun x => 0 then ↑L1.integralCLM (Integrable.toL1 (fun x => 0) hf) else 0) = 0
α : Type u_2
E : Type u_1
F : Type ?u.871391
𝕜 : Type ?u.871394
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 α
⊢ (∫ (x : α), 0 ∂μ) = 0
simp only [integral, L1.integral]
no goals
α : Type u_2
E : Type u_1
F : Type ?u.871391
𝕜 : Type ?u.871394
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 α
⊢ (if hf : Integrable fun x => 0 then ↑L1.integralCLM (Integrable.toL1 (fun x => 0) hf) else 0) = 0
exact setToFun_zero (dominatedFinMeasAdditive_weightedSMul μ)