src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
 changeset 63040 eb4ddd18d635 parent 61879 e4f9d8f094fe
```     1.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sun Apr 24 21:31:14 2016 +0200
1.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Mon Apr 25 16:09:26 2016 +0200
1.3 @@ -86,9 +86,9 @@
1.4  \<close>
1.5
1.6  lemma h'_lf:
1.7 -  assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
1.8 -      SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
1.9 -    and H'_def: "H' \<equiv> H + lin x0"
1.10 +  assumes h'_def: "\<And>x. h' x = (let (y, a) =
1.11 +      SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi)"
1.12 +    and H'_def: "H' = H + lin x0"
1.13      and HE: "H \<unlhd> E"
1.14    assumes "linearform H h"
1.15    assumes x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
1.16 @@ -192,9 +192,9 @@
1.17  \<close>
1.18
1.19  lemma h'_norm_pres:
1.20 -  assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
1.21 -      SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
1.22 -    and H'_def: "H' \<equiv> H + lin x0"
1.23 +  assumes h'_def: "\<And>x. h' x = (let (y, a) =
1.24 +      SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi)"
1.25 +    and H'_def: "H' = H + lin x0"
1.26      and x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
1.27    assumes E: "vectorspace E" and HE: "subspace H E"
1.28      and "seminorm E p" and "linearform H h"
```