src/HOL/Topological_Spaces.thy
changeset 61810 3c5040d5694a
parent 61806 d2e62ae01cd8
child 61907 f0c894ab18c9
     1.1 --- a/src/HOL/Topological_Spaces.thy	Tue Dec 08 20:21:59 2015 +0100
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Dec 09 17:35:22 2015 +0000
     1.3 @@ -471,7 +471,7 @@
     1.4  
     1.5  lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)"
     1.6    by (auto simp: eventually_at_filter filter_eq_iff eventually_sup 
     1.7 -           elim: eventually_elim2 eventually_elim1)
     1.8 +           elim: eventually_elim2 eventually_mono)
     1.9  
    1.10  lemma eventually_at_split:
    1.11    "eventually P (at (x::'a::linorder_topology)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
    1.12 @@ -551,7 +551,7 @@
    1.13    fix a assume "a < max x y"
    1.14    then show "eventually (\<lambda>x. a < max (X x) (Y x)) net"
    1.15      using order_tendstoD(1)[OF X, of a] order_tendstoD(1)[OF Y, of a]
    1.16 -    by (auto simp: less_max_iff_disj elim: eventually_elim1)
    1.17 +    by (auto simp: less_max_iff_disj elim: eventually_mono)
    1.18  next
    1.19    fix a assume "max x y < a"
    1.20    then show "eventually (\<lambda>x. max (X x) (Y x) < a) net"
    1.21 @@ -572,7 +572,7 @@
    1.22    fix a assume "min x y < a"
    1.23    then show "eventually (\<lambda>x. min (X x) (Y x) < a) net"
    1.24      using order_tendstoD(2)[OF X, of a] order_tendstoD(2)[OF Y, of a]
    1.25 -    by (auto simp: min_less_iff_disj elim: eventually_elim1)
    1.26 +    by (auto simp: min_less_iff_disj elim: eventually_mono)
    1.27  qed
    1.28  
    1.29  lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) ---> a) (at a within s)"
    1.30 @@ -613,14 +613,14 @@
    1.31    assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
    1.32        and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
    1.33    shows "(f ---> l) F"
    1.34 -  using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
    1.35 +  using assms by (intro order_tendstoI) (auto elim!: eventually_mono)
    1.36  
    1.37  lemma decreasing_tendsto:
    1.38    fixes f :: "_ \<Rightarrow> 'a::order_topology"
    1.39    assumes bdd: "eventually (\<lambda>n. l \<le> f n) F"
    1.40        and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F"
    1.41    shows "(f ---> l) F"
    1.42 -  using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
    1.43 +  using assms by (intro order_tendstoI) (auto elim!: eventually_mono)
    1.44  
    1.45  lemma tendsto_sandwich:
    1.46    fixes f g h :: "'a \<Rightarrow> 'b::order_topology"
    1.47 @@ -773,7 +773,7 @@
    1.48  lemma tendsto_at_within_iff_tendsto_nhds:
    1.49    "(g ---> g l) (at l within S) \<longleftrightarrow> (g ---> g l) (inf (nhds l) (principal S))"
    1.50    unfolding tendsto_def eventually_at_filter eventually_inf_principal
    1.51 -  by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
    1.52 +  by (intro ext all_cong imp_cong) (auto elim!: eventually_mono)
    1.53  
    1.54  subsection \<open>Limits on sequences\<close>
    1.55  
    1.56 @@ -1152,7 +1152,7 @@
    1.57    {
    1.58      fix F S assume "\<forall>n. F n \<in> A n" "open S" "x \<in> S"
    1.59      with A(3)[of S] have "eventually (\<lambda>n. F n \<in> S) sequentially"
    1.60 -      by (auto elim: eventually_elim1 simp: subset_eq)
    1.61 +      by (auto elim: eventually_mono simp: subset_eq)
    1.62    }
    1.63    with A show "\<exists>A. (\<forall>i. open (A i)) \<and> (\<forall>i. x \<in> A i) \<and> (\<forall>F. (\<forall>n. F n \<in> A n) \<longrightarrow> F ----> x)"
    1.64      by (intro exI[of _ A]) (auto simp: tendsto_def)
    1.65 @@ -1187,7 +1187,7 @@
    1.66      by (auto simp: eventually_inf_principal eventually_nhds)
    1.67    moreover fix f assume "\<forall>n. f n \<in> s" "f ----> a"
    1.68    ultimately show "eventually (\<lambda>n. P (f n)) sequentially"
    1.69 -    by (auto dest!: topological_tendstoD elim: eventually_elim1)
    1.70 +    by (auto dest!: topological_tendstoD elim: eventually_mono)
    1.71  qed
    1.72  
    1.73  lemma (in first_countable_topology) eventually_nhds_iff_sequentially:
    1.74 @@ -1243,7 +1243,7 @@
    1.75  lemma tendsto_at_iff_tendsto_nhds:
    1.76    "g -- l --> g l \<longleftrightarrow> (g ---> g l) (nhds l)"
    1.77    unfolding tendsto_def eventually_at_filter
    1.78 -  by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
    1.79 +  by (intro ext all_cong imp_cong) (auto elim!: eventually_mono)
    1.80  
    1.81  lemma tendsto_compose:
    1.82    "g -- l --> g l \<Longrightarrow> (f ---> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
    1.83 @@ -1758,7 +1758,7 @@
    1.84    with \<open>finite D\<close> have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
    1.85      by (simp add: eventually_ball_finite)
    1.86    with \<open>s \<subseteq> \<Union>D\<close> have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
    1.87 -    by (auto elim!: eventually_mono')
    1.88 +    by (auto elim!: eventually_mono)
    1.89    thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"
    1.90      by (simp add: eventually_nhds subset_eq)
    1.91  qed