α : Type u_2
E : Type u_1
F : Type ?u.1315198
𝕜 : Type ?u.1315201
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.1317892
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
h₁ : Integrable f
h₂ : Integrable f
⊢ ↑‖∫ (x : α), f x ∂ν‖₊ ≤ ∫⁻ (x : α), ↑‖f x‖₊ ∂ν
α : Type u_2
E : Type u_1
F : Type ?u.1315198
𝕜 : Type ?u.1315201
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.1317892
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
h₁ : Integrable f
h₂ : Integrable f
⊢ ↑(nndist (∫ (x : α), f x ∂μ) (∫ (x : α), f x ∂μ + ν)) ≤ ∫⁻ (x : α), ↑‖f x‖₊ ∂ν
rw [integral_add_measure h₁ h₂, nndist_comm, nndist_eq_nnnorm, add_sub_cancel']
no goals
α : Type u_2
E : Type u_1
F : Type ?u.1315198
𝕜 : Type ?u.1315201
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.1317892
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
h₁ : Integrable f
h₂ : Integrable f
⊢ ↑‖∫ (x : α), f x ∂ν‖₊ ≤ ∫⁻ (x : α), ↑‖f x‖₊ ∂ν
exact ennnorm_integral_le_lintegral_ennnorm _