α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Nonempty α
f : { x // x ∈ lp E ⊤ }
C : ℝ
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
⊢ C ∈ upperBounds (Set.range fun 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 ⊤ }
C : ℝ
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
⊢ ‖f‖ ≤ C
refine' (isLUB_norm f).2 _
case intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Nonempty α
f : { x // x ∈ lp E ⊤ }
C : ℝ
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
i : α
⊢ (fun i => ‖↑f i‖) i ≤ C
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Nonempty α
f : { x // x ∈ lp E ⊤ }
C : ℝ
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
⊢ C ∈ upperBounds (Set.range fun i => ‖↑f i‖)
rintro - ⟨i, rfl⟩
no goals
case intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Nonempty α
f : { x // x ∈ lp E ⊤ }
C : ℝ
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
i : α
⊢ (fun i => ‖↑f i‖) i ≤ C
exact hCf i