Theory Convex_Euclidean_Space_More

section‹Convexity›

theory Convex_Euclidean_Space_More
  imports "HOL-Analysis.Starlike"
begin

lemma connected_Int_rel_frontier:
  assumes "connected S"
      and "S ⊆ affine hull T"
      and "S ∩ T ≠ {}"
      and "S - T ≠ {}"
    shows "S ∩ rel_frontier T ≠ {}"
proof
  assume *: "S ∩ rel_frontier T = {}"
  let ?E1 = "S ∩ rel_interior T"
  let ?E2 = "S - closure T"
  have "openin (top_of_set S) ?E1"
    by (meson assms(2) openin_Int openin_rel_interior
        openin_subtopology_Int_subset openin_subtopology_self)
  moreover have "openin (top_of_set S) ?E2"
    by (meson closed_closedin closed_closure closedin_self
        closedin_subtopology_refl openin_subtopology_diff_closed)
  moreover have "S ⊆ ?E1 ∪ ?E2"
    using "*" rel_frontier_def by fastforce
  moreover have "?E1 ∩ ?E2 = {}"
    using rel_interior_subset_closure by fastforce
  moreover have "?E1 ≠ {}"
    using assms(3) calculation(3) closure_subset by fastforce
  moreover have "?E2 ≠ {}"
    using assms(4) calculation(3) rel_interior_subset by fastforce
  ultimately show "False"
    using connected_openin[of S] assms(1) by blast
qed

end