α : Type u_1
β : Type u_2
γ : Type ?u.690087
δ : Type ?u.690090
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
⊢ (∫⁻ (a : α), edist (f a) (g a) ∂μ) ≤ ∫⁻ (a : α), edist (f a) (h a) + edist (g a) (h a) ∂μ
α : Type u_1
β : Type u_2
γ : Type ?u.690087
δ : Type ?u.690090
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
⊢ (∫⁻ (a : α), edist (f a) (g a) ∂μ) ≤ (∫⁻ (a : α), edist (f a) (h a) ∂μ) + ∫⁻ (a : α), edist (g a) (h a) ∂μ
rw [← lintegral_add_left' (hf.edist hh)]
α : Type u_1
β : Type u_2
γ : Type ?u.690087
δ : Type ?u.690090
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
a : α
⊢ edist (f a) (g a) ≤ edist (f a) (h a) + edist (g a) (h a)
α : Type u_1
β : Type u_2
γ : Type ?u.690087
δ : Type ?u.690090
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
⊢ (∫⁻ (a : α), edist (f a) (g a) ∂μ) ≤ ∫⁻ (a : α), edist (f a) (h a) + edist (g a) (h a) ∂μ
refine' lintegral_mono fun a => _
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.690087
δ : Type ?u.690090
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
a : α
⊢ edist (f a) (g a) ≤ edist (f a) (h a) + edist (g a) (h a)
apply edist_triangle_right