--- 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