src/HOL/Analysis/Starlike.thy
 changeset 66765 c1dfa973b269 parent 66641 ff2e0115fea4 child 66793 deabce3ccf1f
equal 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 -`