equal
deleted
inserted
replaced
574 apply (simp add: g2D con_g2) |
574 apply (simp add: g2D con_g2) |
575 done |
575 done |
576 qed |
576 qed |
577 |
577 |
578 subsection \<open>Valid paths, and their start and finish\<close> |
578 subsection \<open>Valid paths, and their start and finish\<close> |
579 |
|
580 lemma Diff_Un_eq: "A - (B \<union> C) = A - B - C" |
|
581 by blast |
|
582 |
579 |
583 definition valid_path :: "(real \<Rightarrow> 'a :: real_normed_vector) \<Rightarrow> bool" |
580 definition valid_path :: "(real \<Rightarrow> 'a :: real_normed_vector) \<Rightarrow> bool" |
584 where "valid_path f \<equiv> f piecewise_C1_differentiable_on {0..1::real}" |
581 where "valid_path f \<equiv> f piecewise_C1_differentiable_on {0..1::real}" |
585 |
582 |
586 definition closed_path :: "(real \<Rightarrow> 'a :: real_normed_vector) \<Rightarrow> bool" |
583 definition closed_path :: "(real \<Rightarrow> 'a :: real_normed_vector) \<Rightarrow> bool" |