--- a/src/HOL/Hahn_Banach/Function_Norm.thy Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy Mon Oct 19 17:45:36 2015 +0200
@@ -12,7 +12,7 @@
text \<open>
A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"}
- is \emph{continuous}, iff it is bounded, i.e.
+ is \<^emph>\<open>continuous\<close>, iff it is bounded, i.e.
\begin{center}
@{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
\end{center}
@@ -46,7 +46,7 @@
\begin{center}
@{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
\end{center}
- is called the \emph{norm} of @{text f}.
+ is called the \<^emph>\<open>norm\<close> of @{text f}.
For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be
defined as
@@ -194,7 +194,8 @@
qed
text \<open>
- \medskip The fundamental property of function norms is:
+ \<^medskip>
+ The fundamental property of function norms is:
\begin{center}
@{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
\end{center}
@@ -235,7 +236,8 @@
qed
text \<open>
- \medskip The function norm is the least positive real number for
+ \<^medskip>
+ The function norm is the least positive real number for
which the following inequation holds:
\begin{center}
@{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
--- a/src/HOL/Hahn_Banach/Function_Order.thy Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Function_Order.thy Mon Oct 19 17:45:36 2015 +0200
@@ -11,7 +11,7 @@
subsection \<open>The graph of a function\<close>
text \<open>
- We define the \emph{graph} of a (real) function @{text f} with
+ We define the \<^emph>\<open>graph\<close> of a (real) function @{text f} with
domain @{text F} as the set
\begin{center}
@{text "{(x, f x). x \<in> F}"}
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Mon Oct 19 17:45:36 2015 +0200
@@ -15,42 +15,36 @@
subsection \<open>The Hahn-Banach Theorem for vector spaces\<close>
+paragraph \<open>Hahn-Banach Theorem.\<close>
text \<open>
- \textbf{Hahn-Banach Theorem.} Let @{text F} be a subspace of a real
- vector space @{text E}, let @{text p} be a semi-norm on @{text E},
- and @{text f} be a linear form defined on @{text F} such that @{text
- f} is bounded by @{text p}, i.e. @{text "\<forall>x \<in> F. f x \<le> p x"}. Then
- @{text f} can be extended to a linear form @{text h} on @{text E}
- such that @{text h} is norm-preserving, i.e. @{text h} is also
- bounded by @{text p}.
+ Let @{text F} be a subspace of a real vector space @{text E}, let @{text
+ p} be a semi-norm on @{text E}, and @{text f} be a linear form defined on
+ @{text F} such that @{text f} is bounded by @{text p}, i.e. @{text "\<forall>x \<in>
+ F. f x \<le> p x"}. Then @{text f} can be extended to a linear form @{text h}
+ on @{text E} such that @{text h} is norm-preserving, i.e. @{text h} is
+ also bounded by @{text p}.
+\<close>
- \bigskip
- \textbf{Proof Sketch.}
- \begin{enumerate}
-
- \item Define @{text M} as the set of norm-preserving extensions of
+paragraph \<open>Proof Sketch.\<close>
+text \<open>
+ \<^enum> Define @{text M} as the set of norm-preserving extensions of
@{text f} to subspaces of @{text E}. The linear forms in @{text M}
are ordered by domain extension.
- \item We show that every non-empty chain in @{text M} has an upper
+ \<^enum> We show that every non-empty chain in @{text M} has an upper
bound in @{text M}.
- \item With Zorn's Lemma we conclude that there is a maximal function
+ \<^enum> With Zorn's Lemma we conclude that there is a maximal function
@{text g} in @{text M}.
- \item The domain @{text H} of @{text g} is the whole space @{text
+ \<^enum> The domain @{text H} of @{text g} is the whole space @{text
E}, as shown by classical contradiction:
- \begin{itemize}
+ \<^item> Assuming @{text g} is not defined on whole @{text E}, it can
+ still be extended in a norm-preserving way to a super-space @{text
+ H'} of @{text H}.
- \item Assuming @{text g} is not defined on whole @{text E}, it can
- still be extended in a norm-preserving way to a super-space @{text
- H'} of @{text H}.
-
- \item Thus @{text g} can not be maximal. Contradiction!
-
- \end{itemize}
- \end{enumerate}
+ \<^item> Thus @{text g} can not be maximal. Contradiction!
\<close>
theorem Hahn_Banach:
@@ -60,7 +54,7 @@
shows "\<exists>h. linearform E h \<and> (\<forall>x \<in> F. h x = f x) \<and> (\<forall>x \<in> E. h x \<le> p x)"
-- \<open>Let @{text E} be a vector space, @{text F} a subspace of @{text E}, @{text p} a seminorm on @{text E},\<close>
-- \<open>and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p},\<close>
- -- \<open>then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \skp\<close>
+ -- \<open>then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \<^smallskip>\<close>
proof -
interpret vectorspace E by fact
interpret subspace F E by fact
@@ -104,7 +98,7 @@
qed
}
then have "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> x = g"
- -- \<open>With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \skp\<close>
+ -- \<open>With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \<^smallskip>\<close>
proof (rule Zorn's_Lemma)
-- \<open>We show that @{text M} is non-empty:\<close>
show "graph F f \<in> M"
@@ -127,16 +121,16 @@
and hp: "\<forall>x \<in> H. h x \<le> p x" unfolding M_def ..
-- \<open>@{text g} is a norm-preserving extension of @{text f}, in other words:\<close>
-- \<open>@{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E},\<close>
- -- \<open>and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp\<close>
+ -- \<open>and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \<^smallskip>\<close>
from HE E have H: "vectorspace H"
by (rule subspace.vectorspace)
have HE_eq: "H = E"
- -- \<open>We show that @{text h} is defined on whole @{text E} by classical contradiction. \skp\<close>
+ -- \<open>We show that @{text h} is defined on whole @{text E} by classical contradiction. \<^smallskip>\<close>
proof (rule classical)
assume neq: "H \<noteq> E"
-- \<open>Assume @{text h} is not defined on whole @{text E}. Then show that @{text h} can be extended\<close>
- -- \<open>in a norm-preserving way to a function @{text h'} with the graph @{text g'}. \skp\<close>
+ -- \<open>in a norm-preserving way to a function @{text h'} with the graph @{text g'}. \<^smallskip>\<close>
have "\<exists>g' \<in> M. g \<subseteq> g' \<and> g \<noteq> g'"
proof -
from HE have "H \<subseteq> E" ..
@@ -152,7 +146,7 @@
qed
def H' \<equiv> "H + lin x'"
- -- \<open>Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \skp\<close>
+ -- \<open>Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \<^smallskip>\<close>
have HH': "H \<unlhd> H'"
proof (unfold H'_def)
from x'E have "vectorspace (lin x')" ..
@@ -164,7 +158,7 @@
\<and> xi \<le> p (y + x') - h y"
-- \<open>Pick a real number @{text \<xi>} that fulfills certain inequations; this will\<close>
-- \<open>be used to establish that @{text h'} is a norm-preserving extension of @{text h}.
- \label{ex-xi-use}\skp\<close>
+ \label{ex-xi-use}\<^smallskip>\<close>
proof -
from H have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y \<le> xi
\<and> xi \<le> p (y + x') - h y"
@@ -191,10 +185,10 @@
def h' \<equiv> "\<lambda>x. let (y, a) =
SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H in h y + a * xi"
- -- \<open>Define the extension @{text h'} of @{text h} to @{text H'} using @{text \<xi>}. \skp\<close>
+ -- \<open>Define the extension @{text h'} of @{text h} to @{text H'} using @{text \<xi>}. \<^smallskip>\<close>
have "g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'"
- -- \<open>@{text h'} is an extension of @{text h} \dots \skp\<close>
+ -- \<open>@{text h'} is an extension of @{text h} \dots \<^smallskip>\<close>
proof
show "g \<subseteq> graph H' h'"
proof -
@@ -231,7 +225,7 @@
qed
qed
moreover have "graph H' h' \<in> M"
- -- \<open>and @{text h'} is norm-preserving. \skp\<close>
+ -- \<open>and @{text h'} is norm-preserving. \<^smallskip>\<close>
proof (unfold M_def)
show "graph H' h' \<in> norm_pres_extensions E p F f"
proof (rule norm_pres_extensionI2)
@@ -279,7 +273,7 @@
ultimately show ?thesis ..
qed
then have "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp
- -- \<open>So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \skp\<close>
+ -- \<open>So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \<^smallskip>\<close>
with gx show "H = E" by contradiction
qed
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Mon Oct 19 17:45:36 2015 +0200
@@ -24,7 +24,8 @@
Subsequently we show some properties of this extension @{text h'} of
@{text h}.
- \medskip This lemma will be used to show the existence of a linear
+ \<^medskip>
+ This lemma will be used to show the existence of a linear
extension of @{text f} (see page \pageref{ex-xi-use}). It is a
consequence of the completeness of @{text \<real>}. To show
\begin{center}
@@ -84,7 +85,8 @@
qed
text \<open>
- \medskip The function @{text h'} is defined as a @{text "h' x = h y
+ \<^medskip>
+ The function @{text h'} is defined as a @{text "h' x = h y
+ a \<cdot> \<xi>"} where @{text "x = y + a \<cdot> \<xi>"} is a linear extension of
@{text h} to @{text H'}.
\<close>
@@ -190,7 +192,9 @@
qed
qed
-text \<open>\medskip The linear extension @{text h'} of @{text h}
+text \<open>
+ \<^medskip>
+ The linear extension @{text h'} of @{text h}
is bounded by the seminorm @{text p}.\<close>
lemma h'_norm_pres:
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Mon Oct 19 17:45:36 2015 +0200
@@ -18,11 +18,13 @@
graph H h"}. We will show some properties about the limit function
@{text h}, i.e.\ the supremum of the chain @{text c}.
- \medskip Let @{text c} be a chain of norm-preserving extensions of
+ \<^medskip>
+ Let @{text c} be a chain of norm-preserving extensions of
the function @{text f} and let @{text "graph H h"} be the supremum
of @{text c}. Every element in @{text H} is member of one of the
elements of the chain.
\<close>
+
lemmas [dest?] = chainsD
lemmas chainsE2 [elim?] = chainsD2 [elim_format]
@@ -54,7 +56,8 @@
qed
text \<open>
- \medskip Let @{text c} be a chain of norm-preserving extensions of
+ \<^medskip>
+ Let @{text c} be a chain of norm-preserving extensions of
the function @{text f} and let @{text "graph H h"} be the supremum
of @{text c}. Every element in the domain @{text H} of the supremum
function is member of the domain @{text H'} of some function @{text
@@ -82,7 +85,8 @@
qed
text \<open>
- \medskip Any two elements @{text x} and @{text y} in the domain
+ \<^medskip>
+ Any two elements @{text x} and @{text y} in the domain
@{text H} of the supremum function @{text h} are both in the domain
@{text H'} of some function @{text h'}, such that @{text h} extends
@{text h'}.
@@ -154,7 +158,8 @@
qed
text \<open>
- \medskip The relation induced by the graph of the supremum of a
+ \<^medskip>
+ The relation induced by the graph of the supremum of a
chain @{text c} is definite, i.~e.~t is the graph of a function.
\<close>
@@ -204,7 +209,8 @@
qed
text \<open>
- \medskip The limit function @{text h} is linear. Every element
+ \<^medskip>
+ The limit function @{text h} is linear. Every element
@{text x} in the domain of @{text h} is in the domain of a function
@{text h'} in the chain of norm preserving extensions. Furthermore,
@{text h} is an extension of @{text h'} so the function values of
@@ -259,7 +265,8 @@
qed
text \<open>
- \medskip The limit of a non-empty chain of norm preserving
+ \<^medskip>
+ The limit of a non-empty chain of norm preserving
extensions of @{text f} is an extension of @{text f}, since every
element of the chain is an extension of @{text f} and the supremum
is an extension for every element of the chain.
@@ -285,7 +292,8 @@
qed
text \<open>
- \medskip The domain @{text H} of the limit function is a superspace
+ \<^medskip>
+ The domain @{text H} of the limit function is a superspace
of @{text F}, since @{text F} is a subset of @{text H}. The
existence of the @{text 0} element in @{text F} and the closure
properties follow from the fact that @{text F} is a vector space.
@@ -310,7 +318,8 @@
qed
text \<open>
- \medskip The domain @{text H} of the limit function is a subspace of
+ \<^medskip>
+ The domain @{text H} of the limit function is a subspace of
@{text E}.
\<close>
@@ -366,7 +375,8 @@
qed
text \<open>
- \medskip The limit function is bounded by the norm @{text p} as
+ \<^medskip>
+ The limit function is bounded by the norm @{text p} as
well, since all elements in the chain are bounded by @{text p}.
\<close>
@@ -387,7 +397,8 @@
qed
text \<open>
- \medskip The following lemma is a property of linear forms on real
+ \<^medskip>
+ The following lemma is a property of linear forms on real
vector spaces. It will be used for the lemma @{text abs_Hahn_Banach}
(see page \pageref{abs-Hahn_Banach}). \label{abs-ineq-iff} For real
vector spaces the following inequations are equivalent:
--- a/src/HOL/Hahn_Banach/Linearform.thy Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Linearform.thy Mon Oct 19 17:45:36 2015 +0200
@@ -9,7 +9,7 @@
begin
text \<open>
- A \emph{linear form} is a function on a vector space into the reals
+ A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals
that is additive and multiplicative.
\<close>
--- a/src/HOL/Hahn_Banach/Normed_Space.thy Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy Mon Oct 19 17:45:36 2015 +0200
@@ -11,7 +11,7 @@
subsection \<open>Quasinorms\<close>
text \<open>
- A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space
+ A \<^emph>\<open>seminorm\<close> @{text "\<parallel>\<cdot>\<parallel>"} 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>
@@ -57,7 +57,7 @@
subsection \<open>Norms\<close>
text \<open>
- A \emph{norm} @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the
+ A \<^emph>\<open>norm\<close> @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the
@{text 0} vector to @{text 0}.
\<close>
@@ -68,8 +68,8 @@
subsection \<open>Normed vector spaces\<close>
text \<open>
- A vector space together with a norm is called a \emph{normed
- space}.
+ 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 Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Subspace.thy Mon Oct 19 17:45:36 2015 +0200
@@ -12,7 +12,7 @@
text \<open>
A non-empty subset @{text U} of a vector space @{text V} is a
- \emph{subspace} of @{text V}, iff @{text U} is closed under addition
+ \<^emph>\<open>subspace\<close> of @{text V}, iff @{text U} is closed under addition
and scalar multiplication.
\<close>
@@ -50,7 +50,8 @@
qed
text \<open>
- \medskip Similar as for linear spaces, the existence of the zero
+ \<^medskip>
+ Similar as for linear spaces, the existence of the zero
element in every subspace follows from the non-emptiness of the
carrier set and by vector space laws.
\<close>
@@ -76,7 +77,7 @@
from x show ?thesis by (simp add: negate_eq1)
qed
-text \<open>\medskip Further derived laws: every subspace is a vector space.\<close>
+text \<open>\<^medskip> Further derived laws: every subspace is a vector space.\<close>
lemma (in subspace) vectorspace [iff]:
assumes "vectorspace V"
@@ -139,7 +140,7 @@
subsection \<open>Linear closure\<close>
text \<open>
- The \emph{linear closure} of a vector @{text x} is the set of all
+ The \<^emph>\<open>linear closure\<close> of a vector @{text x} is the set of all
scalar multiples of @{text x}.
\<close>
@@ -226,7 +227,7 @@
subsection \<open>Sum of two vectorspaces\<close>
text \<open>
- The \emph{sum} of two vectorspaces @{text U} and @{text V} is the
+ The \<^emph>\<open>sum\<close> of two vectorspaces @{text U} and @{text V} is the
set of all sums of elements from @{text U} and @{text V}.
\<close>
@@ -328,7 +329,7 @@
subsection \<open>Direct sums\<close>
text \<open>
- The sum of @{text U} and @{text V} is called \emph{direct}, iff the
+ The sum of @{text U} and @{text V} is called \<^emph>\<open>direct\<close>, iff the
zero element is the only common element of @{text U} and @{text
V}. For every element @{text x} of the direct sum of @{text U} and
@{text V} the decomposition in @{text "x = u + v"} with
--- a/src/HOL/Hahn_Banach/Vector_Space.thy Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy Mon Oct 19 17:45:36 2015 +0200
@@ -23,7 +23,7 @@
subsection \<open>Vector space laws\<close>
text \<open>
- A \emph{vector space} is a non-empty set @{text V} of elements from
+ A \<^emph>\<open>vector space\<close> is a non-empty set @{text V} of elements from
@{typ 'a} with the following vector space laws: The set @{text V} is
closed under addition and scalar multiplication, addition is
associative and commutative; @{text "- x"} is the inverse of @{text
@@ -122,7 +122,7 @@
diff_mult_distrib1 diff_mult_distrib2
-text \<open>\medskip Further derived laws:\<close>
+text \<open>\<^medskip> Further derived laws:\<close>
lemma mult_zero_left [simp]: "x \<in> V \<Longrightarrow> 0 \<cdot> x = 0"
proof -
--- a/src/HOL/Hahn_Banach/document/root.tex Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/document/root.tex Mon Oct 19 17:45:36 2015 +0200
@@ -8,7 +8,6 @@
\urlstyle{rm}
\newcommand{\isasymsup}{\isamath{\sup\,}}
-\newcommand{\skp}{\smallskip}
\begin{document}