--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Oct 01 23:26:31 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Oct 02 15:07:41 2015 +0100
@@ -1908,9 +1908,6 @@
text \<open>Picking an orthogonal replacement for a spanning set.\<close>
-(* FIXME : Move to some general theory ?*)
-definition "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y\<in> S. x\<noteq>y \<longrightarrow> R x y)"
-
lemma vector_sub_project_orthogonal:
fixes b x :: "'a::euclidean_space"
shows "b \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *\<^sub>R b) = 0"