src/HOL/Limits.thy
changeset 41970 47d6e13d1710
parent 39302 d7728f65b353
child 44079 bcc60791b7b9
     1.1 --- a/src/HOL/Limits.thy	Mon Mar 14 14:37:33 2011 +0100
     1.2 +++ b/src/HOL/Limits.thy	Mon Mar 14 14:37:35 2011 +0100
     1.3 @@ -103,7 +103,6 @@
     1.4    shows "eventually (\<lambda>i. R i) net"
     1.5  using assms by (auto elim!: eventually_rev_mp)
     1.6  
     1.7 -
     1.8  subsection {* Finer-than relation *}
     1.9  
    1.10  text {* @{term "net \<le> net'"} means that @{term net} is finer than
    1.11 @@ -231,7 +230,6 @@
    1.12    "eventually (\<lambda>x. False) net \<longleftrightarrow> net = bot"
    1.13  unfolding expand_net_eq by (auto elim: eventually_rev_mp)
    1.14  
    1.15 -
    1.16  subsection {* Map function for nets *}
    1.17  
    1.18  definition netmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a net \<Rightarrow> 'b net" where
    1.19 @@ -287,6 +285,13 @@
    1.20  by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp)
    1.21  
    1.22  
    1.23 +definition
    1.24 +  trivial_limit :: "'a net \<Rightarrow> bool" where
    1.25 +  "trivial_limit net \<longleftrightarrow> eventually (\<lambda>x. False) net"
    1.26 +
    1.27 +lemma trivial_limit_sequentially[intro]: "\<not> trivial_limit sequentially"
    1.28 +  by (auto simp add: trivial_limit_def eventually_sequentially)
    1.29 +
    1.30  subsection {* Standard Nets *}
    1.31  
    1.32  definition within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where
    1.33 @@ -827,4 +832,29 @@
    1.34      \<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) net"
    1.35  by (simp add: mult.tendsto tendsto_inverse divide_inverse)
    1.36  
    1.37 +lemma tendsto_unique:
    1.38 +  fixes f :: "'a \<Rightarrow> 'b::t2_space"
    1.39 +  assumes "\<not> trivial_limit net"  "(f ---> l) net"  "(f ---> l') net"
    1.40 +  shows "l = l'"
    1.41 +proof (rule ccontr)
    1.42 +  assume "l \<noteq> l'"
    1.43 +  obtain U V where "open U" "open V" "l \<in> U" "l' \<in> V" "U \<inter> V = {}"
    1.44 +    using hausdorff [OF `l \<noteq> l'`] by fast
    1.45 +  have "eventually (\<lambda>x. f x \<in> U) net"
    1.46 +    using `(f ---> l) net` `open U` `l \<in> U` by (rule topological_tendstoD)
    1.47 +  moreover
    1.48 +  have "eventually (\<lambda>x. f x \<in> V) net"
    1.49 +    using `(f ---> l') net` `open V` `l' \<in> V` by (rule topological_tendstoD)
    1.50 +  ultimately
    1.51 +  have "eventually (\<lambda>x. False) net"
    1.52 +  proof (rule eventually_elim2)
    1.53 +    fix x
    1.54 +    assume "f x \<in> U" "f x \<in> V"
    1.55 +    hence "f x \<in> U \<inter> V" by simp
    1.56 +    with `U \<inter> V = {}` show "False" by simp
    1.57 +  qed
    1.58 +  with `\<not> trivial_limit net` show "False"
    1.59 +    by (simp add: trivial_limit_def)
    1.60 +qed
    1.61 +
    1.62  end