--- a/src/HOL/Complex.thy Mon Jun 08 09:58:41 2009 +0200
+++ b/src/HOL/Complex.thy Mon Jun 08 07:22:35 2009 -0700
@@ -281,8 +281,8 @@
definition dist_complex_def:
"dist x y = cmod (x - y)"
-definition topo_complex_def [code del]:
- "topo = {S::complex set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
+definition open_complex_def [code del]:
+ "open (S :: complex set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
lemmas cmod_def = complex_norm_def
@@ -290,7 +290,7 @@
by (simp add: complex_norm_def)
instance proof
- fix r :: real and x y :: complex
+ fix r :: real and x y :: complex and S :: "complex set"
show "0 \<le> norm x"
by (induct x) simp
show "(norm x = 0) = (x = 0)"
@@ -308,8 +308,8 @@
by (rule complex_sgn_def)
show "dist x y = cmod (x - y)"
by (rule dist_complex_def)
- show "topo = {S::complex set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
- by (rule topo_complex_def)
+ show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+ by (rule open_complex_def)
qed
end
--- a/src/HOL/Library/Euclidean_Space.thy Mon Jun 08 09:58:41 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy Mon Jun 08 07:22:35 2009 -0700
@@ -331,6 +331,63 @@
lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)"
by (simp add: Cart_eq)
+subsection {* Topological space *}
+
+instantiation "^" :: (topological_space, finite) topological_space
+begin
+
+definition open_vector_def:
+ "open (S :: ('a ^ 'b) set) \<longleftrightarrow>
+ (\<forall>x\<in>S. \<exists>A. (\<forall>i. open (A i) \<and> x$i \<in> A i) \<and>
+ (\<forall>y. (\<forall>i. y$i \<in> A i) \<longrightarrow> y \<in> S))"
+
+instance proof
+ show "open (UNIV :: ('a ^ 'b) set)"
+ unfolding open_vector_def by auto
+next
+ fix S T :: "('a ^ 'b) set"
+ assume "open S" "open T" thus "open (S \<inter> T)"
+ unfolding open_vector_def
+ apply clarify
+ apply (drule (1) bspec)+
+ apply (clarify, rename_tac Sa Ta)
+ apply (rule_tac x="\<lambda>i. Sa i \<inter> Ta i" in exI)
+ apply (simp add: open_Int)
+ done
+next
+ fix K :: "('a ^ 'b) set set"
+ assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
+ unfolding open_vector_def
+ apply clarify
+ apply (drule (1) bspec)
+ apply (drule (1) bspec)
+ apply clarify
+ apply (rule_tac x=A in exI)
+ apply fast
+ done
+qed
+
+end
+
+lemma tendsto_Cart_nth:
+ fixes f :: "'a \<Rightarrow> 'b::topological_space ^ 'n::finite"
+ assumes "((\<lambda>x. f x) ---> a) net"
+ shows "((\<lambda>x. f x $ i) ---> a $ i) net"
+proof (rule topological_tendstoI)
+ fix S :: "'b set" assume "open S" "a $ i \<in> S"
+ then have "open ((\<lambda>y. y $ i) -` S)" "a \<in> ((\<lambda>y. y $ i) -` S)"
+ unfolding open_vector_def
+ apply simp_all
+ apply clarify
+ apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI)
+ apply simp
+ done
+ with assms have "eventually (\<lambda>x. f x \<in> (\<lambda>y. y $ i) -` S) net"
+ by (rule topological_tendstoD)
+ then show "eventually (\<lambda>x. f x $ i \<in> S) net"
+ by simp
+qed
+
subsection {* Square root of sum of squares *}
definition
@@ -361,6 +418,9 @@
lemma setL2_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> setL2 f A = 0"
unfolding setL2_def by simp
+lemma setL2_constant: "setL2 (\<lambda>x. y) A = sqrt (of_nat (card A)) * \<bar>y\<bar>"
+ unfolding setL2_def by (simp add: real_sqrt_mult)
+
lemma setL2_mono:
assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i"
assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
@@ -368,6 +428,14 @@
unfolding setL2_def
by (simp add: setsum_nonneg setsum_mono power_mono prems)
+lemma setL2_strict_mono:
+ assumes "finite K" and "K \<noteq> {}"
+ assumes "\<And>i. i \<in> K \<Longrightarrow> f i < g i"
+ assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
+ shows "setL2 f K < setL2 g K"
+ unfolding setL2_def
+ by (simp add: setsum_strict_mono power_strict_mono assms)
+
lemma setL2_right_distrib:
"0 \<le> r \<Longrightarrow> r * setL2 f A = setL2 (\<lambda>x. r * f x) A"
unfolding setL2_def
@@ -500,14 +568,22 @@
subsection {* Metric *}
+(* TODO: move somewhere else *)
+lemma finite_choice: "finite A \<Longrightarrow> \<forall>x\<in>A. \<exists>y. P x y \<Longrightarrow> \<exists>f. \<forall>x\<in>A. P x (f x)"
+apply (induct set: finite, simp_all)
+apply (clarify, rename_tac y)
+apply (rule_tac x="f(x:=y)" in exI, simp)
+done
+
instantiation "^" :: (metric_space, finite) metric_space
begin
definition dist_vector_def:
"dist (x::'a^'b) (y::'a^'b) = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
-definition topo_vector_def:
- "topo = {S::('a ^ 'b) set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
+lemma dist_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
+unfolding dist_vector_def
+by (rule member_le_setL2) simp_all
instance proof
fix x y :: "'a ^ 'b"
@@ -522,34 +598,48 @@
apply (simp add: setL2_mono dist_triangle2)
done
next
- show "topo = {S::('a ^ 'b) set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
- by (rule topo_vector_def)
+ (* FIXME: long proof! *)
+ fix S :: "('a ^ 'b) set"
+ show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+ unfolding open_vector_def open_dist
+ apply safe
+ apply (drule (1) bspec)
+ apply clarify
+ apply (subgoal_tac "\<exists>e>0. \<forall>i y. dist y (x$i) < e \<longrightarrow> y \<in> A i")
+ apply clarify
+ apply (rule_tac x=e in exI, clarify)
+ apply (drule spec, erule mp, clarify)
+ apply (drule spec, drule spec, erule mp)
+ apply (erule le_less_trans [OF dist_nth_le])
+ apply (subgoal_tac "\<forall>i\<in>UNIV. \<exists>e>0. \<forall>y. dist y (x$i) < e \<longrightarrow> y \<in> A i")
+ apply (drule finite_choice [OF finite], clarify)
+ apply (rule_tac x="Min (range f)" in exI, simp)
+ apply clarify
+ apply (drule_tac x=i in spec, clarify)
+ apply (erule (1) bspec)
+ apply (drule (1) bspec, clarify)
+ apply (subgoal_tac "\<exists>r. (\<forall>i::'b. 0 < r i) \<and> e = setL2 r UNIV")
+ apply clarify
+ apply (rule_tac x="\<lambda>i. {y. dist y (x$i) < r i}" in exI)
+ apply (rule conjI)
+ apply clarify
+ apply (rule conjI)
+ apply (clarify, rename_tac y)
+ apply (rule_tac x="r i - dist y (x$i)" in exI, rule conjI, simp)
+ apply clarify
+ apply (simp only: less_diff_eq)
+ apply (erule le_less_trans [OF dist_triangle])
+ apply simp
+ apply clarify
+ apply (drule spec, erule mp)
+ apply (simp add: dist_vector_def setL2_strict_mono)
+ apply (rule_tac x="\<lambda>i. e / sqrt (of_nat CARD('b))" in exI)
+ apply (simp add: divide_pos_pos setL2_constant)
+ done
qed
end
-lemma dist_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
-unfolding dist_vector_def
-by (rule member_le_setL2) simp_all
-
-lemma tendsto_Cart_nth:
- fixes X :: "'a \<Rightarrow> 'b::metric_space ^ 'n::finite"
- assumes "tendsto (\<lambda>n. X n) a net"
- shows "tendsto (\<lambda>n. X n $ i) (a $ i) net"
-proof (rule tendstoI)
- fix e :: real assume "0 < e"
- with assms have "eventually (\<lambda>n. dist (X n) a < e) net"
- by (rule tendstoD)
- thus "eventually (\<lambda>n. dist (X n $ i) (a $ i) < e) net"
- proof (rule eventually_elim1)
- fix n :: 'a
- have "dist (X n $ i) (a $ i) \<le> dist (X n) a"
- by (rule dist_nth_le)
- also assume "dist (X n) a < e"
- finally show "dist (X n $ i) (a $ i) < e" .
- qed
-qed
-
lemma LIMSEQ_Cart_nth:
"(X ----> a) \<Longrightarrow> (\<lambda>n. X n $ i) ----> a $ i"
unfolding LIMSEQ_conv_tendsto by (rule tendsto_Cart_nth)
--- a/src/HOL/Library/Inner_Product.thy Mon Jun 08 09:58:41 2009 +0200
+++ b/src/HOL/Library/Inner_Product.thy Mon Jun 08 07:22:35 2009 -0700
@@ -10,7 +10,13 @@
subsection {* Real inner product spaces *}
-text {* Temporarily relax constraints for @{term dist} and @{term norm}. *}
+text {*
+ Temporarily relax type constraints for @{term "open"},
+ @{term dist}, and @{term norm}.
+*}
+
+setup {* Sign.add_const_constraint
+ (@{const_name "open"}, SOME @{typ "'a::open set \<Rightarrow> bool"}) *}
setup {* Sign.add_const_constraint
(@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"}) *}
@@ -18,7 +24,7 @@
setup {* Sign.add_const_constraint
(@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"}) *}
-class real_inner = real_vector + sgn_div_norm + dist_norm + topo_dist +
+class real_inner = real_vector + sgn_div_norm + dist_norm + open_dist +
fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
assumes inner_commute: "inner x y = inner y x"
and inner_left_distrib: "inner (x + y) z = inner x z + inner y z"
@@ -124,7 +130,13 @@
end
-text {* Re-enable constraints for @{term dist} and @{term norm}. *}
+text {*
+ Re-enable constraints for @{term "open"},
+ @{term dist}, and @{term norm}.
+*}
+
+setup {* Sign.add_const_constraint
+ (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"}) *}
setup {* Sign.add_const_constraint
(@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"}) *}
--- a/src/HOL/Library/Product_Vector.thy Mon Jun 08 09:58:41 2009 +0200
+++ b/src/HOL/Library/Product_Vector.thy Mon Jun 08 07:22:35 2009 -0700
@@ -45,29 +45,29 @@
"*" :: (topological_space, topological_space) topological_space
begin
-definition topo_prod_def:
- "topo = {S. \<forall>x\<in>S. \<exists>A\<in>topo. \<exists>B\<in>topo. x \<in> A \<times> B \<and> A \<times> B \<subseteq> S}"
+definition open_prod_def:
+ "open (S :: ('a \<times> 'b) set) \<longleftrightarrow>
+ (\<forall>x\<in>S. \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S)"
instance proof
- show "(UNIV :: ('a \<times> 'b) set) \<in> topo"
- unfolding topo_prod_def by (auto intro: topo_UNIV)
+ show "open (UNIV :: ('a \<times> 'b) set)"
+ unfolding open_prod_def by auto
next
fix S T :: "('a \<times> 'b) set"
- assume "S \<in> topo" "T \<in> topo" thus "S \<inter> T \<in> topo"
- unfolding topo_prod_def
+ assume "open S" "open T" thus "open (S \<inter> T)"
+ unfolding open_prod_def
apply clarify
apply (drule (1) bspec)+
apply (clarify, rename_tac Sa Ta Sb Tb)
- apply (rule_tac x="Sa \<inter> Ta" in rev_bexI)
- apply (simp add: topo_Int)
- apply (rule_tac x="Sb \<inter> Tb" in rev_bexI)
- apply (simp add: topo_Int)
+ apply (rule_tac x="Sa \<inter> Ta" in exI)
+ apply (rule_tac x="Sb \<inter> Tb" in exI)
+ apply (simp add: open_Int)
apply fast
done
next
- fix T :: "('a \<times> 'b) set set"
- assume "T \<subseteq> topo" thus "\<Union>T \<in> topo"
- unfolding topo_prod_def Bex_def by fast
+ fix K :: "('a \<times> 'b) set set"
+ assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
+ unfolding open_prod_def by fast
qed
end
@@ -104,9 +104,10 @@
(* FIXME: long proof! *)
(* Maybe it would be easier to define topological spaces *)
(* in terms of neighborhoods instead of open sets? *)
- show "topo = {S::('a \<times> 'b) set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
- unfolding topo_prod_def topo_dist
- apply (safe, rename_tac S a b)
+ fix S :: "('a \<times> 'b) set"
+ show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+ unfolding open_prod_def open_dist
+ apply safe
apply (drule (1) bspec)
apply clarify
apply (drule (1) bspec)+
@@ -121,18 +122,19 @@
apply (drule spec, erule mp)
apply (erule le_less_trans [OF real_sqrt_sum_squares_ge2])
- apply (rename_tac S a b)
apply (drule (1) bspec)
apply clarify
apply (subgoal_tac "\<exists>r>0. \<exists>s>0. e = sqrt (r\<twosuperior> + s\<twosuperior>)")
apply clarify
- apply (rule_tac x="{y. dist y a < r}" in rev_bexI)
+ apply (rule_tac x="{y. dist y a < r}" in exI)
+ apply (rule_tac x="{y. dist y b < s}" in exI)
+ apply (rule conjI)
apply clarify
apply (rule_tac x="r - dist x a" in exI, rule conjI, simp)
apply clarify
apply (rule le_less_trans [OF dist_triangle])
apply (erule less_le_trans [OF add_strict_right_mono], simp)
- apply (rule_tac x="{y. dist y b < s}" in rev_bexI)
+ apply (rule conjI)
apply clarify
apply (rule_tac x="s - dist x b" in exI, rule conjI, simp)
apply clarify
@@ -160,45 +162,61 @@
unfolding dist_prod_def by simp
lemma tendsto_fst:
- assumes "tendsto f a net"
- shows "tendsto (\<lambda>x. fst (f x)) (fst a) net"
-proof (rule tendstoI)
- fix r :: real assume "0 < r"
- have "eventually (\<lambda>x. dist (f x) a < r) net"
- using `tendsto f a net` `0 < r` by (rule tendstoD)
- thus "eventually (\<lambda>x. dist (fst (f x)) (fst a) < r) net"
- by (rule eventually_elim1)
- (rule le_less_trans [OF dist_fst_le])
+ assumes "(f ---> a) net"
+ shows "((\<lambda>x. fst (f x)) ---> fst a) net"
+proof (rule topological_tendstoI)
+ fix S assume "open S" "fst a \<in> S"
+ then have "open (fst -` S)" "a \<in> fst -` S"
+ unfolding open_prod_def
+ apply simp_all
+ apply clarify
+ apply (rule exI, erule conjI)
+ apply (rule exI, rule conjI [OF open_UNIV])
+ apply auto
+ done
+ with assms have "eventually (\<lambda>x. f x \<in> fst -` S) net"
+ by (rule topological_tendstoD)
+ then show "eventually (\<lambda>x. fst (f x) \<in> S) net"
+ by simp
qed
lemma tendsto_snd:
- assumes "tendsto f a net"
- shows "tendsto (\<lambda>x. snd (f x)) (snd a) net"
-proof (rule tendstoI)
- fix r :: real assume "0 < r"
- have "eventually (\<lambda>x. dist (f x) a < r) net"
- using `tendsto f a net` `0 < r` by (rule tendstoD)
- thus "eventually (\<lambda>x. dist (snd (f x)) (snd a) < r) net"
- by (rule eventually_elim1)
- (rule le_less_trans [OF dist_snd_le])
+ assumes "(f ---> a) net"
+ shows "((\<lambda>x. snd (f x)) ---> snd a) net"
+proof (rule topological_tendstoI)
+ fix S assume "open S" "snd a \<in> S"
+ then have "open (snd -` S)" "a \<in> snd -` S"
+ unfolding open_prod_def
+ apply simp_all
+ apply clarify
+ apply (rule exI, rule conjI [OF open_UNIV])
+ apply (rule exI, erule conjI)
+ apply auto
+ done
+ with assms have "eventually (\<lambda>x. f x \<in> snd -` S) net"
+ by (rule topological_tendstoD)
+ then show "eventually (\<lambda>x. snd (f x) \<in> S) net"
+ by simp
qed
lemma tendsto_Pair:
- assumes "tendsto X a net" and "tendsto Y b net"
- shows "tendsto (\<lambda>i. (X i, Y i)) (a, b) net"
-proof (rule tendstoI)
- fix r :: real assume "0 < r"
- then have "0 < r / sqrt 2" (is "0 < ?s")
- by (simp add: divide_pos_pos)
- have "eventually (\<lambda>i. dist (X i) a < ?s) net"
- using `tendsto X a net` `0 < ?s` by (rule tendstoD)
+ assumes "(f ---> a) net" and "(g ---> b) net"
+ shows "((\<lambda>x. (f x, g x)) ---> (a, b)) net"
+proof (rule topological_tendstoI)
+ fix S assume "open S" "(a, b) \<in> S"
+ then obtain A B where "open A" "open B" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S"
+ unfolding open_prod_def by auto
+ have "eventually (\<lambda>x. f x \<in> A) net"
+ using `(f ---> a) net` `open A` `a \<in> A`
+ by (rule topological_tendstoD)
moreover
- have "eventually (\<lambda>i. dist (Y i) b < ?s) net"
- using `tendsto Y b net` `0 < ?s` by (rule tendstoD)
+ have "eventually (\<lambda>x. g x \<in> B) net"
+ using `(g ---> b) net` `open B` `b \<in> B`
+ by (rule topological_tendstoD)
ultimately
- show "eventually (\<lambda>i. dist (X i, Y i) (a, b) < r) net"
+ show "eventually (\<lambda>x. (f x, g x) \<in> S) net"
by (rule eventually_elim2)
- (simp add: real_sqrt_sum_squares_less dist_Pair_Pair)
+ (simp add: subsetD [OF `A \<times> B \<subseteq> S`])
qed
lemma LIMSEQ_fst: "(X ----> a) \<Longrightarrow> (\<lambda>n. fst (X n)) ----> fst a"
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Mon Jun 08 09:58:41 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Mon Jun 08 07:22:35 2009 -0700
@@ -196,29 +196,9 @@
subsection{* The universal Euclidean versions are what we use most of the time *}
definition
- "open" :: "'a::topological_space set \<Rightarrow> bool" where
- "open S \<longleftrightarrow> S \<in> topo"
-
-definition
- closed :: "'a::topological_space set \<Rightarrow> bool" where
- "closed S \<longleftrightarrow> open(UNIV - S)"
-
-definition
euclidean :: "'a::topological_space topology" where
"euclidean = topology open"
-lemma open_UNIV[intro,simp]: "open UNIV"
- unfolding open_def by (rule topo_UNIV)
-
-lemma open_inter[intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)"
- unfolding open_def by (rule topo_Int)
-
-lemma open_Union[intro]: "(\<forall>S\<in>K. open S) \<Longrightarrow> open (\<Union> K)"
- unfolding open_def subset_eq [symmetric] by (rule topo_Union)
-
-lemma open_empty[intro,simp]: "open {}"
- using open_Union [of "{}"] by simp
-
lemma open_openin: "open S \<longleftrightarrow> openin euclidean S"
unfolding euclidean_def
apply (rule cong[where x=S and y=S])
@@ -235,53 +215,11 @@
by (simp add: topspace_euclidean topspace_subtopology)
lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S"
- by (simp add: closed_def closedin_def topspace_euclidean open_openin)
-
-lemma open_Un[intro]:
- fixes S T :: "'a::topological_space set"
- shows "open S \<Longrightarrow> open T \<Longrightarrow> open (S\<union>T)"
- by (auto simp add: open_openin)
+ by (simp add: closed_def closedin_def topspace_euclidean open_openin Compl_eq_Diff_UNIV)
lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
by (simp add: open_openin openin_subopen[symmetric])
-lemma closed_empty[intro, simp]: "closed {}" by (simp add: closed_closedin)
-
-lemma closed_UNIV[simp,intro]: "closed UNIV"
- by (simp add: closed_closedin topspace_euclidean[symmetric])
-
-lemma closed_Un[intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S\<union>T)"
- by (auto simp add: closed_closedin)
-
-lemma closed_Int[intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S\<inter>T)"
- by (auto simp add: closed_closedin)
-
-lemma closed_Inter[intro]: assumes H: "\<forall>S \<in>K. closed S" shows "closed (\<Inter>K)"
- using H
- unfolding closed_closedin
- apply (cases "K = {}")
- apply (simp add: closed_closedin[symmetric])
- apply (rule closedin_Inter, auto)
- done
-
-lemma open_closed: "open S \<longleftrightarrow> closed (UNIV - S)"
- by (simp add: open_openin closed_closedin topspace_euclidean openin_closedin_eq)
-
-lemma closed_open: "closed S \<longleftrightarrow> open(UNIV - S)"
- by (simp add: open_openin closed_closedin topspace_euclidean closedin_def)
-
-lemma open_diff[intro]: "open S \<Longrightarrow> closed T \<Longrightarrow> open (S - T)"
- by (auto simp add: open_openin closed_closedin)
-
-lemma closed_diff[intro]: "closed S \<Longrightarrow> open T \<Longrightarrow> closed(S-T)"
- by (auto simp add: open_openin closed_closedin)
-
-lemma open_Inter[intro]: assumes fS: "finite S" and h: "\<forall>T\<in>S. open T" shows "open (\<Inter>S)"
- using h by (induct rule: finite_induct[OF fS], auto)
-
-lemma closed_Union[intro]: assumes fS: "finite S" and h: "\<forall>T\<in>S. closed T" shows "closed (\<Union>S)"
- using h by (induct rule: finite_induct[OF fS], auto)
-
subsection{* Open and closed balls. *}
definition
@@ -317,11 +255,6 @@
subsection{* Topological properties of open balls *}
-lemma open_dist:
- fixes S :: "'a::metric_space set"
- shows "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'. dist x' x < e \<longrightarrow> x' \<in> S)"
- unfolding open_def topo_dist by simp
-
lemma diff_less_iff: "(a::real) - b > 0 \<longleftrightarrow> a > b"
"(a::real) - b < 0 \<longleftrightarrow> a < b"
"a - b < c \<longleftrightarrow> a < c +b" "a - b > c \<longleftrightarrow> a > c +b" by arith+
@@ -336,7 +269,7 @@
using dist_triangle_alt[where z=x]
apply (clarsimp simp add: diff_less_iff)
apply atomize
- apply (erule_tac x="x'" in allE)
+ apply (erule_tac x="y" in allE)
apply (erule_tac x="xa" in allE)
by arith
@@ -466,7 +399,7 @@
unfolding connected_def openin_open closedin_closed
apply (subst exists_diff) by blast
hence th0: "connected S \<longleftrightarrow> \<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (UNIV - e2) \<and> e1 \<inter> (UNIV - e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (UNIV - e2) \<inter> S \<noteq> {})"
- (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)") apply (simp add: closed_def) by metis
+ (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)") apply (simp add: closed_def Compl_eq_Diff_UNIV) by metis
have th1: "?rhs \<longleftrightarrow> \<not> (\<exists>t' t. closed t'\<and>t = S\<inter>t' \<and> t\<noteq>{} \<and> t\<noteq>S \<and> (\<exists>t'. open t' \<and> t = S \<inter> t'))"
(is "_ \<longleftrightarrow> \<not> (\<exists>t' t. ?Q t' t)")
@@ -546,9 +479,14 @@
(infixr "islimpt" 60) where
"x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))"
- (* FIXME: Sure this form is OK????*)
-lemma islimptE: assumes "x islimpt S" and "x \<in> T" and "open T"
- obtains "(\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x)"
+lemma islimptI:
+ assumes "\<And>T. x \<in> T \<Longrightarrow> open T \<Longrightarrow> \<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
+ shows "x islimpt S"
+ using assms unfolding islimpt_def by auto
+
+lemma islimptE:
+ assumes "x islimpt S" and "x \<in> T" and "open T"
+ obtains y where "y \<in> S" and "y \<in> T" and "y \<noteq> x"
using assms unfolding islimpt_def by auto
lemma islimpt_subset: "x islimpt S \<Longrightarrow> S \<subseteq> T ==> x islimpt T" by (auto simp add: islimpt_def)
@@ -617,7 +555,7 @@
lemma closed_limpt: "closed S \<longleftrightarrow> (\<forall>x. x islimpt S \<longrightarrow> x \<in> S)"
unfolding closed_def
apply (subst open_subopen)
- apply (simp add: islimpt_def subset_eq)
+ apply (simp add: islimpt_def subset_eq Compl_eq_Diff_UNIV)
by (metis DiffE DiffI UNIV_I insertCI insert_absorb mem_def)
lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
@@ -674,7 +612,7 @@
unfolding islimpt_def
apply (rule ccontr, clarsimp, rename_tac A B)
apply (drule_tac x="A \<inter> B" in spec)
- apply (auto simp add: open_inter)
+ apply (auto simp add: open_Int)
done
lemma discrete_imp_closed:
@@ -726,7 +664,7 @@
lemma interior_inter[simp]: "interior(S \<inter> T) = interior S \<inter> interior T"
apply (rule equalityI, simp)
apply (metis Int_lower1 Int_lower2 subset_interior)
- by (metis Int_mono interior_subset open_inter open_interior open_subset_interior)
+ by (metis Int_mono interior_subset open_Int open_interior open_subset_interior)
lemma interior_limit_point [intro]:
fixes x :: "'a::perfect_space"
@@ -765,7 +703,7 @@
assume "x \<notin> interior S"
with `x \<in> R` `open R` obtain y where "y \<in> R - S"
unfolding interior_def expand_set_eq by fast
- from `open R` `closed S` have "open (R - S)" by (rule open_diff)
+ from `open R` `closed S` have "open (R - S)" by (rule open_Diff)
from `R \<subseteq> S \<union> T` have "R - S \<subseteq> T" by fast
from `y \<in> R - S` `open (R - S)` `R - S \<subseteq> T` `interior T = {}`
show "False" unfolding interior_def by fast
@@ -909,31 +847,23 @@
by auto
lemma open_inter_closure_subset:
- fixes S :: "'a::metric_space set"
- (* FIXME: generalize to topological_space *)
- shows "open S \<Longrightarrow> (S \<inter> (closure T)) \<subseteq> closure(S \<inter> T)"
+ "open S \<Longrightarrow> (S \<inter> (closure T)) \<subseteq> closure(S \<inter> T)"
proof
fix x
assume as: "open S" "x \<in> S \<inter> closure T"
{ assume *:"x islimpt T"
- { fix e::real
- assume "e > 0"
- from as `open S` obtain e' where "e' > 0" and e':"\<forall>x'. dist x' x < e' \<longrightarrow> x' \<in> S"
- unfolding open_dist
- by auto
- let ?e = "min e e'"
- from `e>0` `e'>0` have "?e > 0"
- by simp
- then obtain y where y:"y\<in>T" "y \<noteq> x \<and> dist y x < ?e"
- using islimpt_approachable[of x T] using *
- by blast
- hence "\<exists>x'\<in>S \<inter> T. x' \<noteq> x \<and> dist x' x < e" using e'
- using y
- by(rule_tac x=y in bexI, simp+)
- }
- hence "x islimpt S \<inter> T"
- using islimpt_approachable[of x "S \<inter> T"]
- by blast
+ have "x islimpt (S \<inter> T)"
+ proof (rule islimptI)
+ fix A
+ assume "x \<in> A" "open A"
+ with as have "x \<in> A \<inter> S" "open (A \<inter> S)"
+ by (simp_all add: open_Int)
+ with * obtain y where "y \<in> T" "y \<in> A \<inter> S" "y \<noteq> x"
+ by (rule islimptE)
+ hence "y \<in> S \<inter> T" "y \<in> A \<and> y \<noteq> x"
+ by simp_all
+ thus "\<exists>y\<in>(S \<inter> T). y \<in> A \<and> y \<noteq> x" ..
+ qed
}
then show "x \<in> closure (S \<inter> T)" using as
unfolding closure_def
@@ -958,7 +888,7 @@
definition "frontier S = closure S - interior S"
lemma frontier_closed: "closed(frontier S)"
- by (simp add: frontier_def closed_diff closed_closure)
+ by (simp add: frontier_def closed_Diff)
lemma frontier_closures: "frontier S = (closure S) \<inter> (closure(UNIV - S))"
by (auto simp add: frontier_def interior_closure)
@@ -1030,7 +960,7 @@
lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S"
using frontier_complement frontier_subset_eq[of "UNIV - S"]
- unfolding open_closed by auto
+ unfolding open_closed Compl_eq_Diff_UNIV by auto
subsection{* Common nets and The "within" modifier for nets. *}
@@ -1069,7 +999,7 @@
thus "\<not> a islimpt S"
unfolding trivial_limit_def
unfolding Rep_net_within Rep_net_at
- unfolding islimpt_def open_def [symmetric]
+ unfolding islimpt_def
apply (clarsimp simp add: expand_set_eq)
apply (rename_tac T, rule_tac x=T in exI)
apply (clarsimp, drule_tac x=y in spec, simp)
@@ -1079,7 +1009,7 @@
thus "trivial_limit (at a within S)"
unfolding trivial_limit_def
unfolding Rep_net_within Rep_net_at
- unfolding islimpt_def open_def [symmetric]
+ unfolding islimpt_def
apply (clarsimp simp add: image_image)
apply (rule_tac x=T in image_eqI)
apply (auto simp add: expand_set_eq)
@@ -1170,49 +1100,51 @@
subsection{* Limits, defined as vacuously true when the limit is trivial. *}
-notation tendsto (infixr "--->" 55)
-
text{* Notation Lim to avoid collition with lim defined in analysis *}
-definition "Lim net f = (THE l. (f ---> l) net)"
+definition
+ Lim :: "'a net \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b" where
+ "Lim net f = (THE l. (f ---> l) net)"
lemma Lim:
"(f ---> l) net \<longleftrightarrow>
trivial_limit net \<or>
(\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
- unfolding tendsto_def trivial_limit_eq by auto
+ unfolding tendsto_iff trivial_limit_eq by auto
text{* Show that they yield usual definitions in the various cases. *}
lemma Lim_within_le: "(f ---> l)(at a within S) \<longleftrightarrow>
(\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> dist (f x) l < e)"
- by (auto simp add: tendsto_def eventually_within_le)
+ by (auto simp add: tendsto_iff eventually_within_le)
lemma Lim_within: "(f ---> l) (at a within S) \<longleftrightarrow>
(\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)"
- by (auto simp add: tendsto_def eventually_within)
+ by (auto simp add: tendsto_iff eventually_within)
lemma Lim_at: "(f ---> l) (at a) \<longleftrightarrow>
(\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)"
- by (auto simp add: tendsto_def eventually_at)
+ by (auto simp add: tendsto_iff eventually_at)
lemma Lim_at_iff_LIM: "(f ---> l) (at a) \<longleftrightarrow> f -- a --> l"
unfolding Lim_at LIM_def by (simp only: zero_less_dist_iff)
lemma Lim_at_infinity:
"(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x::real^'n::finite. norm x >= b \<longrightarrow> dist (f x) l < e)"
- by (auto simp add: tendsto_def eventually_at_infinity)
+ by (auto simp add: tendsto_iff eventually_at_infinity)
lemma Lim_sequentially:
"(S ---> l) sequentially \<longleftrightarrow>
(\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (S n) l < e)"
- by (auto simp add: tendsto_def eventually_sequentially)
+ by (auto simp add: tendsto_iff eventually_sequentially)
lemma Lim_sequentially_iff_LIMSEQ: "(S ---> l) sequentially \<longleftrightarrow> S ----> l"
unfolding Lim_sequentially LIMSEQ_def ..
-lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
- unfolding tendsto_def by (auto elim: eventually_rev_mono)
+lemma Lim_eventually:
+ fixes l :: "'a::metric_space" (* FIXME: generalize to t2_space *)
+ shows "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
+ unfolding tendsto_iff by (auto elim: eventually_rev_mono)
text{* The expected monotonicity property. *}
@@ -1227,7 +1159,8 @@
shows "(f ---> l) (net within (S \<union> T))"
using assms unfolding tendsto_def Limits.eventually_within
apply clarify
- apply (drule spec, drule (1) mp)+
+ apply (drule spec, drule (1) mp, drule (1) mp)
+ apply (drule spec, drule (1) mp, drule (1) mp)
apply (auto elim: eventually_elim2)
done
@@ -1240,9 +1173,11 @@
lemma Lim_at_within: "(f ---> l) net ==> (f ---> l)(net within S)"
unfolding tendsto_def Limits.eventually_within
+ apply (clarify, drule spec, drule (1) mp, drule (1) mp)
by (auto elim!: eventually_elim1)
lemma Lim_within_open:
+ fixes l :: "'a::metric_space" (* FIXME: generalize to topological_space *)
assumes"a \<in> S" "open S"
shows "(f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)" (is "?lhs \<longleftrightarrow> ?rhs")
proof
@@ -1253,13 +1188,13 @@
hence "eventually (\<lambda>x. x \<in> S \<longrightarrow> dist (f x) l < e) (at a)"
unfolding Limits.eventually_within .
then obtain T where "open T" "a \<in> T" "\<forall>x\<in>T. x \<noteq> a \<longrightarrow> x \<in> S \<longrightarrow> dist (f x) l < e"
- unfolding eventually_at_topological open_def by fast
+ unfolding eventually_at_topological by fast
hence "open (T \<inter> S)" "a \<in> T \<inter> S" "\<forall>x\<in>(T \<inter> S). x \<noteq> a \<longrightarrow> dist (f x) l < e"
using assms by auto
hence "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<noteq> a \<longrightarrow> dist (f x) l < e)"
by fast
hence "eventually (\<lambda>x. dist (f x) l < e) (at a)"
- unfolding eventually_at_topological open_def Bex_def .
+ unfolding eventually_at_topological .
}
thus ?rhs by (rule tendstoI)
next
@@ -1270,7 +1205,9 @@
text{* Another limit point characterization. *}
lemma islimpt_sequential:
- "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S -{x}) \<and> (f ---> x) sequentially)" (is "?lhs = ?rhs")
+ fixes x :: "'a::metric_space" (* FIXME: generalize to topological_space *)
+ shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S -{x}) \<and> (f ---> x) sequentially)"
+ (is "?lhs = ?rhs")
proof
assume ?lhs
then obtain f where f:"\<forall>y. y>0 \<longrightarrow> f y \<in> S \<and> f y \<noteq> x \<and> dist (f y) x < y"
@@ -1319,11 +1256,11 @@
apply (simp add: pos_less_divide_eq `0 < b` mult_commute)
done
}
- thus ?thesis unfolding tendsto_def by simp
+ thus ?thesis unfolding tendsto_iff by simp
qed
lemma Lim_const: "((\<lambda>x. a) ---> a) net"
- by (auto simp add: Lim trivial_limit_def)
+ unfolding tendsto_def by simp
lemma Lim_cmul:
fixes f :: "'a \<Rightarrow> real ^ 'n::finite"
@@ -1357,7 +1294,7 @@
apply simp
done
}
- thus ?thesis unfolding tendsto_def by simp
+ thus ?thesis unfolding tendsto_iff by simp
qed
lemma Lim_sub:
@@ -1379,7 +1316,7 @@
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
assumes "eventually (\<lambda>x. norm(f x) <= g x) net" "((\<lambda>x. vec1(g x)) ---> 0) net"
shows "(f ---> 0) net"
-proof(simp add: tendsto_def, rule+)
+proof(simp add: tendsto_iff, rule+)
fix e::real assume "0<e"
{ fix x
assume "norm (f x) \<le> g x" "dist (vec1 (g x)) 0 < e"
@@ -1389,12 +1326,12 @@
thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
using eventually_and[of "\<lambda>x. norm(f x) <= g x" "\<lambda>x. dist (vec1 (g x)) 0 < e" net]
using eventually_mono[of "(\<lambda>x. norm (f x) \<le> g x \<and> dist (vec1 (g x)) 0 < e)" "(\<lambda>x. dist (f x) 0 < e)" net]
- using assms `e>0` unfolding tendsto_def by auto
+ using assms `e>0` unfolding tendsto_iff by auto
qed
lemma Lim_component: "(f ---> l) net
==> ((\<lambda>a. vec1((f a :: real ^'n::finite)$i)) ---> vec1(l$i)) net"
- unfolding tendsto_def
+ unfolding tendsto_iff
apply (simp add: dist_norm vec1_sub[symmetric] norm_vec1 vector_minus_component[symmetric] del: vector_minus_component)
apply (auto simp del: vector_minus_component)
apply (erule_tac x=e in allE)
@@ -1410,7 +1347,7 @@
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(simp add: tendsto_def, rule+)
+proof(simp add: tendsto_iff, rule+)
fix e::real assume "e>0"
{ fix x
assume "norm (f x) \<le> norm (g x)" "dist (g x) 0 < e"
@@ -1418,17 +1355,18 @@
thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
using eventually_and[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_def by blast
+ using assms `e>0` unfolding tendsto_iff by blast
qed
text{* Deducing things about the limit from the elements. *}
lemma Lim_in_closed_set:
+ fixes l :: "'a::metric_space" (* FIXME: generalize to topological_space *)
assumes "closed S" "eventually (\<lambda>x. f(x) \<in> S) net" "\<not>(trivial_limit net)" "(f ---> l) net"
shows "l \<in> S"
proof (rule ccontr)
assume "l \<notin> S"
- obtain e where e:"e>0" "ball l e \<subseteq> UNIV - S" using assms(1) `l \<notin> S` unfolding closed_def open_contains_ball by auto
+ obtain e where e:"e>0" "ball l e \<subseteq> UNIV - S" using assms(1) `l \<notin> S` unfolding closed_def open_contains_ball Compl_eq_Diff_UNIV by auto
hence *:"\<forall>x. dist l x < e \<longrightarrow> x \<notin> S" by auto
have "eventually (\<lambda>x. dist (f x) l < e) net"
using assms(4) `e>0` by (rule tendstoD)
@@ -1583,17 +1521,21 @@
by (auto elim: eventually_rev_mono)
}
thus "((\<lambda>x. h (f x) (g x)) ---> h l m) net"
- unfolding tendsto_def by simp
+ unfolding tendsto_iff by simp
qed
text{* These are special for limits out of the same vector space. *}
-lemma Lim_within_id: "(id ---> a) (at a within s)" by (auto simp add: Lim_within id_def)
+lemma Lim_within_id: "(id ---> a) (at a within s)"
+ unfolding tendsto_def Limits.eventually_within eventually_at_topological
+ by auto
+
lemma Lim_at_id: "(id ---> a) (at a)"
apply (subst within_UNIV[symmetric]) by (simp add: Lim_within_id)
lemma Lim_at_zero:
fixes a :: "'a::real_normed_vector"
+ fixes l :: "'b::metric_space" (* FIXME: generalize to topological_space *)
shows "(f ---> l) (at a) \<longleftrightarrow> ((\<lambda>x. f(a + x)) ---> l) (at 0)" (is "?lhs = ?rhs")
proof
assume "?lhs"
@@ -1673,13 +1615,15 @@
qed
lemma Lim_transform_eventually:
+ fixes l :: "'a::metric_space" (* FIXME: generalize to t2_space *)
shows "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
- unfolding tendsto_def
+ unfolding tendsto_iff
apply (clarify, drule spec, drule (1) mp)
apply (erule (1) eventually_elim2, simp)
done
lemma Lim_transform_within:
+ fixes l :: "'b::metric_space" (* TODO: generalize *)
assumes "0 < d" "(\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x')"
"(f ---> l) (at x within S)"
shows "(g ---> l) (at x within S)"
@@ -1693,6 +1637,7 @@
done
lemma Lim_transform_at:
+ fixes l :: "'b::metric_space" (* TODO: generalize *)
shows "0 < d \<Longrightarrow> (\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x') \<Longrightarrow>
(f ---> l) (at x) ==> (g ---> l) (at x)"
apply (subst within_UNIV[symmetric])
@@ -1703,6 +1648,7 @@
lemma Lim_transform_away_within:
fixes a b :: "'a::metric_space"
+ fixes l :: "'b::metric_space" (* TODO: generalize *)
assumes "a\<noteq>b" "\<forall>x\<in> S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
and "(f ---> l) (at a within S)"
shows "(g ---> l) (at a within S)"
@@ -1714,6 +1660,7 @@
lemma Lim_transform_away_at:
fixes a b :: "'a::metric_space"
+ fixes l :: "'b::metric_space" (* TODO: generalize *)
assumes ab: "a\<noteq>b" and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
and fl: "(f ---> l) (at a)"
shows "(g ---> l) (at a)"
@@ -1724,6 +1671,7 @@
lemma Lim_transform_within_open:
fixes a :: "'a::metric_space"
+ fixes l :: "'b::metric_space" (* TODO: generalize *)
assumes "open S" "a \<in> S" "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x" "(f ---> l) (at a)"
shows "(g ---> l) (at a)"
proof-
@@ -1738,19 +1686,22 @@
(* FIXME: Only one congruence rule for tendsto can be used at a time! *)
lemma Lim_cong_within[cong add]:
- fixes a :: "'a::metric_space" shows
- "(\<And>x. x \<noteq> a \<Longrightarrow> f x = g x) ==> ((\<lambda>x. f x) ---> l) (at a within S) \<longleftrightarrow> ((g ---> l) (at a within S))"
+ fixes a :: "'a::metric_space"
+ fixes l :: "'b::metric_space" (* TODO: generalize *)
+ shows "(\<And>x. x \<noteq> a \<Longrightarrow> f x = g x) ==> ((\<lambda>x. f x) ---> l) (at a within S) \<longleftrightarrow> ((g ---> l) (at a within S))"
by (simp add: Lim_within dist_nz[symmetric])
lemma Lim_cong_at[cong add]:
- fixes a :: "'a::metric_space" shows
- "(\<And>x. x \<noteq> a ==> f x = g x) ==> (((\<lambda>x. f x) ---> l) (at a) \<longleftrightarrow> ((g ---> l) (at a)))"
+ fixes a :: "'a::metric_space"
+ fixes l :: "'b::metric_space" (* TODO: generalize *)
+ shows "(\<And>x. x \<noteq> a ==> f x = g x) ==> (((\<lambda>x. f x) ---> l) (at a) \<longleftrightarrow> ((g ---> l) (at a)))"
by (simp add: Lim_at dist_nz[symmetric])
text{* Useful lemmas on closure and set of possible sequential limits.*}
lemma closure_sequential:
- "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially)" (is "?lhs = ?rhs")
+ fixes l :: "'a::metric_space" (* TODO: generalize *)
+ shows "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially)" (is "?lhs = ?rhs")
proof
assume "?lhs" moreover
{ assume "l \<in> S"
@@ -1785,17 +1736,23 @@
text{* Some other lemmas about sequences. *}
-lemma seq_offset: "(f ---> l) sequentially ==> ((\<lambda>i. f( i + k)) ---> l) sequentially"
+lemma seq_offset:
+ fixes l :: "'a::metric_space" (* TODO: generalize *)
+ shows "(f ---> l) sequentially ==> ((\<lambda>i. f( i + k)) ---> l) sequentially"
apply (auto simp add: Lim_sequentially)
by (metis trans_le_add1 )
-lemma seq_offset_neg: "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
+lemma seq_offset_neg:
+ fixes l :: "'a::metric_space" (* TODO: generalize *)
+ shows "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
apply (simp add: Lim_sequentially)
apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k")
apply metis
by arith
-lemma seq_offset_rev: "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
+lemma seq_offset_rev:
+ fixes l :: "'a::metric_space" (* TODO: generalize *)
+ shows "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
apply (simp add: Lim_sequentially)
apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k \<and> (n - k) + k = n")
by metis arith
@@ -1817,6 +1774,7 @@
unfolding Collect_neg_eq [symmetric] not_le
apply (clarsimp simp add: open_dist, rename_tac y)
apply (rule_tac x="dist x y - e" in exI, clarsimp)
+apply (rename_tac x')
apply (cut_tac x=x and y=x' and z=y in dist_triangle)
apply simp
done
@@ -2019,8 +1977,9 @@
lemma lim_within_interior:
fixes x :: "'a::metric_space"
+ fixes l :: "'b::metric_space" (* TODO: generalize *)
shows "x \<in> interior S ==> ((f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x))"
- by (simp add: tendsto_def eventually_within_interior)
+ by (simp add: tendsto_iff eventually_within_interior)
lemma netlimit_within_interior:
fixes x :: "'a::{perfect_space, real_normed_vector}"
@@ -2243,7 +2202,9 @@
subsection{* Compactness (the definition is the one based on convegent subsequences). *}
-definition "compact S \<longleftrightarrow>
+definition
+ compact :: "'a::metric_space set \<Rightarrow> bool" where (* TODO: generalize *)
+ "compact S \<longleftrightarrow>
(\<forall>f. (\<forall>n::nat. f n \<in> S) \<longrightarrow>
(\<exists>l\<in>S. \<exists>r. (\<forall>m n. m < n \<longrightarrow> r m < r n) \<and> ((f o r) ---> l) sequentially))"
@@ -2258,7 +2219,9 @@
ultimately show "Suc n \<le> r (Suc n)" by auto
qed
-lemma lim_subsequence: "\<forall>m n. m < n \<longrightarrow> r m < r n \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially"
+lemma lim_subsequence:
+ fixes l :: "'a::metric_space" (* TODO: generalize *)
+ shows "\<forall>m n. m < n \<longrightarrow> r m < r n \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially"
unfolding Lim_sequentially by (simp, metis monotone_bigger le_trans)
lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
@@ -2702,6 +2665,7 @@
qed
lemma sequence_infinite_lemma:
+ fixes l :: "'a::metric_space" (* TODO: generalize *)
assumes "\<forall>n::nat. (f n \<noteq> l)" "(f ---> l) sequentially"
shows "infinite {y. (\<exists> n. y = f n)}"
proof(rule ccontr)
@@ -2716,6 +2680,7 @@
qed
lemma sequence_unique_limpt:
+ fixes l :: "'a::metric_space" (* TODO: generalize *)
assumes "\<forall>n::nat. (f n \<noteq> l)" "(f ---> l) sequentially" "l' islimpt {y. (\<exists>n. y = f n)}"
shows "l' = l"
proof(rule ccontr)
@@ -2896,7 +2861,7 @@
lemma open_delete:
fixes s :: "'a::metric_space set"
shows "open s ==> open(s - {x})"
- using open_diff[of s "{x}"] closed_sing
+ using open_Diff[of s "{x}"] closed_sing
by blast
text{* Finite intersection property. I could make it an equivalence in fact. *}
@@ -2909,7 +2874,7 @@
proof
assume as:"s \<inter> (\<Inter> f) = {}"
hence "s \<subseteq> \<Union>op - UNIV ` f" by auto
- moreover have "Ball (op - UNIV ` f) open" using open_diff closed_diff using assms(2) by auto
+ moreover have "Ball (op - UNIV ` f) open" using open_Diff closed_Diff using assms(2) by auto
ultimately obtain f' where f':"f' \<subseteq> op - UNIV ` f" "finite f'" "s \<subseteq> \<Union>f'" using assms(1)[unfolded compact_eq_heine_borel, THEN spec[where x="(\<lambda>t. UNIV - t) ` f"]] by auto
hence "finite (op - UNIV ` f') \<and> op - UNIV ` f' \<subseteq> f" by(auto simp add: Diff_Diff_Int)
hence "s \<inter> \<Inter>op - UNIV ` f' \<noteq> {}" using assms(3)[THEN spec[where x="op - UNIV ` f'"]] by auto
@@ -3051,15 +3016,18 @@
subsection{* Define continuity over a net to take in restrictions of the set. *}
-definition "continuous net f \<longleftrightarrow> (f ---> f(netlimit net)) net"
+definition
+ continuous :: "'a::metric_space net \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> bool" where
+ "continuous net f \<longleftrightarrow> (f ---> f(netlimit net)) net"
+ (* FIXME: generalize 'b to topological_space *)
lemma continuous_trivial_limit:
"trivial_limit net ==> continuous net f"
- unfolding continuous_def tendsto_def trivial_limit_eq by auto
+ unfolding continuous_def tendsto_iff trivial_limit_eq by auto
lemma continuous_within: "continuous (at x within s) f \<longleftrightarrow> (f ---> f(x)) (at x within s)"
unfolding continuous_def
- unfolding tendsto_def
+ unfolding tendsto_iff
using netlimit_within[of x s]
by (cases "trivial_limit (at x within s)") (auto simp add: trivial_limit_eventually)
@@ -3151,7 +3119,7 @@
shows "continuous_on s f"
proof(simp add: continuous_at continuous_on_def, rule, rule, rule)
fix x and e::real assume "x\<in>s" "e>0"
- hence "eventually (\<lambda>xa. dist (f xa) (f x) < e) (at x)" using assms unfolding continuous_at tendsto_def by auto
+ hence "eventually (\<lambda>xa. dist (f xa) (f x) < e) (at x)" using assms unfolding continuous_at tendsto_iff by auto
then obtain d where d:"d>0" "\<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" unfolding eventually_at by auto
{ fix x' assume "\<not> 0 < dist x' x"
hence "x=x'"
@@ -3624,7 +3592,7 @@
proof-
obtain T where T: "open T" "{x \<in> s. f x \<in> t} = s \<inter> T"
using continuous_open_in_preimage[OF assms(1,3)] unfolding openin_open by auto
- thus ?thesis using open_inter[of s T, OF assms(2)] by auto
+ thus ?thesis using open_Int[of s T, OF assms(2)] by auto
qed
lemma continuous_closed_preimage:
@@ -4027,7 +3995,7 @@
proof-
{ fix e::real and x assume "0 < dist x a" "dist x a < e" "e>0"
hence "\<bar>x $ i - a $ i\<bar> < e" using component_le_norm[of "x - a" i] unfolding dist_norm by auto }
- thus ?thesis unfolding continuous_at tendsto_def eventually_at dist_vec1 by auto
+ thus ?thesis unfolding continuous_at tendsto_iff eventually_at dist_vec1 by auto
qed
lemma continuous_on_vec1_component:
@@ -4209,7 +4177,7 @@
have "eventually (\<lambda>x. dist ((vec1 o inverse o f) x) (vec1(inverse l)) < e) net"
by (auto elim: eventually_rev_mono)
}
- thus ?thesis unfolding tendsto_def by auto
+ thus ?thesis unfolding tendsto_iff by auto
qed
lemma continuous_inv:
@@ -5060,7 +5028,7 @@
ultimately have "eventually (\<lambda>x. \<bar>a \<bullet> f x - a \<bullet> l\<bar> < e) net"
by (auto elim: eventually_rev_mono)
}
- thus ?thesis unfolding tendsto_def
+ thus ?thesis unfolding tendsto_iff
by (auto simp add: dist_vec1)
qed
@@ -5116,13 +5084,13 @@
lemma open_halfspace_lt: "open {x::real^_. a \<bullet> x < b}"
proof-
have "UNIV - {x. b \<le> a \<bullet> x} = {x. a \<bullet> x < b}" by auto
- thus ?thesis using closed_halfspace_ge[unfolded closed_def, of b a] by auto
+ thus ?thesis using closed_halfspace_ge[unfolded closed_def Compl_eq_Diff_UNIV, of b a] by auto
qed
lemma open_halfspace_gt: "open {x::real^_. a \<bullet> x > b}"
proof-
have "UNIV - {x. b \<ge> a \<bullet> x} = {x. a \<bullet> x > b}" by auto
- thus ?thesis using closed_halfspace_le[unfolded closed_def, of a b] by auto
+ thus ?thesis using closed_halfspace_le[unfolded closed_def Compl_eq_Diff_UNIV, of a b] by auto
qed
lemma open_halfspace_component_lt:
@@ -5168,11 +5136,17 @@
text{* Limits relative to a union. *}
+lemma eventually_within_Un:
+ "eventually P (net within (s \<union> t)) \<longleftrightarrow>
+ eventually P (net within s) \<and> eventually P (net within t)"
+ unfolding Limits.eventually_within
+ by (auto elim!: eventually_rev_mp)
+
lemma Lim_within_union:
"(f ---> l) (net within (s \<union> t)) \<longleftrightarrow>
(f ---> l) (net within s) \<and> (f ---> l) (net within t)"
- unfolding tendsto_def Limits.eventually_within
- by (auto elim!: eventually_elim1 intro: eventually_conjI)
+ unfolding tendsto_def
+ by (auto simp add: eventually_within_Un)
lemma continuous_on_union:
assumes "closed s" "closed t" "continuous_on s f" "continuous_on t f"
--- a/src/HOL/Lim.thy Mon Jun 08 09:58:41 2009 +0200
+++ b/src/HOL/Lim.thy Mon Jun 08 07:22:35 2009 -0700
@@ -29,8 +29,8 @@
subsection {* Limits of Functions *}
-lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> tendsto f L (at a)"
-unfolding LIM_def tendsto_def eventually_at ..
+lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> (f ---> L) (at a)"
+unfolding LIM_def tendsto_iff eventually_at ..
lemma metric_LIM_I:
"(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
--- a/src/HOL/Limits.thy Mon Jun 08 09:58:41 2009 +0200
+++ b/src/HOL/Limits.thy Mon Jun 08 07:22:35 2009 -0700
@@ -114,7 +114,7 @@
definition
at :: "'a::topological_space \<Rightarrow> 'a net" where
- [code del]: "at a = Abs_net ((\<lambda>S. S - {a}) ` {S\<in>topo. a \<in> S})"
+ [code del]: "at a = Abs_net ((\<lambda>S. S - {a}) ` {S. open S \<and> a \<in> S})"
lemma Rep_net_sequentially:
"Rep_net sequentially = range (\<lambda>n. {n..})"
@@ -136,13 +136,13 @@
done
lemma Rep_net_at:
- "Rep_net (at a) = ((\<lambda>S. S - {a}) ` {S\<in>topo. a \<in> S})"
+ "Rep_net (at a) = ((\<lambda>S. S - {a}) ` {S. open S \<and> a \<in> S})"
unfolding at_def
apply (rule Abs_net_inverse')
apply (rule image_nonempty)
-apply (rule_tac x="UNIV" in exI, simp add: topo_UNIV)
+apply (rule_tac x="UNIV" in exI, simp)
apply (clarsimp, rename_tac S T)
-apply (rule_tac x="S \<inter> T" in exI, auto simp add: topo_Int)
+apply (rule_tac x="S \<inter> T" in exI, auto simp add: open_Int)
done
lemma eventually_sequentially:
@@ -154,16 +154,16 @@
unfolding eventually_def Rep_net_within by auto
lemma eventually_at_topological:
- "eventually P (at a) \<longleftrightarrow> (\<exists>S\<in>topo. a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
+ "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
unfolding eventually_def Rep_net_at by auto
lemma eventually_at:
fixes a :: "'a::metric_space"
shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
-unfolding eventually_at_topological topo_dist
+unfolding eventually_at_topological open_dist
apply safe
apply fast
-apply (rule_tac x="{x. dist x a < d}" in bexI, simp)
+apply (rule_tac x="{x. dist x a < d}" in exI, simp)
apply clarsimp
apply (rule_tac x="d - dist x a" in exI, clarsimp)
apply (simp only: less_diff_eq)
@@ -175,20 +175,21 @@
definition
Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
- [code del]: "Bfun S net = (\<exists>K>0. eventually (\<lambda>i. norm (S i) \<le> K) net)"
+ [code del]: "Bfun f net = (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) net)"
-lemma BfunI: assumes K: "eventually (\<lambda>i. norm (X i) \<le> K) net" shows "Bfun X net"
+lemma BfunI:
+ assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) net" shows "Bfun f net"
unfolding Bfun_def
proof (intro exI conjI allI)
show "0 < max K 1" by simp
next
- show "eventually (\<lambda>i. norm (X i) \<le> max K 1) net"
+ show "eventually (\<lambda>x. norm (f x) \<le> max K 1) net"
using K by (rule eventually_elim1, simp)
qed
lemma BfunE:
- assumes "Bfun S net"
- obtains B where "0 < B" and "eventually (\<lambda>i. norm (S i) \<le> B) net"
+ assumes "Bfun f net"
+ obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) net"
using assms unfolding Bfun_def by fast
@@ -196,30 +197,30 @@
definition
Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
- [code del]: "Zfun S net = (\<forall>r>0. eventually (\<lambda>i. norm (S i) < r) net)"
+ [code del]: "Zfun f net = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) net)"
lemma ZfunI:
- "(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>i. norm (S i) < r) net) \<Longrightarrow> Zfun S net"
+ "(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) net) \<Longrightarrow> Zfun f net"
unfolding Zfun_def by simp
lemma ZfunD:
- "\<lbrakk>Zfun S net; 0 < r\<rbrakk> \<Longrightarrow> eventually (\<lambda>i. norm (S i) < r) net"
+ "\<lbrakk>Zfun f net; 0 < r\<rbrakk> \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) net"
unfolding Zfun_def by simp
lemma Zfun_ssubst:
- "eventually (\<lambda>i. X i = Y i) net \<Longrightarrow> Zfun Y net \<Longrightarrow> Zfun X net"
+ "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> Zfun g net \<Longrightarrow> Zfun f net"
unfolding Zfun_def by (auto elim!: eventually_rev_mp)
-lemma Zfun_zero: "Zfun (\<lambda>i. 0) net"
+lemma Zfun_zero: "Zfun (\<lambda>x. 0) net"
unfolding Zfun_def by simp
-lemma Zfun_norm_iff: "Zfun (\<lambda>i. norm (S i)) net = Zfun (\<lambda>i. S i) net"
+lemma Zfun_norm_iff: "Zfun (\<lambda>x. norm (f x)) net = Zfun (\<lambda>x. f x) net"
unfolding Zfun_def by simp
lemma Zfun_imp_Zfun:
- assumes X: "Zfun X net"
- assumes Y: "eventually (\<lambda>i. norm (Y i) \<le> norm (X i) * K) net"
- shows "Zfun (\<lambda>n. Y n) net"
+ assumes f: "Zfun f net"
+ assumes g: "eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) net"
+ shows "Zfun (\<lambda>x. g x) net"
proof (cases)
assume K: "0 < K"
show ?thesis
@@ -227,16 +228,16 @@
fix r::real assume "0 < r"
hence "0 < r / K"
using K by (rule divide_pos_pos)
- then have "eventually (\<lambda>i. norm (X i) < r / K) net"
- using ZfunD [OF X] by fast
- with Y show "eventually (\<lambda>i. norm (Y i) < r) net"
+ then have "eventually (\<lambda>x. norm (f x) < r / K) net"
+ using ZfunD [OF f] by fast
+ with g show "eventually (\<lambda>x. norm (g x) < r) net"
proof (rule eventually_elim2)
- fix i
- assume *: "norm (Y i) \<le> norm (X i) * K"
- assume "norm (X i) < r / K"
- hence "norm (X i) * K < r"
+ fix x
+ assume *: "norm (g x) \<le> norm (f x) * K"
+ assume "norm (f x) < r / K"
+ hence "norm (f x) * K < r"
by (simp add: pos_less_divide_eq K)
- thus "norm (Y i) < r"
+ thus "norm (g x) < r"
by (simp add: order_le_less_trans [OF *])
qed
qed
@@ -247,68 +248,68 @@
proof (rule ZfunI)
fix r :: real
assume "0 < r"
- from Y show "eventually (\<lambda>i. norm (Y i) < r) net"
+ from g show "eventually (\<lambda>x. norm (g x) < r) net"
proof (rule eventually_elim1)
- fix i
- assume "norm (Y i) \<le> norm (X i) * K"
- also have "\<dots> \<le> norm (X i) * 0"
+ fix x
+ assume "norm (g x) \<le> norm (f x) * K"
+ also have "\<dots> \<le> norm (f x) * 0"
using K norm_ge_zero by (rule mult_left_mono)
- finally show "norm (Y i) < r"
+ finally show "norm (g x) < r"
using `0 < r` by simp
qed
qed
qed
-lemma Zfun_le: "\<lbrakk>Zfun Y net; \<forall>n. norm (X n) \<le> norm (Y n)\<rbrakk> \<Longrightarrow> Zfun X net"
+lemma Zfun_le: "\<lbrakk>Zfun g net; \<forall>x. norm (f x) \<le> norm (g x)\<rbrakk> \<Longrightarrow> Zfun f net"
by (erule_tac K="1" in Zfun_imp_Zfun, simp)
lemma Zfun_add:
- assumes X: "Zfun X net" and Y: "Zfun Y net"
- shows "Zfun (\<lambda>n. X n + Y n) net"
+ assumes f: "Zfun f net" and g: "Zfun g net"
+ shows "Zfun (\<lambda>x. f x + g x) net"
proof (rule ZfunI)
fix r::real assume "0 < r"
hence r: "0 < r / 2" by simp
- have "eventually (\<lambda>i. norm (X i) < r/2) net"
- using X r by (rule ZfunD)
+ have "eventually (\<lambda>x. norm (f x) < r/2) net"
+ using f r by (rule ZfunD)
moreover
- have "eventually (\<lambda>i. norm (Y i) < r/2) net"
- using Y r by (rule ZfunD)
+ have "eventually (\<lambda>x. norm (g x) < r/2) net"
+ using g r by (rule ZfunD)
ultimately
- show "eventually (\<lambda>i. norm (X i + Y i) < r) net"
+ show "eventually (\<lambda>x. norm (f x + g x) < r) net"
proof (rule eventually_elim2)
- fix i
- assume *: "norm (X i) < r/2" "norm (Y i) < r/2"
- have "norm (X i + Y i) \<le> norm (X i) + norm (Y i)"
+ fix x
+ assume *: "norm (f x) < r/2" "norm (g x) < r/2"
+ have "norm (f x + g x) \<le> norm (f x) + norm (g x)"
by (rule norm_triangle_ineq)
also have "\<dots> < r/2 + r/2"
using * by (rule add_strict_mono)
- finally show "norm (X i + Y i) < r"
+ finally show "norm (f x + g x) < r"
by simp
qed
qed
-lemma Zfun_minus: "Zfun X net \<Longrightarrow> Zfun (\<lambda>i. - X i) net"
+lemma Zfun_minus: "Zfun f net \<Longrightarrow> Zfun (\<lambda>x. - f x) net"
unfolding Zfun_def by simp
-lemma Zfun_diff: "\<lbrakk>Zfun X net; Zfun Y net\<rbrakk> \<Longrightarrow> Zfun (\<lambda>i. X i - Y i) net"
+lemma Zfun_diff: "\<lbrakk>Zfun f net; Zfun g net\<rbrakk> \<Longrightarrow> Zfun (\<lambda>x. f x - g x) net"
by (simp only: diff_minus Zfun_add Zfun_minus)
lemma (in bounded_linear) Zfun:
- assumes X: "Zfun X net"
- shows "Zfun (\<lambda>n. f (X n)) net"
+ assumes g: "Zfun g net"
+ shows "Zfun (\<lambda>x. f (g x)) net"
proof -
obtain K where "\<And>x. norm (f x) \<le> norm x * K"
using bounded by fast
- then have "eventually (\<lambda>i. norm (f (X i)) \<le> norm (X i) * K) net"
+ then have "eventually (\<lambda>x. norm (f (g x)) \<le> norm (g x) * K) net"
by simp
- with X show ?thesis
+ with g show ?thesis
by (rule Zfun_imp_Zfun)
qed
lemma (in bounded_bilinear) Zfun:
- assumes X: "Zfun X net"
- assumes Y: "Zfun Y net"
- shows "Zfun (\<lambda>n. X n ** Y n) net"
+ assumes f: "Zfun f net"
+ assumes g: "Zfun g net"
+ shows "Zfun (\<lambda>x. f x ** g x) net"
proof (rule ZfunI)
fix r::real assume r: "0 < r"
obtain K where K: "0 < K"
@@ -316,32 +317,32 @@
using pos_bounded by fast
from K have K': "0 < inverse K"
by (rule positive_imp_inverse_positive)
- have "eventually (\<lambda>i. norm (X i) < r) net"
- using X r by (rule ZfunD)
+ have "eventually (\<lambda>x. norm (f x) < r) net"
+ using f r by (rule ZfunD)
moreover
- have "eventually (\<lambda>i. norm (Y i) < inverse K) net"
- using Y K' by (rule ZfunD)
+ have "eventually (\<lambda>x. norm (g x) < inverse K) net"
+ using g K' by (rule ZfunD)
ultimately
- show "eventually (\<lambda>i. norm (X i ** Y i) < r) net"
+ show "eventually (\<lambda>x. norm (f x ** g x) < r) net"
proof (rule eventually_elim2)
- fix i
- assume *: "norm (X i) < r" "norm (Y i) < inverse K"
- have "norm (X i ** Y i) \<le> norm (X i) * norm (Y i) * K"
+ fix x
+ assume *: "norm (f x) < r" "norm (g x) < inverse K"
+ have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K"
by (rule norm_le)
- also have "norm (X i) * norm (Y i) * K < r * inverse K * K"
+ also have "norm (f x) * norm (g x) * K < r * inverse K * K"
by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero * K)
also from K have "r * inverse K * K = r"
by simp
- finally show "norm (X i ** Y i) < r" .
+ finally show "norm (f x ** g x) < r" .
qed
qed
lemma (in bounded_bilinear) Zfun_left:
- "Zfun X net \<Longrightarrow> Zfun (\<lambda>n. X n ** a) net"
+ "Zfun f net \<Longrightarrow> Zfun (\<lambda>x. f x ** a) net"
by (rule bounded_linear_left [THEN bounded_linear.Zfun])
lemma (in bounded_bilinear) Zfun_right:
- "Zfun X net \<Longrightarrow> Zfun (\<lambda>n. a ** X n) net"
+ "Zfun f net \<Longrightarrow> Zfun (\<lambda>x. a ** f x) net"
by (rule bounded_linear_right [THEN bounded_linear.Zfun])
lemmas Zfun_mult = mult.Zfun
@@ -352,28 +353,55 @@
subsection{* Limits *}
definition
- tendsto :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool" where
- [code del]: "tendsto f l net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
+ tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
+ (infixr "--->" 55)
+where [code del]:
+ "(f ---> l) net \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
-lemma tendstoI:
- "(\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net)
- \<Longrightarrow> tendsto f l net"
+lemma topological_tendstoI:
+ "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net)
+ \<Longrightarrow> (f ---> l) net"
+ unfolding tendsto_def by auto
+
+lemma topological_tendstoD:
+ "(f ---> l) net \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net"
unfolding tendsto_def by auto
-lemma tendstoD:
- "tendsto f l net \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
- unfolding tendsto_def by auto
+lemma tendstoI:
+ assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
+ shows "(f ---> l) net"
+apply (rule topological_tendstoI)
+apply (simp add: open_dist)
+apply (drule (1) bspec, clarify)
+apply (drule assms)
+apply (erule eventually_elim1, simp)
+done
-lemma tendsto_Zfun_iff: "tendsto (\<lambda>n. X n) L net = Zfun (\<lambda>n. X n - L) net"
-by (simp only: tendsto_def Zfun_def dist_norm)
+lemma tendstoD:
+ "(f ---> l) net \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
+apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD)
+apply (clarsimp simp add: open_dist)
+apply (rule_tac x="e - dist x l" in exI, clarsimp)
+apply (simp only: less_diff_eq)
+apply (erule le_less_trans [OF dist_triangle])
+apply simp
+apply simp
+done
-lemma tendsto_const: "tendsto (\<lambda>n. k) k net"
+lemma tendsto_iff:
+ "(f ---> l) net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
+using tendstoI tendstoD by fast
+
+lemma tendsto_Zfun_iff: "(f ---> a) net = Zfun (\<lambda>x. f x - a) net"
+by (simp only: tendsto_iff Zfun_def dist_norm)
+
+lemma tendsto_const: "((\<lambda>x. k) ---> k) net"
by (simp add: tendsto_def)
lemma tendsto_norm:
fixes a :: "'a::real_normed_vector"
- shows "tendsto X a net \<Longrightarrow> tendsto (\<lambda>n. norm (X n)) (norm a) net"
-apply (simp add: tendsto_def dist_norm, safe)
+ shows "(f ---> a) net \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) net"
+apply (simp add: tendsto_iff dist_norm, safe)
apply (drule_tac x="e" in spec, safe)
apply (erule eventually_elim1)
apply (erule order_le_less_trans [OF norm_triangle_ineq3])
@@ -391,30 +419,30 @@
lemma tendsto_add:
fixes a b :: "'a::real_normed_vector"
- shows "\<lbrakk>tendsto X a net; tendsto Y b net\<rbrakk> \<Longrightarrow> tendsto (\<lambda>n. X n + Y n) (a + b) net"
+ shows "\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> a + b) net"
by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add)
lemma tendsto_minus:
fixes a :: "'a::real_normed_vector"
- shows "tendsto X a net \<Longrightarrow> tendsto (\<lambda>n. - X n) (- a) net"
+ shows "(f ---> a) net \<Longrightarrow> ((\<lambda>x. - f x) ---> - a) net"
by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus)
lemma tendsto_minus_cancel:
fixes a :: "'a::real_normed_vector"
- shows "tendsto (\<lambda>n. - X n) (- a) net \<Longrightarrow> tendsto X a net"
+ shows "((\<lambda>x. - f x) ---> - a) net \<Longrightarrow> (f ---> a) net"
by (drule tendsto_minus, simp)
lemma tendsto_diff:
fixes a b :: "'a::real_normed_vector"
- shows "\<lbrakk>tendsto X a net; tendsto Y b net\<rbrakk> \<Longrightarrow> tendsto (\<lambda>n. X n - Y n) (a - b) net"
+ shows "\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) net"
by (simp add: diff_minus tendsto_add tendsto_minus)
lemma (in bounded_linear) tendsto:
- "tendsto X a net \<Longrightarrow> tendsto (\<lambda>n. f (X n)) (f a) net"
+ "(g ---> a) net \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) net"
by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
lemma (in bounded_bilinear) tendsto:
- "\<lbrakk>tendsto X a net; tendsto Y b net\<rbrakk> \<Longrightarrow> tendsto (\<lambda>n. X n ** Y n) (a ** b) net"
+ "\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) ---> a ** b) net"
by (simp only: tendsto_Zfun_iff prod_diff_prod
Zfun_add Zfun Zfun_left Zfun_right)
@@ -422,31 +450,31 @@
subsection {* Continuity of Inverse *}
lemma (in bounded_bilinear) Zfun_prod_Bfun:
- assumes X: "Zfun X net"
- assumes Y: "Bfun Y net"
- shows "Zfun (\<lambda>n. X n ** Y n) net"
+ assumes f: "Zfun f net"
+ assumes g: "Bfun g net"
+ shows "Zfun (\<lambda>x. f x ** g x) net"
proof -
obtain K where K: "0 \<le> K"
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
using nonneg_bounded by fast
obtain B where B: "0 < B"
- and norm_Y: "eventually (\<lambda>i. norm (Y i) \<le> B) net"
- using Y by (rule BfunE)
- have "eventually (\<lambda>i. norm (X i ** Y i) \<le> norm (X i) * (B * K)) net"
- using norm_Y proof (rule eventually_elim1)
- fix i
- assume *: "norm (Y i) \<le> B"
- have "norm (X i ** Y i) \<le> norm (X i) * norm (Y i) * K"
+ and norm_g: "eventually (\<lambda>x. norm (g x) \<le> B) net"
+ using g by (rule BfunE)
+ have "eventually (\<lambda>x. norm (f x ** g x) \<le> norm (f x) * (B * K)) net"
+ using norm_g proof (rule eventually_elim1)
+ fix x
+ assume *: "norm (g x) \<le> B"
+ have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K"
by (rule norm_le)
- also have "\<dots> \<le> norm (X i) * B * K"
- by (intro mult_mono' order_refl norm_Y norm_ge_zero
+ also have "\<dots> \<le> norm (f x) * B * K"
+ by (intro mult_mono' order_refl norm_g norm_ge_zero
mult_nonneg_nonneg K *)
- also have "\<dots> = norm (X i) * (B * K)"
+ also have "\<dots> = norm (f x) * (B * K)"
by (rule mult_assoc)
- finally show "norm (X i ** Y i) \<le> norm (X i) * (B * K)" .
+ finally show "norm (f x ** g x) \<le> norm (f x) * (B * K)" .
qed
- with X show ?thesis
- by (rule Zfun_imp_Zfun)
+ with f show ?thesis
+ by (rule Zfun_imp_Zfun)
qed
lemma (in bounded_bilinear) flip:
@@ -460,10 +488,10 @@
using bounded by fast
lemma (in bounded_bilinear) Bfun_prod_Zfun:
- assumes X: "Bfun X net"
- assumes Y: "Zfun Y net"
- shows "Zfun (\<lambda>n. X n ** Y n) net"
-using flip Y X by (rule bounded_bilinear.Zfun_prod_Bfun)
+ assumes f: "Bfun f net"
+ assumes g: "Zfun g net"
+ shows "Zfun (\<lambda>x. f x ** g x) net"
+using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun)
lemma inverse_diff_inverse:
"\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
@@ -479,44 +507,44 @@
lemma Bfun_inverse:
fixes a :: "'a::real_normed_div_algebra"
- assumes X: "tendsto X a net"
+ assumes f: "(f ---> a) net"
assumes a: "a \<noteq> 0"
- shows "Bfun (\<lambda>n. inverse (X n)) net"
+ shows "Bfun (\<lambda>x. inverse (f x)) net"
proof -
from a have "0 < norm a" by simp
hence "\<exists>r>0. r < norm a" by (rule dense)
then obtain r where r1: "0 < r" and r2: "r < norm a" by fast
- have "eventually (\<lambda>i. dist (X i) a < r) net"
- using tendstoD [OF X r1] by fast
- hence "eventually (\<lambda>i. norm (inverse (X i)) \<le> inverse (norm a - r)) net"
+ have "eventually (\<lambda>x. dist (f x) a < r) net"
+ using tendstoD [OF f r1] by fast
+ hence "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse (norm a - r)) net"
proof (rule eventually_elim1)
- fix i
- assume "dist (X i) a < r"
- hence 1: "norm (X i - a) < r"
+ fix x
+ assume "dist (f x) a < r"
+ hence 1: "norm (f x - a) < r"
by (simp add: dist_norm)
- hence 2: "X i \<noteq> 0" using r2 by auto
- hence "norm (inverse (X i)) = inverse (norm (X i))"
+ hence 2: "f x \<noteq> 0" using r2 by auto
+ hence "norm (inverse (f x)) = inverse (norm (f x))"
by (rule nonzero_norm_inverse)
also have "\<dots> \<le> inverse (norm a - r)"
proof (rule le_imp_inverse_le)
show "0 < norm a - r" using r2 by simp
next
- have "norm a - norm (X i) \<le> norm (a - X i)"
+ have "norm a - norm (f x) \<le> norm (a - f x)"
by (rule norm_triangle_ineq2)
- also have "\<dots> = norm (X i - a)"
+ also have "\<dots> = norm (f x - a)"
by (rule norm_minus_commute)
also have "\<dots> < r" using 1 .
- finally show "norm a - r \<le> norm (X i)" by simp
+ finally show "norm a - r \<le> norm (f x)" by simp
qed
- finally show "norm (inverse (X i)) \<le> inverse (norm a - r)" .
+ finally show "norm (inverse (f x)) \<le> inverse (norm a - r)" .
qed
thus ?thesis by (rule BfunI)
qed
lemma tendsto_inverse_lemma:
fixes a :: "'a::real_normed_div_algebra"
- shows "\<lbrakk>tendsto X a net; a \<noteq> 0; eventually (\<lambda>i. X i \<noteq> 0) net\<rbrakk>
- \<Longrightarrow> tendsto (\<lambda>i. inverse (X i)) (inverse a) net"
+ shows "\<lbrakk>(f ---> a) net; a \<noteq> 0; eventually (\<lambda>x. f x \<noteq> 0) net\<rbrakk>
+ \<Longrightarrow> ((\<lambda>x. inverse (f x)) ---> inverse a) net"
apply (subst tendsto_Zfun_iff)
apply (rule Zfun_ssubst)
apply (erule eventually_elim1)
@@ -530,23 +558,23 @@
lemma tendsto_inverse:
fixes a :: "'a::real_normed_div_algebra"
- assumes X: "tendsto X a net"
+ assumes f: "(f ---> a) net"
assumes a: "a \<noteq> 0"
- shows "tendsto (\<lambda>i. inverse (X i)) (inverse a) net"
+ shows "((\<lambda>x. inverse (f x)) ---> inverse a) net"
proof -
from a have "0 < norm a" by simp
- with X have "eventually (\<lambda>i. dist (X i) a < norm a) net"
+ with f have "eventually (\<lambda>x. dist (f x) a < norm a) net"
by (rule tendstoD)
- then have "eventually (\<lambda>i. X i \<noteq> 0) net"
+ then have "eventually (\<lambda>x. f x \<noteq> 0) net"
unfolding dist_norm by (auto elim!: eventually_elim1)
- with X a show ?thesis
+ with f a show ?thesis
by (rule tendsto_inverse_lemma)
qed
lemma tendsto_divide:
fixes a b :: "'a::real_normed_field"
- shows "\<lbrakk>tendsto X a net; tendsto Y b net; b \<noteq> 0\<rbrakk>
- \<Longrightarrow> tendsto (\<lambda>n. X n / Y n) (a / b) net"
+ shows "\<lbrakk>(f ---> a) net; (g ---> b) net; b \<noteq> 0\<rbrakk>
+ \<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) net"
by (simp add: mult.tendsto tendsto_inverse divide_inverse)
end
--- a/src/HOL/RealVector.thy Mon Jun 08 09:58:41 2009 +0200
+++ b/src/HOL/RealVector.thy Mon Jun 08 07:22:35 2009 -0700
@@ -418,13 +418,77 @@
subsection {* Topological spaces *}
-class topo =
- fixes topo :: "'a set set"
+class "open" =
+ fixes "open" :: "'a set \<Rightarrow> bool"
+
+class topological_space = "open" +
+ assumes open_UNIV [simp, intro]: "open UNIV"
+ assumes open_Int [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)"
+ assumes open_Union [intro]: "\<forall>S\<in>K. open S \<Longrightarrow> open (\<Union> K)"
+begin
+
+definition
+ closed :: "'a set \<Rightarrow> bool" where
+ "closed S \<longleftrightarrow> open (- S)"
+
+lemma open_empty [intro, simp]: "open {}"
+ using open_Union [of "{}"] by simp
+
+lemma open_Un [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<union> T)"
+ using open_Union [of "{S, T}"] by simp
+
+lemma open_UN [intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)"
+ unfolding UN_eq by (rule open_Union) auto
+
+lemma open_INT [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
+ by (induct set: finite) auto
+
+lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
+ unfolding Inter_def by (rule open_INT)
+
+lemma closed_empty [intro, simp]: "closed {}"
+ unfolding closed_def by simp
+
+lemma closed_Un [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<union> T)"
+ unfolding closed_def by auto
-class topological_space = topo +
- assumes topo_UNIV: "UNIV \<in> topo"
- assumes topo_Int: "A \<in> topo \<Longrightarrow> B \<in> topo \<Longrightarrow> A \<inter> B \<in> topo"
- assumes topo_Union: "T \<subseteq> topo \<Longrightarrow> \<Union>T \<in> topo"
+lemma closed_Inter [intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> K)"
+ unfolding closed_def Inter_def by auto
+
+lemma closed_UNIV [intro, simp]: "closed UNIV"
+ unfolding closed_def by simp
+
+lemma closed_Int [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<inter> T)"
+ unfolding closed_def by auto
+
+lemma closed_INT [intro]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)"
+ unfolding closed_def by auto
+
+lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
+ by (induct set: finite) auto
+
+lemma closed_Union [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"
+ unfolding Union_def by (rule closed_UN)
+
+lemma open_closed: "open S \<longleftrightarrow> closed (- S)"
+ unfolding closed_def by simp
+
+lemma closed_open: "closed S \<longleftrightarrow> open (- S)"
+ unfolding closed_def by simp
+
+lemma open_Diff [intro]: "open S \<Longrightarrow> closed T \<Longrightarrow> open (S - T)"
+ unfolding closed_open Diff_eq by (rule open_Int)
+
+lemma closed_Diff [intro]: "closed S \<Longrightarrow> open T \<Longrightarrow> closed (S - T)"
+ unfolding open_closed Diff_eq by (rule closed_Int)
+
+lemma open_Compl [intro]: "closed S \<Longrightarrow> open (- S)"
+ unfolding closed_open .
+
+lemma closed_Compl [intro]: "open S \<Longrightarrow> closed (- S)"
+ unfolding open_closed .
+
+end
subsection {* Metric spaces *}
@@ -432,10 +496,10 @@
class dist =
fixes dist :: "'a \<Rightarrow> 'a \<Rightarrow> real"
-class topo_dist = topo + dist +
- assumes topo_dist: "topo = {S. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
+class open_dist = "open" + dist +
+ assumes open_dist: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
-class metric_space = topo_dist +
+class metric_space = open_dist +
assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
assumes dist_triangle2: "dist x y \<le> dist x z + dist y z"
begin
@@ -470,20 +534,20 @@
proof
have "\<exists>e::real. 0 < e"
by (fast intro: zero_less_one)
- then show "UNIV \<in> topo"
- unfolding topo_dist by simp
+ then show "open UNIV"
+ unfolding open_dist by simp
next
- fix A B assume "A \<in> topo" "B \<in> topo"
- then show "A \<inter> B \<in> topo"
- unfolding topo_dist
+ fix S T assume "open S" "open T"
+ then show "open (S \<inter> T)"
+ unfolding open_dist
apply clarify
apply (drule (1) bspec)+
apply (clarify, rename_tac r s)
apply (rule_tac x="min r s" in exI, simp)
done
next
- fix T assume "T \<subseteq> topo" thus "\<Union>T \<in> topo"
- unfolding topo_dist by fast
+ fix K assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
+ unfolding open_dist by fast
qed
end
@@ -500,7 +564,7 @@
class dist_norm = dist + norm + minus +
assumes dist_norm: "dist x y = norm (x - y)"
-class real_normed_vector = real_vector + sgn_div_norm + dist_norm + topo_dist +
+class real_normed_vector = real_vector + sgn_div_norm + dist_norm + open_dist +
assumes norm_ge_zero [simp]: "0 \<le> norm x"
and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
@@ -537,14 +601,14 @@
definition dist_real_def:
"dist x y = \<bar>x - y\<bar>"
-definition topo_real_def [code del]:
- "topo = {S::real set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
+definition open_real_def [code del]:
+ "open (S :: real set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
instance
apply (intro_classes, unfold real_norm_def real_scaleR_def)
apply (rule dist_real_def)
+apply (rule open_real_def)
apply (simp add: real_sgn_def)
-apply (rule topo_real_def)
apply (rule abs_ge_zero)
apply (rule abs_eq_0)
apply (rule abs_triangle_ineq)
@@ -735,6 +799,11 @@
subsection {* Extra type constraints *}
+text {* Only allow @{term "open"} in class @{text topological_space}. *}
+
+setup {* Sign.add_const_constraint
+ (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"}) *}
+
text {* Only allow @{term dist} in class @{text metric_space}. *}
setup {* Sign.add_const_constraint
--- a/src/HOL/SEQ.thy Mon Jun 08 09:58:41 2009 +0200
+++ b/src/HOL/SEQ.thy Mon Jun 08 07:22:35 2009 -0700
@@ -193,8 +193,8 @@
subsection {* Limits of Sequences *}
-lemma LIMSEQ_conv_tendsto: "(X ----> L) \<longleftrightarrow> tendsto X L sequentially"
-unfolding LIMSEQ_def tendsto_def eventually_sequentially ..
+lemma LIMSEQ_conv_tendsto: "(X ----> L) \<longleftrightarrow> (X ---> L) sequentially"
+unfolding LIMSEQ_def tendsto_iff eventually_sequentially ..
lemma LIMSEQ_iff:
fixes L :: "'a::real_normed_vector"