--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Nov 05 09:07:14 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Nov 05 14:17:18 2010 +0100
@@ -1065,10 +1065,16 @@
text {* Individual closure properties. *}
+lemma span_span: "span (span A) = span A"
+ unfolding span_def hull_hull ..
+
lemma (in real_vector) span_superset: "x \<in> S ==> x \<in> span S" by (metis span_clauses(1))
lemma (in real_vector) span_0: "0 \<in> span S" by (metis subspace_span subspace_0)
+lemma span_inc: "S \<subseteq> span S"
+ by (metis subset_eq span_superset)
+
lemma (in real_vector) dependent_0: assumes "0\<in>A" shows "dependent A"
unfolding dependent_def apply(rule_tac x=0 in bexI)
using assms span_0 by auto
@@ -1485,12 +1491,6 @@
lemma mem_delete: "x \<in> (A - {a}) \<longleftrightarrow> x \<noteq> a \<and> x \<in> A"
by blast
-lemma span_span: "span (span A) = span A"
- unfolding span_def hull_hull ..
-
-lemma span_inc: "S \<subseteq> span S"
- by (metis subset_eq span_superset)
-
lemma spanning_subset_independent:
assumes BA: "B \<subseteq> A" and iA: "independent A"
and AsB: "A \<subseteq> span B"