equal
deleted
inserted
replaced
10 |
10 |
11 lemma path_connected_interval [simp]: |
11 lemma path_connected_interval [simp]: |
12 fixes a b::"'a::ordered_euclidean_space" |
12 fixes a b::"'a::ordered_euclidean_space" |
13 shows "path_connected {a..b}" |
13 shows "path_connected {a..b}" |
14 using is_interval_cc is_interval_path_connected by blast |
14 using is_interval_cc is_interval_path_connected by blast |
|
15 |
|
16 lemma segment_to_closest_point: |
|
17 fixes S :: "'a :: euclidean_space set" |
|
18 shows "\<lbrakk>closed S; S \<noteq> {}\<rbrakk> \<Longrightarrow> open_segment a (closest_point S a) \<inter> S = {}" |
|
19 apply (subst disjoint_iff_not_equal) |
|
20 apply (clarify dest!: dist_in_open_segment) |
|
21 by (metis closest_point_le dist_commute le_less_trans less_irrefl) |
|
22 |
|
23 lemma segment_to_point_exists: |
|
24 fixes S :: "'a :: euclidean_space set" |
|
25 assumes "closed S" "S \<noteq> {}" |
|
26 obtains b where "b \<in> S" "open_segment a b \<inter> S = {}" |
|
27 by (metis assms segment_to_closest_point closest_point_exists that) |
|
28 |
15 |
29 |
16 subsection \<open>The Brouwer reduction theorem\<close> |
30 subsection \<open>The Brouwer reduction theorem\<close> |
17 |
31 |
18 theorem Brouwer_reduction_theorem_gen: |
32 theorem Brouwer_reduction_theorem_gen: |
19 fixes S :: "'a::euclidean_space set" |
33 fixes S :: "'a::euclidean_space set" |