9374

1 
(* Title: HOL/Real/HahnBanach/HahnBanach.thy


2 
ID: $Id$


3 
Author: Gertrud Bauer, TU Munich


4 
*)


5 


6 
header {* The HahnBanach Theorem *}


7 


8 
theory HahnBanach = HahnBanachLemmas:


9 


10 
text {*


11 
We present the proof of two different versions of the HahnBanach


12 
Theorem, closely following \cite[\S36]{Heuser:1986}.


13 
*}


14 


15 
subsection {* The HahnBanach Theorem for vector spaces *}


16 


17 
text {*


18 
{\bf HahnBanach Theorem.}\quad


19 
Let $F$ be a subspace of a real vector space $E$, let $p$ be a seminorm on


20 
$E$, and $f$ be a linear form defined on $F$ such that $f$ is bounded by


21 
$p$, i.e. $\All {x\in F} f\ap x \leq p\ap x$. Then $f$ can be extended to


22 
a linear form $h$ on $E$ such that $h$ is normpreserving, i.e. $h$ is also


23 
bounded by $p$.


24 


25 
\bigskip


26 
{\bf Proof Sketch.}


27 
\begin{enumerate}


28 
\item Define $M$ as the set of normpreserving extensions of $f$ to subspaces


29 
of $E$. The linear forms in $M$ are ordered by domain extension.


30 
\item We show that every nonempty chain in $M$ has an upper bound in $M$.


31 
\item With Zorn's Lemma we conclude that there is a maximal function $g$ in


32 
$M$.


33 
\item The domain $H$ of $g$ is the whole space $E$, as shown by classical


34 
contradiction:


35 
\begin{itemize}


36 
\item Assuming $g$ is not defined on whole $E$, it can still be extended in a


37 
normpreserving way to a superspace $H'$ of $H$.


38 
\item Thus $g$ can not be maximal. Contradiction!


39 
\end{itemize}


40 
\end{enumerate}


41 
\bigskip


42 
*}


43 


44 
(*


45 
text {* {\bf Theorem.} Let $f$ be a linear form defined on a subspace


46 
$F$ of a real vector space $E$, such that $f$ is bounded by a seminorm


47 
$p$.


48 


49 
Then $f$ can be extended to a linear form $h$ on $E$ that is again


50 
bounded by $p$.


51 


52 
\bigskip{\bf Proof Outline.}


53 
First we define the set $M$ of all normpreserving extensions of $f$.


54 
We show that every chain in $M$ has an upper bound in $M$.


55 
With Zorn's lemma we can conclude that $M$ has a maximal element $g$.


56 
We further show by contradiction that the domain $H$ of $g$ is the whole


57 
vector space $E$.


58 
If $H \neq E$, then $g$ can be extended in


59 
a normpreserving way to a greater vector space $H_0$.


60 
So $g$ cannot be maximal in $M$.


61 
\bigskip


62 
*}


63 
*)

8084

64 

9256

65 
theorem HahnBanach:

9374

66 
"[ is_vectorspace E; is_subspace F E; is_seminorm E p;

9379

67 
is_linearform F f; \\<forall>x \\<in> F. f x <= p x ]


68 
==> \\<exists>h. is_linearform E h \\<and> (\\<forall>x \\<in> F. h x = f x)


69 
\\<and> (\\<forall>x \\<in> E. h x <= p x)"

9256

70 
 {* Let $E$ be a vector space, $F$ a subspace of $E$, $p$ a seminorm on $E$, *}


71 
 {* and $f$ a linear form on $F$ such that $f$ is bounded by $p$, *}


72 
 {* then $f$ can be extended to a linear form $h$ on $E$ in a normpreserving way. \skp *}

9035

73 
proof 

8084

74 
assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p"

9379

75 
and "is_linearform F f" "\\<forall>x \\<in> F. f x <= p x"

9256

76 
 {* Assume the context of the theorem. \skp *}

9035

77 
def M == "norm_pres_extensions E p F f"

9256

78 
 {* Define $M$ as the set of all normpreserving extensions of $F$. \skp *}

9035

79 
{

9379

80 
fix c assume "c \\<in> chain M" "\\<exists>x. x \\<in> c"

9394

81 
have "\\<Union>c \\<in> M"

9374

82 
 {* Show that every nonempty chain $c$ of $M$ has an upper bound in $M$: *}


83 
 {* $\Union c$ is greater than any element of the chain $c$, so it suffices to show $\Union c \in M$. *}

9035

84 
proof (unfold M_def, rule norm_pres_extensionI)

9394

85 
show "\\<exists>H h. graph H h = \\<Union>c

9379

86 
\\<and> is_linearform H h


87 
\\<and> is_subspace H E


88 
\\<and> is_subspace F H


89 
\\<and> graph F f \\<subseteq> graph H h


90 
\\<and> (\\<forall>x \\<in> H. h x <= p x)"

9035

91 
proof (intro exI conjI)

9394

92 
let ?H = "domain (\\<Union>c)"


93 
let ?h = "funct (\\<Union>c)"

8084

94 

9394

95 
show a: "graph ?H ?h = \\<Union>c"

9035

96 
proof (rule graph_domain_funct)

9394

97 
fix x y z assume "(x, y) \\<in> \\<Union>c" "(x, z) \\<in> \\<Union>c"

9035

98 
show "z = y" by (rule sup_definite)


99 
qed


100 
show "is_linearform ?H ?h"


101 
by (simp! add: sup_lf a)

9374

102 
show "is_subspace ?H E"


103 
by (rule sup_subE, rule a) (simp!)+

9035

104 
show "is_subspace F ?H"

9374

105 
by (rule sup_supF, rule a) (simp!)+

9379

106 
show "graph F f \\<subseteq> graph ?H ?h"

9374

107 
by (rule sup_ext, rule a) (simp!)+

9379

108 
show "\\<forall>x \\<in> ?H. ?h x <= p x"

9374

109 
by (rule sup_norm_pres, rule a) (simp!)+

9035

110 
qed


111 
qed

9256

112 

9035

113 
}

9379

114 
hence "\\<exists>g \\<in> M. \\<forall>x \\<in> M. g \\<subseteq> x > g = x"

9374

115 
 {* With Zorn's Lemma we can conclude that there is a maximal element in $M$.\skp *}

9035

116 
proof (rule Zorn's_Lemma)

9374

117 
 {* We show that $M$ is nonempty: *}

9379

118 
have "graph F f \\<in> norm_pres_extensions E p F f"

9035

119 
proof (rule norm_pres_extensionI2)


120 
have "is_vectorspace F" ..


121 
thus "is_subspace F F" ..


122 
qed (blast!)+

9379

123 
thus "graph F f \\<in> M" by (simp!)

9035

124 
qed


125 
thus ?thesis


126 
proof

9379

127 
fix g assume "g \\<in> M" "\\<forall>x \\<in> M. g \\<subseteq> x > g = x"

9256

128 
 {* We consider such a maximal element $g \in M$. \skp *}

9475

129 
obtain H h where "graph H h = g" "is_linearform H h"


130 
"is_subspace H E" "is_subspace F H" "graph F f \\<subseteq> graph H h"


131 
"\\<forall>x \\<in> H. h x <= p x"


132 
 {* $g$ is a normpreserving extension of $f$, in other words: *}


133 
 {* $g$ is the graph of some linear form $h$ defined on a subspace $H$ of $E$, *}


134 
 {* and $h$ is an extension of $f$ that is again bounded by $p$. \skp *}


135 
proof 


136 
have "\\<exists>H h. graph H h = g \\<and> is_linearform H h


137 
\\<and> is_subspace H E \\<and> is_subspace F H


138 
\\<and> graph F f \\<subseteq> graph H h


139 
\\<and> (\\<forall>x \\<in> H. h x <= p x)"


140 
by (simp! add: norm_pres_extension_D)


141 
thus ?thesis by (elim exE conjE) rule


142 
qed


143 
have h: "is_vectorspace H" ..


144 
have "H = E"


145 
 {* We show that $h$ is defined on whole $E$ by classical contradiction. \skp *}


146 
proof (rule classical)


147 
assume "H \\<noteq> E"


148 
 {* Assume $h$ is not defined on whole $E$. Then show that $h$ can be extended *}


149 
 {* in a normpreserving way to a function $h'$ with the graph $g'$. \skp *}


150 
have "\\<exists>g' \\<in> M. g \\<subseteq> g' \\<and> g \\<noteq> g'"

9035

151 
proof 

9475

152 
obtain x' where "x' \\<in> E" "x' \\<notin> H"


153 
 {* Pick $x' \in E \setminus H$. \skp *}


154 
proof 


155 
have "\\<exists>x' \\<in> E. x' \\<notin> H"


156 
proof (rule set_less_imp_diff_not_empty)


157 
have "H \\<subseteq> E" ..


158 
thus "H \\<subset> E" ..

9035

159 
qed

9475

160 
thus ?thesis by blast


161 
qed


162 
have x': "x' \\<noteq> 0"


163 
proof (rule classical)


164 
presume "x' = 0"


165 
with h have "x' \\<in> H" by simp


166 
thus ?thesis by contradiction


167 
qed blast


168 
def H' == "H + lin x'"


169 
 {* Define $H'$ as the direct sum of $H$ and the linear closure of $x'$. \skp *}


170 
obtain xi where "\\<forall>y \\<in> H.  p (y + x')  h y <= xi


171 
\\<and> xi <= p (y + x')  h y"


172 
 {* Pick a real number $\xi$ that fulfills certain inequations; this will *}


173 
 {* be used to establish that $h'$ is a normpreserving extension of $h$.


174 
\label{exxiuse}\skp *}


175 
proof 


176 
from h have "\\<exists>xi. \\<forall>y \\<in> H.  p (y + x')  h y <= xi


177 
\\<and> xi <= p (y + x')  h y"


178 
proof (rule ex_xi)


179 
fix u v assume "u \\<in> H" "v \\<in> H"


180 
from h have "h v  h u = h (v  u)"


181 
by (simp! add: linearform_diff)


182 
also have "... <= p (v  u)"


183 
by (simp!)


184 
also have "v  u = x' +  x' + v +  u"


185 
by (simp! add: diff_eq1)


186 
also have "... = v + x' +  (u + x')"


187 
by (simp!)


188 
also have "... = (v + x')  (u + x')"


189 
by (simp! add: diff_eq1)


190 
also have "p ... <= p (v + x') + p (u + x')"


191 
by (rule seminorm_diff_subadditive) (simp_all!)


192 
finally have "h v  h u <= p (v + x') + p (u + x')" .

9261

193 

9475

194 
thus " p (u + x')  h u <= p (v + x')  h v"


195 
by (rule real_diff_ineq_swap)


196 
qed


197 
thus ?thesis by rule rule


198 
qed


199 


200 
def h' == "\\<lambda>x. let (y,a) = SOME (y,a). x = y + a \\<cdot> x' \\<and> y \\<in> H


201 
in (h y) + a * xi"


202 
 {* Define the extension $h'$ of $h$ to $H'$ using $\xi$. \skp *}


203 
show ?thesis


204 
proof


205 
show "g \\<subseteq> graph H' h' \\<and> g \\<noteq> graph H' h'"


206 
 {* Show that $h'$ is an extension of $h$ \dots \skp *}


207 
proof


208 
show "g \\<subseteq> graph H' h'"

9261

209 
proof 

9475

210 
have "graph H h \\<subseteq> graph H' h'"


211 
proof (rule graph_extI)


212 
fix t assume "t \\<in> H"


213 
have "(SOME (y, a). t = y + a \\<cdot> x' \\<and> y \\<in> H)


214 
= (t, #0)"


215 
by (rule decomp_H'_H) (assumption+, rule x')


216 
thus "h t = h' t" by (simp! add: Let_def)


217 
next


218 
show "H \\<subseteq> H'"


219 
proof (rule subspace_subset)


220 
show "is_subspace H H'"


221 
proof (unfold H'_def, rule subspace_vs_sum1)


222 
show "is_vectorspace H" ..


223 
show "is_vectorspace (lin x')" ..


224 
qed


225 
qed


226 
qed


227 
thus ?thesis by (simp!)

9261

228 
qed

9475

229 
show "g \\<noteq> graph H' h'"


230 
proof 


231 
have "graph H h \\<noteq> graph H' h'"

9374

232 
proof

9475

233 
assume e: "graph H h = graph H' h'"


234 
have "x' \\<in> H'"


235 
proof (unfold H'_def, rule vs_sumI)


236 
show "x' = 0 + x'" by (simp!)


237 
from h show "0 \\<in> H" ..


238 
show "x' \\<in> lin x'" by (rule x_lin_x)


239 
qed


240 
hence "(x', h' x') \\<in> graph H' h'" ..


241 
with e have "(x', h' x') \\<in> graph H h" by simp


242 
hence "x' \\<in> H" ..


243 
thus False by contradiction

9035

244 
qed

9475

245 
thus ?thesis by (simp!)

9035

246 
qed


247 
qed

9475

248 
show "graph H' h' \\<in> M"


249 
 {* and $h'$ is normpreserving. \skp *}


250 
proof 


251 
have "graph H' h' \\<in> norm_pres_extensions E p F f"


252 
proof (rule norm_pres_extensionI2)


253 
show "is_linearform H' h'"


254 
by (rule h'_lf) (simp! add: x')+


255 
show "is_subspace H' E"


256 
by (unfold H'_def)


257 
(rule vs_sum_subspace [OF _ lin_subspace])


258 
have "is_subspace F H" .


259 
also from h lin_vs


260 
have [fold H'_def]: "is_subspace H (H + lin x')" ..


261 
finally (subspace_trans [OF _ h])


262 
show f_h': "is_subspace F H'" .


263 


264 
show "graph F f \\<subseteq> graph H' h'"


265 
proof (rule graph_extI)


266 
fix x assume "x \\<in> F"


267 
have "f x = h x" ..


268 
also have " ... = h x + #0 * xi" by simp


269 
also


270 
have "... = (let (y,a) = (x, #0) in h y + a * xi)"


271 
by (simp add: Let_def)


272 
also have


273 
"(x, #0) = (SOME (y, a). x = y + a \\<cdot> x' \\<and> y \\<in> H)"


274 
by (rule decomp_H'_H [RS sym]) (simp! add: x')+


275 
also have


276 
"(let (y,a) = (SOME (y,a). x = y + a \\<cdot> x' \\<and> y \\<in> H)


277 
in h y + a * xi) = h' x" by (simp!)


278 
finally show "f x = h' x" .


279 
next


280 
from f_h' show "F \\<subseteq> H'" ..


281 
qed


282 


283 
show "\\<forall>x \\<in> H'. h' x <= p x"


284 
by (rule h'_norm_pres) (assumption+, rule x')


285 
qed


286 
thus "graph H' h' \\<in> M" by (simp!)


287 
qed

9035

288 
qed

9256

289 
qed

9475

290 
hence "\\<not> (\\<forall>x \\<in> M. g \\<subseteq> x > g = x)" by simp


291 
 {* So the graph $g$ of $h$ cannot be maximal. Contradiction! \skp *}


292 
thus "H = E" by contradiction


293 
qed


294 
thus "\\<exists>h. is_linearform E h \\<and> (\\<forall>x \\<in> F. h x = f x)


295 
\\<and> (\\<forall>x \\<in> E. h x <= p x)"


296 
proof (intro exI conjI)


297 
assume eq: "H = E"


298 
from eq show "is_linearform E h" by (simp!)


299 
show "\\<forall>x \\<in> F. h x = f x"


300 
proof


301 
fix x assume "x \\<in> F" have "f x = h x " ..


302 
thus "h x = f x" ..

9035

303 
qed

9475

304 
from eq show "\\<forall>x \\<in> E. h x <= p x" by (force!)

9035

305 
qed


306 
qed

9475

307 
qed

9374

308 


309 


310 
subsection {* Alternative formulation *}


311 


312 
text {* The following alternative formulation of the HahnBanach


313 
Theorem\label{absHahnBanach} uses the fact that for a real linear form


314 
$f$ and a seminorm $p$ the


315 
following inequations are equivalent:\footnote{This was shown in lemma


316 
$\idt{abs{\dsh}ineq{\dsh}iff}$ (see page \pageref{absineqiff}).}


317 
\begin{matharray}{ll}


318 
\forall x\in H.\ap h\ap x\leq p\ap x& {\rm and}\\


319 
\forall x\in H.\ap h\ap x\leq p\ap x\\


320 
\end{matharray}


321 
*}


322 


323 
theorem abs_HahnBanach:

9475

324 
"[ is_vectorspace E; is_subspace F E; is_linearform F f;


325 
is_seminorm E p; \\<forall>x \\<in> F. f x <= p x ]


326 
==> \\<exists>g. is_linearform E g \\<and> (\\<forall>x \\<in> F. g x = f x)


327 
\\<and> (\\<forall>x \\<in> E. g x <= p x)"

9374

328 
proof 

9475

329 
assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p"


330 
"is_linearform F f" "\\<forall>x \\<in> F. f x <= p x"


331 
have "\\<forall>x \\<in> F. f x <= p x" by (rule abs_ineq_iff [RS iffD1])


332 
hence "\\<exists>g. is_linearform E g \\<and> (\\<forall>x \\<in> F. g x = f x)


333 
\\<and> (\\<forall>x \\<in> E. g x <= p x)"


334 
by (simp! only: HahnBanach)


335 
thus ?thesis


336 
proof (elim exE conjE)


337 
fix g assume "is_linearform E g" "\\<forall>x \\<in> F. g x = f x"


338 
"\\<forall>x \\<in> E. g x <= p x"


339 
hence "\\<forall>x \\<in> E. g x <= p x"


340 
by (simp! add: abs_ineq_iff [OF subspace_refl])


341 
thus ?thesis by (intro exI conjI)


342 
qed

9374

343 
qed


344 


345 
subsection {* The HahnBanach Theorem for normed spaces *}


346 


347 
text {* Every continuous linear form $f$ on a subspace $F$ of a


348 
norm space $E$, can be extended to a continuous linear form $g$ on


349 
$E$ such that $\fnorm{f} = \fnorm {g}$. *}


350 


351 
theorem norm_HahnBanach:

9475

352 
"[ is_normed_vectorspace E norm; is_subspace F E;


353 
is_linearform F f; is_continuous F norm f ]


354 
==> \\<exists>g. is_linearform E g


355 
\\<and> is_continuous E norm g


356 
\\<and> (\\<forall>x \\<in> F. g x = f x)


357 
\\<and> \\<parallel>g\\<parallel>E,norm = \\<parallel>f\\<parallel>F,norm"

9374

358 
proof 

9475

359 
assume e_norm: "is_normed_vectorspace E norm"


360 
assume f: "is_subspace F E" "is_linearform F f"


361 
assume f_cont: "is_continuous F norm f"


362 
have e: "is_vectorspace E" ..


363 
hence f_norm: "is_normed_vectorspace F norm" ..


364 


365 
txt{* We define a function $p$ on $E$ as follows:


366 
\begin{matharray}{l}


367 
p \: x = \fnorm f \cdot \norm x\\


368 
\end{matharray}


369 
*}


370 


371 
def p == "\\<lambda>x. \\<parallel>f\\<parallel>F,norm * norm x"


372 


373 
txt{* $p$ is a seminorm on $E$: *}


374 


375 
have q: "is_seminorm E p"


376 
proof


377 
fix x y a assume "x \\<in> E" "y \\<in> E"


378 


379 
txt{* $p$ is positive definite: *}

9374

380 

9475

381 
show "#0 <= p x"


382 
proof (unfold p_def, rule real_le_mult_order1a)


383 
from f_cont f_norm show "#0 <= \\<parallel>f\\<parallel>F,norm" ..


384 
show "#0 <= norm x" ..


385 
qed


386 


387 
txt{* $p$ is absolutely homogenous: *}

9374

388 

9475

389 
show "p (a \\<cdot> x) = a * p x"


390 
proof 


391 
have "p (a \\<cdot> x) = \\<parallel>f\\<parallel>F,norm * norm (a \\<cdot> x)"


392 
by (simp!)


393 
also have "norm (a \\<cdot> x) = a * norm x"


394 
by (rule normed_vs_norm_abs_homogenous)


395 
also have "\\<parallel>f\\<parallel>F,norm * ( a * norm x )


396 
= a * (\\<parallel>f\\<parallel>F,norm * norm x)"


397 
by (simp! only: real_mult_left_commute)


398 
also have "... = a * p x" by (simp!)


399 
finally show ?thesis .


400 
qed


401 


402 
txt{* Furthermore, $p$ is subadditive: *}

9374

403 

9475

404 
show "p (x + y) <= p x + p y"


405 
proof 


406 
have "p (x + y) = \\<parallel>f\\<parallel>F,norm * norm (x + y)"


407 
by (simp!)


408 
also


409 
have "... <= \\<parallel>f\\<parallel>F,norm * (norm x + norm y)"


410 
proof (rule real_mult_le_le_mono1a)


411 
from f_cont f_norm show "#0 <= \\<parallel>f\\<parallel>F,norm" ..


412 
show "norm (x + y) <= norm x + norm y" ..


413 
qed


414 
also have "... = \\<parallel>f\\<parallel>F,norm * norm x


415 
+ \\<parallel>f\\<parallel>F,norm * norm y"


416 
by (simp! only: real_add_mult_distrib2)


417 
finally show ?thesis by (simp!)


418 
qed


419 
qed

9374

420 

9475

421 
txt{* $f$ is bounded by $p$. *}


422 


423 
have "\\<forall>x \\<in> F. f x <= p x"


424 
proof


425 
fix x assume "x \\<in> F"


426 
from f_norm show "f x <= p x"


427 
by (simp! add: norm_fx_le_norm_f_norm_x)


428 
qed


429 


430 
txt{* Using the fact that $p$ is a seminorm and


431 
$f$ is bounded by $p$ we can apply the HahnBanach Theorem


432 
for real vector spaces.


433 
So $f$ can be extended in a normpreserving way to some function


434 
$g$ on the whole vector space $E$. *}


435 


436 
with e f q


437 
have "\\<exists>g. is_linearform E g \\<and> (\\<forall>x \\<in> F. g x = f x)


438 
\\<and> (\\<forall>x \\<in> E. g x <= p x)"


439 
by (simp! add: abs_HahnBanach)

9374

440 

9475

441 
thus ?thesis


442 
proof (elim exE conjE)


443 
fix g


444 
assume "is_linearform E g" and a: "\\<forall>x \\<in> F. g x = f x"


445 
and b: "\\<forall>x \\<in> E. g x <= p x"


446 


447 
show "\\<exists>g. is_linearform E g


448 
\\<and> is_continuous E norm g


449 
\\<and> (\\<forall>x \\<in> F. g x = f x)


450 
\\<and> \\<parallel>g\\<parallel>E,norm = \\<parallel>f\\<parallel>F,norm"


451 
proof (intro exI conjI)


452 


453 
txt{* We furthermore have to show that


454 
$g$ is also continuous: *}


455 


456 
show g_cont: "is_continuous E norm g"


457 
proof


458 
fix x assume "x \\<in> E"


459 
with b show "g x <= \\<parallel>f\\<parallel>F,norm * norm x"


460 
by (simp add: p_def)


461 
qed

9374

462 

9475

463 
txt {* To complete the proof, we show that


464 
$\fnorm g = \fnorm f$. \label{order_antisym} *}


465 


466 
show "\\<parallel>g\\<parallel>E,norm = \\<parallel>f\\<parallel>F,norm"


467 
(is "?L = ?R")


468 
proof (rule order_antisym)


469 


470 
txt{* First we show $\fnorm g \leq \fnorm f$. The function norm


471 
$\fnorm g$ is defined as the smallest $c\in\bbbR$ such that


472 
\begin{matharray}{l}


473 
\All {x\in E} {g\ap x \leq c \cdot \norm x}


474 
\end{matharray}


475 
Furthermore holds


476 
\begin{matharray}{l}


477 
\All {x\in E} {g\ap x \leq \fnorm f \cdot \norm x}


478 
\end{matharray}


479 
*}


480 


481 
have "\\<forall>x \\<in> E. g x <= \\<parallel>f\\<parallel>F,norm * norm x"


482 
proof


483 
fix x assume "x \\<in> E"


484 
show "g x <= \\<parallel>f\\<parallel>F,norm * norm x"

9374

485 
by (simp!)


486 
qed


487 

9475

488 
with g_cont e_norm show "?L <= ?R"


489 
proof (rule fnorm_le_ub)


490 
from f_cont f_norm show "#0 <= \\<parallel>f\\<parallel>F,norm" ..

9374

491 
qed


492 

9475

493 
txt{* The other direction is achieved by a similar


494 
argument. *}

9374

495 

9475

496 
have "\\<forall>x \\<in> F. f x <= \\<parallel>g\\<parallel>E,norm * norm x"


497 
proof


498 
fix x assume "x \\<in> F"


499 
from a have "g x = f x" ..


500 
hence "f x = g x" by simp


501 
also from g_cont


502 
have "... <= \\<parallel>g\\<parallel>E,norm * norm x"


503 
proof (rule norm_fx_le_norm_f_norm_x)


504 
show "x \\<in> E" ..

9374

505 
qed

9475

506 
finally show "f x <= \\<parallel>g\\<parallel>E,norm * norm x" .


507 
qed


508 
thus "?R <= ?L"


509 
proof (rule fnorm_le_ub [OF f_cont f_norm])


510 
from g_cont show "#0 <= \\<parallel>g\\<parallel>E,norm" ..

9374

511 
qed


512 
qed


513 
qed

9475

514 
qed


515 
qed

9374

516 

9475

517 
end
