α : Type u_1
E : Type ?u.2937028
F : Type u_2
G : Type ?u.2937034
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → F
x : α
⊢ (fun x => ↑‖(f + g) x‖₊) x ≤ ((fun x => ↑‖f x‖₊) + fun x => ↑‖g x‖₊) x
α : Type u_1
E : Type ?u.2937028
F : Type u_2
G : Type ?u.2937034
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → F
⊢ snormEssSup (f + g) μ ≤ snormEssSup f μ + snormEssSup g μ
refine' le_trans (essSup_mono_ae (eventually_of_forall fun x => _)) (ENNReal.essSup_add_le _ _)
α : Type u_1
E : Type ?u.2937028
F : Type u_2
G : Type ?u.2937034
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → F
x : α
⊢ ‖f x + g x‖₊ ≤ ‖f x‖₊ + ‖g x‖₊
α : Type u_1
E : Type ?u.2937028
F : Type u_2
G : Type ?u.2937034
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → F
x : α
⊢ (fun x => ↑‖(f + g) x‖₊) x ≤ ((fun x => ↑‖f x‖₊) + fun x => ↑‖g x‖₊) x
simp_rw [Pi.add_apply, ← ENNReal.coe_add, ENNReal.coe_le_coe]
no goals
α : Type u_1
E : Type ?u.2937028
F : Type u_2
G : Type ?u.2937034
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → F
x : α
⊢ ‖f x + g x‖₊ ≤ ‖f x‖₊ + ‖g x‖₊
exact nnnorm_add_le _ _