equal
deleted
inserted
replaced
841 using exists_path_subpath_to_frontier [OF g _ g1] closure_closed [OF S] g0 by auto |
841 using exists_path_subpath_to_frontier [OF g _ g1] closure_closed [OF S] g0 by auto |
842 show ?thesis |
842 show ?thesis |
843 apply (rule that [OF \<open>path h\<close>]) |
843 apply (rule that [OF \<open>path h\<close>]) |
844 using assms h |
844 using assms h |
845 apply auto |
845 apply auto |
846 apply (metis diff_single_insert frontier_subset_eq insert_iff interior_subset subset_iff) |
846 apply (metis Diff_single_insert frontier_subset_eq insert_iff interior_subset subset_iff) |
847 done |
847 done |
848 qed |
848 qed |
849 |
849 |
850 subsection \<open>Reparametrizing a closed curve to start at some chosen point\<close> |
850 subsection \<open>Reparametrizing a closed curve to start at some chosen point\<close> |
851 |
851 |