equal
deleted
inserted
replaced
2441 proof (intro topological_tendstoI) |
2441 proof (intro topological_tendstoI) |
2442 fix S |
2442 fix S |
2443 assume "open S" and "x \<in> S" |
2443 assume "open S" and "x \<in> S" |
2444 then have S: "open S" "ereal x \<in> ereal ` S" |
2444 then have S: "open S" "ereal x \<in> ereal ` S" |
2445 by (simp_all add: inj_image_mem_iff) |
2445 by (simp_all add: inj_image_mem_iff) |
2446 have "\<forall>x. f x \<in> ereal ` S \<longrightarrow> real_of_ereal (f x) \<in> S" |
|
2447 by auto |
|
2448 from this lim[THEN topological_tendstoD, OF open_ereal, OF S] |
|
2449 show "eventually (\<lambda>x. real_of_ereal (f x) \<in> S) net" |
2446 show "eventually (\<lambda>x. real_of_ereal (f x) \<in> S) net" |
2450 by (rule eventually_mono) |
2447 by (auto intro: eventually_mono' [OF lim[THEN topological_tendstoD, OF open_ereal, OF S]]) |
2451 qed |
2448 qed |
2452 |
2449 |
2453 lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net" |
2450 lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net" |
2454 by (auto dest!: lim_real_of_ereal) |
2451 by (auto dest!: lim_real_of_ereal) |
2455 |
2452 |