equal
deleted
inserted
replaced
5443 shows "rel_interior S <= rel_interior T" |
5443 shows "rel_interior S <= rel_interior T" |
5444 proof- |
5444 proof- |
5445 have *: "S Int closure T = S" using assms by auto |
5445 have *: "S Int closure T = S" using assms by auto |
5446 have "~(rel_interior S <= rel_frontier T)" |
5446 have "~(rel_interior S <= rel_frontier T)" |
5447 using closure_mono[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T] |
5447 using closure_mono[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T] |
5448 closure_closed convex_closure_rel_interior[of S] closure_subset[of S] assms by auto |
5448 closure_closed[of S] convex_closure_rel_interior[of S] closure_subset[of S] assms by auto |
5449 hence "(rel_interior S) Int (rel_interior (closure T)) ~= {}" |
5449 hence "(rel_interior S) Int (rel_interior (closure T)) ~= {}" |
5450 using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T] by auto |
5450 using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T] by auto |
5451 hence "rel_interior S Int rel_interior T = rel_interior (S Int closure T)" using assms convex_closure |
5451 hence "rel_interior S Int rel_interior T = rel_interior (S Int closure T)" using assms convex_closure |
5452 convex_rel_interior_inter_two[of S "closure T"] convex_rel_interior_closure[of T] by auto |
5452 convex_rel_interior_inter_two[of S "closure T"] convex_rel_interior_closure[of T] by auto |
5453 also have "...=rel_interior (S)" using * by auto |
5453 also have "...=rel_interior (S)" using * by auto |