diff -r 88eb92a52f9b -r d8045bc0544e src/HOL/Analysis/Bounded_Continuous_Function.thy
--- a/src/HOL/Analysis/Bounded_Continuous_Function.thy	Fri Nov 03 10:55:15 2023 +0100
+++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy	Fri Nov 03 16:20:06 2023 +0000
@@ -244,10 +244,6 @@
 
 end
 
-lemma bounded_norm_le_SUP_norm:
-  "bounded (range f) \<Longrightarrow> norm (f x) \<le> (SUP x. norm (f x))"
-  by (auto intro!: cSUP_upper bounded_imp_bdd_above simp: bounded_norm_comp)
-
 instantiation\<^marker>\<open>tag unimportant\<close> bcontfun :: (topological_space, real_normed_vector) real_normed_vector
 begin