equal
deleted
inserted
replaced
42 lemma injective_imp_simple_path: "injective_path g \<Longrightarrow> simple_path g" |
42 lemma injective_imp_simple_path: "injective_path g \<Longrightarrow> simple_path g" |
43 unfolding injective_path_def simple_path_def |
43 unfolding injective_path_def simple_path_def |
44 by auto |
44 by auto |
45 |
45 |
46 lemma path_image_nonempty: "path_image g \<noteq> {}" |
46 lemma path_image_nonempty: "path_image g \<noteq> {}" |
47 unfolding path_image_def image_is_empty interval_eq_empty |
47 unfolding path_image_def image_is_empty box_eq_empty |
48 by auto |
48 by auto |
49 |
49 |
50 lemma pathstart_in_path_image[intro]: "pathstart g \<in> path_image g" |
50 lemma pathstart_in_path_image[intro]: "pathstart g \<in> path_image g" |
51 unfolding pathstart_def path_image_def |
51 unfolding pathstart_def path_image_def |
52 by auto |
52 by auto |
62 done |
62 done |
63 |
63 |
64 lemma compact_path_image[intro]: "path g \<Longrightarrow> compact (path_image g)" |
64 lemma compact_path_image[intro]: "path g \<Longrightarrow> compact (path_image g)" |
65 unfolding path_def path_image_def |
65 unfolding path_def path_image_def |
66 apply (erule compact_continuous_image) |
66 apply (erule compact_continuous_image) |
67 apply (rule compact_interval) |
67 apply (rule compact_Icc) |
68 done |
68 done |
69 |
69 |
70 lemma reversepath_reversepath[simp]: "reversepath (reversepath g) = g" |
70 lemma reversepath_reversepath[simp]: "reversepath (reversepath g) = g" |
71 unfolding reversepath_def |
71 unfolding reversepath_def |
72 by auto |
72 by auto |