p✝ : ℝ≥0∞
𝕜 : Type ?u.208827
𝕜' : Type ?u.208830
ι : Type u_2
α : ι → Type ?u.208838
β✝ : ι → Type ?u.208843
inst✝³ : Fintype ι
inst✝² : Fact (1 ≤ p✝)
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → PseudoMetricSpace (β i)
hp : p ≠ ⊤
x y : PiLp p β
⊢ dist x y = (∑ x_1 : ι, dist (x x_1) (y x_1) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
p✝ : ℝ≥0∞
𝕜 : Type ?u.208827
𝕜' : Type ?u.208830
ι : Type u_2
α : ι → Type ?u.208838
β✝ : ι → Type ?u.208843
inst✝³ : Fintype ι
inst✝² : Fact (1 ≤ p✝)
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → PseudoMetricSpace (β i)
hp : p ≠ ⊤
x y : PiLp p β
⊢ ↑(nndist x y) = ↑((∑ i : ι, nndist (x i) (y i) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p))
push_cast
no goals
p✝ : ℝ≥0∞
𝕜 : Type ?u.208827
𝕜' : Type ?u.208830
ι : Type u_2
α : ι → Type ?u.208838
β✝ : ι → Type ?u.208843
inst✝³ : Fintype ι
inst✝² : Fact (1 ≤ p✝)
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → PseudoMetricSpace (β i)
hp : p ≠ ⊤
x y : PiLp p β
⊢ dist x y = (∑ x_1 : ι, dist (x x_1) (y x_1) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
exact dist_eq_sum (p.toReal_pos_iff_ne_top.mpr hp) _ _