α : Type u_2
E : α → Type u_1
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.912341
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : (i : α) → E i
i : α
⊢ (fun y => y ^ ENNReal.toReal p) ‖lp.single p i (f i)‖ = (fun y => y ^ ENNReal.toReal p) ‖f i‖
α : Type u_2
E : α → Type u_1
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.912341
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : (i : α) → E i
i : α
⊢ ‖lp.single p i (f i)‖ = ‖f i‖
refine' Real.rpow_left_injOn hp.ne' (norm_nonneg' _) (norm_nonneg _) _
no goals
α : Type u_2
E : α → Type u_1
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.912341
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : (i : α) → E i
i : α
⊢ (fun y => y ^ ENNReal.toReal p) ‖lp.single p i (f i)‖ = (fun y => y ^ ENNReal.toReal p) ‖f i‖
simpa using lp.norm_sum_single hp f {i}