10555 proof (cases "S = {} \<or> T = {}") |
10555 proof (cases "S = {} \<or> T = {}") |
10556 case True with that show ?thesis by auto |
10556 case True with that show ?thesis by auto |
10557 next |
10557 next |
10558 case False |
10558 case False |
10559 define f where "f \<equiv> \<lambda>x. setdist {x} T - setdist {x} S" |
10559 define f where "f \<equiv> \<lambda>x. setdist {x} T - setdist {x} S" |
10560 have contf: "\<And>x. isCont f x" |
10560 have contf: "continuous_on UNIV f" |
10561 unfolding f_def by (intro continuous_intros continuous_at_setdist) |
10561 unfolding f_def by (intro continuous_intros continuous_on_setdist) |
10562 show ?thesis |
10562 show ?thesis |
10563 proof (rule_tac U = "{x. f x > 0}" and V = "{x. f x < 0}" in that) |
10563 proof (rule_tac U = "{x. f x > 0}" and V = "{x. f x < 0}" in that) |
10564 show "{x. 0 < f x} \<inter> {x. f x < 0} = {}" |
10564 show "{x. 0 < f x} \<inter> {x. f x < 0} = {}" |
10565 by auto |
10565 by auto |
10566 show "open {x. 0 < f x}" |
10566 show "open {x. 0 < f x}" |
10567 by (simp add: open_Collect_less contf) |
10567 by (simp add: open_Collect_less contf continuous_on_const) |
10568 show "open {x. f x < 0}" |
10568 show "open {x. f x < 0}" |
10569 by (simp add: open_Collect_less contf) |
10569 by (simp add: open_Collect_less contf continuous_on_const) |
10570 show "S \<subseteq> {x. 0 < f x}" |
10570 show "S \<subseteq> {x. 0 < f x}" |
10571 apply (clarsimp simp add: f_def setdist_sing_in_set) |
10571 apply (clarsimp simp add: f_def setdist_sing_in_set) |
10572 using assms |
10572 using assms |
10573 by (metis False IntI empty_iff le_less setdist_eq_0_sing_2 setdist_pos_le setdist_sym) |
10573 by (metis False IntI empty_iff le_less setdist_eq_0_sing_2 setdist_pos_le setdist_sym) |
10574 show "T \<subseteq> {x. f x < 0}" |
10574 show "T \<subseteq> {x. f x < 0}" |