equal
deleted
inserted
replaced
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 selectI2EX) |
100 is_continuous_def Sup_def, elim conjE, rule someI2EX) |
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 |