p : ℝ≥0∞
𝕜 : Type ?u.210631
𝕜' : Type ?u.210634
ι : Type u_2
α : ι → Type ?u.210642
β✝ : ι → Type ?u.210647
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → PseudoMetricSpace (β i)
x y : PiLp ⊤ β
⊢ dist x y = ⨆ (i : ι), dist (x i) (y i)
p : ℝ≥0∞
𝕜 : Type ?u.210631
𝕜' : Type ?u.210634
ι : Type u_2
α : ι → Type ?u.210642
β✝ : ι → Type ?u.210647
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → PseudoMetricSpace (β i)
x y : PiLp ⊤ β
⊢ ↑(nndist x y) = ↑(⨆ (i : ι), nndist (x i) (y i))
push_cast
no goals
p : ℝ≥0∞
𝕜 : Type ?u.210631
𝕜' : Type ?u.210634
ι : Type u_2
α : ι → Type ?u.210642
β✝ : ι → Type ?u.210647
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → PseudoMetricSpace (β i)
x y : PiLp ⊤ β
⊢ dist x y = ⨆ (i : ι), dist (x i) (y i)
exact dist_eq_iSup _ _