src/HOL/Real/HahnBanach/FunctionNorm.thy
 changeset 9408 d3d56e1d2ec1 parent 9394 1ff8a6234c6a child 9503 3324cbbecef8
1.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Sun Jul 23 11:59:21 2000 +0200
1.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Sun Jul 23 12:01:05 2000 +0200
1.3 @@ -30,11 +30,11 @@
1.4    fix x assume "x \\<in> V" show "|f x| <= c * norm x" by (rule r)
1.5  qed
1.7 -lemma continuous_linearform [intro??]:
1.8 +lemma continuous_linearform [intro?]:
1.9    "is_continuous V norm f ==> is_linearform V f"
1.10    by (unfold is_continuous_def) force
1.12 -lemma continuous_bounded [intro??]:
1.13 +lemma continuous_bounded [intro?]:
1.14    "is_continuous V norm f
1.15    ==> \\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x"
1.16    by (unfold is_continuous_def) force
1.17 @@ -93,7 +93,7 @@
1.18  text {* The following lemma states that every continuous linear form
1.19  on a normed space $(V, \norm{\cdot})$ has a function norm. *}
1.21 -lemma ex_fnorm [intro??]:
1.22 +lemma ex_fnorm [intro?]:
1.23    "[| is_normed_vectorspace V norm; is_continuous V norm f|]
1.24       ==> is_function_norm f V norm \\<parallel>f\\<parallel>V,norm"
1.25  proof (unfold function_norm_def is_function_norm_def
1.26 @@ -193,7 +193,7 @@
1.28  text {* The norm of a continuous function is always $\geq 0$. *}
1.30 -lemma fnorm_ge_zero [intro??]:
1.31 +lemma fnorm_ge_zero [intro?]:
1.32    "[| is_continuous V norm f; is_normed_vectorspace V norm |]
1.33     ==> #0 <= \\<parallel>f\\<parallel>V,norm"
1.34  proof -