tuned
authorhaftmann
Thu Mar 05 08:23:10 2009 +0100 (2009-03-05)
changeset 303039c4f4ac0d038
parent 30302 5ffa9d4dbea7
child 30304 d8e4cd2ac2a1
tuned
src/HOL/Library/Euclidean_Space.thy
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Thu Mar 05 08:23:09 2009 +0100
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Thu Mar 05 08:23:10 2009 +0100
     1.3 @@ -4396,7 +4396,7 @@
     1.4    assumes iB: "independent (B:: (real ^'n) set)"
     1.5    shows "\<exists>g. linear g \<and> (\<forall>x\<in>B. g x = f x)"
     1.6  proof-
     1.7 -  from maximal_independent_subset_extend[of B "UNIV"] iB
     1.8 +  from maximal_independent_subset_extend[of B UNIV] iB
     1.9    obtain C where C: "B \<subseteq> C" "independent C" "\<And>x. x \<in> span C" by auto
    1.10    
    1.11    from C(2) independent_bound[of C] linear_independent_extend_lemma[of C f]