--- a/src/HOL/Topological_Spaces.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Topological_Spaces.thy Fri Mar 22 10:41:43 2013 +0100
@@ -724,6 +724,9 @@
"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 at_def eventually_within eventually_nhds by simp
+lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
+ unfolding filter_eq_iff eventually_within eventually_at_topological by (metis open_Int Int_iff)
+
lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
unfolding trivial_limit_def eventually_at_topological
by (safe, case_tac "S = {a}", simp, fast, fast)
@@ -869,6 +872,9 @@
by (auto elim!: allE[of _ "\<lambda>x. x \<in> S"] eventually_rev_mp)
qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def)
+lemma tendsto_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
+ by (auto simp: tendsto_def eventually_within elim!: eventually_elim1)
+
lemma filterlim_at:
"(LIM x F. f x :> at b) \<longleftrightarrow> (eventually (\<lambda>x. f x \<noteq> b) F \<and> (f ---> b) F)"
by (simp add: at_def filterlim_within)
@@ -1540,6 +1546,9 @@
("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
"f -- a --> L \<equiv> (f ---> L) (at a)"
+lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l) (at a within S) \<longleftrightarrow> (f -- a --> l)"
+ unfolding tendsto_def by (simp add: at_within_open)
+
lemma LIM_const_not_eq[tendsto_intros]:
fixes a :: "'a::perfect_space"
fixes k L :: "'b::t2_space"
@@ -1629,6 +1638,10 @@
definition continuous_on :: "'a set \<Rightarrow> ('a :: topological_space \<Rightarrow> 'b :: topological_space) \<Rightarrow> bool" where
"continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. (f ---> f x) (at x within s))"
+lemma continuous_on_cong [cong]:
+ "s = t \<Longrightarrow> (\<And>x. x \<in> t \<Longrightarrow> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
+ unfolding continuous_on_def by (intro ball_cong filterlim_cong) (auto simp: eventually_within)
+
lemma continuous_on_topological:
"continuous_on s f \<longleftrightarrow>
(\<forall>x\<in>s. \<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow> (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
@@ -1655,6 +1668,11 @@
qed
qed
+lemma continuous_on_open_vimage:
+ "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>B. open B \<longrightarrow> open (f -` B \<inter> s))"
+ unfolding continuous_on_open_invariant
+ by (metis open_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
+
lemma continuous_on_closed_invariant:
"continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> (\<exists>A. closed A \<and> A \<inter> s = f -` B \<inter> s))"
proof -
@@ -1664,6 +1682,36 @@
unfolding continuous_on_open_invariant by (intro *) (auto simp: open_closed[symmetric])
qed
+lemma continuous_on_closed_vimage:
+ "closed s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> closed (f -` B \<inter> s))"
+ unfolding continuous_on_closed_invariant
+ by (metis closed_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
+
+lemma continuous_on_open_Union:
+ "(\<And>s. s \<in> S \<Longrightarrow> open s) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on s f) \<Longrightarrow> continuous_on (\<Union>S) f"
+ unfolding continuous_on_def by (simp add: tendsto_within_open open_Union)
+
+lemma continuous_on_open_UN:
+ "(\<And>s. s \<in> S \<Longrightarrow> open (A s)) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on (A s) f) \<Longrightarrow> continuous_on (\<Union>s\<in>S. A s) f"
+ unfolding Union_image_eq[symmetric] by (rule continuous_on_open_Union) auto
+
+lemma continuous_on_closed_Un:
+ "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
+ by (auto simp add: continuous_on_closed_vimage closed_Un Int_Un_distrib)
+
+lemma continuous_on_If:
+ assumes closed: "closed s" "closed t" and cont: "continuous_on s f" "continuous_on t g"
+ and P: "\<And>x. x \<in> s \<Longrightarrow> \<not> P x \<Longrightarrow> f x = g x" "\<And>x. x \<in> t \<Longrightarrow> P x \<Longrightarrow> f x = g x"
+ shows "continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)" (is "continuous_on _ ?h")
+proof-
+ from P have "\<forall>x\<in>s. f x = ?h x" "\<forall>x\<in>t. g x = ?h x"
+ by auto
+ with cont have "continuous_on s ?h" "continuous_on t ?h"
+ by simp_all
+ with closed show ?thesis
+ by (rule continuous_on_closed_Un)
+qed
+
ML {*
structure Continuous_On_Intros = Named_Thms
@@ -1686,6 +1734,10 @@
"continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
unfolding continuous_on_topological by simp metis
+lemma continuous_on_compose2:
+ "continuous_on t g \<Longrightarrow> continuous_on s f \<Longrightarrow> t = f ` s \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
+ using continuous_on_compose[of s f g] by (simp add: comp_def)
+
subsubsection {* Continuity at a point *}
definition continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
@@ -1749,6 +1801,12 @@
lemma continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
by (auto intro: within_le filterlim_mono simp: continuous_at continuous_within)
+lemma continuous_on_eq_continuous_at: "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. isCont f x)"
+ by (simp add: continuous_on_def continuous_at tendsto_within_open)
+
+lemma continuous_on_subset: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous_on t f"
+ unfolding continuous_on_def by (metis subset_eq tendsto_within_subset)
+
lemma continuous_at_imp_continuous_on: "\<forall>x\<in>s. isCont f x \<Longrightarrow> continuous_on s f"
by (auto intro: continuous_at_within simp: continuous_on_eq_continuous_within)
@@ -1801,8 +1859,101 @@
using assms unfolding ball_simps[symmetric] SUP_def
by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s])
+lemma compact_inter_closed [intro]:
+ assumes "compact s" and "closed t"
+ shows "compact (s \<inter> t)"
+proof (rule compactI)
+ fix C assume C: "\<forall>c\<in>C. open c" and cover: "s \<inter> t \<subseteq> \<Union>C"
+ from C `closed t` have "\<forall>c\<in>C \<union> {-t}. open c" by auto
+ moreover from cover have "s \<subseteq> \<Union>(C \<union> {-t})" by auto
+ ultimately have "\<exists>D\<subseteq>C \<union> {-t}. finite D \<and> s \<subseteq> \<Union>D"
+ using `compact s` unfolding compact_eq_heine_borel by auto
+ then guess D ..
+ then show "\<exists>D\<subseteq>C. finite D \<and> s \<inter> t \<subseteq> \<Union>D"
+ by (intro exI[of _ "D - {-t}"]) auto
+qed
+
end
+lemma (in t2_space) compact_imp_closed:
+ assumes "compact s" shows "closed s"
+unfolding closed_def
+proof (rule openI)
+ fix y assume "y \<in> - s"
+ let ?C = "\<Union>x\<in>s. {u. open u \<and> x \<in> u \<and> eventually (\<lambda>y. y \<notin> u) (nhds y)}"
+ note `compact s`
+ moreover have "\<forall>u\<in>?C. open u" by simp
+ moreover have "s \<subseteq> \<Union>?C"
+ proof
+ fix x assume "x \<in> s"
+ with `y \<in> - s` have "x \<noteq> y" by clarsimp
+ hence "\<exists>u v. open u \<and> open v \<and> x \<in> u \<and> y \<in> v \<and> u \<inter> v = {}"
+ by (rule hausdorff)
+ with `x \<in> s` show "x \<in> \<Union>?C"
+ unfolding eventually_nhds by auto
+ qed
+ ultimately obtain D where "D \<subseteq> ?C" and "finite D" and "s \<subseteq> \<Union>D"
+ by (rule compactE)
+ from `D \<subseteq> ?C` have "\<forall>x\<in>D. eventually (\<lambda>y. y \<notin> x) (nhds y)" by auto
+ with `finite D` have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
+ by (simp add: eventually_Ball_finite)
+ with `s \<subseteq> \<Union>D` have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
+ by (auto elim!: eventually_mono [rotated])
+ thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"
+ by (simp add: eventually_nhds subset_eq)
+qed
+
+lemma compact_continuous_image:
+ assumes f: "continuous_on s f" and s: "compact s"
+ shows "compact (f ` s)"
+proof (rule compactI)
+ fix C assume "\<forall>c\<in>C. open c" and cover: "f`s \<subseteq> \<Union>C"
+ with f have "\<forall>c\<in>C. \<exists>A. open A \<and> A \<inter> s = f -` c \<inter> s"
+ unfolding continuous_on_open_invariant by blast
+ then guess A unfolding bchoice_iff .. note A = this
+ with cover have "\<forall>c\<in>C. open (A c)" "s \<subseteq> (\<Union>c\<in>C. A c)"
+ by (fastforce simp add: subset_eq set_eq_iff)+
+ from compactE_image[OF s this] obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> (\<Union>c\<in>D. A c)" .
+ with A show "\<exists>D \<subseteq> C. finite D \<and> f`s \<subseteq> \<Union>D"
+ by (intro exI[of _ D]) (fastforce simp add: subset_eq set_eq_iff)+
+qed
+
+lemma continuous_on_inv:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space"
+ assumes "continuous_on s f" "compact s" "\<forall>x\<in>s. g (f x) = x"
+ shows "continuous_on (f ` s) g"
+unfolding continuous_on_topological
+proof (clarsimp simp add: assms(3))
+ fix x :: 'a and B :: "'a set"
+ assume "x \<in> s" and "open B" and "x \<in> B"
+ have 1: "\<forall>x\<in>s. f x \<in> f ` (s - B) \<longleftrightarrow> x \<in> s - B"
+ using assms(3) by (auto, metis)
+ have "continuous_on (s - B) f"
+ using `continuous_on s f` Diff_subset
+ by (rule continuous_on_subset)
+ moreover have "compact (s - B)"
+ using `open B` and `compact s`
+ unfolding Diff_eq by (intro compact_inter_closed closed_Compl)
+ ultimately have "compact (f ` (s - B))"
+ by (rule compact_continuous_image)
+ hence "closed (f ` (s - B))"
+ by (rule compact_imp_closed)
+ hence "open (- f ` (s - B))"
+ by (rule open_Compl)
+ moreover have "f x \<in> - f ` (s - B)"
+ using `x \<in> s` and `x \<in> B` by (simp add: 1)
+ moreover have "\<forall>y\<in>s. f y \<in> - f ` (s - B) \<longrightarrow> y \<in> B"
+ by (simp add: 1)
+ ultimately show "\<exists>A. open A \<and> f x \<in> A \<and> (\<forall>y\<in>s. f y \<in> A \<longrightarrow> y \<in> B)"
+ by fast
+qed
+
+lemma continuous_on_inv_into:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space"
+ assumes s: "continuous_on s f" "compact s" and f: "inj_on f s"
+ shows "continuous_on (f ` s) (the_inv_into s f)"
+ by (rule continuous_on_inv[OF s]) (auto simp: the_inv_into_f_f[OF f])
+
lemma (in linorder_topology) compact_attains_sup:
assumes "compact S" "S \<noteq> {}"
shows "\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s"
@@ -1841,21 +1992,6 @@
by fastforce
qed
-lemma compact_continuous_image:
- assumes f: "continuous_on s f" and s: "compact s"
- shows "compact (f ` s)"
-proof (rule compactI)
- fix C assume "\<forall>c\<in>C. open c" and cover: "f`s \<subseteq> \<Union>C"
- with f have "\<forall>c\<in>C. \<exists>A. open A \<and> A \<inter> s = f -` c \<inter> s"
- unfolding continuous_on_open_invariant by blast
- then guess A unfolding bchoice_iff .. note A = this
- with cover have "\<forall>c\<in>C. open (A c)" "s \<subseteq> (\<Union>c\<in>C. A c)"
- by (fastforce simp add: subset_eq set_eq_iff)+
- from compactE_image[OF s this] obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> (\<Union>c\<in>D. A c)" .
- with A show "\<exists>D \<subseteq> C. finite D \<and> f`s \<subseteq> \<Union>D"
- by (intro exI[of _ D]) (fastforce simp add: subset_eq set_eq_iff)+
-qed
-
lemma continuous_attains_sup:
fixes f :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f \<Longrightarrow> (\<exists>x\<in>s. \<forall>y\<in>s. f y \<le> f x)"