--- a/src/HOL/Analysis/Path_Connected.thy Tue Apr 16 19:50:30 2019 +0000
+++ b/src/HOL/Analysis/Path_Connected.thy Wed Apr 17 17:48:28 2019 +0100
@@ -2109,6 +2109,14 @@
by (metis Int_absorb1 mem_Collect_eq path_component_of_equiv path_component_of_subset_topspace topspace_subtopology)
qed
+lemma path_connectedin_euclidean [simp]:
+ "path_connectedin euclidean S \<longleftrightarrow> path_connected S"
+ by (auto simp: path_connectedin_def path_connected_space_iff_path_component path_connected_component)
+
+lemma path_connected_space_euclidean_subtopology [simp]:
+ "path_connected_space(subtopology euclidean S) \<longleftrightarrow> path_connected S"
+ using path_connectedin_topspace by force
+
lemma Union_path_components_of:
"\<Union>(path_components_of X) = topspace X"
by (auto simp: path_components_of_def path_component_of_equiv)