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