author huffman Sat, 13 Jun 2009 07:33:50 -0700 changeset 31654 83662a8604c2 parent 31593 dc65b2f78664 child 31655 bcb1eb2197f8
generalize lemma Lim_unique to t2_space
```--- 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 \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b" where
+  Lim :: "'a net \<Rightarrow> ('a \<Rightarrow> 'b::t2_space) \<Rightarrow> '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 \<Rightarrow> 'b::metric_space"
+  fixes f :: "'a \<Rightarrow> 'b::t2_space"
assumes "\<not> trivial_limit net"  "(f ---> l) net"  "(f ---> l') net"
shows "l = l'"
proof (rule ccontr)
-  let ?d = "dist l l' / 2"
assume "l \<noteq> l'"
-  then have "0 < ?d" by (simp add: dist_nz)
-  have "eventually (\<lambda>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 \<in> U" "l' \<in> V" "U \<inter> V = {}"
+    using hausdorff [OF `l \<noteq> l'`] by fast
+  have "eventually (\<lambda>x. f x \<in> U) net"
+    using `(f ---> l) net` `open U` `l \<in> U` by (rule topological_tendstoD)
moreover
-  have "eventually (\<lambda>x. dist (f x) l' < ?d) net"
-    using `(f ---> l') net` `0 < ?d` by (rule tendstoD)
+  have "eventually (\<lambda>x. f x \<in> V) net"
+    using `(f ---> l') net` `open V` `l' \<in> V` by (rule topological_tendstoD)
ultimately
have "eventually (\<lambda>x. False) net"
proof (rule eventually_elim2)
fix x
-    assume *: "dist (f x) l < ?d" "dist (f x) l' < ?d"
-    have "dist l l' \<le> dist (f x) l + dist (f x) l'"
-      by (rule dist_triangle_alt)
-    also from * have "\<dots> < ?d + ?d"
-    also have "\<dots> = dist l l'" by simp
-    finally show "False" by simp
+    assume "f x \<in> U" "f x \<in> V"
+    hence "f x \<in> U \<inter> V" by simp
+    with `U \<inter> V = {}` show "False" by simp
qed
with `\<not> trivial_limit net` show "False"