new theorem at_within_cbox_finite
authorpaulson <lp15@cam.ac.uk>
Thu Oct 05 15:35:24 2017 +0100 (20 months ago)
changeset 66765c1dfa973b269
parent 66764 006deaf5c3dc
child 66769 97f16ada519c
new theorem at_within_cbox_finite
src/HOL/Analysis/Starlike.thy
     1.1 --- a/src/HOL/Analysis/Starlike.thy	Wed Oct 04 20:16:53 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Starlike.thy	Thu Oct 05 15:35:24 2017 +0100
     1.3 @@ -3794,6 +3794,16 @@
     1.4      shows "a < x \<Longrightarrow> x < b \<Longrightarrow> (at x within {a..b}) = at x"
     1.5    by (metis at_within_interior greaterThanLessThan_iff interior_atLeastAtMost)
     1.6  
     1.7 +lemma at_within_cbox_finite:
     1.8 +  assumes "x \<in> box a b" "x \<notin> S" "finite S"
     1.9 +  shows "(at x within cbox a b - S) = at x"
    1.10 +proof -
    1.11 +  have "interior (cbox a b - S) = box a b - S"
    1.12 +    using \<open>finite S\<close> by (simp add: interior_diff finite_imp_closed)
    1.13 +  then show ?thesis
    1.14 +    using at_within_interior assms by fastforce
    1.15 +qed
    1.16 +
    1.17  lemma affine_independent_convex_affine_hull:
    1.18    fixes s :: "'a::euclidean_space set"
    1.19    assumes "~affine_dependent s" "t \<subseteq> s"