--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri Sep 13 00:55:44 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Thu Sep 12 09:03:52 2013 -0700
@@ -587,7 +587,7 @@
qed
lemma open_path_component:
- fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
+ fixes s :: "'a::real_normed_vector set"
assumes "open s"
shows "open {y. path_component s x y}"
unfolding open_contains_ball
@@ -620,7 +620,7 @@
qed
lemma open_non_path_component:
- fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
+ fixes s :: "'a::real_normed_vector set"
assumes "open s"
shows "open(s - {y. path_component s x y})"
unfolding open_contains_ball
@@ -648,7 +648,7 @@
qed
lemma connected_open_path_connected:
- fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
+ fixes s :: "'a::real_normed_vector set"
assumes "open s" "connected s"
shows "path_connected s"
unfolding path_connected_component_set