summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 20 Dec 2015 13:56:02 +0100 | |

changeset 61879 | e4f9d8f094fe |

parent 61878 | fa4dbb82732f |

child 61880 | ff4d33058566 |

child 61883 | c0f34fe6aa61 |

tuned whitespace;

--- a/src/HOL/Hahn_Banach/Function_Norm.thy Sun Dec 20 13:11:47 2015 +0100 +++ b/src/HOL/Hahn_Banach/Function_Norm.thy Sun Dec 20 13:56:02 2015 +0100 @@ -11,8 +11,8 @@ subsection \<open>Continuous linear forms\<close> text \<open> - A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> is \<^emph>\<open>continuous\<close>, - iff it is bounded, i.e. + A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> is \<^emph>\<open>continuous\<close>, iff + it is bounded, i.e. \begin{center} \<open>\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close> \end{center} @@ -52,20 +52,20 @@ \<open>\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>\<close> \end{center} - For the case \<open>V = {0}\<close> the supremum would be taken from an empty set. - Since \<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this - situation it must be guaranteed that there is an element in this set. This - element must be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties. - Furthermore it does not have to change the norm in all other cases, so it - must be \<open>0\<close>, as all other elements are \<open>{} \<ge> 0\<close>. + For the case \<open>V = {0}\<close> the supremum would be taken from an empty set. Since + \<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this situation it + must be guaranteed that there is an element in this set. This element must + be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties. Furthermore it does + not have to change the norm in all other cases, so it must be \<open>0\<close>, as all + other elements are \<open>{} \<ge> 0\<close>. Thus we define the set \<open>B\<close> where the supremum is taken from as follows: \begin{center} \<open>{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}\<close> \end{center} - \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists - (otherwise it is undefined). + \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists (otherwise + it is undefined). \<close> locale fn_norm =

--- a/src/HOL/Hahn_Banach/Function_Order.thy Sun Dec 20 13:11:47 2015 +0100 +++ b/src/HOL/Hahn_Banach/Function_Order.thy Sun Dec 20 13:56:02 2015 +0100 @@ -11,14 +11,12 @@ subsection \<open>The graph of a function\<close> text \<open> - We define the \<^emph>\<open>graph\<close> of a (real) function \<open>f\<close> with - domain \<open>F\<close> as the set + We define the \<^emph>\<open>graph\<close> of a (real) function \<open>f\<close> with domain \<open>F\<close> as the set \begin{center} \<open>{(x, f x). x \<in> F}\<close> \end{center} - So we are modeling partial functions by specifying the domain and - the mapping function. We use the term ``function'' also for its - graph. + So we are modeling partial functions by specifying the domain and the + mapping function. We use the term ``function'' also for its graph. \<close> type_synonym 'a graph = "('a \<times> real) set" @@ -41,8 +39,8 @@ subsection \<open>Functions ordered by domain extension\<close> text \<open> - A function \<open>h'\<close> is an extension of \<open>h\<close>, iff the graph of - \<open>h\<close> is a subset of the graph of \<open>h'\<close>. + A function \<open>h'\<close> is an extension of \<open>h\<close>, iff the graph of \<open>h\<close> is a subset of + the graph of \<open>h'\<close>. \<close> lemma graph_extI: @@ -93,8 +91,8 @@ subsection \<open>Norm-preserving extensions of a function\<close> text \<open> - Given a linear form \<open>f\<close> on the space \<open>F\<close> and a seminorm \<open>p\<close> on \<open>E\<close>. The - set of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are + Given a linear form \<open>f\<close> on the space \<open>F\<close> and a seminorm \<open>p\<close> on \<open>E\<close>. The set + of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are bounded by \<open>p\<close>, is defined as follows. \<close>

--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy Sun Dec 20 13:11:47 2015 +0100 +++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Sun Dec 20 13:56:02 2015 +0100 @@ -18,28 +18,26 @@ paragraph \<open>Hahn-Banach Theorem.\<close> text \<open> - Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm - on \<open>E\<close>, and \<open>f\<close> be a linear form defined on \<open>F\<close> such that \<open>f\<close> is bounded - by \<open>p\<close>, i.e. \<open>\<forall>x \<in> F. f x \<le> p x\<close>. Then \<open>f\<close> can be extended to a linear - form \<open>h\<close> on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded - by \<open>p\<close>. + Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm on + \<open>E\<close>, and \<open>f\<close> be a linear form defined on \<open>F\<close> such that \<open>f\<close> is bounded by + \<open>p\<close>, i.e. \<open>\<forall>x \<in> F. f x \<le> p x\<close>. Then \<open>f\<close> can be extended to a linear form \<open>h\<close> + on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded by \<open>p\<close>. \<close> paragraph \<open>Proof Sketch.\<close> text \<open> - \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces - of \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension. + \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces of + \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension. \<^enum> We show that every non-empty chain in \<open>M\<close> has an upper bound in \<open>M\<close>. - \<^enum> With Zorn's Lemma we conclude that there is a maximal function \<open>g\<close> in - \<open>M\<close>. + \<^enum> With Zorn's Lemma we conclude that there is a maximal function \<open>g\<close> in \<open>M\<close>. \<^enum> The domain \<open>H\<close> of \<open>g\<close> is the whole space \<open>E\<close>, as shown by classical contradiction: - \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can still be extended in - a norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>. + \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can still be extended in a + norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>. \<^item> Thus \<open>g\<close> can not be maximal. Contradiction! \<close> @@ -292,14 +290,13 @@ text \<open> The following alternative formulation of the Hahn-Banach - Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear form - \<open>f\<close> and a seminorm \<open>p\<close> the following inequality are - equivalent:\footnote{This was shown in lemma @{thm [source] abs_ineq_iff} - (see page \pageref{abs-ineq-iff}).} + Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear form \<open>f\<close> + and a seminorm \<open>p\<close> the following inequality are equivalent:\footnote{This + was shown in lemma @{thm [source] abs_ineq_iff} (see page + \pageref{abs-ineq-iff}).} \begin{center} \begin{tabular}{lll} - \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and & - \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\ + \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and & \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\ \end{tabular} \end{center} \<close> @@ -336,9 +333,8 @@ subsection \<open>The Hahn-Banach Theorem for normed spaces\<close> text \<open> - Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a norm space \<open>E\<close>, - can be extended to a continuous linear form \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> = - \<parallel>g\<parallel>\<close>. + Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a norm space \<open>E\<close>, can + be extended to a continuous linear form \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> = \<parallel>g\<parallel>\<close>. \<close> theorem norm_Hahn_Banach: @@ -420,10 +416,10 @@ OF F_norm, folded B_def fn_norm_def]) qed - txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded by \<open>p\<close> we - can apply the Hahn-Banach Theorem for real vector spaces. So \<open>f\<close> can be - extended in a norm-preserving way to some function \<open>g\<close> on the whole - vector space \<open>E\<close>.\<close> + txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded by \<open>p\<close> we can + apply the Hahn-Banach Theorem for real vector spaces. So \<open>f\<close> can be + extended in a norm-preserving way to some function \<open>g\<close> on the whole vector + space \<open>E\<close>.\<close> with E FE linearform q obtain g where linearformE: "linearform E g"

--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Sun Dec 20 13:11:47 2015 +0100 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Sun Dec 20 13:56:02 2015 +0100 @@ -9,14 +9,13 @@ begin text \<open> - In this section the following context is presumed. Let \<open>E\<close> be a real - vector space with a seminorm \<open>q\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of \<open>E\<close> and \<open>f\<close> - a linear function on \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a - superspace of \<open>F\<close> and a linear form \<open>h\<close> on \<open>H\<close>. \<open>H\<close> is a not equal to \<open>E\<close> - and \<open>x\<^sub>0\<close> is an element in \<open>E - H\<close>. \<open>H\<close> is extended to the direct sum \<open>H' - = H + lin x\<^sub>0\<close>, so for any \<open>x \<in> H'\<close> the decomposition of \<open>x = y + a \<cdot> x\<close> - with \<open>y \<in> H\<close> is unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y + a \<cdot> \<xi>\<close> - for a certain \<open>\<xi>\<close>. + In this section the following context is presumed. Let \<open>E\<close> be a real vector + space with a seminorm \<open>q\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of \<open>E\<close> and \<open>f\<close> a linear + function on \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a superspace of + \<open>F\<close> and a linear form \<open>h\<close> on \<open>H\<close>. \<open>H\<close> is a not equal to \<open>E\<close> and \<open>x\<^sub>0\<close> is an + element in \<open>E - H\<close>. \<open>H\<close> is extended to the direct sum \<open>H' = H + lin x\<^sub>0\<close>, so + for any \<open>x \<in> H'\<close> the decomposition of \<open>x = y + a \<cdot> x\<close> with \<open>y \<in> H\<close> is + unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y + a \<cdot> \<xi>\<close> for a certain \<open>\<xi>\<close>. Subsequently we show some properties of this extension \<open>h'\<close> of \<open>h\<close>. @@ -82,8 +81,8 @@ text \<open> \<^medskip> - The function \<open>h'\<close> is defined as a \<open>h' x = h y + a \<cdot> \<xi>\<close> where - \<open>x = y + a \<cdot> \<xi>\<close> is a linear extension of \<open>h\<close> to \<open>H'\<close>. + The function \<open>h'\<close> is defined as a \<open>h' x = h y + a \<cdot> \<xi>\<close> where \<open>x = y + a \<cdot> \<xi>\<close> + is a linear extension of \<open>h\<close> to \<open>H'\<close>. \<close> lemma h'_lf:

--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Sun Dec 20 13:11:47 2015 +0100 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Sun Dec 20 13:56:02 2015 +0100 @@ -10,17 +10,16 @@ text \<open> This section contains some lemmas that will be used in the proof of the - Hahn-Banach Theorem. In this section the following context is presumed. - Let \<open>E\<close> be a real vector space with a seminorm \<open>p\<close> on \<open>E\<close>. \<open>F\<close> is a - subspace of \<open>E\<close> and \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close> of - norm-preserving extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will - show some properties about the limit function \<open>h\<close>, i.e.\ the supremum of - the chain \<open>c\<close>. + Hahn-Banach Theorem. In this section the following context is presumed. Let + \<open>E\<close> be a real vector space with a seminorm \<open>p\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of + \<open>E\<close> and \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close> of norm-preserving + extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will show some properties + about the limit function \<open>h\<close>, i.e.\ the supremum of the chain \<open>c\<close>. \<^medskip> - Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and - let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of - one of the elements of the chain. + Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and let + \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of one of + the elements of the chain. \<close> lemmas [dest?] = chainsD @@ -55,10 +54,10 @@ text \<open> \<^medskip> - Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and - let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of - the supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>, - such that \<open>h\<close> extends \<open>h'\<close>. + Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and let + \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of the + supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>, such + that \<open>h\<close> extends \<open>h'\<close>. \<close> lemma some_H'h': @@ -83,9 +82,9 @@ text \<open> \<^medskip> - Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function - \<open>h\<close> are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> - extends \<open>h'\<close>. + Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function \<open>h\<close> + are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> extends + \<open>h'\<close>. \<close> lemma some_H'h'2: @@ -99,8 +98,8 @@ \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H' \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)" proof - - txt \<open>\<open>y\<close> is in the domain \<open>H''\<close> of some function \<open>h''\<close>, - such that \<open>h\<close> extends \<open>h''\<close>.\<close> + txt \<open>\<open>y\<close> is in the domain \<open>H''\<close> of some function \<open>h''\<close>, such that \<open>h\<close> + extends \<open>h''\<close>.\<close> from M cM u and y obtain H' h' where y_hy: "(y, h y) \<in> graph H' h'" @@ -121,10 +120,9 @@ "graph F f \<subseteq> graph H'' h''" "\<forall>x \<in> H''. h'' x \<le> p x" by (rule some_H'h't [elim_format]) blast - txt \<open>Since both \<open>h'\<close> and \<open>h''\<close> are elements of the chain, - \<open>h''\<close> is an extension of \<open>h'\<close> or vice versa. Thus both - \<open>x\<close> and \<open>y\<close> are contained in the greater - one. \label{cases1}\<close> + txt \<open>Since both \<open>h'\<close> and \<open>h''\<close> are elements of the chain, \<open>h''\<close> is an + extension of \<open>h'\<close> or vice versa. Thus both \<open>x\<close> and \<open>y\<close> are contained in + the greater one. \label{cases1}\<close> from cM c'' c' consider "graph H'' h'' \<subseteq> graph H' h'" | "graph H' h' \<subseteq> graph H'' h''" by (blast dest: chainsD) @@ -205,11 +203,11 @@ text \<open> \<^medskip> - The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close> - is in the domain of a function \<open>h'\<close> in the chain of norm preserving - extensions. Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function - values of \<open>x\<close> are identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close> - is linear by construction of \<open>M\<close>. + The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close> is + in the domain of a function \<open>h'\<close> in the chain of norm preserving extensions. + Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function values of \<open>x\<close> are + identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close> is linear by + construction of \<open>M\<close>. \<close> lemma sup_lf: @@ -286,8 +284,8 @@ text \<open> \<^medskip> - The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is - a subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure + The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is a + subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure properties follow from the fact that \<open>F\<close> is a vector space. \<close> @@ -367,8 +365,8 @@ text \<open> \<^medskip> - The limit function is bounded by the norm \<open>p\<close> as well, since all elements - in the chain are bounded by \<open>p\<close>. + The limit function is bounded by the norm \<open>p\<close> as well, since all elements in + the chain are bounded by \<open>p\<close>. \<close> lemma sup_norm_pres: @@ -389,10 +387,10 @@ text \<open> \<^medskip> - The following lemma is a property of linear forms on real vector spaces. - It will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page - \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces - the following inequality are equivalent: + The following lemma is a property of linear forms on real vector spaces. It + will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page + \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces the + following inequality are equivalent: \begin{center} \begin{tabular}{lll} \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &

--- a/src/HOL/Hahn_Banach/Normed_Space.thy Sun Dec 20 13:11:47 2015 +0100 +++ b/src/HOL/Hahn_Banach/Normed_Space.thy Sun Dec 20 13:56:02 2015 +0100 @@ -11,9 +11,9 @@ subsection \<open>Quasinorms\<close> text \<open> - A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space into the reals - that has the following properties: it is positive definite, absolute - homogeneous and subadditive. + A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space into the reals that + has the following properties: it is positive definite, absolute homogeneous + and subadditive. \<close> locale seminorm = @@ -57,8 +57,7 @@ subsection \<open>Norms\<close> text \<open> - A \<^emph>\<open>norm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a seminorm that maps only the - \<open>0\<close> vector to \<open>0\<close>. + A \<^emph>\<open>norm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a seminorm that maps only the \<open>0\<close> vector to \<open>0\<close>. \<close> locale norm = seminorm + @@ -68,8 +67,7 @@ subsection \<open>Normed vector spaces\<close> text \<open> - A vector space together with a norm is called a \<^emph>\<open>normed - space\<close>. + A vector space together with a norm is called a \<^emph>\<open>normed space\<close>. \<close> locale normed_vectorspace = vectorspace + norm

--- a/src/HOL/Hahn_Banach/Subspace.thy Sun Dec 20 13:11:47 2015 +0100 +++ b/src/HOL/Hahn_Banach/Subspace.thy Sun Dec 20 13:56:02 2015 +0100 @@ -139,8 +139,8 @@ subsection \<open>Linear closure\<close> text \<open> - The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all scalar multiples - of \<open>x\<close>. + The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all scalar multiples of + \<open>x\<close>. \<close> definition lin :: "('a::{minus,plus,zero}) \<Rightarrow> 'a set" @@ -318,7 +318,7 @@ qed qed -text\<open>The sum of two subspaces is a vectorspace.\<close> +text \<open>The sum of two subspaces is a vectorspace.\<close> lemma sum_vs [intro?]: "U \<unlhd> E \<Longrightarrow> V \<unlhd> E \<Longrightarrow> vectorspace E \<Longrightarrow> vectorspace (U + V)" @@ -328,10 +328,10 @@ subsection \<open>Direct sums\<close> text \<open> - The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the zero element is the - only common element of \<open>U\<close> and \<open>V\<close>. For every element \<open>x\<close> of the direct - sum of \<open>U\<close> and \<open>V\<close> the decomposition in \<open>x = u + v\<close> with \<open>u \<in> U\<close> and - \<open>v \<in> V\<close> is unique. + The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the zero element is the only + common element of \<open>U\<close> and \<open>V\<close>. For every element \<open>x\<close> of the direct sum of + \<open>U\<close> and \<open>V\<close> the decomposition in \<open>x = u + v\<close> with \<open>u \<in> U\<close> and \<open>v \<in> V\<close> is + unique. \<close> lemma decomp: @@ -434,8 +434,8 @@ text \<open> Since for any element \<open>y + a \<cdot> x'\<close> of the direct sum of a vectorspace \<open>H\<close> - and the linear closure of \<open>x'\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are unique, - it follows from \<open>y \<in> H\<close> that \<open>a = 0\<close>. + and the linear closure of \<open>x'\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are unique, it + follows from \<open>y \<in> H\<close> that \<open>a = 0\<close>. \<close> lemma decomp_H'_H:

--- a/src/HOL/Hahn_Banach/Vector_Space.thy Sun Dec 20 13:11:47 2015 +0100 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy Sun Dec 20 13:56:02 2015 +0100 @@ -23,13 +23,13 @@ subsection \<open>Vector space laws\<close> text \<open> - A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from @{typ 'a} with - the following vector space laws: The set \<open>V\<close> is closed under addition and - scalar multiplication, addition is associative and commutative; \<open>- x\<close> is - the inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of - addition. Addition and multiplication are distributive; scalar - multiplication is associative and the real number \<open>1\<close> is the neutral - element of scalar multiplication. + A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from @{typ 'a} with the + following vector space laws: The set \<open>V\<close> is closed under addition and scalar + multiplication, addition is associative and commutative; \<open>- x\<close> is the + inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of addition. + Addition and multiplication are distributive; scalar multiplication is + associative and the real number \<open>1\<close> is the neutral element of scalar + multiplication. \<close> locale vectorspace = @@ -78,8 +78,10 @@ lemmas add_ac = add_assoc add_commute add_left_commute -text \<open>The existence of the zero element of a vector space follows from the - non-emptiness of carrier set.\<close> +text \<open> + The existence of the zero element of a vector space follows from the + non-emptiness of carrier set. +\<close> lemma zero [iff]: "0 \<in> V" proof -

--- a/src/HOL/Hahn_Banach/Zorn_Lemma.thy Sun Dec 20 13:11:47 2015 +0100 +++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy Sun Dec 20 13:56:02 2015 +0100 @@ -9,13 +9,13 @@ begin text \<open> - Zorn's Lemmas states: if every linear ordered subset of an ordered - set \<open>S\<close> has an upper bound in \<open>S\<close>, then there exists a - maximal element in \<open>S\<close>. In our application, \<open>S\<close> is a - set of sets ordered by set inclusion. Since the union of a chain of - sets is an upper bound for all elements of the chain, the conditions - of Zorn's lemma can be modified: if \<open>S\<close> is non-empty, it - suffices to show that for every non-empty chain \<open>c\<close> in \<open>S\<close> the union of \<open>c\<close> also lies in \<open>S\<close>. + Zorn's Lemmas states: if every linear ordered subset of an ordered set \<open>S\<close> + has an upper bound in \<open>S\<close>, then there exists a maximal element in \<open>S\<close>. In + our application, \<open>S\<close> is a set of sets ordered by set inclusion. Since the + union of a chain of sets is an upper bound for all elements of the chain, + the conditions of Zorn's lemma can be modified: if \<open>S\<close> is non-empty, it + suffices to show that for every non-empty chain \<open>c\<close> in \<open>S\<close> the union of \<open>c\<close> + also lies in \<open>S\<close>. \<close> theorem Zorn's_Lemma: @@ -28,16 +28,14 @@ fix c assume "c \<in> chains S" show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y" proof cases - - txt \<open>If \<open>c\<close> is an empty chain, then every element in - \<open>S\<close> is an upper bound of \<open>c\<close>.\<close> + txt \<open>If \<open>c\<close> is an empty chain, then every element in \<open>S\<close> is an upper + bound of \<open>c\<close>.\<close> assume "c = {}" with aS show ?thesis by fast - txt \<open>If \<open>c\<close> is non-empty, then \<open>\<Union>c\<close> is an upper - bound of \<open>c\<close>, lying in \<open>S\<close>.\<close> - + txt \<open>If \<open>c\<close> is non-empty, then \<open>\<Union>c\<close> is an upper bound of \<open>c\<close>, lying in + \<open>S\<close>.\<close> next assume "c \<noteq> {}" show ?thesis