α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Nonempty α
f : { x // x ∈ lp E ⊤ }
⊢ IsLUB (Set.range fun i => ‖↑f i‖) (⨆ (i : α), ‖↑f i‖)
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Nonempty α
f : { x // x ∈ lp E ⊤ }
⊢ IsLUB (Set.range fun i => ‖↑f i‖) ‖f‖
rw [lp.norm_eq_ciSup]
no goals
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Nonempty α
f : { x // x ∈ lp E ⊤ }
⊢ IsLUB (Set.range fun i => ‖↑f i‖) (⨆ (i : α), ‖↑f i‖)
exact isLUB_ciSup (lp.memℓp f)