no goals
α : Type u_2
β : Type u_1
γ : Type ?u.940671
δ : Type ?u.940674
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : α → β
hf : Integrable f
hg : Integrable g
a : α
⊢ ↑‖f a + g a‖₊ ≤ ↑‖f a‖₊ + ↑‖g a‖₊
exact_mod_cast nnnorm_add_le _ _