src/HOL/Real/HahnBanach/FunctionNorm.thy
 changeset 9998 09bf8fcd1c6e parent 9969 4753185f1dd2 child 10606 e3229a37d53f
equal 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 `