p : ℝ≥0∞
𝕜 : Type ?u.22498
𝕜' : Type ?u.22501
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.22514
inst✝¹ : Fintype ι
inst✝ : (i : ι) → Dist (α i)
f g : PiLp ⊤ α
⊢ (if ⊤ = 0 then ↑(Finset.card (Finite.toFinset (_ : Set.Finite {i | f i ≠ g i})))
    else if ⊤ = ⊤ then ⨆ (i : ι), dist (f i) (g i) else (∑ i : ι, dist (f i) (g i) ^ 0) ^ (1 / 0)) =
    ⨆ (i : ι), dist (f i) (g i)
p : ℝ≥0∞
𝕜 : Type ?u.22498
𝕜' : Type ?u.22501
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.22514
inst✝¹ : Fintype ι
inst✝ : (i : ι) → Dist (α i)
f g : PiLp ⊤ α
⊢ dist f g = ⨆ (i : ι), dist (f i) (g i)
dsimp [dist]
no goals
p : ℝ≥0∞
𝕜 : Type ?u.22498
𝕜' : Type ?u.22501
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.22514
inst✝¹ : Fintype ι
inst✝ : (i : ι) → Dist (α i)
f g : PiLp ⊤ α
⊢ (if ⊤ = 0 then ↑(Finset.card (Finite.toFinset (_ : Set.Finite {i | f i ≠ g i})))
    else if ⊤ = ⊤ then ⨆ (i : ι), dist (f i) (g i) else (∑ i : ι, dist (f i) (g i) ^ 0) ^ (1 / 0)) =
    ⨆ (i : ι), dist (f i) (g i)
exact if_neg ENNReal.top_ne_zero