3138 subsection \<open>Collinearity\<close> |
3138 subsection \<open>Collinearity\<close> |
3139 |
3139 |
3140 definition collinear :: "'a::real_vector set \<Rightarrow> bool" |
3140 definition collinear :: "'a::real_vector set \<Rightarrow> bool" |
3141 where "collinear S \<longleftrightarrow> (\<exists>u. \<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u)" |
3141 where "collinear S \<longleftrightarrow> (\<exists>u. \<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u)" |
3142 |
3142 |
|
3143 lemma collinear_alt: |
|
3144 "collinear S \<longleftrightarrow> (\<exists>u v. \<forall>x \<in> S. \<exists>c. x = u + c *\<^sub>R v)" (is "?lhs = ?rhs") |
|
3145 proof |
|
3146 assume ?lhs |
|
3147 then show ?rhs |
|
3148 unfolding collinear_def by (metis Groups.add_ac(2) diff_add_cancel) |
|
3149 next |
|
3150 assume ?rhs |
|
3151 then obtain u v where *: "\<And>x. x \<in> S \<Longrightarrow> \<exists>c. x = u + c *\<^sub>R v" |
|
3152 by (auto simp: ) |
|
3153 have "\<exists>c. x - y = c *\<^sub>R v" if "x \<in> S" "y \<in> S" for x y |
|
3154 by (metis *[OF \<open>x \<in> S\<close>] *[OF \<open>y \<in> S\<close>] scaleR_left.diff add_diff_cancel_left) |
|
3155 then show ?lhs |
|
3156 using collinear_def by blast |
|
3157 qed |
|
3158 |
|
3159 lemma collinear: |
|
3160 fixes S :: "'a::{perfect_space,real_vector} set" |
|
3161 shows "collinear S \<longleftrightarrow> (\<exists>u. u \<noteq> 0 \<and> (\<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u))" |
|
3162 proof - |
|
3163 have "\<exists>v. v \<noteq> 0 \<and> (\<forall>x\<in>S. \<forall>y\<in>S. \<exists>c. x - y = c *\<^sub>R v)" |
|
3164 if "\<forall>x\<in>S. \<forall>y\<in>S. \<exists>c. x - y = c *\<^sub>R u" "u=0" for u |
|
3165 proof - |
|
3166 have "\<forall>x\<in>S. \<forall>y\<in>S. x = y" |
|
3167 using that by auto |
|
3168 moreover |
|
3169 obtain v::'a where "v \<noteq> 0" |
|
3170 using UNIV_not_singleton [of 0] by auto |
|
3171 ultimately have "\<forall>x\<in>S. \<forall>y\<in>S. \<exists>c. x - y = c *\<^sub>R v" |
|
3172 by auto |
|
3173 then show ?thesis |
|
3174 using \<open>v \<noteq> 0\<close> by blast |
|
3175 qed |
|
3176 then show ?thesis |
|
3177 apply (clarsimp simp: collinear_def) |
|
3178 by (metis real_vector.scale_zero_right vector_fraction_eq_iff) |
|
3179 qed |
|
3180 |
3143 lemma collinear_subset: "\<lbrakk>collinear T; S \<subseteq> T\<rbrakk> \<Longrightarrow> collinear S" |
3181 lemma collinear_subset: "\<lbrakk>collinear T; S \<subseteq> T\<rbrakk> \<Longrightarrow> collinear S" |
3144 by (meson collinear_def subsetCE) |
3182 by (meson collinear_def subsetCE) |
3145 |
3183 |
3146 lemma collinear_empty [iff]: "collinear {}" |
3184 lemma collinear_empty [iff]: "collinear {}" |
3147 by (simp add: collinear_def) |
3185 by (simp add: collinear_def) |