src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 50324 0a1242d5e7d4
parent 50245 dea9363887a6
child 50526 899c9c4e4a4c
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 03 18:19:01 2012 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 03 18:19:02 2012 +0100
     1.3 @@ -1102,28 +1102,10 @@
     1.4  subsection {* Filters and the ``eventually true'' quantifier *}
     1.5  
     1.6  definition
     1.7 -  at_infinity :: "'a::real_normed_vector filter" where
     1.8 -  "at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
     1.9 -
    1.10 -definition
    1.11    indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter"
    1.12      (infixr "indirection" 70) where
    1.13    "a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
    1.14  
    1.15 -text{* Prove That They are all filters. *}
    1.16 -
    1.17 -lemma eventually_at_infinity:
    1.18 -  "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. norm x >= b \<longrightarrow> P x)"
    1.19 -unfolding at_infinity_def
    1.20 -proof (rule eventually_Abs_filter, rule is_filter.intro)
    1.21 -  fix P Q :: "'a \<Rightarrow> bool"
    1.22 -  assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<exists>s. \<forall>x. s \<le> norm x \<longrightarrow> Q x"
    1.23 -  then obtain r s where
    1.24 -    "\<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<forall>x. s \<le> norm x \<longrightarrow> Q x" by auto
    1.25 -  then have "\<forall>x. max r s \<le> norm x \<longrightarrow> P x \<and> Q x" by simp
    1.26 -  then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x \<and> Q x" ..
    1.27 -qed auto
    1.28 -
    1.29  text {* Identify Trivial limits, where we can't approach arbitrarily closely. *}
    1.30  
    1.31  lemma trivial_limit_within: