src/HOL/Multivariate_Analysis/Linear_Algebra.thy

--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu May 28 10:18:46 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu May 28 14:33:35 2015 +0100
@@ -1657,6 +1657,11 @@
   using maximal_independent_subset[of V] independent_bound
   by auto
 
+corollary dim_le_card:
+  fixes s :: "'a::euclidean_space set"
+  shows "finite s \<Longrightarrow> dim s \<le> card s"
+by (metis basis_exists card_mono)
+
 text {* Consequences of independence or spanning for cardinality. *}
 
 lemma independent_card_le_dim: