src/HOL/Real/HahnBanach/Subspace.thy
changeset 8169 77b3bc101de5
parent 7978 1b99ee57d131
child 8203 2fcc6017cb72
equal deleted inserted replaced
8168:9d2ac5439089 8169:77b3bc101de5
   389             thus ?thesis; by contradiction;
   389             thus ?thesis; by contradiction;
   390           qed;
   390           qed;
   391        qed;
   391        qed;
   392       qed;
   392       qed;
   393       show "{<0>} <= H Int lin x0";
   393       show "{<0>} <= H Int lin x0";
   394       proof (intro subsetI, elim singletonE, intro IntI, 
   394       proof -;
   395         (simp only:)+);
   395 	have "<0>: H Int lin x0";
   396         show "<0>:H"; ..;
   396 	proof (rule IntI);
   397         from lin_vs; show "<0> : lin x0"; ..;
   397 	  show "<0>:H"; ..;
       
   398 	  from lin_vs; show "<0> : lin x0"; ..;
       
   399 	qed;
       
   400 	thus ?thesis; by simp;
   398       qed;
   401       qed;
   399     qed;
   402     qed;
   400     show "is_subspace (lin x0) E"; ..;
   403     show "is_subspace (lin x0) E"; ..;
   401   qed;
   404   qed;
   402   
   405