add lemmas eventually_nhds_metric and tendsto_mono
authorhuffman
Mon May 03 18:40:48 2010 -0700 (2010-05-03)
changeset 36656fec55067ae9b
parent 36655 88f0125c3bd2
child 36657 f376af79f6b7
add lemmas eventually_nhds_metric and tendsto_mono
src/HOL/Limits.thy
     1.1 --- a/src/HOL/Limits.thy	Mon May 03 17:39:46 2010 -0700
     1.2 +++ b/src/HOL/Limits.thy	Mon May 03 18:40:48 2010 -0700
     1.3 @@ -329,14 +329,9 @@
     1.4    thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x \<and> Q x)" by - rule
     1.5  qed auto
     1.6  
     1.7 -lemma eventually_at_topological:
     1.8 -  "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
     1.9 -unfolding at_def eventually_within eventually_nhds by simp
    1.10 -
    1.11 -lemma eventually_at:
    1.12 -  fixes a :: "'a::metric_space"
    1.13 -  shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
    1.14 -unfolding eventually_at_topological open_dist
    1.15 +lemma eventually_nhds_metric:
    1.16 +  "eventually P (nhds a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. dist x a < d \<longrightarrow> P x)"
    1.17 +unfolding eventually_nhds open_dist
    1.18  apply safe
    1.19  apply fast
    1.20  apply (rule_tac x="{x. dist x a < d}" in exI, simp)
    1.21 @@ -346,6 +341,15 @@
    1.22  apply (erule le_less_trans [OF dist_triangle])
    1.23  done
    1.24  
    1.25 +lemma eventually_at_topological:
    1.26 +  "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
    1.27 +unfolding at_def eventually_within eventually_nhds by simp
    1.28 +
    1.29 +lemma eventually_at:
    1.30 +  fixes a :: "'a::metric_space"
    1.31 +  shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
    1.32 +unfolding at_def eventually_within eventually_nhds_metric by auto
    1.33 +
    1.34  
    1.35  subsection {* Boundedness *}
    1.36  
    1.37 @@ -544,6 +548,9 @@
    1.38  
    1.39  setup Tendsto_Intros.setup
    1.40  
    1.41 +lemma tendsto_mono: "net \<le> net' \<Longrightarrow> (f ---> l) net' \<Longrightarrow> (f ---> l) net"
    1.42 +unfolding tendsto_def le_net_def by fast
    1.43 +
    1.44  lemma topological_tendstoI:
    1.45    "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net)
    1.46      \<Longrightarrow> (f ---> l) net"