p : ℝ≥0∞
𝕜 : Type ?u.291243
𝕜' : Type ?u.291246
ι : Type u_2
α : ι → Type ?u.291254
β✝ : ι → Type ?u.291259
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ dist x y = Real.sqrt (∑ x_1 : ι, dist (x x_1) (y x_1) ^ 2)
p : ℝ≥0∞
𝕜 : Type ?u.291243
𝕜' : Type ?u.291246
ι : Type u_2
α : ι → Type ?u.291254
β✝ : ι → Type ?u.291259
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ ↑(nndist x y) = ↑(↑NNReal.sqrt (∑ i : ι, nndist (x i) (y i) ^ 2))
push_cast
no goals
p : ℝ≥0∞
𝕜 : Type ?u.291243
𝕜' : Type ?u.291246
ι : Type u_2
α : ι → Type ?u.291254
β✝ : ι → Type ?u.291259
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ dist x y = Real.sqrt (∑ x_1 : ι, dist (x x_1) (y x_1) ^ 2)
exact dist_eq_of_L2 _ _