src/HOL/Analysis/Linear_Algebra.thy
changeset 63938 f6ce08859d4c
parent 63918 6bf55e6e0b75
child 64122 74fde524799e
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Wed Sep 21 16:59:51 2016 +0100
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Sep 22 15:44:47 2016 +0100
     1.3 @@ -457,7 +457,7 @@
     1.4  lemma span_neg: "x \<in> span S \<Longrightarrow> - x \<in> span S"
     1.5    by (metis subspace_neg subspace_span)
     1.6  
     1.7 -lemma span_sub: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
     1.8 +lemma span_diff: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
     1.9    by (metis subspace_span subspace_diff)
    1.10  
    1.11  lemma (in real_vector) span_setsum: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> span S) \<Longrightarrow> setsum f A \<in> span S"
    1.12 @@ -2615,7 +2615,7 @@
    1.13      from gxy have th0: "g (x - y) = 0"
    1.14        by (simp add: linear_diff[OF g(1)])
    1.15      have th1: "x - y \<in> span B"
    1.16 -      using x' y' by (metis span_sub)
    1.17 +      using x' y' by (metis span_diff)
    1.18      have "x = y"
    1.19        using g0[OF th1 th0] by simp
    1.20    }