src/HOL/Multivariate_Analysis/Euclidean_Space.thy

 lemma DIM_complex[simp]: "DIM(complex) = 2"
   by (rule dimension_complex_def)
 
 subsubsection {* Type @{typ "'a \<times> 'b"} *}
 
-lemma disjoint_iff: "A \<inter> B = {} \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)"
-  by auto (* TODO: move elsewhere *)
-
 instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
 begin
 
 definition
   "Basis = (\<lambda>u. (u, 0)) ` Basis \<union> (\<lambda>v. (0, v)) ` Basis"

     unfolding Basis_prod_def ball_Un ball_simps
     by (simp add: inner_prod_def prod_eq_iff euclidean_all_zero_iff)
 next
   show "DIM('a \<times> 'b) = card (Basis :: ('a \<times> 'b) set)"
     unfolding dimension_prod_def Basis_prod_def
-    by (simp add: card_Un_disjoint disjoint_iff
+    by (simp add: card_Un_disjoint disjoint_iff_not_equal
       card_image inj_on_def dimension_def)
 next
   show "basis ` {..<DIM('a \<times> 'b)} = (Basis :: ('a \<times> 'b) set)"
     by (auto simp add: Basis_prod_def dimension_prod_def basis_prod_def
       image_def elim!: Basis_elim)