p : ℝ≥0∞
𝕜 : Type ?u.289391
𝕜' : Type ?u.289394
ι : Type u_2
α : ι → Type ?u.289402
β✝ : ι → Type ?u.289407
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ Real.sqrt (∑ i : ι, ‖(x - y) i‖ ^ 2) = Real.sqrt (∑ x_1 : ι, ‖x x_1 - y x_1‖ ^ 2)
p : ℝ≥0∞
𝕜 : Type ?u.289391
𝕜' : Type ?u.289394
ι : Type u_2
α : ι → Type ?u.289402
β✝ : ι → Type ?u.289407
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ dist x y = Real.sqrt (∑ i : ι, dist (x i) (y i) ^ 2)
simp_rw [dist_eq_norm, norm_eq_of_L2, Pi.sub_apply]
no goals
p : ℝ≥0∞
𝕜 : Type ?u.289391
𝕜' : Type ?u.289394
ι : Type u_2
α : ι → Type ?u.289402
β✝ : ι → Type ?u.289407
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ Real.sqrt (∑ i : ι, ‖(x - y) i‖ ^ 2) = Real.sqrt (∑ x_1 : ι, ‖x x_1 - y x_1‖ ^ 2)
rfl