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.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.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.31  lemma trivial_limit_within: