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.6    
     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.11  
    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.20  
    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.27  
    1.28  text {* The norm of a continuous function is always $\geq 0$. *}
    1.29  
    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 -