α : Type u_1
E : Type ?u.1057071
F : Type ?u.1057074
𝕜 : Type ?u.1057077
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.1059768
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
⊢ (∫ (a : α), f a ∂μ) = ∫ (a : α), ↑(Real.toNNReal (f a)) - ↑(Real.toNNReal (-f a)) ∂μ

α : Type u_1
E : Type ?u.1057071
F : Type ?u.1057074
𝕜 : Type ?u.1057077
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.1059768
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
⊢ Integrable fun a => ↑(Real.toNNReal (-f a))
α : Type u_1
E : Type ?u.1057071
F : Type ?u.1057074
𝕜 : Type ?u.1057077
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.1059768
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
⊢ (∫ (a : α), f a ∂μ) = (∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ) - ∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ
rw [← integral_sub hf.real_toNNReal]
no goals
α : Type u_1
E : Type ?u.1057071
F : Type ?u.1057074
𝕜 : Type ?u.1057077
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.1059768
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
⊢ (∫ (a : α), f a ∂μ) = ∫ (a : α), ↑(Real.toNNReal (f a)) - ↑(Real.toNNReal (-f a)) ∂μ
simp
no goals
α : Type u_1
E : Type ?u.1057071
F : Type ?u.1057074
𝕜 : Type ?u.1057077
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.1059768
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
⊢ Integrable fun a => ↑(Real.toNNReal (-f a))
exact hf.neg.real_toNNReal