134 using assms inj_on_eq_iff [of f] |
134 using assms inj_on_eq_iff [of f] |
135 by (auto simp: arc_def inj_on_def path_linear_image_eq) |
135 by (auto simp: arc_def inj_on_def path_linear_image_eq) |
136 |
136 |
137 |
137 |
138 subsection\<^marker>\<open>tag unimportant\<close>\<open>Basic lemmas about paths\<close> |
138 subsection\<^marker>\<open>tag unimportant\<close>\<open>Basic lemmas about paths\<close> |
|
139 |
|
140 lemma path_of_real: "path complex_of_real" |
|
141 unfolding path_def by (intro continuous_intros) |
|
142 |
|
143 lemma path_const: "path (\<lambda>t. a)" for a::"'a::real_normed_vector" |
|
144 unfolding path_def by (intro continuous_intros) |
|
145 |
|
146 lemma path_minus: "path g \<Longrightarrow> path (\<lambda>t. - g t)" for g::"real\<Rightarrow>'a::real_normed_vector" |
|
147 unfolding path_def by (intro continuous_intros) |
|
148 |
|
149 lemma path_add: "\<lbrakk>path f; path g\<rbrakk> \<Longrightarrow> path (\<lambda>t. f t + g t)" for f::"real\<Rightarrow>'a::real_normed_vector" |
|
150 unfolding path_def by (intro continuous_intros) |
|
151 |
|
152 lemma path_diff: "\<lbrakk>path f; path g\<rbrakk> \<Longrightarrow> path (\<lambda>t. f t - g t)" for f::"real\<Rightarrow>'a::real_normed_vector" |
|
153 unfolding path_def by (intro continuous_intros) |
|
154 |
|
155 lemma path_mult: "\<lbrakk>path f; path g\<rbrakk> \<Longrightarrow> path (\<lambda>t. f t * g t)" for f::"real\<Rightarrow>'a::real_normed_field" |
|
156 unfolding path_def by (intro continuous_intros) |
139 |
157 |
140 lemma pathin_iff_path_real [simp]: "pathin euclideanreal g \<longleftrightarrow> path g" |
158 lemma pathin_iff_path_real [simp]: "pathin euclideanreal g \<longleftrightarrow> path g" |
141 by (simp add: pathin_def path_def) |
159 by (simp add: pathin_def path_def) |
142 |
160 |
143 lemma continuous_on_path: "path f \<Longrightarrow> t \<subseteq> {0..1} \<Longrightarrow> continuous_on t f" |
161 lemma continuous_on_path: "path f \<Longrightarrow> t \<subseteq> {0..1} \<Longrightarrow> continuous_on t f" |