src/HOL/Analysis/Linear_Algebra.thy
changeset 63881 b746b19197bd
parent 63680 6e1e8b5abbfa
child 63886 685fb01256af
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Sep 15 14:33:55 2016 +0100
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Sep 15 15:48:37 2016 +0100
     1.3 @@ -3125,6 +3125,9 @@
     1.4  definition collinear :: "'a::real_vector set \<Rightarrow> bool"
     1.5    where "collinear S \<longleftrightarrow> (\<exists>u. \<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u)"
     1.6  
     1.7 +lemma collinear_subset: "\<lbrakk>collinear T; S \<subseteq> T\<rbrakk> \<Longrightarrow> collinear S"
     1.8 +  by (meson collinear_def subsetCE)
     1.9 +
    1.10  lemma collinear_empty [iff]: "collinear {}"
    1.11    by (simp add: collinear_def)
    1.12