src/HOL/Multivariate_Analysis/Linear_Algebra.thy

   "\<exists>B. (B :: ('a::euclidean_space) set) \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = dim V)"
   unfolding dim_def some_eq_ex[of "\<lambda>n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = n)"]
   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:
   fixes B :: "'a::euclidean_space set"
   assumes "B \<subseteq> V"