src/HOL/Analysis/Starlike.thy
changeset 66765 c1dfa973b269
parent 66641 ff2e0115fea4
child 66793 deabce3ccf1f
equal deleted inserted replaced
66764:006deaf5c3dc 66765:c1dfa973b269
  3792 lemma at_within_closed_interval:
  3792 lemma at_within_closed_interval:
  3793     fixes x::real
  3793     fixes x::real
  3794     shows "a < x \<Longrightarrow> x < b \<Longrightarrow> (at x within {a..b}) = at x"
  3794     shows "a < x \<Longrightarrow> x < b \<Longrightarrow> (at x within {a..b}) = at x"
  3795   by (metis at_within_interior greaterThanLessThan_iff interior_atLeastAtMost)
  3795   by (metis at_within_interior greaterThanLessThan_iff interior_atLeastAtMost)
  3796 
  3796 
       
  3797 lemma at_within_cbox_finite:
       
  3798   assumes "x \<in> box a b" "x \<notin> S" "finite S"
       
  3799   shows "(at x within cbox a b - S) = at x"
       
  3800 proof -
       
  3801   have "interior (cbox a b - S) = box a b - S"
       
  3802     using \<open>finite S\<close> by (simp add: interior_diff finite_imp_closed)
       
  3803   then show ?thesis
       
  3804     using at_within_interior assms by fastforce
       
  3805 qed
       
  3806 
  3797 lemma affine_independent_convex_affine_hull:
  3807 lemma affine_independent_convex_affine_hull:
  3798   fixes s :: "'a::euclidean_space set"
  3808   fixes s :: "'a::euclidean_space set"
  3799   assumes "~affine_dependent s" "t \<subseteq> s"
  3809   assumes "~affine_dependent s" "t \<subseteq> s"
  3800     shows "convex hull t = affine hull t \<inter> convex hull s"
  3810     shows "convex hull t = affine hull t \<inter> convex hull s"
  3801 proof -
  3811 proof -