src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 53597 ea99a7964174
parent 53374 a14d2a854c02
child 53640 3170b5eb9f5a
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 12 09:33:36 2013 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 12 09:39:02 2013 -0700
     1.3 @@ -978,9 +978,6 @@
     1.4      unfolding th0 th1 by simp
     1.5  qed
     1.6  
     1.7 -lemma connected_empty[simp, intro]: "connected {}"  (* FIXME duplicate? *)
     1.8 -  by simp
     1.9 -
    1.10  
    1.11  subsection{* Limit points *}
    1.12  
    1.13 @@ -2125,32 +2122,20 @@
    1.14  
    1.15  text{* Some other lemmas about sequences. *}
    1.16  
    1.17 -lemma sequentially_offset:
    1.18 +lemma sequentially_offset: (* TODO: move to Topological_Spaces.thy *)
    1.19    assumes "eventually (\<lambda>i. P i) sequentially"
    1.20    shows "eventually (\<lambda>i. P (i + k)) sequentially"
    1.21 -  using assms unfolding eventually_sequentially by (metis trans_le_add1)
    1.22 -
    1.23 -lemma seq_offset:
    1.24 -  assumes "(f ---> l) sequentially"
    1.25 -  shows "((\<lambda>i. f (i + k)) ---> l) sequentially"
    1.26 -  using assms by (rule LIMSEQ_ignore_initial_segment) (* FIXME: redundant *)
    1.27 -
    1.28 -lemma seq_offset_neg:
    1.29 +  using assms by (rule eventually_sequentially_seg [THEN iffD2])
    1.30 +
    1.31 +lemma seq_offset_neg: (* TODO: move to Topological_Spaces.thy *)
    1.32    "(f ---> l) sequentially \<Longrightarrow> ((\<lambda>i. f(i - k)) ---> l) sequentially"
    1.33 -  apply (rule topological_tendstoI)
    1.34 -  apply (drule (2) topological_tendstoD)
    1.35 -  apply (simp only: eventually_sequentially)
    1.36 -  apply (subgoal_tac "\<And>N k (n::nat). N + k <= n \<Longrightarrow> N <= n - k")
    1.37 -  apply metis
    1.38 +  apply (erule filterlim_compose)
    1.39 +  apply (simp add: filterlim_def le_sequentially eventually_filtermap eventually_sequentially)
    1.40    apply arith
    1.41    done
    1.42  
    1.43 -lemma seq_offset_rev:
    1.44 -  "((\<lambda>i. f(i + k)) ---> l) sequentially \<Longrightarrow> (f ---> l) sequentially"
    1.45 -  by (rule LIMSEQ_offset) (* FIXME: redundant *)
    1.46 -
    1.47  lemma seq_harmonic: "((\<lambda>n. inverse (real n)) ---> 0) sequentially"
    1.48 -  using LIMSEQ_inverse_real_of_nat by (rule LIMSEQ_imp_Suc)
    1.49 +  using LIMSEQ_inverse_real_of_nat by (rule LIMSEQ_imp_Suc) (* TODO: move to Limits.thy *)
    1.50  
    1.51  subsection {* More properties of closed balls *}
    1.52