src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
changeset 44142 8e27e0177518
parent 44132 0f35a870ecf1
child 44170 510ac30f44c0
     1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Aug 10 17:02:03 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Aug 10 18:02:16 2011 -0700
     1.3 @@ -198,9 +198,6 @@
     1.4    from this show ?thesis by auto
     1.5  qed
     1.6  
     1.7 -lemma basis_0[simp]:"(basis i::'a::euclidean_space) = 0 \<longleftrightarrow> i\<ge>DIM('a)"
     1.8 -  using norm_basis[of i, where 'a='a] unfolding norm_eq_zero[where 'a='a,THEN sym] by auto
     1.9 -
    1.10  lemma basis_to_basis_subspace_isomorphism:
    1.11    assumes s: "subspace (S:: ('n::euclidean_space) set)"
    1.12    and t: "subspace (T :: ('m::euclidean_space) set)"
    1.13 @@ -2142,7 +2139,7 @@
    1.14    apply (simp add: rel_interior, safe)
    1.15    apply (force simp add: open_contains_ball)
    1.16    apply (rule_tac x="ball x e" in exI)
    1.17 -  apply (simp add: open_ball centre_in_ball)
    1.18 +  apply (simp add: centre_in_ball)
    1.19    done
    1.20  
    1.21  lemma rel_interior_ball: