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"