generalize lemmas
authorhuffman
Wed Mar 05 13:59:25 2014 -0800 (2014-03-05)
changeset 5592730c41a8eca0e
parent 55926 3ef14caf5637
child 55928 2d7582309d73
generalize lemmas
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 05 21:51:30 2014 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 05 13:59:25 2014 -0800
     1.3 @@ -6377,7 +6377,6 @@
     1.4  text{* "Isometry" (up to constant bounds) of injective linear map etc.           *}
     1.5  
     1.6  lemma cauchy_isometric:
     1.7 -  fixes x :: "nat \<Rightarrow> 'a::euclidean_space"
     1.8    assumes e: "e > 0"
     1.9      and s: "subspace s"
    1.10      and f: "bounded_linear f"
    1.11 @@ -6412,7 +6411,6 @@
    1.12  qed
    1.13  
    1.14  lemma complete_isometric_image:
    1.15 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
    1.16    assumes "0 < e"
    1.17      and s: "subspace s"
    1.18      and f: "bounded_linear f"