author | wenzelm |
Sun, 07 Nov 2021 19:53:37 +0100 | |
changeset 74726 | 33ed2eb06d68 |
parent 63040 | eb4ddd18d635 |
child 80914 | d97fdabd9e2b |
permissions | -rw-r--r-- |
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29291
diff
changeset
|
1 |
(* Title: HOL/Hahn_Banach/Function_Norm.thy |
7566 | 2 |
Author: Gertrud Bauer, TU Munich |
3 |
*) |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
4 |
|
58889 | 5 |
section \<open>The norm of a function\<close> |
7808 | 6 |
|
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29291
diff
changeset
|
7 |
theory Function_Norm |
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29291
diff
changeset
|
8 |
imports Normed_Space Function_Order |
27612 | 9 |
begin |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
10 |
|
58744 | 11 |
subsection \<open>Continuous linear forms\<close> |
7917 | 12 |
|
58744 | 13 |
text \<open> |
61879 | 14 |
A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> is \<^emph>\<open>continuous\<close>, iff |
15 |
it is bounded, i.e. |
|
10687 | 16 |
\begin{center} |
61539 | 17 |
\<open>\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close> |
10687 | 18 |
\end{center} |
61540 | 19 |
In our application no other functions than linear forms are considered, so |
20 |
we can define continuous linear forms as bounded linear forms: |
|
58744 | 21 |
\<close> |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
22 |
|
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset
|
23 |
locale continuous = linearform + |
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset
|
24 |
fixes norm :: "_ \<Rightarrow> real" ("\<parallel>_\<parallel>") |
13515 | 25 |
assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
26 |
|
14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
14214
diff
changeset
|
27 |
declare continuous.intro [intro?] continuous_axioms.intro [intro?] |
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
14214
diff
changeset
|
28 |
|
10687 | 29 |
lemma continuousI [intro]: |
27611 | 30 |
fixes norm :: "_ \<Rightarrow> real" ("\<parallel>_\<parallel>") |
31 |
assumes "linearform V f" |
|
13515 | 32 |
assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" |
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset
|
33 |
shows "continuous V f norm" |
13515 | 34 |
proof |
23378 | 35 |
show "linearform V f" by fact |
13515 | 36 |
from r have "\<exists>c. \<forall>x\<in>V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by blast |
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset
|
37 |
then show "continuous_axioms V f norm" .. |
13515 | 38 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
39 |
|
11472 | 40 |
|
58744 | 41 |
subsection \<open>The norm of a linear form\<close> |
7917 | 42 |
|
58744 | 43 |
text \<open> |
61539 | 44 |
The least real number \<open>c\<close> for which holds |
10687 | 45 |
\begin{center} |
61539 | 46 |
\<open>\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close> |
10687 | 47 |
\end{center} |
61539 | 48 |
is called the \<^emph>\<open>norm\<close> of \<open>f\<close>. |
7917 | 49 |
|
61540 | 50 |
For non-trivial vector spaces \<open>V \<noteq> {0}\<close> the norm can be defined as |
10687 | 51 |
\begin{center} |
61539 | 52 |
\<open>\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>\<close> |
10687 | 53 |
\end{center} |
7917 | 54 |
|
61879 | 55 |
For the case \<open>V = {0}\<close> the supremum would be taken from an empty set. Since |
56 |
\<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this situation it |
|
57 |
must be guaranteed that there is an element in this set. This element must |
|
58 |
be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties. Furthermore it does |
|
59 |
not have to change the norm in all other cases, so it must be \<open>0\<close>, as all |
|
60 |
other elements are \<open>{} \<ge> 0\<close>. |
|
7917 | 61 |
|
61540 | 62 |
Thus we define the set \<open>B\<close> where the supremum is taken from as follows: |
10687 | 63 |
\begin{center} |
61539 | 64 |
\<open>{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}\<close> |
10687 | 65 |
\end{center} |
66 |
||
61879 | 67 |
\<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists (otherwise |
68 |
it is undefined). |
|
58744 | 69 |
\<close> |
7917 | 70 |
|
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset
|
71 |
locale fn_norm = |
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset
|
72 |
fixes norm :: "_ \<Rightarrow> real" ("\<parallel>_\<parallel>") |
13547 | 73 |
fixes B defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}" |
74 |
fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999) |
|
13515 | 75 |
defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)" |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
76 |
|
27611 | 77 |
locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm |
78 |
||
13547 | 79 |
lemma (in fn_norm) B_not_empty [intro]: "0 \<in> B V f" |
80 |
by (simp add: B_def) |
|
7917 | 81 |
|
58744 | 82 |
text \<open> |
61540 | 83 |
The following lemma states that every continuous linear form on a normed |
84 |
space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> has a function norm. |
|
58744 | 85 |
\<close> |
10687 | 86 |
|
27611 | 87 |
lemma (in normed_vectorspace_with_fn_norm) fn_norm_works: |
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset
|
88 |
assumes "continuous V f norm" |
13515 | 89 |
shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" |
90 |
proof - |
|
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset
|
91 |
interpret continuous V f norm by fact |
58744 | 92 |
txt \<open>The existence of the supremum is shown using the |
13515 | 93 |
completeness of the reals. Completeness means, that every |
58744 | 94 |
non-empty bounded set of reals has a supremum.\<close> |
13515 | 95 |
have "\<exists>a. lub (B V f) a" |
96 |
proof (rule real_complete) |
|
61539 | 97 |
txt \<open>First we have to show that \<open>B\<close> is non-empty:\<close> |
13515 | 98 |
have "0 \<in> B V f" .. |
27612 | 99 |
then show "\<exists>x. x \<in> B V f" .. |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
100 |
|
61539 | 101 |
txt \<open>Then we have to show that \<open>B\<close> is bounded:\<close> |
13515 | 102 |
show "\<exists>c. \<forall>y \<in> B V f. y \<le> c" |
103 |
proof - |
|
61539 | 104 |
txt \<open>We know that \<open>f\<close> is bounded by some value \<open>c\<close>.\<close> |
13515 | 105 |
from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
106 |
|
61540 | 107 |
txt \<open>To prove the thesis, we have to show that there is some \<open>b\<close>, such |
108 |
that \<open>y \<le> b\<close> for all \<open>y \<in> B\<close>. Due to the definition of \<open>B\<close> there are |
|
109 |
two cases.\<close> |
|
7917 | 110 |
|
63040 | 111 |
define b where "b = max c 0" |
13515 | 112 |
have "\<forall>y \<in> B V f. y \<le> b" |
113 |
proof |
|
114 |
fix y assume y: "y \<in> B V f" |
|
115 |
show "y \<le> b" |
|
116 |
proof cases |
|
117 |
assume "y = 0" |
|
27612 | 118 |
then show ?thesis unfolding b_def by arith |
13515 | 119 |
next |
61539 | 120 |
txt \<open>The second case is \<open>y = \<bar>f x\<bar> / \<parallel>x\<parallel>\<close> for some |
121 |
\<open>x \<in> V\<close> with \<open>x \<noteq> 0\<close>.\<close> |
|
13515 | 122 |
assume "y \<noteq> 0" |
123 |
with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>" |
|
124 |
and x: "x \<in> V" and neq: "x \<noteq> 0" |
|
36778
739a9379e29b
avoid using real-specific versions of generic lemmas
huffman
parents:
32960
diff
changeset
|
125 |
by (auto simp add: B_def divide_inverse) |
13515 | 126 |
from x neq have gt: "0 < \<parallel>x\<parallel>" .. |
7917 | 127 |
|
58744 | 128 |
txt \<open>The thesis follows by a short calculation using the |
61539 | 129 |
fact that \<open>f\<close> is bounded.\<close> |
13515 | 130 |
|
131 |
note y_rep |
|
132 |
also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>" |
|
14334 | 133 |
proof (rule mult_right_mono) |
23378 | 134 |
from c x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. |
14334 | 135 |
from gt have "0 < inverse \<parallel>x\<parallel>" |
136 |
by (rule positive_imp_inverse_positive) |
|
27612 | 137 |
then show "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le) |
13515 | 138 |
qed |
139 |
also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)" |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
50918
diff
changeset
|
140 |
by (rule Groups.mult.assoc) |
13515 | 141 |
also |
142 |
from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp |
|
27612 | 143 |
then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp |
44887 | 144 |
also have "c * 1 \<le> b" by (simp add: b_def) |
13515 | 145 |
finally show "y \<le> b" . |
9035 | 146 |
qed |
13515 | 147 |
qed |
27612 | 148 |
then show ?thesis .. |
9035 | 149 |
qed |
150 |
qed |
|
27612 | 151 |
then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex) |
13515 | 152 |
qed |
153 |
||
27611 | 154 |
lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]: |
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset
|
155 |
assumes "continuous V f norm" |
13515 | 156 |
assumes b: "b \<in> B V f" |
157 |
shows "b \<le> \<parallel>f\<parallel>\<hyphen>V" |
|
158 |
proof - |
|
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset
|
159 |
interpret continuous V f norm by fact |
13547 | 160 |
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" |
58744 | 161 |
using \<open>continuous V f norm\<close> by (rule fn_norm_works) |
13515 | 162 |
from this and b show ?thesis .. |
163 |
qed |
|
164 |
||
27611 | 165 |
lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB: |
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset
|
166 |
assumes "continuous V f norm" |
13515 | 167 |
assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y" |
168 |
shows "\<parallel>f\<parallel>\<hyphen>V \<le> y" |
|
169 |
proof - |
|
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset
|
170 |
interpret continuous V f norm by fact |
13547 | 171 |
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" |
58744 | 172 |
using \<open>continuous V f norm\<close> by (rule fn_norm_works) |
13515 | 173 |
from this and b show ?thesis .. |
9035 | 174 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
175 |
|
61539 | 176 |
text \<open>The norm of a continuous function is always \<open>\<ge> 0\<close>.\<close> |
7917 | 177 |
|
27611 | 178 |
lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]: |
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset
|
179 |
assumes "continuous V f norm" |
13515 | 180 |
shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V" |
9035 | 181 |
proof - |
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset
|
182 |
interpret continuous V f norm by fact |
61539 | 183 |
txt \<open>The function norm is defined as the supremum of \<open>B\<close>. |
184 |
So it is \<open>\<ge> 0\<close> if all elements in \<open>B\<close> are \<open>\<ge> |
|
185 |
0\<close>, provided the supremum exists and \<open>B\<close> is not empty.\<close> |
|
13547 | 186 |
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" |
58744 | 187 |
using \<open>continuous V f norm\<close> by (rule fn_norm_works) |
13515 | 188 |
moreover have "0 \<in> B V f" .. |
189 |
ultimately show ?thesis .. |
|
9035 | 190 |
qed |
10687 | 191 |
|
58744 | 192 |
text \<open> |
61486 | 193 |
\<^medskip> |
194 |
The fundamental property of function norms is: |
|
10687 | 195 |
\begin{center} |
61539 | 196 |
\<open>\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close> |
10687 | 197 |
\end{center} |
58744 | 198 |
\<close> |
7917 | 199 |
|
27611 | 200 |
lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong: |
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset
|
201 |
assumes "continuous V f norm" "linearform V f" |
13515 | 202 |
assumes x: "x \<in> V" |
203 |
shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" |
|
27611 | 204 |
proof - |
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset
|
205 |
interpret continuous V f norm by fact |
29291 | 206 |
interpret linearform V f by fact |
27612 | 207 |
show ?thesis |
208 |
proof cases |
|
27611 | 209 |
assume "x = 0" |
210 |
then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp |
|
211 |
also have "f 0 = 0" by rule unfold_locales |
|
212 |
also have "\<bar>\<dots>\<bar> = 0" by simp |
|
213 |
also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V" |
|
58744 | 214 |
using \<open>continuous V f norm\<close> by (rule fn_norm_ge_zero) |
27611 | 215 |
from x have "0 \<le> norm x" .. |
216 |
with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff) |
|
217 |
finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" . |
|
218 |
next |
|
219 |
assume "x \<noteq> 0" |
|
220 |
with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp |
|
221 |
then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp |
|
222 |
also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" |
|
223 |
proof (rule mult_right_mono) |
|
224 |
from x show "0 \<le> \<parallel>x\<parallel>" .. |
|
225 |
from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f" |
|
36778
739a9379e29b
avoid using real-specific versions of generic lemmas
huffman
parents:
32960
diff
changeset
|
226 |
by (auto simp add: B_def divide_inverse) |
58744 | 227 |
with \<open>continuous V f norm\<close> show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
228 |
by (rule fn_norm_ub) |
27611 | 229 |
qed |
230 |
finally show ?thesis . |
|
9035 | 231 |
qed |
232 |
qed |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
233 |
|
58744 | 234 |
text \<open> |
61486 | 235 |
\<^medskip> |
61540 | 236 |
The function norm is the least positive real number for which the |
237 |
following inequality holds: |
|
10687 | 238 |
\begin{center} |
61539 | 239 |
\<open>\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close> |
10687 | 240 |
\end{center} |
58744 | 241 |
\<close> |
7917 | 242 |
|
27611 | 243 |
lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]: |
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset
|
244 |
assumes "continuous V f norm" |
50918 | 245 |
assumes ineq: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c" |
13515 | 246 |
shows "\<parallel>f\<parallel>\<hyphen>V \<le> c" |
27611 | 247 |
proof - |
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset
|
248 |
interpret continuous V f norm by fact |
27612 | 249 |
show ?thesis |
250 |
proof (rule fn_norm_leastB [folded B_def fn_norm_def]) |
|
27611 | 251 |
fix b assume b: "b \<in> B V f" |
252 |
show "b \<le> c" |
|
253 |
proof cases |
|
254 |
assume "b = 0" |
|
255 |
with ge show ?thesis by simp |
|
256 |
next |
|
257 |
assume "b \<noteq> 0" |
|
258 |
with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>" |
|
13515 | 259 |
and x_neq: "x \<noteq> 0" and x: "x \<in> V" |
36778
739a9379e29b
avoid using real-specific versions of generic lemmas
huffman
parents:
32960
diff
changeset
|
260 |
by (auto simp add: B_def divide_inverse) |
27611 | 261 |
note b_rep |
262 |
also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>" |
|
263 |
proof (rule mult_right_mono) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
264 |
have "0 < \<parallel>x\<parallel>" using x x_neq .. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
265 |
then show "0 \<le> inverse \<parallel>x\<parallel>" by simp |
50918 | 266 |
from x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by (rule ineq) |
27611 | 267 |
qed |
268 |
also have "\<dots> = c" |
|
269 |
proof - |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
270 |
from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
271 |
then show ?thesis by simp |
27611 | 272 |
qed |
273 |
finally show ?thesis . |
|
13515 | 274 |
qed |
58744 | 275 |
qed (insert \<open>continuous V f norm\<close>, simp_all add: continuous_def) |
27611 | 276 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
277 |
|
10687 | 278 |
end |