# HG changeset patch # User huffman # Date 1314214782 25200 # Node ID fcaacc214a3644e872e9975564389753f923f789 # Parent d02b01e5ab8ffc281258fa6870408724ed2665f6 remove unused lemmas dimensionI, dimension_eq diff -r d02b01e5ab8f -r fcaacc214a36 src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Aug 24 11:56:57 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Aug 24 12:39:42 2011 -0700 @@ -1436,30 +1436,6 @@ apply (simp add: inner_setsum_right dot_basis) done -lemma dimensionI: - assumes "\d. \ 0 < d; basis ` {d..} = {0::'a::euclidean_space}; - independent (basis ` {.. 'a) {.. \ P d" - shows "P DIM('a::euclidean_space)" - using DIM_positive basis_finite independent_basis basis_inj - by (rule assms) - -lemma (in euclidean_space) dimension_eq: - assumes "\i. i < d \ basis i \ 0" - assumes "\i. d \ i \ basis i = 0" - shows "DIM('a) = d" -proof (rule linorder_cases [of "DIM('a)" d]) - assume "DIM('a) < d" - hence "basis DIM('a) \ 0" by (rule assms) - thus ?thesis by simp -next - assume "d < DIM('a)" - hence "basis d \ 0" by simp - thus ?thesis by (simp add: assms) -next - assume "DIM('a) = d" thus ?thesis . -qed - lemma (in euclidean_space) range_basis: "range basis = insert 0 (basis ` {..