α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < ENNReal.toReal p
C : ℝ
hC : 0 ≤ C
f : { x // x ∈ lp E p }
hf : (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p) ≤ C ^ ENNReal.toReal p
⊢ (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p) ≤ C ^ ENNReal.toReal p
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < ENNReal.toReal p
C : ℝ
hC : 0 ≤ C
f : { x // x ∈ lp E p }
hf : (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p) ≤ C ^ ENNReal.toReal p
⊢ ‖f‖ ≤ C
rw [← Real.rpow_le_rpow_iff (norm_nonneg' _) hC hp, norm_rpow_eq_tsum hp]
no goals
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < ENNReal.toReal p
C : ℝ
hC : 0 ≤ C
f : { x // x ∈ lp E p }
hf : (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p) ≤ C ^ ENNReal.toReal p
⊢ (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p) ≤ C ^ ENNReal.toReal p
exact hf