case a
p : ℝ≥0∞
𝕜 : Type ?u.236805
𝕜' : Type ?u.236808
ι : Type u_2
α : ι → Type ?u.236816
β✝ : ι → Type ?u.236821
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ⊤ β
⊢ ↑‖f‖₊ = ↑(⨆ (i : ι), ‖f i‖₊)
p : ℝ≥0∞
𝕜 : Type ?u.236805
𝕜' : Type ?u.236808
ι : Type u_2
α : ι → Type ?u.236816
β✝ : ι → Type ?u.236821
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ⊤ β
⊢ ‖f‖₊ = ⨆ (i : ι), ‖f i‖₊
ext
no goals
case a
p : ℝ≥0∞
𝕜 : Type ?u.236805
𝕜' : Type ?u.236808
ι : Type u_2
α : ι → Type ?u.236816
β✝ : ι → Type ?u.236821
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ⊤ β
⊢ ↑‖f‖₊ = ↑(⨆ (i : ι), ‖f i‖₊)
simp [NNReal.coe_iSup, norm_eq_ciSup]