no goals
α : Type u_2
E : α → Type u_1
p✝ q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.858705
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
p : ℝ≥0∞
i : α
a : E i
⊢ ↑(lp.single p i a) i = a
rw [lp.single_apply, dif_pos rfl]