no goals
𝓕 : Type ?u.1232898
𝕜 : Type ?u.1232901
α : Type u_1
ι : Type ?u.1232907
κ : Type ?u.1232910
E : Type u_2
F : Type ?u.1232916
G : Type ?u.1232919
inst✝¹ : NormedAddGroup E
inst✝ : TopologicalSpace α
f : α → E
hf : Continuous f
h : HasCompactSupport f
⊢ ∃ C, ∀ (x : α), ‖f x‖ ≤ C
simpa [bddAbove_def] using hf.norm.bddAbove_range_of_hasCompactSupport h.norm