src/HOL/Real/HahnBanach/Subspace.thy
 changeset 7927 b50446a33c16 parent 7917 5e5b9813cce7 child 7978 1b99ee57d131
     1.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Mon Oct 25 19:24:31 1999 +0200
1.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Mon Oct 25 19:24:43 1999 +0200
1.3 @@ -213,9 +213,8 @@
1.4  instance set :: (plus) plus; by intro_classes;
1.5
1.6  defs vs_sum_def:
1.7 -  "U + V == {x. EX u:U. EX v:V. x = u + v}";
1.8 +  "U + V == {x. EX u:U. EX v:V. x = u + v}";(***
1.9
1.10 -(***
1.11  constdefs
1.12    vs_sum ::
1.13    "['a::{minus, plus} set, 'a set] => 'a set"         (infixl "+" 65)
1.14 @@ -318,7 +317,7 @@
1.15  text {* The sum of $U$ and $V$ is called \emph{direct}, iff the zero
1.16  element is the only common element of $U$ and $V$. For every element
1.17  $x$ of the direct sum of $U$ and $V$ the decomposition in
1.18 -$x = u + v$ with $u:U$ and $v:V$ is unique.*};
1.19 +$x = u + v$ with $u \in U$ and $v \in V$ is unique.*};
1.20
1.21  lemma decomp:
1.22    "[| is_vectorspace E; is_subspace U E; is_subspace V E;
1.23 @@ -352,7 +351,7 @@
1.24  text {* An application of the previous lemma will be used in the
1.25  proof of the Hahn-Banach theorem: for an element $y + a \mult x_0$
1.26  of the direct sum of a vectorspace $H$ and the linear closure of
1.27 -$x_0$ the components $y:H$ and $a$ are unique. *};
1.28 +$x_0$ the components $y \in H$ and $a$ are unique. *};
1.29
1.30  lemma decomp_H0:
1.31    "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H;
1.32 @@ -426,7 +425,7 @@
1.33
1.34  text {* The components $y\in H$ and $a$ in $y \plus a \mult x_0$
1.35  are unique, so the function $h_0$ defined by
1.36 -$h_0 (y \plus a \mult x_0) = h y + a * xi$ is definite. *};
1.37 +$h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *};
1.38
1.39  lemma h0_definite:
1.40    "[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)