--- a/src/HOL/Analysis/Smooth_Paths.thy Mon Dec 02 14:22:03 2019 +0100
+++ b/src/HOL/Analysis/Smooth_Paths.thy Mon Dec 02 14:22:28 2019 +0100
@@ -9,36 +9,6 @@
subsection\<^marker>\<open>tag unimportant\<close> \<open>Homeomorphisms of arc images\<close>
-lemma homeomorphism_arc:
- fixes g :: "real \<Rightarrow> 'a::t2_space"
- assumes "arc g"
- obtains h where "homeomorphism {0..1} (path_image g) g h"
-using assms by (force simp: arc_def homeomorphism_compact path_def path_image_def)
-
-lemma homeomorphic_arc_image_interval:
- fixes g :: "real \<Rightarrow> 'a::t2_space" and a::real
- assumes "arc g" "a < b"
- shows "(path_image g) homeomorphic {a..b}"
-proof -
- have "(path_image g) homeomorphic {0..1::real}"
- by (meson assms(1) homeomorphic_def homeomorphic_sym homeomorphism_arc)
- also have "\<dots> homeomorphic {a..b}"
- using assms by (force intro: homeomorphic_closed_intervals_real)
- finally show ?thesis .
-qed
-
-lemma homeomorphic_arc_images:
- fixes g :: "real \<Rightarrow> 'a::t2_space" and h :: "real \<Rightarrow> 'b::t2_space"
- assumes "arc g" "arc h"
- shows "(path_image g) homeomorphic (path_image h)"
-proof -
- have "(path_image g) homeomorphic {0..1::real}"
- by (meson assms homeomorphic_def homeomorphic_sym homeomorphism_arc)
- also have "\<dots> homeomorphic (path_image h)"
- by (meson assms homeomorphic_def homeomorphism_arc)
- finally show ?thesis .
-qed
-
lemma path_connected_arc_complement:
fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
assumes "arc \<gamma>" "2 \<le> DIM('a)"
@@ -487,4 +457,4 @@
lemma valid_path_rectpath [simp, intro]: "valid_path (rectpath a b)"
by (simp add: Let_def rectpath_def)
-end
\ No newline at end of file
+end