--- 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