# HG changeset patch
# User huffman
# Date 1272937248 25200
# Node ID fec55067ae9b728007853da5f921da59fa22920e
# Parent  88f0125c3bd27200ab802f1a17c6e97e2ea289f5
add lemmas eventually_nhds_metric and tendsto_mono

diff -r 88f0125c3bd2 -r fec55067ae9b src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon May 03 17:39:46 2010 -0700
+++ b/src/HOL/Limits.thy	Mon May 03 18:40:48 2010 -0700
@@ -329,14 +329,9 @@
   thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x \<and> Q x)" by - rule
 qed auto
 
-lemma eventually_at_topological:
-  "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
-unfolding at_def eventually_within eventually_nhds by simp
-
-lemma eventually_at:
-  fixes a :: "'a::metric_space"
-  shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
-unfolding eventually_at_topological open_dist
+lemma eventually_nhds_metric:
+  "eventually P (nhds a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. dist x a < d \<longrightarrow> P x)"
+unfolding eventually_nhds open_dist
 apply safe
 apply fast
 apply (rule_tac x="{x. dist x a < d}" in exI, simp)
@@ -346,6 +341,15 @@
 apply (erule le_less_trans [OF dist_triangle])
 done
 
+lemma eventually_at_topological:
+  "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
+unfolding at_def eventually_within eventually_nhds by simp
+
+lemma eventually_at:
+  fixes a :: "'a::metric_space"
+  shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
+unfolding at_def eventually_within eventually_nhds_metric by auto
+
 
 subsection {* Boundedness *}
 
@@ -544,6 +548,9 @@
 
 setup Tendsto_Intros.setup
 
+lemma tendsto_mono: "net \<le> net' \<Longrightarrow> (f ---> l) net' \<Longrightarrow> (f ---> l) net"
+unfolding tendsto_def le_net_def by fast
+
 lemma topological_tendstoI:
   "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net)
     \<Longrightarrow> (f ---> l) net"