src/HOL/Topological_Spaces.thy
changeset 57275 0ddb5b755cdc
parent 57025 e7fd64f82876
child 57276 49c51eeaa623
     1.1 --- a/src/HOL/Topological_Spaces.thy	Wed Jun 18 15:23:40 2014 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Jun 18 07:31:12 2014 +0200
     1.3 @@ -789,13 +789,13 @@
     1.4    by (simp add: at_eq_bot_iff not_open_singleton)
     1.5  
     1.6  lemma eventually_at_right:
     1.7 -  fixes x :: "'a :: {no_top, linorder_topology}"
     1.8 +  fixes x :: "'a :: linorder_topology"
     1.9 +  assumes gt_ex: "x < y"
    1.10    shows "eventually P (at_right x) \<longleftrightarrow> (\<exists>b. x < b \<and> (\<forall>z. x < z \<and> z < b \<longrightarrow> P z))"
    1.11    unfolding eventually_at_topological
    1.12  proof safe
    1.13 -  obtain y where "x < y" using gt_ex[of x] ..
    1.14 +  note gt_ex
    1.15    moreover fix S assume "open S" "x \<in> S" note open_right[OF this, of y]
    1.16 -  moreover note gt_ex[of x]
    1.17    moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {x<..} \<longrightarrow> P s"
    1.18    ultimately show "\<exists>b>x. \<forall>z. x < z \<and> z < b \<longrightarrow> P z"
    1.19      by (auto simp: subset_eq Ball_def)
    1.20 @@ -806,11 +806,12 @@
    1.21  qed
    1.22  
    1.23  lemma eventually_at_left:
    1.24 -  fixes x :: "'a :: {no_bot, linorder_topology}"
    1.25 +  fixes x :: "'a :: linorder_topology"
    1.26 +  assumes lt_ex: "y < x"
    1.27    shows "eventually P (at_left x) \<longleftrightarrow> (\<exists>b. x > b \<and> (\<forall>z. b < z \<and> z < x \<longrightarrow> P z))"
    1.28    unfolding eventually_at_topological
    1.29  proof safe
    1.30 -  obtain y where "y < x" using lt_ex[of x] ..
    1.31 +  note lt_ex
    1.32    moreover fix S assume "open S" "x \<in> S" note open_left[OF this, of y]
    1.33    moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s"
    1.34    ultimately show "\<exists>b<x. \<forall>z. b < z \<and> z < x \<longrightarrow> P z"
    1.35 @@ -821,13 +822,21 @@
    1.36      by (intro exI[of _ "{b <..}"]) auto
    1.37  qed
    1.38  
    1.39 +lemma trivial_limit_at_right_top: "at_right (top::_::{order_top, linorder_topology}) = bot"
    1.40 +  unfolding filter_eq_iff eventually_at_topological by auto
    1.41 +
    1.42 +lemma trivial_limit_at_left_bot: "at_left (bot::_::{order_bot, linorder_topology}) = bot"
    1.43 +  unfolding filter_eq_iff eventually_at_topological by auto
    1.44 +
    1.45  lemma trivial_limit_at_left_real [simp]:
    1.46 -  "\<not> trivial_limit (at_left (x::'a::{no_bot, unbounded_dense_linorder, linorder_topology}))"
    1.47 -  unfolding trivial_limit_def eventually_at_left by (auto dest: dense)
    1.48 +  "\<not> trivial_limit (at_left (x::'a::{no_bot, dense_order, linorder_topology}))"
    1.49 +  using lt_ex[of x]
    1.50 +  by safe (auto simp add: trivial_limit_def eventually_at_left dest: dense)
    1.51  
    1.52  lemma trivial_limit_at_right_real [simp]:
    1.53 -  "\<not> trivial_limit (at_right (x::'a::{no_top, unbounded_dense_linorder, linorder_topology}))"
    1.54 -  unfolding trivial_limit_def eventually_at_right by (auto dest: dense)
    1.55 +  "\<not> trivial_limit (at_right (x::'a::{no_top, dense_order, linorder_topology}))"
    1.56 +  using gt_ex[of x]
    1.57 +  by safe (auto simp add: trivial_limit_def eventually_at_right dest: dense)
    1.58  
    1.59  lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)"
    1.60    by (auto simp: eventually_at_filter filter_eq_iff eventually_sup 
    1.61 @@ -867,6 +876,15 @@
    1.62    "F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"
    1.63    by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)
    1.64  
    1.65 +lemma filterlim_mono_eventually:
    1.66 +  assumes "filterlim f F G" and ord: "F \<le> F'" "G' \<le> G"
    1.67 +  assumes eq: "eventually (\<lambda>x. f x = f' x) G'"
    1.68 +  shows "filterlim f' F' G'"
    1.69 +  apply (rule filterlim_cong[OF refl refl eq, THEN iffD1])
    1.70 +  apply (rule filterlim_mono[OF _ ord])
    1.71 +  apply fact
    1.72 +  done
    1.73 +
    1.74  lemma filterlim_principal:
    1.75    "(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
    1.76    unfolding filterlim_def eventually_filtermap le_principal ..
    1.77 @@ -1179,7 +1197,7 @@
    1.78    by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
    1.79  
    1.80  lemma filterlim_at_bot_at_right:
    1.81 -  fixes f :: "'a::{no_top, linorder_topology} \<Rightarrow> 'b::linorder"
    1.82 +  fixes f :: "'a::linorder_topology \<Rightarrow> 'b::linorder"
    1.83    assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
    1.84    assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
    1.85    assumes Q: "eventually Q (at_right a)" and bound: "\<And>b. Q b \<Longrightarrow> a < b"
    1.86 @@ -1194,14 +1212,14 @@
    1.87      with x have "P z" by auto
    1.88      have "eventually (\<lambda>x. x \<le> g z) (at_right a)"
    1.89        using bound[OF bij(2)[OF `P z`]]
    1.90 -      unfolding eventually_at_right by (auto intro!: exI[of _ "g z"])
    1.91 +      unfolding eventually_at_right[OF bound[OF bij(2)[OF `P z`]]] by (auto intro!: exI[of _ "g z"])
    1.92      with Q show "eventually (\<lambda>x. f x \<le> z) (at_right a)"
    1.93        by eventually_elim (metis bij `P z` mono)
    1.94    qed
    1.95  qed
    1.96  
    1.97  lemma filterlim_at_top_at_left:
    1.98 -  fixes f :: "'a::{no_bot, linorder_topology} \<Rightarrow> 'b::linorder"
    1.99 +  fixes f :: "'a::linorder_topology \<Rightarrow> 'b::linorder"
   1.100    assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
   1.101    assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
   1.102    assumes Q: "eventually Q (at_left a)" and bound: "\<And>b. Q b \<Longrightarrow> b < a"
   1.103 @@ -1216,7 +1234,7 @@
   1.104      with x have "P z" by auto
   1.105      have "eventually (\<lambda>x. g z \<le> x) (at_left a)"
   1.106        using bound[OF bij(2)[OF `P z`]]
   1.107 -      unfolding eventually_at_left by (auto intro!: exI[of _ "g z"])
   1.108 +      unfolding eventually_at_left[OF bound[OF bij(2)[OF `P z`]]] by (auto intro!: exI[of _ "g z"])
   1.109      with Q show "eventually (\<lambda>x. z \<le> f x) (at_left a)"
   1.110        by eventually_elim (metis bij `P z` mono)
   1.111    qed