no goals
p : ℝ≥0∞
𝕜 : Type ?u.293461
𝕜' : Type ?u.293464
ι : Type u_2
α : ι → Type ?u.293472
β✝ : ι → Type ?u.293477
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ edist x y = (∑ i : ι, edist (x i) (y i) ^ 2) ^ (1 / 2)
simp [PiLp.edist_eq_sum]