# HG changeset patch # User huffman # Date 1244903630 25200 # Node ID 83662a8604c274aecfdf025cc13de2e0c43de4e3 # Parent dc65b2f786647a68f1dad36adc84c78592197488 generalize lemma Lim_unique to t2_space diff -r dc65b2f78664 -r 83662a8604c2 src/HOL/Library/Topology_Euclidean_Space.thy --- a/src/HOL/Library/Topology_Euclidean_Space.thy Sat Jun 13 07:03:51 2009 -0700 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy Sat Jun 13 07:33:50 2009 -0700 @@ -1102,7 +1102,7 @@ text{* Notation Lim to avoid collition with lim defined in analysis *} definition - Lim :: "'a net \ ('a \ 'b::metric_space) \ 'b" where + Lim :: "'a net \ ('a \ 'b::t2_space) \ 'b" where "Lim net f = (THE l. (f ---> l) net)" lemma Lim: @@ -1402,36 +1402,32 @@ text{* Uniqueness of the limit, when nontrivial. *} lemma Lim_unique: - fixes f :: "'a \ 'b::metric_space" + fixes f :: "'a \ 'b::t2_space" assumes "\ trivial_limit net" "(f ---> l) net" "(f ---> l') net" shows "l = l'" proof (rule ccontr) - let ?d = "dist l l' / 2" assume "l \ l'" - then have "0 < ?d" by (simp add: dist_nz) - have "eventually (\x. dist (f x) l < ?d) net" - using `(f ---> l) net` `0 < ?d` by (rule tendstoD) + obtain U V where "open U" "open V" "l \ U" "l' \ V" "U \ V = {}" + using hausdorff [OF `l \ l'`] by fast + have "eventually (\x. f x \ U) net" + using `(f ---> l) net` `open U` `l \ U` by (rule topological_tendstoD) moreover - have "eventually (\x. dist (f x) l' < ?d) net" - using `(f ---> l') net` `0 < ?d` by (rule tendstoD) + have "eventually (\x. f x \ V) net" + using `(f ---> l') net` `open V` `l' \ V` by (rule topological_tendstoD) ultimately have "eventually (\x. False) net" proof (rule eventually_elim2) fix x - assume *: "dist (f x) l < ?d" "dist (f x) l' < ?d" - have "dist l l' \ dist (f x) l + dist (f x) l'" - by (rule dist_triangle_alt) - also from * have "\ < ?d + ?d" - by (rule add_strict_mono) - also have "\ = dist l l'" by simp - finally show "False" by simp + assume "f x \ U" "f x \ V" + hence "f x \ U \ V" by simp + with `U \ V = {}` show "False" by simp qed with `\ trivial_limit net` show "False" by (simp add: eventually_False) qed lemma tendsto_Lim: - fixes f :: "'a \ 'b::metric_space" + fixes f :: "'a \ 'b::t2_space" shows "~(trivial_limit net) \ (f ---> l) net ==> Lim net f = l" unfolding Lim_def using Lim_unique[of net f] by auto