src/HOL/Real/HahnBanach/FunctionNorm.thy
changeset 9998 09bf8fcd1c6e
parent 9969 4753185f1dd2
child 10606 e3229a37d53f
equal deleted inserted replaced
9997:38598a19e701 9998:09bf8fcd1c6e
    95 
    95 
    96 lemma ex_fnorm [intro?]: 
    96 lemma ex_fnorm [intro?]: 
    97   "[| is_normed_vectorspace V norm; is_continuous V norm f|]
    97   "[| is_normed_vectorspace V norm; is_continuous V norm f|]
    98      ==> is_function_norm f V norm \<parallel>f\<parallel>V,norm" 
    98      ==> is_function_norm f V norm \<parallel>f\<parallel>V,norm" 
    99 proof (unfold function_norm_def is_function_norm_def 
    99 proof (unfold function_norm_def is_function_norm_def 
   100   is_continuous_def Sup_def, elim conjE, rule someI2EX)
   100   is_continuous_def Sup_def, elim conjE, rule someI2_ex)
   101   assume "is_normed_vectorspace V norm"
   101   assume "is_normed_vectorspace V norm"
   102   assume "is_linearform V f" 
   102   assume "is_linearform V f" 
   103   and e: "\<exists>c. \<forall>x \<in> V. |f x| <= c * norm x"
   103   and e: "\<exists>c. \<forall>x \<in> V. |f x| <= c * norm x"
   104 
   104 
   105   txt {* The existence of the supremum is shown using the 
   105   txt {* The existence of the supremum is shown using the