src/HOL/Topological_Spaces.thy
changeset 57025 e7fd64f82876
parent 56949 d1a937cbf858
child 57275 0ddb5b755cdc
     1.1 --- a/src/HOL/Topological_Spaces.thy	Tue May 20 16:52:59 2014 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Tue May 20 19:24:39 2014 +0200
     1.3 @@ -1230,6 +1230,22 @@
     1.4    "filterlim f F (at (x::'a::linorder_topology)) \<longleftrightarrow> filterlim f F (at_left x) \<and> filterlim f F (at_right x)"
     1.5    by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup)
     1.6  
     1.7 +lemma eventually_nhds_top:
     1.8 +  fixes P :: "'a :: {order_top, linorder_topology} \<Rightarrow> bool"
     1.9 +  assumes "(b::'a) < top"
    1.10 +  shows "eventually P (nhds top) \<longleftrightarrow> (\<exists>b<top. (\<forall>z. b < z \<longrightarrow> P z))"
    1.11 +  unfolding eventually_nhds
    1.12 +proof safe
    1.13 +  fix S :: "'a set" assume "open S" "top \<in> S"
    1.14 +  note open_left[OF this `b < top`]
    1.15 +  moreover assume "\<forall>s\<in>S. P s"
    1.16 +  ultimately show "\<exists>b<top. \<forall>z>b. P z"
    1.17 +    by (auto simp: subset_eq Ball_def)
    1.18 +next
    1.19 +  fix b assume "b < top" "\<forall>z>b. P z"
    1.20 +  then show "\<exists>S. open S \<and> top \<in> S \<and> (\<forall>xa\<in>S. P xa)"
    1.21 +    by (intro exI[of _ "{b <..}"]) auto
    1.22 +qed
    1.23  
    1.24  subsection {* Limits on sequences *}
    1.25  
    1.26 @@ -1724,6 +1740,50 @@
    1.27     (X -- a --> (L::'b::topological_space))"
    1.28    using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
    1.29  
    1.30 +lemma sequentially_imp_eventually_at_left:
    1.31 +  fixes a :: "'a :: {dense_linorder, linorder_topology, first_countable_topology}"
    1.32 +  assumes b[simp]: "b < a"
    1.33 +  assumes *: "\<And>f. (\<And>n. b < f n) \<Longrightarrow> (\<And>n. f n < a) \<Longrightarrow> incseq f \<Longrightarrow> f ----> a \<Longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
    1.34 +  shows "eventually P (at_left a)"
    1.35 +proof (safe intro!: sequentially_imp_eventually_within)
    1.36 +  fix X assume X: "\<forall>n. X n \<in> {..<a} \<and> X n \<noteq> a" "X ----> a"
    1.37 +  show "eventually (\<lambda>n. P (X n)) sequentially"
    1.38 +  proof (rule ccontr)
    1.39 +    assume "\<not> eventually (\<lambda>n. P (X n)) sequentially"
    1.40 +    from not_eventually_sequentiallyD[OF this]
    1.41 +    obtain r where "subseq r" "\<And>n. \<not> P (X (r n))"
    1.42 +      by auto
    1.43 +    with X have "(X \<circ> r) ----> a"
    1.44 +      by (auto intro: LIMSEQ_subseq_LIMSEQ)
    1.45 +    from order_tendstoD(1)[OF this] obtain s' where s': "\<And>b i. b < a \<Longrightarrow> s' b \<le> i \<Longrightarrow> b < X (r i)"
    1.46 +      unfolding eventually_sequentially comp_def by metis
    1.47 +    def s \<equiv> "rec_nat (s' b) (\<lambda>_ i. max (s' (X (r i))) (Suc i))"
    1.48 +    then have [simp]: "s 0 = s' b" "\<And>n. s (Suc n) = max (s' (X (r (s n)))) (Suc (s n))"
    1.49 +      by auto
    1.50 +    have "eventually (\<lambda>n. P (((X \<circ> r) \<circ> s) n)) sequentially"
    1.51 +    proof (rule *)
    1.52 +      from X show inc: "incseq (X \<circ> r \<circ> s)"
    1.53 +        unfolding incseq_Suc_iff comp_def by (intro allI s'[THEN less_imp_le]) auto
    1.54 +      { fix n show "b < (X \<circ> r \<circ> s) n"
    1.55 +          using inc[THEN incseqD, of 0 n] s'[OF b order_refl] by simp }
    1.56 +      { fix n show "(X \<circ> r \<circ> s) n < a"
    1.57 +          using X by simp }
    1.58 +      from `(X \<circ> r) ----> a` show "(X \<circ> r \<circ> s) ----> a"
    1.59 +        by (rule LIMSEQ_subseq_LIMSEQ) (auto simp: subseq_Suc_iff)
    1.60 +    qed
    1.61 +    with `\<And>n. \<not> P (X (r n))` show False
    1.62 +      by auto
    1.63 +  qed
    1.64 +qed
    1.65 +
    1.66 +lemma tendsto_at_left_sequentially:
    1.67 +  fixes a :: "_ :: {dense_linorder, linorder_topology, first_countable_topology}"
    1.68 +  assumes "b < a"
    1.69 +  assumes *: "\<And>S. (\<And>n. S n < a) \<Longrightarrow> (\<And>n. b < S n) \<Longrightarrow> incseq S \<Longrightarrow> S ----> a \<Longrightarrow> (\<lambda>n. X (S n)) ----> L"
    1.70 +  shows "(X ---> L) (at_left a)"
    1.71 +  using assms unfolding tendsto_def [where l=L]
    1.72 +  by (simp add: sequentially_imp_eventually_at_left)
    1.73 +
    1.74  subsection {* Continuity *}
    1.75  
    1.76  subsubsection {* Continuity on a set *}