--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Mar 25 13:14:33 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Mar 25 14:20:58 2014 +0100
@@ -1319,8 +1319,4 @@
unfolding vec_lambda_beta
by auto
-lemma interval_bij_bij_cart: fixes x::"real^'n" assumes "\<forall>i. a$i < b$i \<and> u$i < v$i"
- shows "interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x"
- using assms by (intro interval_bij_bij) (auto simp: Basis_vec_def inner_axis)
-
end