--- a/src/HOL/Filter.thy Thu Feb 18 17:53:09 2016 +0100
+++ b/src/HOL/Filter.thy Mon Feb 08 17:18:13 2016 +0100
@@ -479,6 +479,29 @@
eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>b\<in>B. eventually P (F b))"
by (subst eventually_Inf_base) auto
+lemma eventually_INF_mono:
+ assumes *: "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F i. P x"
+ assumes T1: "\<And>Q R P. (\<And>x. Q x \<and> R x \<longrightarrow> P x) \<Longrightarrow> (\<And>x. T Q x \<Longrightarrow> T R x \<Longrightarrow> T P x)"
+ assumes T2: "\<And>P. (\<And>x. P x) \<Longrightarrow> (\<And>x. T P x)"
+ assumes **: "\<And>i P. i \<in> I \<Longrightarrow> \<forall>\<^sub>F x in F i. P x \<Longrightarrow> \<forall>\<^sub>F x in F' i. T P x"
+ shows "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F' i. T P x"
+proof -
+ from * obtain X where "finite X" "X \<subseteq> I" "\<forall>\<^sub>F x in \<Sqinter>i\<in>X. F i. P x"
+ unfolding eventually_INF[of _ I] by auto
+ moreover then have "eventually (T P) (INFIMUM X F')"
+ apply (induction X arbitrary: P)
+ apply (auto simp: eventually_inf T2)
+ subgoal for x S P Q R
+ apply (intro exI[of _ "T Q"])
+ apply (auto intro!: **) []
+ apply (intro exI[of _ "T R"])
+ apply (auto intro: T1) []
+ done
+ done
+ ultimately show "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F' i. T P x"
+ by (subst eventually_INF) auto
+qed
+
subsubsection \<open>Map function for filters\<close>
@@ -530,7 +553,6 @@
by (subst (1 2) eventually_INF) auto
qed
-
subsubsection \<open>Standard filters\<close>
definition principal :: "'a set \<Rightarrow> 'a filter" where
@@ -768,9 +790,116 @@
by auto
qed (auto simp: eventually_principal intro: eventually_True)
+lemma eventually_prod1:
+ assumes "B \<noteq> bot"
+ shows "(\<forall>\<^sub>F (x, y) in A \<times>\<^sub>F B. P x) \<longleftrightarrow> (\<forall>\<^sub>F x in A. P x)"
+ unfolding eventually_prod_filter
+proof safe
+ fix R Q assume "\<forall>\<^sub>F x in A. R x" "\<forall>\<^sub>F x in B. Q x" "\<forall>x y. R x \<longrightarrow> Q y \<longrightarrow> P x"
+ moreover with \<open>B \<noteq> bot\<close> obtain y where "Q y" by (auto dest: eventually_happens)
+ ultimately show "eventually P A"
+ by (force elim: eventually_mono)
+next
+ assume "eventually P A"
+ then show "\<exists>Pf Pg. eventually Pf A \<and> eventually Pg B \<and> (\<forall>x y. Pf x \<longrightarrow> Pg y \<longrightarrow> P x)"
+ by (intro exI[of _ P] exI[of _ "\<lambda>x. True"]) auto
+qed
+
+lemma eventually_prod2:
+ assumes "A \<noteq> bot"
+ shows "(\<forall>\<^sub>F (x, y) in A \<times>\<^sub>F B. P y) \<longleftrightarrow> (\<forall>\<^sub>F y in B. P y)"
+ unfolding eventually_prod_filter
+proof safe
+ fix R Q assume "\<forall>\<^sub>F x in A. R x" "\<forall>\<^sub>F x in B. Q x" "\<forall>x y. R x \<longrightarrow> Q y \<longrightarrow> P y"
+ moreover with \<open>A \<noteq> bot\<close> obtain x where "R x" by (auto dest: eventually_happens)
+ ultimately show "eventually P B"
+ by (force elim: eventually_mono)
+next
+ assume "eventually P B"
+ then show "\<exists>Pf Pg. eventually Pf A \<and> eventually Pg B \<and> (\<forall>x y. Pf x \<longrightarrow> Pg y \<longrightarrow> P y)"
+ by (intro exI[of _ P] exI[of _ "\<lambda>x. True"]) auto
+qed
+
+lemma INF_filter_bot_base:
+ fixes F :: "'a \<Rightarrow> 'b filter"
+ assumes *: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. F k \<le> F i \<sqinter> F j"
+ shows "(INF i:I. F i) = bot \<longleftrightarrow> (\<exists>i\<in>I. F i = bot)"
+proof cases
+ assume "\<exists>i\<in>I. F i = bot"
+ moreover then have "(INF i:I. F i) \<le> bot"
+ by (auto intro: INF_lower2)
+ ultimately show ?thesis
+ by (auto simp: bot_unique)
+next
+ assume **: "\<not> (\<exists>i\<in>I. F i = bot)"
+ moreover have "(INF i:I. F i) \<noteq> bot"
+ proof cases
+ assume "I \<noteq> {}"
+ show ?thesis
+ proof (rule INF_filter_not_bot)
+ fix J assume "finite J" "J \<subseteq> I"
+ then have "\<exists>k\<in>I. F k \<le> (\<Sqinter>i\<in>J. F i)"
+ proof (induction J)
+ case empty then show ?case
+ using \<open>I \<noteq> {}\<close> by auto
+ next
+ case (insert i J)
+ moreover then obtain k where "k \<in> I" "F k \<le> (\<Sqinter>i\<in>J. F i)" by auto
+ moreover note *[of i k]
+ ultimately show ?case
+ by auto
+ qed
+ with ** show "(\<Sqinter>i\<in>J. F i) \<noteq> \<bottom>"
+ by (auto simp: bot_unique)
+ qed
+ qed (auto simp add: filter_eq_iff)
+ ultimately show ?thesis
+ by auto
+qed
+
+lemma Collect_empty_eq_bot: "Collect P = {} \<longleftrightarrow> P = \<bottom>"
+ by auto
+
+lemma prod_filter_eq_bot: "A \<times>\<^sub>F B = bot \<longleftrightarrow> A = bot \<or> B = bot"
+ unfolding prod_filter_def
+proof (subst INF_filter_bot_base; clarsimp simp: principal_eq_bot_iff Collect_empty_eq_bot bot_fun_def simp del: Collect_empty_eq)
+ fix A1 A2 B1 B2 assume "\<forall>\<^sub>F x in A. A1 x" "\<forall>\<^sub>F x in A. A2 x" "\<forall>\<^sub>F x in B. B1 x" "\<forall>\<^sub>F x in B. B2 x"
+ then show "\<exists>x. eventually x A \<and> (\<exists>y. eventually y B \<and> Collect x \<times> Collect y \<subseteq> Collect A1 \<times> Collect B1 \<and> Collect x \<times> Collect y \<subseteq> Collect A2 \<times> Collect B2)"
+ by (intro exI[of _ "\<lambda>x. A1 x \<and> A2 x"] exI[of _ "\<lambda>x. B1 x \<and> B2 x"] conjI)
+ (auto simp: eventually_conj_iff)
+next
+ show "(\<exists>x. eventually x A \<and> (\<exists>y. eventually y B \<and> (x = (\<lambda>x. False) \<or> y = (\<lambda>x. False)))) = (A = \<bottom> \<or> B = \<bottom>)"
+ by (auto simp: trivial_limit_def intro: eventually_True)
+qed
+
lemma prod_filter_mono: "F \<le> F' \<Longrightarrow> G \<le> G' \<Longrightarrow> F \<times>\<^sub>F G \<le> F' \<times>\<^sub>F G'"
by (auto simp: le_filter_def eventually_prod_filter)
+lemma prod_filter_mono_iff:
+ assumes nAB: "A \<noteq> bot" "B \<noteq> bot"
+ shows "A \<times>\<^sub>F B \<le> C \<times>\<^sub>F D \<longleftrightarrow> A \<le> C \<and> B \<le> D"
+proof safe
+ assume *: "A \<times>\<^sub>F B \<le> C \<times>\<^sub>F D"
+ moreover with assms have "A \<times>\<^sub>F B \<noteq> bot"
+ by (auto simp: bot_unique prod_filter_eq_bot)
+ ultimately have "C \<times>\<^sub>F D \<noteq> bot"
+ by (auto simp: bot_unique)
+ then have nCD: "C \<noteq> bot" "D \<noteq> bot"
+ by (auto simp: prod_filter_eq_bot)
+
+ show "A \<le> C"
+ proof (rule filter_leI)
+ fix P assume "eventually P C" with *[THEN filter_leD, of "\<lambda>(x, y). P x"] show "eventually P A"
+ using nAB nCD by (simp add: eventually_prod1 eventually_prod2)
+ qed
+
+ show "B \<le> D"
+ proof (rule filter_leI)
+ fix P assume "eventually P D" with *[THEN filter_leD, of "\<lambda>(x, y). P y"] show "eventually P B"
+ using nAB nCD by (simp add: eventually_prod1 eventually_prod2)
+ qed
+qed (intro prod_filter_mono)
+
lemma eventually_prod_same: "eventually P (F \<times>\<^sub>F F) \<longleftrightarrow>
(\<exists>Q. eventually Q F \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y)))"
unfolding eventually_prod_filter
@@ -791,6 +920,52 @@
apply auto
done
+lemma prod_filter_INF:
+ assumes "I \<noteq> {}" "J \<noteq> {}"
+ shows "(INF i:I. A i) \<times>\<^sub>F (INF j:J. B j) = (INF i:I. INF j:J. A i \<times>\<^sub>F B j)"
+proof (safe intro!: antisym INF_greatest)
+ from \<open>I \<noteq> {}\<close> obtain i where "i \<in> I" by auto
+ from \<open>J \<noteq> {}\<close> obtain j where "j \<in> J" by auto
+
+ show "(\<Sqinter>i\<in>I. \<Sqinter>j\<in>J. A i \<times>\<^sub>F B j) \<le> (\<Sqinter>i\<in>I. A i) \<times>\<^sub>F (\<Sqinter>j\<in>J. B j)"
+ unfolding prod_filter_def
+ proof (safe intro!: INF_greatest)
+ fix P Q assume P: "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. A i. P x" and Q: "\<forall>\<^sub>F x in \<Sqinter>j\<in>J. B j. Q x"
+ let ?X = "(\<Sqinter>i\<in>I. \<Sqinter>j\<in>J. \<Sqinter>(P, Q)\<in>{(P, Q). (\<forall>\<^sub>F x in A i. P x) \<and> (\<forall>\<^sub>F x in B j. Q x)}. principal {(x, y). P x \<and> Q y})"
+ have "?X \<le> principal {x. P (fst x)} \<sqinter> principal {x. Q (snd x)}"
+ proof (intro inf_greatest)
+ have "?X \<le> (\<Sqinter>i\<in>I. \<Sqinter>P\<in>{P. eventually P (A i)}. principal {x. P (fst x)})"
+ by (auto intro!: INF_greatest INF_lower2[of j] INF_lower2 \<open>j\<in>J\<close> INF_lower2[of "(_, \<lambda>x. True)"])
+ also have "\<dots> \<le> principal {x. P (fst x)}"
+ unfolding le_principal
+ proof (rule eventually_INF_mono[OF P])
+ fix i P assume "i \<in> I" "eventually P (A i)"
+ then show "\<forall>\<^sub>F x in \<Sqinter>P\<in>{P. eventually P (A i)}. principal {x. P (fst x)}. x \<in> {x. P (fst x)}"
+ unfolding le_principal[symmetric] by (auto intro!: INF_lower)
+ qed auto
+ finally show "?X \<le> principal {x. P (fst x)}" .
+
+ have "?X \<le> (\<Sqinter>i\<in>J. \<Sqinter>P\<in>{P. eventually P (B i)}. principal {x. P (snd x)})"
+ by (auto intro!: INF_greatest INF_lower2[of i] INF_lower2 \<open>i\<in>I\<close> INF_lower2[of "(\<lambda>x. True, _)"])
+ also have "\<dots> \<le> principal {x. Q (snd x)}"
+ unfolding le_principal
+ proof (rule eventually_INF_mono[OF Q])
+ fix j Q assume "j \<in> J" "eventually Q (B j)"
+ then show "\<forall>\<^sub>F x in \<Sqinter>P\<in>{P. eventually P (B j)}. principal {x. P (snd x)}. x \<in> {x. Q (snd x)}"
+ unfolding le_principal[symmetric] by (auto intro!: INF_lower)
+ qed auto
+ finally show "?X \<le> principal {x. Q (snd x)}" .
+ qed
+ also have "\<dots> = principal {(x, y). P x \<and> Q y}"
+ by auto
+ finally show "?X \<le> principal {(x, y). P x \<and> Q y}" .
+ qed
+qed (intro prod_filter_mono INF_lower)
+
+lemma filtermap_Pair: "filtermap (\<lambda>x. (f x, g x)) F \<le> filtermap f F \<times>\<^sub>F filtermap g F"
+ by (simp add: le_filter_def eventually_filtermap eventually_prod_filter)
+ (auto elim: eventually_elim2)
+
subsection \<open>Limits\<close>
definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
@@ -800,7 +975,7 @@
"_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
translations
- "LIM x F1. f :> F2" == "CONST filterlim (%x. f) F2 F1"
+ "LIM x F1. f :> F2" == "CONST filterlim (\<lambda>x. f) F2 F1"
lemma filterlim_iff:
"(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)"
@@ -907,6 +1082,11 @@
LIM x F. if P x then f x else g x :> G"
unfolding filterlim_iff eventually_inf_principal by (auto simp: eventually_conj_iff)
+lemma filterlim_Pair:
+ "LIM x F. f x :> G \<Longrightarrow> LIM x F. g x :> H \<Longrightarrow> LIM x F. (f x, g x) :> G \<times>\<^sub>F H"
+ unfolding filterlim_def
+ by (rule order_trans[OF filtermap_Pair prod_filter_mono])
+
subsection \<open>Limits to @{const at_top} and @{const at_bot}\<close>
lemma filterlim_at_top:
--- a/src/HOL/Library/Product_Vector.thy Thu Feb 18 17:53:09 2016 +0100
+++ b/src/HOL/Library/Product_Vector.thy Mon Feb 08 17:18:13 2016 +0100
@@ -40,239 +40,6 @@
end
-subsection \<open>Product is a topological space\<close>
-
-instantiation prod :: (topological_space, topological_space) topological_space
-begin
-
-definition open_prod_def[code del]:
- "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)"
-
-lemma open_prod_elim:
- assumes "open S" and "x \<in> S"
- obtains A B where "open A" and "open B" and "x \<in> A \<times> B" and "A \<times> B \<subseteq> S"
-using assms unfolding open_prod_def by fast
-
-lemma open_prod_intro:
- assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S"
- shows "open S"
-using assms unfolding open_prod_def by fast
-
-instance
-proof
- show "open (UNIV :: ('a \<times> 'b) set)"
- unfolding open_prod_def by auto
-next
- fix S T :: "('a \<times> 'b) set"
- assume "open S" "open T"
- show "open (S \<inter> T)"
- proof (rule open_prod_intro)
- fix x assume x: "x \<in> S \<inter> T"
- from x have "x \<in> S" by simp
- obtain Sa Sb where A: "open Sa" "open Sb" "x \<in> Sa \<times> Sb" "Sa \<times> Sb \<subseteq> S"
- using \<open>open S\<close> and \<open>x \<in> S\<close> by (rule open_prod_elim)
- from x have "x \<in> T" by simp
- obtain Ta Tb where B: "open Ta" "open Tb" "x \<in> Ta \<times> Tb" "Ta \<times> Tb \<subseteq> T"
- using \<open>open T\<close> and \<open>x \<in> T\<close> by (rule open_prod_elim)
- let ?A = "Sa \<inter> Ta" and ?B = "Sb \<inter> Tb"
- have "open ?A \<and> open ?B \<and> x \<in> ?A \<times> ?B \<and> ?A \<times> ?B \<subseteq> S \<inter> T"
- using A B by (auto simp add: open_Int)
- thus "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S \<inter> T"
- by fast
- qed
-next
- 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
-
-declare [[code abort: "open::('a::topological_space*'b::topological_space) set \<Rightarrow> bool"]]
-
-lemma open_Times: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<times> T)"
-unfolding open_prod_def by auto
-
-lemma fst_vimage_eq_Times: "fst -` S = S \<times> UNIV"
-by auto
-
-lemma snd_vimage_eq_Times: "snd -` S = UNIV \<times> S"
-by auto
-
-lemma open_vimage_fst: "open S \<Longrightarrow> open (fst -` S)"
-by (simp add: fst_vimage_eq_Times open_Times)
-
-lemma open_vimage_snd: "open S \<Longrightarrow> open (snd -` S)"
-by (simp add: snd_vimage_eq_Times open_Times)
-
-lemma closed_vimage_fst: "closed S \<Longrightarrow> closed (fst -` S)"
-unfolding closed_open vimage_Compl [symmetric]
-by (rule open_vimage_fst)
-
-lemma closed_vimage_snd: "closed S \<Longrightarrow> closed (snd -` S)"
-unfolding closed_open vimage_Compl [symmetric]
-by (rule open_vimage_snd)
-
-lemma closed_Times: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
-proof -
- have "S \<times> T = (fst -` S) \<inter> (snd -` T)" by auto
- thus "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
- by (simp add: closed_vimage_fst closed_vimage_snd closed_Int)
-qed
-
-lemma subset_fst_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> y \<in> B \<Longrightarrow> A \<subseteq> fst ` S"
- unfolding image_def subset_eq by force
-
-lemma subset_snd_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> x \<in> A \<Longrightarrow> B \<subseteq> snd ` S"
- unfolding image_def subset_eq by force
-
-lemma open_image_fst: assumes "open S" shows "open (fst ` S)"
-proof (rule openI)
- fix x assume "x \<in> fst ` S"
- then obtain y where "(x, y) \<in> S" by auto
- then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
- using \<open>open S\<close> unfolding open_prod_def by auto
- from \<open>A \<times> B \<subseteq> S\<close> \<open>y \<in> B\<close> have "A \<subseteq> fst ` S" by (rule subset_fst_imageI)
- with \<open>open A\<close> \<open>x \<in> A\<close> have "open A \<and> x \<in> A \<and> A \<subseteq> fst ` S" by simp
- then show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S" by - (rule exI)
-qed
-
-lemma open_image_snd: assumes "open S" shows "open (snd ` S)"
-proof (rule openI)
- fix y assume "y \<in> snd ` S"
- then obtain x where "(x, y) \<in> S" by auto
- then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
- using \<open>open S\<close> unfolding open_prod_def by auto
- from \<open>A \<times> B \<subseteq> S\<close> \<open>x \<in> A\<close> have "B \<subseteq> snd ` S" by (rule subset_snd_imageI)
- with \<open>open B\<close> \<open>y \<in> B\<close> have "open B \<and> y \<in> B \<and> B \<subseteq> snd ` S" by simp
- then show "\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> snd ` S" by - (rule exI)
-qed
-
-subsubsection \<open>Continuity of operations\<close>
-
-lemma tendsto_fst [tendsto_intros]:
- assumes "(f \<longlongrightarrow> a) F"
- shows "((\<lambda>x. fst (f x)) \<longlongrightarrow> fst a) F"
-proof (rule topological_tendstoI)
- fix S assume "open S" and "fst a \<in> S"
- then have "open (fst -` S)" and "a \<in> fst -` S"
- by (simp_all add: open_vimage_fst)
- with assms have "eventually (\<lambda>x. f x \<in> fst -` S) F"
- by (rule topological_tendstoD)
- then show "eventually (\<lambda>x. fst (f x) \<in> S) F"
- by simp
-qed
-
-lemma tendsto_snd [tendsto_intros]:
- assumes "(f \<longlongrightarrow> a) F"
- shows "((\<lambda>x. snd (f x)) \<longlongrightarrow> snd a) F"
-proof (rule topological_tendstoI)
- fix S assume "open S" and "snd a \<in> S"
- then have "open (snd -` S)" and "a \<in> snd -` S"
- by (simp_all add: open_vimage_snd)
- with assms have "eventually (\<lambda>x. f x \<in> snd -` S) F"
- by (rule topological_tendstoD)
- then show "eventually (\<lambda>x. snd (f x) \<in> S) F"
- by simp
-qed
-
-lemma tendsto_Pair [tendsto_intros]:
- assumes "(f \<longlongrightarrow> a) F" and "(g \<longlongrightarrow> b) F"
- shows "((\<lambda>x. (f x, g x)) \<longlongrightarrow> (a, b)) F"
-proof (rule topological_tendstoI)
- fix S assume "open S" and "(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 fast
- have "eventually (\<lambda>x. f x \<in> A) F"
- using \<open>(f \<longlongrightarrow> a) F\<close> \<open>open A\<close> \<open>a \<in> A\<close>
- by (rule topological_tendstoD)
- moreover
- have "eventually (\<lambda>x. g x \<in> B) F"
- using \<open>(g \<longlongrightarrow> b) F\<close> \<open>open B\<close> \<open>b \<in> B\<close>
- by (rule topological_tendstoD)
- ultimately
- show "eventually (\<lambda>x. (f x, g x) \<in> S) F"
- by (rule eventually_elim2)
- (simp add: subsetD [OF \<open>A \<times> B \<subseteq> S\<close>])
-qed
-
-lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
- unfolding continuous_def by (rule tendsto_fst)
-
-lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
- unfolding continuous_def by (rule tendsto_snd)
-
-lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
- unfolding continuous_def by (rule tendsto_Pair)
-
-lemma continuous_on_fst[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. fst (f x))"
- unfolding continuous_on_def by (auto intro: tendsto_fst)
-
-lemma continuous_on_snd[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. snd (f x))"
- unfolding continuous_on_def by (auto intro: tendsto_snd)
-
-lemma continuous_on_Pair[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. (f x, g x))"
- unfolding continuous_on_def by (auto intro: tendsto_Pair)
-
-lemma continuous_on_swap[continuous_intros]: "continuous_on A prod.swap"
- by (simp add: prod.swap_def continuous_on_fst continuous_on_snd continuous_on_Pair continuous_on_id)
-
-lemma continuous_on_swap_args:
- assumes "continuous_on (A\<times>B) (\<lambda>(x,y). d x y)"
- shows "continuous_on (B\<times>A) (\<lambda>(x,y). d y x)"
-proof -
- have "(\<lambda>(x,y). d y x) = (\<lambda>(x,y). d x y) o prod.swap"
- by force
- then show ?thesis
- apply (rule ssubst)
- apply (rule continuous_on_compose)
- apply (force intro: continuous_on_subset [OF continuous_on_swap])
- apply (force intro: continuous_on_subset [OF assms])
- done
-qed
-
-lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
- by (fact continuous_fst)
-
-lemma isCont_snd [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. snd (f x)) a"
- by (fact continuous_snd)
-
-lemma isCont_Pair [simp]: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
- by (fact continuous_Pair)
-
-subsubsection \<open>Separation axioms\<close>
-
-instance prod :: (t0_space, t0_space) t0_space
-proof
- fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
- hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
- by (simp add: prod_eq_iff)
- thus "\<exists>U. open U \<and> (x \<in> U) \<noteq> (y \<in> U)"
- by (fast dest: t0_space elim: open_vimage_fst open_vimage_snd)
-qed
-
-instance prod :: (t1_space, t1_space) t1_space
-proof
- fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
- hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
- by (simp add: prod_eq_iff)
- thus "\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
- by (fast dest: t1_space elim: open_vimage_fst open_vimage_snd)
-qed
-
-instance prod :: (t2_space, t2_space) t2_space
-proof
- fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
- hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
- by (simp add: prod_eq_iff)
- thus "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
- by (fast dest: hausdorff elim: open_vimage_fst open_vimage_snd)
-qed
-
-lemma isCont_swap[continuous_intros]: "isCont prod.swap a"
- using continuous_on_eq_continuous_within continuous_on_swap by blast
-
subsection \<open>Product is a metric space\<close>
(* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
--- a/src/HOL/Topological_Spaces.thy Thu Feb 18 17:53:09 2016 +0100
+++ b/src/HOL/Topological_Spaces.thy Mon Feb 08 17:18:13 2016 +0100
@@ -2610,4 +2610,254 @@
by (auto simp: filterlim_iff eventually_at_filter eventually_nhds_uniformity continuous_on_def
elim: eventually_mono dest!: uniformly_continuous_onD[OF f])
+section \<open>Product Topology\<close>
+
+
+subsection \<open>Product is a topological space\<close>
+
+instantiation prod :: (topological_space, topological_space) topological_space
+begin
+
+definition open_prod_def[code del]:
+ "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)"
+
+lemma open_prod_elim:
+ assumes "open S" and "x \<in> S"
+ obtains A B where "open A" and "open B" and "x \<in> A \<times> B" and "A \<times> B \<subseteq> S"
+using assms unfolding open_prod_def by fast
+
+lemma open_prod_intro:
+ assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S"
+ shows "open S"
+using assms unfolding open_prod_def by fast
+
+instance
+proof
+ show "open (UNIV :: ('a \<times> 'b) set)"
+ unfolding open_prod_def by auto
+next
+ fix S T :: "('a \<times> 'b) set"
+ assume "open S" "open T"
+ show "open (S \<inter> T)"
+ proof (rule open_prod_intro)
+ fix x assume x: "x \<in> S \<inter> T"
+ from x have "x \<in> S" by simp
+ obtain Sa Sb where A: "open Sa" "open Sb" "x \<in> Sa \<times> Sb" "Sa \<times> Sb \<subseteq> S"
+ using \<open>open S\<close> and \<open>x \<in> S\<close> by (rule open_prod_elim)
+ from x have "x \<in> T" by simp
+ obtain Ta Tb where B: "open Ta" "open Tb" "x \<in> Ta \<times> Tb" "Ta \<times> Tb \<subseteq> T"
+ using \<open>open T\<close> and \<open>x \<in> T\<close> by (rule open_prod_elim)
+ let ?A = "Sa \<inter> Ta" and ?B = "Sb \<inter> Tb"
+ have "open ?A \<and> open ?B \<and> x \<in> ?A \<times> ?B \<and> ?A \<times> ?B \<subseteq> S \<inter> T"
+ using A B by (auto simp add: open_Int)
+ thus "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S \<inter> T"
+ by fast
+ qed
+next
+ 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
+
+declare [[code abort: "open::('a::topological_space*'b::topological_space) set \<Rightarrow> bool"]]
+
+lemma open_Times: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<times> T)"
+unfolding open_prod_def by auto
+
+lemma fst_vimage_eq_Times: "fst -` S = S \<times> UNIV"
+by auto
+
+lemma snd_vimage_eq_Times: "snd -` S = UNIV \<times> S"
+by auto
+
+lemma open_vimage_fst: "open S \<Longrightarrow> open (fst -` S)"
+by (simp add: fst_vimage_eq_Times open_Times)
+
+lemma open_vimage_snd: "open S \<Longrightarrow> open (snd -` S)"
+by (simp add: snd_vimage_eq_Times open_Times)
+
+lemma closed_vimage_fst: "closed S \<Longrightarrow> closed (fst -` S)"
+unfolding closed_open vimage_Compl [symmetric]
+by (rule open_vimage_fst)
+
+lemma closed_vimage_snd: "closed S \<Longrightarrow> closed (snd -` S)"
+unfolding closed_open vimage_Compl [symmetric]
+by (rule open_vimage_snd)
+
+lemma closed_Times: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
+proof -
+ have "S \<times> T = (fst -` S) \<inter> (snd -` T)" by auto
+ thus "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
+ by (simp add: closed_vimage_fst closed_vimage_snd closed_Int)
+qed
+
+lemma subset_fst_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> y \<in> B \<Longrightarrow> A \<subseteq> fst ` S"
+ unfolding image_def subset_eq by force
+
+lemma subset_snd_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> x \<in> A \<Longrightarrow> B \<subseteq> snd ` S"
+ unfolding image_def subset_eq by force
+
+lemma open_image_fst: assumes "open S" shows "open (fst ` S)"
+proof (rule openI)
+ fix x assume "x \<in> fst ` S"
+ then obtain y where "(x, y) \<in> S" by auto
+ then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
+ using \<open>open S\<close> unfolding open_prod_def by auto
+ from \<open>A \<times> B \<subseteq> S\<close> \<open>y \<in> B\<close> have "A \<subseteq> fst ` S" by (rule subset_fst_imageI)
+ with \<open>open A\<close> \<open>x \<in> A\<close> have "open A \<and> x \<in> A \<and> A \<subseteq> fst ` S" by simp
+ then show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S" by - (rule exI)
+qed
+
+lemma open_image_snd: assumes "open S" shows "open (snd ` S)"
+proof (rule openI)
+ fix y assume "y \<in> snd ` S"
+ then obtain x where "(x, y) \<in> S" by auto
+ then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
+ using \<open>open S\<close> unfolding open_prod_def by auto
+ from \<open>A \<times> B \<subseteq> S\<close> \<open>x \<in> A\<close> have "B \<subseteq> snd ` S" by (rule subset_snd_imageI)
+ with \<open>open B\<close> \<open>y \<in> B\<close> have "open B \<and> y \<in> B \<and> B \<subseteq> snd ` S" by simp
+ then show "\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> snd ` S" by - (rule exI)
+qed
+
+lemma nhds_prod: "nhds (a, b) = nhds a \<times>\<^sub>F nhds b"
+ unfolding nhds_def
+proof (subst prod_filter_INF, auto intro!: antisym INF_greatest simp: principal_prod_principal)
+ fix S T assume "open S" "a \<in> S" "open T" "b \<in> T"
+ then show "(INF x : {S. open S \<and> (a, b) \<in> S}. principal x) \<le> principal (S \<times> T)"
+ by (intro INF_lower) (auto intro!: open_Times)
+next
+ fix S' assume "open S'" "(a, b) \<in> S'"
+ then obtain S T where "open S" "a \<in> S" "open T" "b \<in> T" "S \<times> T \<subseteq> S'"
+ by (auto elim: open_prod_elim)
+ then show "(INF x : {S. open S \<and> a \<in> S}. INF y : {S. open S \<and> b \<in> S}. principal (x \<times> y)) \<le> principal S'"
+ by (auto intro!: INF_lower2)
+qed
+
+subsubsection \<open>Continuity of operations\<close>
+
+lemma tendsto_fst [tendsto_intros]:
+ assumes "(f \<longlongrightarrow> a) F"
+ shows "((\<lambda>x. fst (f x)) \<longlongrightarrow> fst a) F"
+proof (rule topological_tendstoI)
+ fix S assume "open S" and "fst a \<in> S"
+ then have "open (fst -` S)" and "a \<in> fst -` S"
+ by (simp_all add: open_vimage_fst)
+ with assms have "eventually (\<lambda>x. f x \<in> fst -` S) F"
+ by (rule topological_tendstoD)
+ then show "eventually (\<lambda>x. fst (f x) \<in> S) F"
+ by simp
+qed
+
+lemma tendsto_snd [tendsto_intros]:
+ assumes "(f \<longlongrightarrow> a) F"
+ shows "((\<lambda>x. snd (f x)) \<longlongrightarrow> snd a) F"
+proof (rule topological_tendstoI)
+ fix S assume "open S" and "snd a \<in> S"
+ then have "open (snd -` S)" and "a \<in> snd -` S"
+ by (simp_all add: open_vimage_snd)
+ with assms have "eventually (\<lambda>x. f x \<in> snd -` S) F"
+ by (rule topological_tendstoD)
+ then show "eventually (\<lambda>x. snd (f x) \<in> S) F"
+ by simp
+qed
+
+lemma tendsto_Pair [tendsto_intros]:
+ assumes "(f \<longlongrightarrow> a) F" and "(g \<longlongrightarrow> b) F"
+ shows "((\<lambda>x. (f x, g x)) \<longlongrightarrow> (a, b)) F"
+proof (rule topological_tendstoI)
+ fix S assume "open S" and "(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 fast
+ have "eventually (\<lambda>x. f x \<in> A) F"
+ using \<open>(f \<longlongrightarrow> a) F\<close> \<open>open A\<close> \<open>a \<in> A\<close>
+ by (rule topological_tendstoD)
+ moreover
+ have "eventually (\<lambda>x. g x \<in> B) F"
+ using \<open>(g \<longlongrightarrow> b) F\<close> \<open>open B\<close> \<open>b \<in> B\<close>
+ by (rule topological_tendstoD)
+ ultimately
+ show "eventually (\<lambda>x. (f x, g x) \<in> S) F"
+ by (rule eventually_elim2)
+ (simp add: subsetD [OF \<open>A \<times> B \<subseteq> S\<close>])
+qed
+
+lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
+ unfolding continuous_def by (rule tendsto_fst)
+
+lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
+ unfolding continuous_def by (rule tendsto_snd)
+
+lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
+ unfolding continuous_def by (rule tendsto_Pair)
+
+lemma continuous_on_fst[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. fst (f x))"
+ unfolding continuous_on_def by (auto intro: tendsto_fst)
+
+lemma continuous_on_snd[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. snd (f x))"
+ unfolding continuous_on_def by (auto intro: tendsto_snd)
+
+lemma continuous_on_Pair[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. (f x, g x))"
+ unfolding continuous_on_def by (auto intro: tendsto_Pair)
+
+lemma continuous_on_swap[continuous_intros]: "continuous_on A prod.swap"
+ by (simp add: prod.swap_def continuous_on_fst continuous_on_snd continuous_on_Pair continuous_on_id)
+
+lemma continuous_on_swap_args:
+ assumes "continuous_on (A\<times>B) (\<lambda>(x,y). d x y)"
+ shows "continuous_on (B\<times>A) (\<lambda>(x,y). d y x)"
+proof -
+ have "(\<lambda>(x,y). d y x) = (\<lambda>(x,y). d x y) o prod.swap"
+ by force
+ then show ?thesis
+ apply (rule ssubst)
+ apply (rule continuous_on_compose)
+ apply (force intro: continuous_on_subset [OF continuous_on_swap])
+ apply (force intro: continuous_on_subset [OF assms])
+ done
+qed
+
+lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
+ by (fact continuous_fst)
+
+lemma isCont_snd [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. snd (f x)) a"
+ by (fact continuous_snd)
+
+lemma isCont_Pair [simp]: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
+ by (fact continuous_Pair)
+
+subsubsection \<open>Separation axioms\<close>
+
+instance prod :: (t0_space, t0_space) t0_space
+proof
+ fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
+ hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
+ by (simp add: prod_eq_iff)
+ thus "\<exists>U. open U \<and> (x \<in> U) \<noteq> (y \<in> U)"
+ by (fast dest: t0_space elim: open_vimage_fst open_vimage_snd)
+qed
+
+instance prod :: (t1_space, t1_space) t1_space
+proof
+ fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
+ hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
+ by (simp add: prod_eq_iff)
+ thus "\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
+ by (fast dest: t1_space elim: open_vimage_fst open_vimage_snd)
+qed
+
+instance prod :: (t2_space, t2_space) t2_space
+proof
+ fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
+ hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
+ by (simp add: prod_eq_iff)
+ thus "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
+ by (fast dest: hausdorff elim: open_vimage_fst open_vimage_snd)
+qed
+
+lemma isCont_swap[continuous_intros]: "isCont prod.swap a"
+ using continuous_on_eq_continuous_within continuous_on_swap by blast
+
+end