α : Type u_1
E : Type u_2
F : Type ?u.1303582
𝕜 : Type ?u.1303585
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 : Type ?u.1306276
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
m : MeasurableSpace α
f : α → E
⊢ (if hf : Integrable fun x => f x then ↑L1.integralCLM (Integrable.toL1 (fun x => f x) hf) else 0) = 0
α : Type u_1
E : Type u_2
F : Type ?u.1303582
𝕜 : Type ?u.1303585
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 : Type ?u.1306276
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
m : MeasurableSpace α
f : α → E
⊢ (∫ (x : α), f x ∂0) = 0
simp only [integral, L1.integral]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.1303582
𝕜 : Type ?u.1303585
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 : Type ?u.1306276
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
m : MeasurableSpace α
f : α → E
⊢ (if hf : Integrable fun x => f x then ↑L1.integralCLM (Integrable.toL1 (fun x => f x) hf) else 0) = 0
exact setToFun_measure_zero (dominatedFinMeasAdditive_weightedSMul _) rfl