case inl
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E ⊤ }
C : ℝ
hC : 0 ≤ C
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
h✝ : IsEmpty α
⊢ ‖f‖ ≤ C

case inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E ⊤ }
C : ℝ
hC : 0 ≤ C
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
h✝ : Nonempty α
⊢ ‖f‖ ≤ C
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E ⊤ }
C : ℝ
hC : 0 ≤ C
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
⊢ ‖f‖ ≤ C
cases isEmpty_or_nonempty α
no goals
case inl
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E ⊤ }
C : ℝ
hC : 0 ≤ C
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
h✝ : IsEmpty α
⊢ ‖f‖ ≤ C
simpa [eq_zero' f] using hC
no goals
case inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E ⊤ }
C : ℝ
hC : 0 ≤ C
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
h✝ : Nonempty α
⊢ ‖f‖ ≤ C
exact norm_le_of_forall_le' C hCf