# HG changeset patch # User paulson # Date 1507214124 -3600 # Node ID c1dfa973b26966cb0fd49824c38a04acb5fadb71 # Parent 006deaf5c3dcd9a623eb8434e691099a47fe24ec new theorem at_within_cbox_finite diff -r 006deaf5c3dc -r c1dfa973b269 src/HOL/Analysis/Starlike.thy --- a/src/HOL/Analysis/Starlike.thy Wed Oct 04 20:16:53 2017 +0200 +++ b/src/HOL/Analysis/Starlike.thy Thu Oct 05 15:35:24 2017 +0100 @@ -3794,6 +3794,16 @@ shows "a < x \ x < b \ (at x within {a..b}) = at x" by (metis at_within_interior greaterThanLessThan_iff interior_atLeastAtMost) +lemma at_within_cbox_finite: + assumes "x \ box a b" "x \ 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 \finite S\ 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 \ s"