8695 shows "rel_frontier(S \<inter> T) = frontier S \<inter> T" |
8695 shows "rel_frontier(S \<inter> T) = frontier S \<inter> T" |
8696 using assms |
8696 using assms |
8697 apply (simp add: rel_frontier_def convex_affine_closure_Int frontier_def) |
8697 apply (simp add: rel_frontier_def convex_affine_closure_Int frontier_def) |
8698 by (metis Diff_Int_distrib2 Int_emptyI convex_affine_closure_Int convex_affine_rel_interior_Int empty_iff interior_rel_interior_gen) |
8698 by (metis Diff_Int_distrib2 Int_emptyI convex_affine_closure_Int convex_affine_rel_interior_Int empty_iff interior_rel_interior_gen) |
8699 |
8699 |
|
8700 lemma rel_interior_convex_Int_affine: |
|
8701 fixes S :: "'a::euclidean_space set" |
|
8702 assumes "convex S" "affine T" "interior S \<inter> T \<noteq> {}" |
|
8703 shows "rel_interior(S \<inter> T) = interior S \<inter> T" |
|
8704 proof - |
|
8705 obtain a where aS: "a \<in> interior S" and aT:"a \<in> T" |
|
8706 using assms by force |
|
8707 have "rel_interior S = interior S" |
|
8708 by (metis (no_types) aS affine_hull_nonempty_interior equals0D rel_interior_interior) |
|
8709 then show ?thesis |
|
8710 by (metis (no_types) affine_imp_convex assms convex_rel_interior_inter_two hull_same rel_interior_affine_hull) |
|
8711 qed |
|
8712 |
|
8713 lemma closure_convex_Int_affine: |
|
8714 fixes S :: "'a::euclidean_space set" |
|
8715 assumes "convex S" "affine T" "rel_interior S \<inter> T \<noteq> {}" |
|
8716 shows "closure(S \<inter> T) = closure S \<inter> T" |
|
8717 proof |
|
8718 have "closure (S \<inter> T) \<subseteq> closure T" |
|
8719 by (simp add: closure_mono) |
|
8720 also have "... \<subseteq> T" |
|
8721 by (simp add: affine_closed assms) |
|
8722 finally show "closure(S \<inter> T) \<subseteq> closure S \<inter> T" |
|
8723 by (simp add: closure_mono) |
|
8724 next |
|
8725 obtain a where "a \<in> rel_interior S" "a \<in> T" |
|
8726 using assms by auto |
|
8727 then have ssT: "subspace ((\<lambda>x. (-a)+x) ` T)" and "a \<in> S" |
|
8728 using affine_diffs_subspace rel_interior_subset assms by blast+ |
|
8729 show "closure S \<inter> T \<subseteq> closure (S \<inter> T)" |
|
8730 proof |
|
8731 fix x assume "x \<in> closure S \<inter> T" |
|
8732 show "x \<in> closure (S \<inter> T)" |
|
8733 proof (cases "x = a") |
|
8734 case True |
|
8735 then show ?thesis |
|
8736 using \<open>a \<in> S\<close> \<open>a \<in> T\<close> closure_subset by fastforce |
|
8737 next |
|
8738 case False |
|
8739 then have "x \<in> closure(open_segment a x)" |
|
8740 by auto |
|
8741 then show ?thesis |
|
8742 using \<open>x \<in> closure S \<inter> T\<close> assms convex_affine_closure_Int by blast |
|
8743 qed |
|
8744 qed |
|
8745 qed |
|
8746 |
|
8747 lemma rel_frontier_convex_Int_affine: |
|
8748 fixes S :: "'a::euclidean_space set" |
|
8749 assumes "convex S" "affine T" "interior S \<inter> T \<noteq> {}" |
|
8750 shows "rel_frontier(S \<inter> T) = frontier S \<inter> T" |
|
8751 by (simp add: assms convex_affine_rel_frontier_Int) |
|
8752 |
8700 lemma subset_rel_interior_convex: |
8753 lemma subset_rel_interior_convex: |
8701 fixes S T :: "'n::euclidean_space set" |
8754 fixes S T :: "'n::euclidean_space set" |
8702 assumes "convex S" |
8755 assumes "convex S" |
8703 and "convex T" |
8756 and "convex T" |
8704 and "S \<le> closure T" |
8757 and "S \<le> closure T" |