equal
deleted
inserted
replaced
175 unfolding dist_prod_def by simp |
175 unfolding dist_prod_def by simp |
176 |
176 |
177 lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y" |
177 lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y" |
178 unfolding dist_prod_def by simp |
178 unfolding dist_prod_def by simp |
179 |
179 |
180 lemma tendsto_fst: |
180 lemma tendsto_fst [tendsto_intros]: |
181 assumes "(f ---> a) net" |
181 assumes "(f ---> a) net" |
182 shows "((\<lambda>x. fst (f x)) ---> fst a) net" |
182 shows "((\<lambda>x. fst (f x)) ---> fst a) net" |
183 proof (rule topological_tendstoI) |
183 proof (rule topological_tendstoI) |
184 fix S assume "open S" "fst a \<in> S" |
184 fix S assume "open S" "fst a \<in> S" |
185 then have "open (fst -` S)" "a \<in> fst -` S" |
185 then have "open (fst -` S)" "a \<in> fst -` S" |
194 by (rule topological_tendstoD) |
194 by (rule topological_tendstoD) |
195 then show "eventually (\<lambda>x. fst (f x) \<in> S) net" |
195 then show "eventually (\<lambda>x. fst (f x) \<in> S) net" |
196 by simp |
196 by simp |
197 qed |
197 qed |
198 |
198 |
199 lemma tendsto_snd: |
199 lemma tendsto_snd [tendsto_intros]: |
200 assumes "(f ---> a) net" |
200 assumes "(f ---> a) net" |
201 shows "((\<lambda>x. snd (f x)) ---> snd a) net" |
201 shows "((\<lambda>x. snd (f x)) ---> snd a) net" |
202 proof (rule topological_tendstoI) |
202 proof (rule topological_tendstoI) |
203 fix S assume "open S" "snd a \<in> S" |
203 fix S assume "open S" "snd a \<in> S" |
204 then have "open (snd -` S)" "a \<in> snd -` S" |
204 then have "open (snd -` S)" "a \<in> snd -` S" |
213 by (rule topological_tendstoD) |
213 by (rule topological_tendstoD) |
214 then show "eventually (\<lambda>x. snd (f x) \<in> S) net" |
214 then show "eventually (\<lambda>x. snd (f x) \<in> S) net" |
215 by simp |
215 by simp |
216 qed |
216 qed |
217 |
217 |
218 lemma tendsto_Pair: |
218 lemma tendsto_Pair [tendsto_intros]: |
219 assumes "(f ---> a) net" and "(g ---> b) net" |
219 assumes "(f ---> a) net" and "(g ---> b) net" |
220 shows "((\<lambda>x. (f x, g x)) ---> (a, b)) net" |
220 shows "((\<lambda>x. (f x, g x)) ---> (a, b)) net" |
221 proof (rule topological_tendstoI) |
221 proof (rule topological_tendstoI) |
222 fix S assume "open S" "(a, b) \<in> S" |
222 fix S assume "open S" "(a, b) \<in> S" |
223 then obtain A B where "open A" "open B" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S" |
223 then obtain A B where "open A" "open B" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S" |