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)