# HG changeset patch
# User wenzelm
# Date 1507217976 -7200
# Node ID 97f16ada519c26205f989b3158b695c736191749
# Parent  c1dfa973b26966cb0fd49824c38a04acb5fadb71# Parent  f27488f47a47219b35038d9d87ad6937631d586d
merged

diff -r f27488f47a47 -r 97f16ada519c src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Thu Oct 05 17:37:47 2017 +0200
+++ b/src/HOL/Analysis/Starlike.thy	Thu Oct 05 17:39:36 2017 +0200
@@ -3794,6 +3794,16 @@
     shows "a < x \<Longrightarrow> x < b \<Longrightarrow> (at x within {a..b}) = at x"
   by (metis at_within_interior greaterThanLessThan_iff interior_atLeastAtMost)
 
+lemma at_within_cbox_finite:
+  assumes "x \<in> box a b" "x \<notin> S" "finite S"
+  shows "(at x within cbox a b - S) = at x"
+proof -
+  have "interior (cbox a b - S) = box a b - S"
+    using \<open>finite S\<close> by (simp add: interior_diff finite_imp_closed)
+  then show ?thesis
+    using at_within_interior assms by fastforce
+qed
+
 lemma affine_independent_convex_affine_hull:
   fixes s :: "'a::euclidean_space set"
   assumes "~affine_dependent s" "t \<subseteq> s"