--- a/src/HOL/IsaMakefile Wed Aug 17 23:37:23 2011 +0200
+++ b/src/HOL/IsaMakefile Wed Aug 17 23:41:47 2011 +0200
@@ -1580,7 +1580,7 @@
HOLCF/Library/Sum_Cpo.thy \
HOLCF/Library/HOLCF_Library.thy \
HOLCF/Library/ROOT.ML
- @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Library
+ @cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF Library
## HOLCF-IMP
--- a/src/HOL/Lim.thy Wed Aug 17 23:37:23 2011 +0200
+++ b/src/HOL/Lim.thy Wed Aug 17 23:41:47 2011 +0200
@@ -132,12 +132,8 @@
assumes f: "f -- a --> l"
assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l"
shows "g -- a --> m"
-apply (rule tendstoI, drule tendstoD [OF f])
-apply (simp add: eventually_at_topological, safe)
-apply (rule_tac x="S" in exI, safe)
-apply (drule_tac x="x" in bspec, safe)
-apply (erule (1) order_le_less_trans [OF le])
-done
+ by (rule metric_tendsto_imp_tendsto [OF f],
+ auto simp add: eventually_at_topological le)
lemma LIM_imp_LIM:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
@@ -145,9 +141,8 @@
assumes f: "f -- a --> l"
assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
shows "g -- a --> m"
-apply (rule metric_LIM_imp_LIM [OF f])
-apply (simp add: dist_norm le)
-done
+ by (rule metric_LIM_imp_LIM [OF f],
+ simp add: dist_norm le)
lemma LIM_norm:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
@@ -259,27 +254,7 @@
assumes g: "g -- b --> c"
assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)"
shows "(\<lambda>x. g (f x)) -- a --> c"
-proof (rule topological_tendstoI)
- fix C assume C: "open C" "c \<in> C"
- obtain B where B: "open B" "b \<in> B"
- and gC: "\<And>y. y \<in> B \<Longrightarrow> y \<noteq> b \<Longrightarrow> g y \<in> C"
- using topological_tendstoD [OF g C]
- unfolding eventually_at_topological by fast
- obtain A where A: "open A" "a \<in> A"
- and fB: "\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x \<in> B"
- using topological_tendstoD [OF f B]
- unfolding eventually_at_topological by fast
- have "eventually (\<lambda>x. f x \<noteq> b \<longrightarrow> g (f x) \<in> C) (at a)"
- unfolding eventually_at_topological
- proof (intro exI conjI ballI impI)
- show "open A" and "a \<in> A" using A .
- next
- fix x assume "x \<in> A" and "x \<noteq> a" and "f x \<noteq> b"
- then show "g (f x) \<in> C" by (simp add: gC fB)
- qed
- with inj show "eventually (\<lambda>x. g (f x) \<in> C) (at a)"
- by (rule eventually_rev_mp)
-qed
+ using g f inj by (rule tendsto_compose_eventually)
lemma metric_LIM_compose2:
assumes f: "f -- a --> b"
@@ -568,102 +543,49 @@
subsection {* Relation of LIM and LIMSEQ *}
lemma LIMSEQ_SEQ_conv1:
- fixes a :: "'a::metric_space" and L :: "'b::metric_space"
- assumes X: "X -- a --> L"
- shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
-proof (safe intro!: metric_LIMSEQ_I)
- fix S :: "nat \<Rightarrow> 'a"
- fix r :: real
- assume rgz: "0 < r"
- assume as: "\<forall>n. S n \<noteq> a"
- assume S: "S ----> a"
- from metric_LIM_D [OF X rgz] obtain s
- where sgz: "0 < s"
- and aux: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < s\<rbrakk> \<Longrightarrow> dist (X x) L < r"
- by fast
- from metric_LIMSEQ_D [OF S sgz]
- obtain no where "\<forall>n\<ge>no. dist (S n) a < s" by blast
- hence "\<forall>n\<ge>no. dist (X (S n)) L < r" by (simp add: aux as)
- thus "\<exists>no. \<forall>n\<ge>no. dist (X (S n)) L < r" ..
-qed
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
+ assumes f: "f -- a --> l"
+ shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
+ using tendsto_compose_eventually [OF f, where F=sequentially] by simp
-
-lemma LIMSEQ_SEQ_conv2:
- fixes a :: real and L :: "'a::metric_space"
- assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
- shows "X -- a --> L"
+lemma LIMSEQ_SEQ_conv2_lemma:
+ fixes a :: "'a::metric_space"
+ assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> eventually (\<lambda>x. P (S x)) sequentially"
+ shows "eventually P (at a)"
proof (rule ccontr)
- assume "\<not> (X -- a --> L)"
- hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s --> dist (X x) L < r)"
- unfolding LIM_def dist_norm .
- hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x - a\<bar> < s --> dist (X x) L < r)" by simp
- hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> dist (X x) L \<ge> r)" by (simp add: not_less)
- then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> dist (X x) L \<ge> r))" by auto
-
- let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
- have "\<And>n. \<exists>x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
- using rdef by simp
- hence F: "\<And>n. ?F n \<noteq> a \<and> \<bar>?F n - a\<bar> < inverse (real (Suc n)) \<and> dist (X (?F n)) L \<ge> r"
+ let ?I = "\<lambda>n. inverse (real (Suc n))"
+ let ?F = "\<lambda>n::nat. SOME x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
+ assume "\<not> eventually P (at a)"
+ hence P: "\<forall>d>0. \<exists>x. x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
+ unfolding eventually_at by simp
+ hence "\<And>n. \<exists>x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
+ hence F: "\<And>n. ?F n \<noteq> a \<and> dist (?F n) a < ?I n \<and> \<not> P (?F n)"
by (rule someI_ex)
hence F1: "\<And>n. ?F n \<noteq> a"
- and F2: "\<And>n. \<bar>?F n - a\<bar> < inverse (real (Suc n))"
- and F3: "\<And>n. dist (X (?F n)) L \<ge> r"
+ and F2: "\<And>n. dist (?F n) a < ?I n"
+ and F3: "\<And>n. \<not> P (?F n)"
by fast+
-
have "?F ----> a"
- proof (rule LIMSEQ_I, unfold real_norm_def)
- fix e::real
- assume "0 < e"
- (* choose no such that inverse (real (Suc n)) < e *)
- then have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean)
- then obtain m where nodef: "inverse (real (Suc m)) < e" by auto
- show "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n - a\<bar> < e"
- proof (intro exI allI impI)
- fix n
- assume mlen: "m \<le> n"
- have "\<bar>?F n - a\<bar> < inverse (real (Suc n))"
- by (rule F2)
- also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))"
- using mlen by auto
- also from nodef have
- "inverse (real (Suc m)) < e" .
- finally show "\<bar>?F n - a\<bar> < e" .
- qed
- qed
-
+ using LIMSEQ_inverse_real_of_nat
+ by (rule metric_tendsto_imp_tendsto,
+ simp add: dist_norm F2 [THEN less_imp_le])
moreover have "\<forall>n. ?F n \<noteq> a"
by (rule allI) (rule F1)
-
- moreover note `\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L`
- ultimately have "(\<lambda>n. X (?F n)) ----> L" by simp
-
- moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)"
- proof -
- {
- fix no::nat
- obtain n where "n = no + 1" by simp
- then have nolen: "no \<le> n" by simp
- (* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
- have "dist (X (?F n)) L \<ge> r"
- by (rule F3)
- with nolen have "\<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r" by fast
- }
- then have "(\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r)" by simp
- with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> e)" by auto
- thus ?thesis by (unfold LIMSEQ_def, auto simp add: not_less)
- qed
- ultimately show False by simp
+ ultimately have "eventually (\<lambda>n. P (?F n)) sequentially"
+ using assms by simp
+ thus "False" by (simp add: F3)
qed
+lemma LIMSEQ_SEQ_conv2:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
+ assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
+ shows "f -- a --> l"
+ using assms unfolding tendsto_def [where l=l]
+ by (simp add: LIMSEQ_SEQ_conv2_lemma)
+
lemma LIMSEQ_SEQ_conv:
- "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::real) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
- (X -- a --> (L::'a::metric_space))"
-proof
- assume "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
- thus "X -- a --> L" by (rule LIMSEQ_SEQ_conv2)
-next
- assume "(X -- a --> L)"
- thus "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by (rule LIMSEQ_SEQ_conv1)
-qed
+ "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
+ (X -- a --> (L::'b::topological_space))"
+ using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
end
--- a/src/HOL/Limits.thy Wed Aug 17 23:37:23 2011 +0200
+++ b/src/HOL/Limits.thy Wed Aug 17 23:41:47 2011 +0200
@@ -627,6 +627,33 @@
by (rule eventually_mono)
qed
+lemma tendsto_compose_eventually:
+ assumes g: "(g ---> m) (at l)"
+ assumes f: "(f ---> l) F"
+ assumes inj: "eventually (\<lambda>x. f x \<noteq> l) F"
+ shows "((\<lambda>x. g (f x)) ---> m) F"
+proof (rule topological_tendstoI)
+ fix B assume B: "open B" "m \<in> B"
+ obtain A where A: "open A" "l \<in> A"
+ and gB: "\<And>y. y \<in> A \<Longrightarrow> y \<noteq> l \<Longrightarrow> g y \<in> B"
+ using topological_tendstoD [OF g B]
+ unfolding eventually_at_topological by fast
+ show "eventually (\<lambda>x. g (f x) \<in> B) F"
+ using topological_tendstoD [OF f A] inj
+ by (rule eventually_elim2) (simp add: gB)
+qed
+
+lemma metric_tendsto_imp_tendsto:
+ assumes f: "(f ---> a) F"
+ assumes le: "eventually (\<lambda>x. dist (g x) b \<le> dist (f x) a) F"
+ shows "(g ---> b) F"
+proof (rule tendstoI)
+ fix e :: real assume "0 < e"
+ with f have "eventually (\<lambda>x. dist (f x) a < e) F" by (rule tendstoD)
+ with le show "eventually (\<lambda>x. dist (g x) b < e) F"
+ using le_less_trans by (rule eventually_elim2)
+qed
+
subsubsection {* Distance and norms *}
lemma tendsto_dist [tendsto_intros]:
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Aug 17 23:37:23 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Aug 17 23:41:47 2011 +0200
@@ -1237,16 +1237,10 @@
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
assumes "eventually (\<lambda>x. norm (f x) \<le> g x) net" "(g ---> 0) net"
shows "(f ---> 0) net"
-proof(simp add: tendsto_iff, rule+)
- fix e::real assume "0<e"
- { fix x
- assume "norm (f x) \<le> g x" "dist (g x) 0 < e"
- hence "dist (f x) 0 < e" by (simp add: dist_norm)
- }
- thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
- using eventually_conj_iff[of "\<lambda>x. norm(f x) <= g x" "\<lambda>x. dist (g x) 0 < e" net]
- using eventually_mono[of "(\<lambda>x. norm (f x) \<le> g x \<and> dist (g x) 0 < e)" "(\<lambda>x. dist (f x) 0 < e)" net]
- using assms `e>0` unfolding tendsto_iff by auto
+proof (rule metric_tendsto_imp_tendsto)
+ show "(g ---> 0) net" by fact
+ show "eventually (\<lambda>x. dist (f x) 0 \<le> dist (g x) 0) net"
+ using assms(1) by (rule eventually_elim1, simp add: dist_norm)
qed
lemma Lim_transform_bound:
@@ -1254,16 +1248,8 @@
fixes g :: "'a \<Rightarrow> 'c::real_normed_vector"
assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net" "(g ---> 0) net"
shows "(f ---> 0) net"
-proof (rule tendstoI)
- fix e::real assume "e>0"
- { fix x
- assume "norm (f x) \<le> norm (g x)" "dist (g x) 0 < e"
- hence "dist (f x) 0 < e" by (simp add: dist_norm)}
- thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
- using eventually_conj_iff[of "\<lambda>x. norm (f x) \<le> norm (g x)" "\<lambda>x. dist (g x) 0 < e" net]
- using eventually_mono[of "\<lambda>x. norm (f x) \<le> norm (g x) \<and> dist (g x) 0 < e" "\<lambda>x. dist (f x) 0 < e" net]
- using assms `e>0` unfolding tendsto_iff by blast
-qed
+ using assms(1) tendsto_norm_zero [OF assms(2)]
+ by (rule Lim_null_comparison)
text{* Deducing things about the limit from the elements. *}
@@ -1287,60 +1273,45 @@
lemma Lim_dist_ubound:
assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. dist a (f x) <= e) net"
shows "dist a l <= e"
-proof (rule ccontr)
- assume "\<not> dist a l \<le> e"
- then have "0 < dist a l - e" by simp
- with assms(2) have "eventually (\<lambda>x. dist (f x) l < dist a l - e) net"
- by (rule tendstoD)
- with assms(3) have "eventually (\<lambda>x. dist a (f x) \<le> e \<and> dist (f x) l < dist a l - e) net"
- by (rule eventually_conj)
- then obtain w where "dist a (f w) \<le> e" "dist (f w) l < dist a l - e"
- using assms(1) eventually_happens by auto
- hence "dist a (f w) + dist (f w) l < e + (dist a l - e)"
- by (rule add_le_less_mono)
- hence "dist a (f w) + dist (f w) l < dist a l"
- by simp
- also have "\<dots> \<le> dist a (f w) + dist (f w) l"
- by (rule dist_triangle)
- finally show False by simp
+proof-
+ have "dist a l \<in> {..e}"
+ proof (rule Lim_in_closed_set)
+ show "closed {..e}" by simp
+ show "eventually (\<lambda>x. dist a (f x) \<in> {..e}) net" by (simp add: assms)
+ show "\<not> trivial_limit net" by fact
+ show "((\<lambda>x. dist a (f x)) ---> dist a l) net" by (intro tendsto_intros assms)
+ qed
+ thus ?thesis by simp
qed
lemma Lim_norm_ubound:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) <= e) net"
shows "norm(l) <= e"
-proof (rule ccontr)
- assume "\<not> norm l \<le> e"
- then have "0 < norm l - e" by simp
- with assms(2) have "eventually (\<lambda>x. dist (f x) l < norm l - e) net"
- by (rule tendstoD)
- with assms(3) have "eventually (\<lambda>x. norm (f x) \<le> e \<and> dist (f x) l < norm l - e) net"
- by (rule eventually_conj)
- then obtain w where "norm (f w) \<le> e" "dist (f w) l < norm l - e"
- using assms(1) eventually_happens by auto
- hence "norm (f w - l) < norm l - e" "norm (f w) \<le> e" by (simp_all add: dist_norm)
- hence "norm (f w - l) + norm (f w) < norm l" by simp
- hence "norm (f w - l - f w) < norm l" by (rule le_less_trans [OF norm_triangle_ineq4])
- thus False using `\<not> norm l \<le> e` by simp
+proof-
+ have "norm l \<in> {..e}"
+ proof (rule Lim_in_closed_set)
+ show "closed {..e}" by simp
+ show "eventually (\<lambda>x. norm (f x) \<in> {..e}) net" by (simp add: assms)
+ show "\<not> trivial_limit net" by fact
+ show "((\<lambda>x. norm (f x)) ---> norm l) net" by (intro tendsto_intros assms)
+ qed
+ thus ?thesis by simp
qed
lemma Lim_norm_lbound:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
assumes "\<not> (trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. e <= norm(f x)) net"
shows "e \<le> norm l"
-proof (rule ccontr)
- assume "\<not> e \<le> norm l"
- then have "0 < e - norm l" by simp
- with assms(2) have "eventually (\<lambda>x. dist (f x) l < e - norm l) net"
- by (rule tendstoD)
- with assms(3) have "eventually (\<lambda>x. e \<le> norm (f x) \<and> dist (f x) l < e - norm l) net"
- by (rule eventually_conj)
- then obtain w where "e \<le> norm (f w)" "dist (f w) l < e - norm l"
- using assms(1) eventually_happens by auto
- hence "norm (f w - l) + norm l < e" "e \<le> norm (f w)" by (simp_all add: dist_norm)
- hence "norm (f w - l) + norm l < norm (f w)" by (rule less_le_trans)
- hence "norm (f w - l + l) < norm (f w)" by (rule le_less_trans [OF norm_triangle_ineq])
- thus False by simp
+proof-
+ have "norm l \<in> {e..}"
+ proof (rule Lim_in_closed_set)
+ show "closed {e..}" by simp
+ show "eventually (\<lambda>x. norm (f x) \<in> {e..}) net" by (simp add: assms)
+ show "\<not> trivial_limit net" by fact
+ show "((\<lambda>x. norm (f x)) ---> norm l) net" by (intro tendsto_intros assms)
+ qed
+ thus ?thesis by simp
qed
text{* Uniqueness of the limit, when nontrivial. *}
@@ -1371,40 +1342,7 @@
fixes a :: "'a::real_normed_vector"
fixes l :: "'b::topological_space"
shows "(f ---> l) (at a) \<longleftrightarrow> ((\<lambda>x. f(a + x)) ---> l) (at 0)" (is "?lhs = ?rhs")
-proof
- assume "?lhs"
- { fix S assume "open S" "l \<in> S"
- with `?lhs` have "eventually (\<lambda>x. f x \<in> S) (at a)"
- by (rule topological_tendstoD)
- then obtain d where d: "d>0" "\<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<in> S"
- unfolding Limits.eventually_at by fast
- { fix x::"'a" assume "x \<noteq> 0 \<and> dist x 0 < d"
- hence "f (a + x) \<in> S" using d
- apply(erule_tac x="x+a" in allE)
- by (auto simp add: add_commute dist_norm dist_commute)
- }
- hence "\<exists>d>0. \<forall>x. x \<noteq> 0 \<and> dist x 0 < d \<longrightarrow> f (a + x) \<in> S"
- using d(1) by auto
- hence "eventually (\<lambda>x. f (a + x) \<in> S) (at 0)"
- unfolding Limits.eventually_at .
- }
- thus "?rhs" by (rule topological_tendstoI)
-next
- assume "?rhs"
- { fix S assume "open S" "l \<in> S"
- with `?rhs` have "eventually (\<lambda>x. f (a + x) \<in> S) (at 0)"
- by (rule topological_tendstoD)
- then obtain d where d: "d>0" "\<forall>x. x \<noteq> 0 \<and> dist x 0 < d \<longrightarrow> f (a + x) \<in> S"
- unfolding Limits.eventually_at by fast
- { fix x::"'a" assume "x \<noteq> a \<and> dist x a < d"
- hence "f x \<in> S" using d apply(erule_tac x="x-a" in allE)
- by(auto simp add: add_commute dist_norm dist_commute)
- }
- hence "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<in> S" using d(1) by auto
- hence "eventually (\<lambda>x. f x \<in> S) (at a)" unfolding Limits.eventually_at .
- }
- thus "?lhs" by (rule topological_tendstoI)
-qed
+ using LIM_offset_zero LIM_offset_zero_cancel ..
text{* It's also sometimes useful to extract the limit point from the filter. *}
@@ -1447,10 +1385,7 @@
fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector"
assumes "((\<lambda>x. f x - g x) ---> 0) net" "(f ---> l) net"
shows "(g ---> l) net"
-proof-
- from assms have "((\<lambda>x. f x - g x - f x) ---> 0 - l) net" using tendsto_diff[of "\<lambda>x. f x - g x" 0 net f l] by auto
- thus "?thesis" using tendsto_minus [of "\<lambda> x. - g x" "-l" net] by auto
-qed
+ using tendsto_diff [OF assms(2) assms(1)] by simp
lemma Lim_transform_eventually:
"eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net \<Longrightarrow> (g ---> l) net"
@@ -4882,56 +4817,28 @@
(* Moved interval_open_subset_closed a bit upwards *)
-lemma open_interval_lemma: fixes x :: "real" shows
- "a < x \<Longrightarrow> x < b ==> (\<exists>d>0. \<forall>x'. abs(x' - x) < d --> a < x' \<and> x' < b)"
- by(rule_tac x="min (x - a) (b - x)" in exI, auto)
-
-lemma open_interval[intro]: fixes a :: "'a::ordered_euclidean_space" shows "open {a<..<b}"
+lemma open_interval[intro]:
+ fixes a b :: "'a::ordered_euclidean_space" shows "open {a<..<b}"
proof-
- { fix x assume x:"x\<in>{a<..<b}"
- { fix i assume "i<DIM('a)"
- hence "\<exists>d>0. \<forall>x'. abs (x' - (x$$i)) < d \<longrightarrow> a$$i < x' \<and> x' < b$$i"
- using x[unfolded mem_interval, THEN spec[where x=i]]
- using open_interval_lemma[of "a$$i" "x$$i" "b$$i"] by auto }
- hence "\<forall>i\<in>{..<DIM('a)}. \<exists>d>0. \<forall>x'. abs (x' - (x$$i)) < d \<longrightarrow> a$$i < x' \<and> x' < b$$i" by auto
- from bchoice[OF this] guess d .. note d=this
- let ?d = "Min (d ` {..<DIM('a)})"
- have **:"finite (d ` {..<DIM('a)})" "d ` {..<DIM('a)} \<noteq> {}" by auto
- have "?d>0" using Min_gr_iff[OF **] using d by auto
- moreover
- { fix x' assume as:"dist x' x < ?d"
- { fix i assume i:"i<DIM('a)"
- hence "\<bar>x'$$i - x $$ i\<bar> < d i"
- using norm_bound_component_lt[OF as[unfolded dist_norm], of i]
- unfolding euclidean_simps Min_gr_iff[OF **] by auto
- hence "a $$ i < x' $$ i" "x' $$ i < b $$ i" using i and d[THEN bspec[where x=i]] by auto }
- hence "a < x' \<and> x' < b" apply(subst(2) eucl_less,subst(1) eucl_less) by auto }
- ultimately have "\<exists>e>0. \<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a<..<b}" by auto
- }
- thus ?thesis unfolding open_dist using open_interval_lemma by auto
-qed
-
-lemma closed_interval[intro]: fixes a :: "'a::ordered_euclidean_space" shows "closed {a .. b}"
+ have "open (\<Inter>i<DIM('a). (\<lambda>x. x$$i) -` {a$$i<..<b$$i})"
+ by (intro open_INT finite_lessThan ballI continuous_open_vimage allI
+ linear_continuous_at bounded_linear_euclidean_component
+ open_real_greaterThanLessThan)
+ also have "(\<Inter>i<DIM('a). (\<lambda>x. x$$i) -` {a$$i<..<b$$i}) = {a<..<b}"
+ by (auto simp add: eucl_less [where 'a='a])
+ finally show "open {a<..<b}" .
+qed
+
+lemma closed_interval[intro]:
+ fixes a b :: "'a::ordered_euclidean_space" shows "closed {a .. b}"
proof-
- { fix x i assume i:"i<DIM('a)"
- assume as:"\<forall>e>0. \<exists>x'\<in>{a..b}. x' \<noteq> x \<and> dist x' x < e"(* and xab:"a$$i > x$$i \<or> b$$i < x$$i"*)
- { assume xa:"a$$i > x$$i"
- with as obtain y where y:"y\<in>{a..b}" "y \<noteq> x" "dist y x < a$$i - x$$i" by(erule_tac x="a$$i - x$$i" in allE)auto
- hence False unfolding mem_interval and dist_norm
- using component_le_norm[of "y-x" i, unfolded euclidean_simps] and xa using i
- by(auto elim!: allE[where x=i])
- } hence "a$$i \<le> x$$i" by(rule ccontr)auto
- moreover
- { assume xb:"b$$i < x$$i"
- with as obtain y where y:"y\<in>{a..b}" "y \<noteq> x" "dist y x < x$$i - b$$i"
- by(erule_tac x="x$$i - b$$i" in allE)auto
- hence False unfolding mem_interval and dist_norm
- using component_le_norm[of "y-x" i, unfolded euclidean_simps] and xb using i
- by(auto elim!: allE[where x=i])
- } hence "x$$i \<le> b$$i" by(rule ccontr)auto
- ultimately
- have "a $$ i \<le> x $$ i \<and> x $$ i \<le> b $$ i" by auto }
- thus ?thesis unfolding closed_limpt islimpt_approachable mem_interval by auto
+ have "closed (\<Inter>i<DIM('a). (\<lambda>x. x$$i) -` {a$$i .. b$$i})"
+ by (intro closed_INT ballI continuous_closed_vimage allI
+ linear_continuous_at bounded_linear_euclidean_component
+ closed_real_atLeastAtMost)
+ also have "(\<Inter>i<DIM('a). (\<lambda>x. x$$i) -` {a$$i .. b$$i}) = {a .. b}"
+ by (auto simp add: eucl_le [where 'a='a])
+ finally show "closed {a .. b}" .
qed
lemma interior_closed_interval[intro]: fixes a :: "'a::ordered_euclidean_space" shows