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    }
```