src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
changeset 27611 2c01c0bdb385
parent 23378 1d138d6bb461
child 27612 d3eb431db035
     1.1 --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Tue Jul 15 16:02:10 2008 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Tue Jul 15 16:50:09 2008 +0200
     1.3 @@ -399,9 +399,14 @@
     1.4  *}
     1.5  
     1.6  lemma abs_ineq_iff:
     1.7 -  includes subspace H E + vectorspace E + seminorm E p + linearform H h
     1.8 +  assumes "subspace H E" and "vectorspace E" and "seminorm E p"
     1.9 +    and "linearform H h"
    1.10    shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R")
    1.11  proof
    1.12 +  interpret subspace [H E] by fact
    1.13 +  interpret vectorspace [E] by fact
    1.14 +  interpret seminorm [E p] by fact
    1.15 +  interpret linearform [H h] by fact
    1.16    have H: "vectorspace H" using `vectorspace E` ..
    1.17    {
    1.18      assume l: ?L