--- a/src/HOL/Library/Countable_Set.thy Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Library/Countable_Set.thy Tue Jun 14 15:34:21 2016 +0100
@@ -299,6 +299,20 @@
subsection \<open>Misc lemmas\<close>
+lemma countable_subset_image:
+ "countable B \<and> B \<subseteq> (f ` A) \<longleftrightarrow> (\<exists>A'. countable A' \<and> A' \<subseteq> A \<and> (B = f ` A'))"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ apply (rule_tac x="inv_into A f ` B" in exI)
+ apply (auto simp: f_inv_into_f subset_iff image_inv_into_cancel inv_into_into)
+ done
+next
+ assume ?rhs
+ then show ?lhs by force
+qed
+
lemma infinite_countable_subset':
assumes X: "infinite X" shows "\<exists>C\<subseteq>X. countable C \<and> infinite C"
proof -
--- a/src/HOL/Limits.thy Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Limits.thy Tue Jun 14 15:34:21 2016 +0100
@@ -611,21 +611,21 @@
lemma tendsto_setsum [tendsto_intros]:
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_add"
- assumes "\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> a i) F"
- shows "((\<lambda>x. \<Sum>i\<in>S. f i x) \<longlongrightarrow> (\<Sum>i\<in>S. a i)) F"
-proof (cases "finite S")
- assume "finite S" thus ?thesis using assms
+ assumes "\<And>i. i \<in> I \<Longrightarrow> (f i \<longlongrightarrow> a i) F"
+ shows "((\<lambda>x. \<Sum>i\<in>I. f i x) \<longlongrightarrow> (\<Sum>i\<in>I. a i)) F"
+proof (cases "finite I")
+ assume "finite I" thus ?thesis using assms
by (induct, simp, simp add: tendsto_add)
qed simp
lemma continuous_setsum [continuous_intros]:
fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_add"
- shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>S. f i x)"
+ shows "(\<And>i. i \<in> I \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>I. f i x)"
unfolding continuous_def by (rule tendsto_setsum)
lemma continuous_on_setsum [continuous_intros]:
fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::topological_comm_monoid_add"
- shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Sum>i\<in>S. f i x)"
+ shows "(\<And>i. i \<in> I \<Longrightarrow> continuous_on S (f i)) \<Longrightarrow> continuous_on S (\<lambda>x. \<Sum>i\<in>I. f i x)"
unfolding continuous_on_def by (auto intro: tendsto_setsum)
instance nat :: topological_comm_monoid_add
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Jun 14 15:34:21 2016 +0100
@@ -2088,6 +2088,11 @@
by (simp add: \<open>continuous_on t r\<close> continuous_on_diff continuous_on_id continuous_on_norm)
qed
+lemma closedin_self [simp]:
+ fixes S :: "'a :: real_normed_vector set"
+ shows "closedin (subtopology euclidean S) S"
+ by (simp add: closedin_retract)
+
lemma retract_of_contractible:
assumes "contractible t" "s retract_of t"
shows "contractible s"
@@ -2195,4 +2200,97 @@
apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+
done
+subsection\<open>Borsuk-style characterization of separation\<close>
+
+lemma continuous_on_Borsuk_map:
+ "a \<notin> s \<Longrightarrow> continuous_on s (\<lambda>x. inverse(norm (x - a)) *\<^sub>R (x - a))"
+by (rule continuous_intros | force)+
+
+lemma Borsuk_map_into_sphere:
+ "(\<lambda>x. inverse(norm (x - a)) *\<^sub>R (x - a)) ` s \<subseteq> sphere 0 1 \<longleftrightarrow> (a \<notin> s)"
+ by auto (metis eq_iff_diff_eq_0 left_inverse norm_eq_zero)
+
+lemma Borsuk_maps_homotopic_in_path_component:
+ assumes "path_component (- s) a b"
+ shows "homotopic_with (\<lambda>x. True) s (sphere 0 1)
+ (\<lambda>x. inverse(norm(x - a)) *\<^sub>R (x - a))
+ (\<lambda>x. inverse(norm(x - b)) *\<^sub>R (x - b))"
+proof -
+ obtain g where "path g" "path_image g \<subseteq> -s" "pathstart g = a" "pathfinish g = b"
+ using assms by (auto simp: path_component_def)
+ then show ?thesis
+ apply (simp add: path_def path_image_def pathstart_def pathfinish_def homotopic_with_def)
+ apply (rule_tac x = "\<lambda>z. inverse(norm(snd z - (g o fst)z)) *\<^sub>R (snd z - (g o fst)z)" in exI)
+ apply (intro conjI continuous_intros)
+ apply (rule continuous_intros | erule continuous_on_subset | fastforce simp: divide_simps sphere_def)+
+ done
+qed
+
+lemma non_extensible_Borsuk_map:
+ fixes a :: "'a :: euclidean_space"
+ assumes "compact s" and cin: "c \<in> components(- s)" and boc: "bounded c" and "a \<in> c"
+ shows "~ (\<exists>g. continuous_on (s \<union> c) g \<and>
+ g ` (s \<union> c) \<subseteq> sphere 0 1 \<and>
+ (\<forall>x \<in> s. g x = inverse(norm(x - a)) *\<^sub>R (x - a)))"
+proof -
+ have "closed s" using assms by (simp add: compact_imp_closed)
+ have "c \<subseteq> -s"
+ using assms by (simp add: in_components_subset)
+ with \<open>a \<in> c\<close> have "a \<notin> s" by blast
+ then have ceq: "c = connected_component_set (- s) a"
+ by (metis \<open>a \<in> c\<close> cin components_iff connected_component_eq)
+ then have "bounded (s \<union> connected_component_set (- s) a)"
+ using \<open>compact s\<close> boc compact_imp_bounded by auto
+ with bounded_subset_ballD obtain r where "0 < r" and r: "(s \<union> connected_component_set (- s) a) \<subseteq> ball a r"
+ by blast
+ { fix g
+ assume "continuous_on (s \<union> c) g"
+ "g ` (s \<union> c) \<subseteq> sphere 0 1"
+ and [simp]: "\<And>x. x \<in> s \<Longrightarrow> g x = (x - a) /\<^sub>R norm (x - a)"
+ then have [simp]: "\<And>x. x \<in> s \<union> c \<Longrightarrow> norm (g x) = 1"
+ by force
+ have cb_eq: "cball a r = (s \<union> connected_component_set (- s) a) \<union>
+ (cball a r - connected_component_set (- s) a)"
+ using ball_subset_cball [of a r] r by auto
+ have cont1: "continuous_on (s \<union> connected_component_set (- s) a)
+ (\<lambda>x. a + r *\<^sub>R g x)"
+ apply (rule continuous_intros)+
+ using \<open>continuous_on (s \<union> c) g\<close> ceq by blast
+ have cont2: "continuous_on (cball a r - connected_component_set (- s) a)
+ (\<lambda>x. a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
+ by (rule continuous_intros | force simp: \<open>a \<notin> s\<close>)+
+ have 1: "continuous_on (cball a r)
+ (\<lambda>x. if connected_component (- s) a x
+ then a + r *\<^sub>R g x
+ else a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
+ apply (subst cb_eq)
+ apply (rule continuous_on_cases [OF _ _ cont1 cont2])
+ using ceq cin
+ apply (auto intro: closed_Un_complement_component
+ simp: \<open>closed s\<close> open_Compl open_connected_component)
+ done
+ have 2: "(\<lambda>x. a + r *\<^sub>R g x) ` (cball a r \<inter> connected_component_set (- s) a)
+ \<subseteq> sphere a r "
+ using \<open>0 < r\<close> by (force simp: dist_norm ceq)
+ have "retraction (cball a r) (sphere a r)
+ (\<lambda>x. if x \<in> connected_component_set (- s) a
+ then a + r *\<^sub>R g x
+ else a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
+ using \<open>0 < r\<close>
+ apply (simp add: retraction_def dist_norm 1 2, safe)
+ apply (force simp: dist_norm abs_if mult_less_0_iff divide_simps \<open>a \<notin> s\<close>)
+ using r
+ by (auto simp: dist_norm norm_minus_commute)
+ then have False
+ using no_retraction_cball
+ [OF \<open>0 < r\<close>, of a, unfolded retract_of_def, simplified, rule_format,
+ of "\<lambda>x. if x \<in> connected_component_set (- s) a
+ then a + r *\<^sub>R g x
+ else a + r *\<^sub>R inverse(norm(x - a)) *\<^sub>R (x - a)"]
+ by blast
+ }
+ then show ?thesis
+ by blast
+qed
+
end
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Jun 14 15:34:21 2016 +0100
@@ -6196,7 +6196,7 @@
done
qed
-lemma midpoint_eq_endpoint:
+lemma midpoint_eq_endpoint [simp]:
"midpoint a b = a \<longleftrightarrow> a = b"
"midpoint a b = b \<longleftrightarrow> a = b"
unfolding midpoint_eq_iff by auto
@@ -6432,6 +6432,17 @@
apply (simp add: convex_contains_open_segment, clarify)
by (metis (no_types, hide_lams) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment)
+lemma csegment_midpoint_subset: "closed_segment (midpoint a b) b \<subseteq> closed_segment a b"
+ apply (clarsimp simp: midpoint_def in_segment)
+ apply (rule_tac x="(1 + u) / 2" in exI)
+ apply (auto simp: algebra_simps add_divide_distrib diff_divide_distrib)
+ by (metis real_sum_of_halves scaleR_left.add)
+
+lemma notin_segment_midpoint:
+ fixes a :: "'a :: euclidean_space"
+ shows "a \<noteq> b \<Longrightarrow> a \<notin> closed_segment (midpoint a b) b"
+by (auto simp: dist_midpoint dest!: dist_in_closed_segment)
+
subsubsection\<open>More lemmas, especially for working with the underlying formula\<close>
lemma segment_eq_compose:
@@ -10243,7 +10254,7 @@
lemma setdist_empty2 [simp]: "setdist t {} = 0"
by (simp add: setdist_def)
-lemma setdist_pos_le: "0 \<le> setdist s t"
+lemma setdist_pos_le [simp]: "0 \<le> setdist s t"
by (auto simp: setdist_def ex_in_conv [symmetric] intro: cInf_greatest)
lemma le_setdistI:
@@ -10307,10 +10318,10 @@
apply (subst setdist_singletons [symmetric])
by (metis abs_diff_le_iff diff_le_eq setdist_triangle setdist_sym)
-lemma continuous_at_setdist: "continuous (at x) (\<lambda>y. (setdist {y} s))"
+lemma continuous_at_setdist [continuous_intros]: "continuous (at x) (\<lambda>y. (setdist {y} s))"
by (force simp: continuous_at_eps_delta dist_real_def intro: le_less_trans [OF setdist_Lipschitz])
-lemma continuous_on_setdist: "continuous_on t (\<lambda>y. (setdist {y} s))"
+lemma continuous_on_setdist [continuous_intros]: "continuous_on t (\<lambda>y. (setdist {y} s))"
by (metis continuous_at_setdist continuous_at_imp_continuous_on)
lemma uniformly_continuous_on_setdist: "uniformly_continuous_on t (\<lambda>y. (setdist {y} s))"
@@ -10424,34 +10435,44 @@
apply (auto simp: closest_point_in_set)
done
-lemma setdist_eq_0_sing_1 [simp]:
- fixes s :: "'a::euclidean_space set"
- shows "setdist {x} s = 0 \<longleftrightarrow> s = {} \<or> x \<in> closure s"
-by (auto simp: setdist_eq_0_bounded)
-
-lemma setdist_eq_0_sing_2 [simp]:
- fixes s :: "'a::euclidean_space set"
- shows "setdist s {x} = 0 \<longleftrightarrow> s = {} \<or> x \<in> closure s"
-by (auto simp: setdist_eq_0_bounded)
+lemma setdist_eq_0_sing_1:
+ fixes s :: "'a::euclidean_space set"
+ shows "setdist {x} s = 0 \<longleftrightarrow> s = {} \<or> x \<in> closure s"
+ by (auto simp: setdist_eq_0_bounded)
+
+lemma setdist_eq_0_sing_2:
+ fixes s :: "'a::euclidean_space set"
+ shows "setdist s {x} = 0 \<longleftrightarrow> s = {} \<or> x \<in> closure s"
+ by (auto simp: setdist_eq_0_bounded)
lemma setdist_neq_0_sing_1:
fixes s :: "'a::euclidean_space set"
shows "\<lbrakk>setdist {x} s = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> s \<noteq> {} \<and> x \<notin> closure s"
-by auto
+ by (auto simp: setdist_eq_0_sing_1)
lemma setdist_neq_0_sing_2:
- fixes s :: "'a::euclidean_space set"
+ fixes s :: "'a::euclidean_space set"
shows "\<lbrakk>setdist s {x} = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> s \<noteq> {} \<and> x \<notin> closure s"
-by auto
+ by (auto simp: setdist_eq_0_sing_2)
lemma setdist_sing_in_set:
- fixes s :: "'a::euclidean_space set"
- shows "x \<in> s \<Longrightarrow> setdist {x} s = 0"
-using closure_subset by force
+ fixes s :: "'a::euclidean_space set"
+ shows "x \<in> s \<Longrightarrow> setdist {x} s = 0"
+ using closure_subset by (auto simp: setdist_eq_0_sing_1)
lemma setdist_le_sing: "x \<in> s ==> setdist s t \<le> setdist {x} t"
using setdist_subset_left by auto
+lemma setdist_eq_0_closed:
+ fixes s :: "'a::euclidean_space set"
+ shows "closed s \<Longrightarrow> (setdist {x} s = 0 \<longleftrightarrow> s = {} \<or> x \<in> s)"
+by (simp add: setdist_eq_0_sing_1)
+
+lemma setdist_eq_0_closedin:
+ fixes s :: "'a::euclidean_space set"
+ shows "\<lbrakk>closedin (subtopology euclidean u) s; x \<in> u\<rbrakk>
+ \<Longrightarrow> (setdist {x} s = 0 \<longleftrightarrow> s = {} \<or> x \<in> s)"
+ by (auto simp: closedin_limpt setdist_eq_0_sing_1 closure_def)
subsection\<open>Basic lemmas about hyperplanes and halfspaces\<close>
@@ -10506,6 +10527,294 @@
using halfspace_eq_empty_le [of "-a" "-b"]
by simp
+subsection\<open>Use set distance for an easy proof of separation properties\<close>
+
+proposition separation_closures:
+ fixes S :: "'a::euclidean_space set"
+ assumes "S \<inter> closure T = {}" "T \<inter> closure S = {}"
+ obtains U V where "U \<inter> V = {}" "open U" "open V" "S \<subseteq> U" "T \<subseteq> V"
+proof (cases "S = {} \<or> T = {}")
+ case True with that show ?thesis by auto
+next
+ case False
+ define f where "f \<equiv> \<lambda>x. setdist {x} T - setdist {x} S"
+ have contf: "\<And>x. isCont f x"
+ unfolding f_def by (intro continuous_intros continuous_at_setdist)
+ show ?thesis
+ proof (rule_tac U = "{x. f x > 0}" and V = "{x. f x < 0}" in that)
+ show "{x. 0 < f x} \<inter> {x. f x < 0} = {}"
+ by auto
+ show "open {x. 0 < f x}"
+ by (simp add: open_Collect_less contf)
+ show "open {x. f x < 0}"
+ by (simp add: open_Collect_less contf)
+ show "S \<subseteq> {x. 0 < f x}"
+ apply (clarsimp simp add: f_def setdist_sing_in_set)
+ using assms
+ by (metis False IntI empty_iff le_less setdist_eq_0_sing_2 setdist_pos_le setdist_sym)
+ show "T \<subseteq> {x. f x < 0}"
+ apply (clarsimp simp add: f_def setdist_sing_in_set)
+ using assms
+ by (metis False IntI empty_iff le_less setdist_eq_0_sing_2 setdist_pos_le setdist_sym)
+ qed
+qed
+
+lemma separation_normal:
+ fixes S :: "'a::euclidean_space set"
+ assumes "closed S" "closed T" "S \<inter> T = {}"
+ obtains U V where "open U" "open V" "S \<subseteq> U" "T \<subseteq> V" "U \<inter> V = {}"
+using separation_closures [of S T]
+by (metis assms closure_closed disjnt_def inf_commute)
+
+
+lemma separation_normal_local:
+ fixes S :: "'a::euclidean_space set"
+ assumes US: "closedin (subtopology euclidean U) S"
+ and UT: "closedin (subtopology euclidean U) T"
+ and "S \<inter> T = {}"
+ obtains S' T' where "openin (subtopology euclidean U) S'"
+ "openin (subtopology euclidean U) T'"
+ "S \<subseteq> S'" "T \<subseteq> T'" "S' \<inter> T' = {}"
+proof (cases "S = {} \<or> T = {}")
+ case True with that show ?thesis
+ apply safe
+ using UT closedin_subset apply blast
+ using US closedin_subset apply blast
+ done
+next
+ case False
+ define f where "f \<equiv> \<lambda>x. setdist {x} T - setdist {x} S"
+ have contf: "continuous_on U f"
+ unfolding f_def by (intro continuous_intros)
+ show ?thesis
+ proof (rule_tac S' = "{x\<in>U. f x > 0}" and T' = "{x\<in>U. f x < 0}" in that)
+ show "{x \<in> U. 0 < f x} \<inter> {x \<in> U. f x < 0} = {}"
+ by auto
+ have "openin (subtopology euclidean U) {x \<in> U. f x \<in> {0<..}}"
+ apply (rule continuous_openin_preimage [where T=UNIV])
+ apply (simp_all add: contf)
+ using open_greaterThan open_openin by blast
+ then show "openin (subtopology euclidean U) {x \<in> U. 0 < f x}" by simp
+ next
+ have "openin (subtopology euclidean U) {x \<in> U. f x \<in> {..<0}}"
+ apply (rule continuous_openin_preimage [where T=UNIV])
+ apply (simp_all add: contf)
+ using open_lessThan open_openin by blast
+ then show "openin (subtopology euclidean U) {x \<in> U. f x < 0}" by simp
+ next
+ show "S \<subseteq> {x \<in> U. 0 < f x}"
+ apply (clarsimp simp add: f_def setdist_sing_in_set)
+ using assms
+ by (metis False Int_insert_right closedin_imp_subset empty_not_insert insert_absorb insert_subset linorder_neqE_linordered_idom not_le setdist_eq_0_closedin setdist_pos_le)
+ show "T \<subseteq> {x \<in> U. f x < 0}"
+ apply (clarsimp simp add: f_def setdist_sing_in_set)
+ using assms
+ by (metis False closedin_subset disjoint_iff_not_equal insert_absorb insert_subset linorder_neqE_linordered_idom not_less setdist_eq_0_closedin setdist_pos_le topspace_euclidean_subtopology)
+ qed
+qed
+
+lemma separation_normal_compact:
+ fixes S :: "'a::euclidean_space set"
+ assumes "compact S" "closed T" "S \<inter> T = {}"
+ obtains U V where "open U" "compact(closure U)" "open V" "S \<subseteq> U" "T \<subseteq> V" "U \<inter> V = {}"
+proof -
+ have "closed S" "bounded S"
+ using assms by (auto simp: compact_eq_bounded_closed)
+ then obtain r where "r>0" and r: "S \<subseteq> ball 0 r"
+ by (auto dest!: bounded_subset_ballD)
+ have **: "closed (T \<union> - ball 0 r)" "S \<inter> (T \<union> - ball 0 r) = {}"
+ using assms r by blast+
+ then show ?thesis
+ apply (rule separation_normal [OF \<open>closed S\<close>])
+ apply (rule_tac U=U and V=V in that)
+ by auto (meson bounded_ball bounded_subset compl_le_swap2 disjoint_eq_subset_Compl)
+qed
+
+subsection\<open>Proper maps, including projections out of compact sets\<close>
+
+lemma finite_indexed_bound:
+ assumes A: "finite A" "\<And>x. x \<in> A \<Longrightarrow> \<exists>n::'a::linorder. P x n"
+ shows "\<exists>m. \<forall>x \<in> A. \<exists>k\<le>m. P x k"
+using A
+proof (induction A)
+ case empty then show ?case by force
+next
+ case (insert a A)
+ then obtain m n where "\<forall>x \<in> A. \<exists>k\<le>m. P x k" "P a n"
+ by force
+ then show ?case
+ apply (rule_tac x="max m n" in exI, safe)
+ using max.cobounded2 apply blast
+ by (meson le_max_iff_disj)
+qed
+
+proposition proper_map:
+ fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
+ assumes "closedin (subtopology euclidean S) K"
+ and com: "\<And>U. \<lbrakk>U \<subseteq> T; compact U\<rbrakk> \<Longrightarrow> compact {x \<in> S. f x \<in> U}"
+ and "f ` S \<subseteq> T"
+ shows "closedin (subtopology euclidean T) (f ` K)"
+proof -
+ have "K \<subseteq> S"
+ using assms closedin_imp_subset by metis
+ obtain C where "closed C" and Keq: "K = S \<inter> C"
+ using assms by (auto simp: closedin_closed)
+ have *: "y \<in> f ` K" if "y \<in> T" and y: "y islimpt f ` K" for y
+ proof -
+ obtain h where "\<forall>n. (\<exists>x\<in>K. h n = f x) \<and> h n \<noteq> y" "inj h" and hlim: "(h \<longlongrightarrow> y) sequentially"
+ using \<open>y \<in> T\<close> y by (force simp: limpt_sequential_inj)
+ then obtain X where X: "\<And>n. X n \<in> K \<and> h n = f (X n) \<and> h n \<noteq> y"
+ by metis
+ then have fX: "\<And>n. f (X n) = h n"
+ by metis
+ have "compact (C \<inter> {a \<in> S. f a \<in> insert y (range (\<lambda>i. f(X(n + i))))})" for n
+ apply (rule closed_Int_compact [OF \<open>closed C\<close>])
+ apply (rule com)
+ using X \<open>K \<subseteq> S\<close> \<open>f ` S \<subseteq> T\<close> \<open>y \<in> T\<close> apply blast
+ apply (rule compact_sequence_with_limit)
+ apply (simp add: fX add.commute [of n] LIMSEQ_ignore_initial_segment [OF hlim])
+ done
+ then have comf: "compact {a \<in> K. f a \<in> insert y (range (\<lambda>i. f(X(n + i))))}" for n
+ by (simp add: Keq Int_def conj_commute)
+ have ne: "\<Inter>\<F> \<noteq> {}"
+ if "finite \<F>"
+ and \<F>: "\<And>t. t \<in> \<F> \<Longrightarrow>
+ (\<exists>n. t = {a \<in> K. f a \<in> insert y (range (\<lambda>i. f (X (n + i))))})"
+ for \<F>
+ proof -
+ obtain m where m: "\<And>t. t \<in> \<F> \<Longrightarrow> \<exists>k\<le>m. t = {a \<in> K. f a \<in> insert y (range (\<lambda>i. f (X (k + i))))}"
+ apply (rule exE)
+ apply (rule finite_indexed_bound [OF \<open>finite \<F>\<close> \<F>], assumption, force)
+ done
+ have "X m \<in> \<Inter>\<F>"
+ using X le_Suc_ex by (fastforce dest: m)
+ then show ?thesis by blast
+ qed
+ have "\<Inter>{{a. a \<in> K \<and> f a \<in> insert y (range (\<lambda>i. f(X(n + i))))} |n. n \<in> UNIV}
+ \<noteq> {}"
+ apply (rule compact_fip_heine_borel)
+ using comf apply force
+ using ne apply (simp add: subset_iff del: insert_iff)
+ done
+ then have "\<exists>x. x \<in> (\<Inter>n. {a \<in> K. f a \<in> insert y (range (\<lambda>i. f (X (n + i))))})"
+ by blast
+ then show ?thesis
+ apply (simp add: image_iff fX)
+ by (metis \<open>inj h\<close> le_add1 not_less_eq_eq rangeI range_ex1_eq)
+ qed
+ with assms closedin_subset show ?thesis
+ by (force simp: closedin_limpt)
+qed
+
+
+lemma compact_continuous_image_eq:
+ fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
+ assumes f: "inj_on f S"
+ shows "continuous_on S f \<longleftrightarrow> (\<forall>T. compact T \<and> T \<subseteq> S \<longrightarrow> compact(f ` T))"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs then show ?rhs
+ by (metis continuous_on_subset compact_continuous_image)
+next
+ assume RHS: ?rhs
+ obtain g where gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
+ by (metis inv_into_f_f f)
+ then have *: "{x \<in> S. f x \<in> U} = g ` U" if "U \<subseteq> f ` S" for U
+ using that by fastforce
+ have gfim: "g ` f ` S \<subseteq> S" using gf by auto
+ have **: "compact {x \<in> f ` S. g x \<in> C}" if C: "C \<subseteq> S" "compact C" for C
+ proof -
+ obtain h :: "'a set \<Rightarrow> 'a" where "h C \<in> C \<and> h C \<notin> S \<or> compact (f ` C)"
+ by (force simp: C RHS)
+ moreover have "f ` C = {b \<in> f ` S. g b \<in> C}"
+ using C gf by auto
+ ultimately show "compact {b \<in> f ` S. g b \<in> C}"
+ using C by auto
+ qed
+ show ?lhs
+ using proper_map [OF _ _ gfim] **
+ by (simp add: continuous_on_closed * closedin_imp_subset)
+qed
+
+lemma proper_map_from_compact:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes contf: "continuous_on S f" and imf: "f ` S \<subseteq> T" and "compact S"
+ "closedin (subtopology euclidean T) K"
+ shows "compact {x. x \<in> S \<and> f x \<in> K}"
+by (rule closedin_compact [OF \<open>compact S\<close>] continuous_closedin_preimage_gen assms)+
+
+lemma proper_map_fst:
+ assumes "compact T" "K \<subseteq> S" "compact K"
+ shows "compact {z \<in> S \<times> T. fst z \<in> K}"
+proof -
+ have "{z \<in> S \<times> T. fst z \<in> K} = K \<times> T"
+ using assms by auto
+ then show ?thesis by (simp add: assms compact_Times)
+qed
+
+lemma closed_map_fst:
+ fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+ assumes "compact T" "closedin (subtopology euclidean (S \<times> T)) c"
+ shows "closedin (subtopology euclidean S) (fst ` c)"
+proof -
+ have *: "fst ` (S \<times> T) \<subseteq> S"
+ by auto
+ show ?thesis
+ using proper_map [OF _ _ *] by (simp add: proper_map_fst assms)
+qed
+
+lemma proper_map_snd:
+ assumes "compact S" "K \<subseteq> T" "compact K"
+ shows "compact {z \<in> S \<times> T. snd z \<in> K}"
+proof -
+ have "{z \<in> S \<times> T. snd z \<in> K} = S \<times> K"
+ using assms by auto
+ then show ?thesis by (simp add: assms compact_Times)
+qed
+
+lemma closed_map_snd:
+ fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+ assumes "compact S" "closedin (subtopology euclidean (S \<times> T)) c"
+ shows "closedin (subtopology euclidean T) (snd ` c)"
+proof -
+ have *: "snd ` (S \<times> T) \<subseteq> T"
+ by auto
+ show ?thesis
+ using proper_map [OF _ _ *] by (simp add: proper_map_snd assms)
+qed
+
+lemma closedin_compact_projection:
+ fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+ assumes "compact S" and clo: "closedin (subtopology euclidean (S \<times> T)) U"
+ shows "closedin (subtopology euclidean T) {y. \<exists>x. x \<in> S \<and> (x, y) \<in> U}"
+proof -
+ have "U \<subseteq> S \<times> T"
+ by (metis clo closedin_imp_subset)
+ then have "{y. \<exists>x. x \<in> S \<and> (x, y) \<in> U} = snd ` U"
+ by force
+ moreover have "closedin (subtopology euclidean T) (snd ` U)"
+ by (rule closed_map_snd [OF assms])
+ ultimately show ?thesis
+ by simp
+qed
+
+
+lemma closed_compact_projection:
+ fixes S :: "'a::euclidean_space set"
+ and T :: "('a * 'b::euclidean_space) set"
+ assumes "compact S" and clo: "closed T"
+ shows "closed {y. \<exists>x. x \<in> S \<and> (x, y) \<in> T}"
+proof -
+ have *: "{y. \<exists>x. x \<in> S \<and> Pair x y \<in> T} =
+ {y. \<exists>x. x \<in> S \<and> Pair x y \<in> ((S \<times> UNIV) \<inter> T)}"
+ by auto
+ show ?thesis
+ apply (subst *)
+ apply (rule closedin_closed_trans [OF _ closed_UNIV])
+ apply (rule closedin_compact_projection [OF \<open>compact S\<close>])
+ by (simp add: clo closedin_closed_Int)
+qed
+
subsubsection\<open>Representing affine hull as a finite intersection of hyperplanes\<close>
proposition affine_hull_convex_Int_nonempty_interior:
@@ -12082,4 +12391,151 @@
by (rule that)
qed
+subsection\<open>Several Variants of Paracompactness\<close>
+
+proposition paracompact:
+ fixes S :: "'a :: euclidean_space set"
+ assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
+ obtains \<C>' where "S \<subseteq> \<Union> \<C>'"
+ and "\<And>U. U \<in> \<C>' \<Longrightarrow> open U \<and> (\<exists>T. T \<in> \<C> \<and> U \<subseteq> T)"
+ and "\<And>x. x \<in> S
+ \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and>
+ finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
+proof (cases "S = {}")
+ case True with that show ?thesis by blast
+next
+ case False
+ have "\<exists>T U. x \<in> U \<and> open U \<and> closure U \<subseteq> T \<and> T \<in> \<C>" if "x \<in> S" for x
+ proof -
+ obtain T where "x \<in> T" "T \<in> \<C>" "open T"
+ using assms \<open>x \<in> S\<close> by blast
+ then obtain e where "e > 0" "cball x e \<subseteq> T"
+ by (force simp: open_contains_cball)
+ then show ?thesis
+ apply (rule_tac x = T in exI)
+ apply (rule_tac x = "ball x e" in exI)
+ using \<open>T \<in> \<C>\<close>
+ apply (simp add: closure_minimal)
+ done
+ qed
+ then obtain F G where Gin: "x \<in> G x" and oG: "open (G x)"
+ and clos: "closure (G x) \<subseteq> F x" and Fin: "F x \<in> \<C>"
+ if "x \<in> S" for x
+ by metis
+ then obtain \<F> where "\<F> \<subseteq> G ` S" "countable \<F>" "\<Union>\<F> = UNION S G"
+ using Lindelof [of "G ` S"] by (metis image_iff)
+ then obtain K where K: "K \<subseteq> S" "countable K" and eq: "UNION K G = UNION S G"
+ by (metis countable_subset_image)
+ with False Gin have "K \<noteq> {}" by force
+ then obtain a :: "nat \<Rightarrow> 'a" where "range a = K"
+ by (metis range_from_nat_into \<open>countable K\<close>)
+ then have odif: "\<And>n. open (F (a n) - \<Union>{closure (G (a m)) |m. m < n})"
+ using \<open>K \<subseteq> S\<close> Fin opC by (fastforce simp add:)
+ let ?C = "range (\<lambda>n. F(a n) - \<Union>{closure(G(a m)) |m. m < n})"
+ have enum_S: "\<exists>n. x \<in> F(a n) \<and> x \<in> G(a n)" if "x \<in> S" for x
+ proof -
+ have "\<exists>y \<in> K. x \<in> G y" using eq that Gin by fastforce
+ then show ?thesis
+ using clos K \<open>range a = K\<close> closure_subset by blast
+ qed
+ have 1: "S \<subseteq> Union ?C"
+ proof
+ fix x assume "x \<in> S"
+ define n where "n \<equiv> LEAST n. x \<in> F(a n)"
+ have n: "x \<in> F(a n)"
+ using enum_S [OF \<open>x \<in> S\<close>] by (force simp: n_def intro: LeastI)
+ have notn: "x \<notin> F(a m)" if "m < n" for m
+ using that not_less_Least by (force simp: n_def)
+ then have "x \<notin> \<Union>{closure (G (a m)) |m. m < n}"
+ using n \<open>K \<subseteq> S\<close> \<open>range a = K\<close> clos notn by fastforce
+ with n show "x \<in> Union ?C"
+ by blast
+ qed
+ have 3: "\<exists>V. open V \<and> x \<in> V \<and> finite {U. U \<in> ?C \<and> (U \<inter> V \<noteq> {})}" if "x \<in> S" for x
+ proof -
+ obtain n where n: "x \<in> F(a n)" "x \<in> G(a n)"
+ using \<open>x \<in> S\<close> enum_S by auto
+ have "{U \<in> ?C. U \<inter> G (a n) \<noteq> {}} \<subseteq> (\<lambda>n. F(a n) - \<Union>{closure(G(a m)) |m. m < n}) ` atMost n"
+ proof clarsimp
+ fix k assume "(F (a k) - \<Union>{closure (G (a m)) |m. m < k}) \<inter> G (a n) \<noteq> {}"
+ then have "k \<le> n"
+ by auto (metis closure_subset not_le subsetCE)
+ then show "F (a k) - \<Union>{closure (G (a m)) |m. m < k}
+ \<in> (\<lambda>n. F (a n) - \<Union>{closure (G (a m)) |m. m < n}) ` {..n}"
+ by force
+ qed
+ moreover have "finite ((\<lambda>n. F(a n) - \<Union>{closure(G(a m)) |m. m < n}) ` atMost n)"
+ by force
+ ultimately have *: "finite {U \<in> ?C. U \<inter> G (a n) \<noteq> {}}"
+ using finite_subset by blast
+ show ?thesis
+ apply (rule_tac x="G (a n)" in exI)
+ apply (intro conjI oG n *)
+ using \<open>K \<subseteq> S\<close> \<open>range a = K\<close> apply blast
+ done
+ qed
+ show ?thesis
+ apply (rule that [OF 1 _ 3])
+ using Fin \<open>K \<subseteq> S\<close> \<open>range a = K\<close> apply (auto simp: odif)
+ done
+qed
+
+
+corollary paracompact_closedin:
+ fixes S :: "'a :: euclidean_space set"
+ assumes cin: "closedin (subtopology euclidean U) S"
+ and oin: "\<And>T. T \<in> \<C> \<Longrightarrow> openin (subtopology euclidean U) T"
+ and "S \<subseteq> \<Union>\<C>"
+ obtains \<C>' where "S \<subseteq> \<Union> \<C>'"
+ and "\<And>V. V \<in> \<C>' \<Longrightarrow> openin (subtopology euclidean U) V \<and> (\<exists>T. T \<in> \<C> \<and> V \<subseteq> T)"
+ and "\<And>x. x \<in> U
+ \<Longrightarrow> \<exists>V. openin (subtopology euclidean U) V \<and> x \<in> V \<and>
+ finite {X. X \<in> \<C>' \<and> (X \<inter> V \<noteq> {})}"
+proof -
+ have "\<exists>Z. open Z \<and> (T = U \<inter> Z)" if "T \<in> \<C>" for T
+ using oin [OF that] by (auto simp: openin_open)
+ then obtain F where opF: "open (F T)" and intF: "U \<inter> F T = T" if "T \<in> \<C>" for T
+ by metis
+ obtain K where K: "closed K" "U \<inter> K = S"
+ using cin by (auto simp: closedin_closed)
+ have 1: "U \<subseteq> \<Union>insert (- K) (F ` \<C>)"
+ by clarsimp (metis Int_iff Union_iff \<open>U \<inter> K = S\<close> \<open>S \<subseteq> \<Union>\<C>\<close> subsetD intF)
+ have 2: "\<And>T. T \<in> insert (- K) (F ` \<C>) \<Longrightarrow> open T"
+ using \<open>closed K\<close> by (auto simp: opF)
+ obtain \<D> where "U \<subseteq> \<Union>\<D>"
+ and D1: "\<And>U. U \<in> \<D> \<Longrightarrow> open U \<and> (\<exists>T. T \<in> insert (- K) (F ` \<C>) \<and> U \<subseteq> T)"
+ and D2: "\<And>x. x \<in> U \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<D>. U \<inter> V \<noteq> {}}"
+ using paracompact [OF 1 2] by auto
+ let ?C = "{U \<inter> V |V. V \<in> \<D> \<and> (V \<inter> K \<noteq> {})}"
+ show ?thesis
+ proof (rule_tac \<C>' = "{U \<inter> V |V. V \<in> \<D> \<and> (V \<inter> K \<noteq> {})}" in that)
+ show "S \<subseteq> \<Union>?C"
+ using \<open>U \<inter> K = S\<close> \<open>U \<subseteq> \<Union>\<D>\<close> K by (blast dest!: subsetD)
+ show "\<And>V. V \<in> ?C \<Longrightarrow> openin (subtopology euclidean U) V \<and> (\<exists>T. T \<in> \<C> \<and> V \<subseteq> T)"
+ using D1 intF by fastforce
+ have *: "{X. (\<exists>V. X = U \<inter> V \<and> V \<in> \<D> \<and> V \<inter> K \<noteq> {}) \<and> X \<inter> (U \<inter> V) \<noteq> {}} \<subseteq>
+ (\<lambda>x. U \<inter> x) ` {U \<in> \<D>. U \<inter> V \<noteq> {}}" for V
+ by blast
+ show "\<exists>V. openin (subtopology euclidean U) V \<and> x \<in> V \<and> finite {X \<in> ?C. X \<inter> V \<noteq> {}}"
+ if "x \<in> U" for x
+ using D2 [OF that]
+ apply clarify
+ apply (rule_tac x="U \<inter> V" in exI)
+ apply (auto intro: that finite_subset [OF *])
+ done
+ qed
+qed
+
+corollary paracompact_closed:
+ fixes S :: "'a :: euclidean_space set"
+ assumes "closed S"
+ and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
+ and "S \<subseteq> \<Union>\<C>"
+ obtains \<C>' where "S \<subseteq> \<Union>\<C>'"
+ and "\<And>U. U \<in> \<C>' \<Longrightarrow> open U \<and> (\<exists>T. T \<in> \<C> \<and> U \<subseteq> T)"
+ and "\<And>x. \<exists>V. open V \<and> x \<in> V \<and>
+ finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
+using paracompact_closedin [of UNIV S \<C>] assms
+by (auto simp: open_openin [symmetric] closed_closedin [symmetric])
+
end
--- a/src/HOL/Multivariate_Analysis/Homeomorphism.thy Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Homeomorphism.thy Tue Jun 14 15:34:21 2016 +0100
@@ -933,7 +933,8 @@
by (simp add: \<open>open U\<close> closed_Compl)
define f :: "'a \<Rightarrow> 'a \<times> 'b" where "f \<equiv> \<lambda>x. (x, One /\<^sub>R setdist {x} (- U))"
have "continuous_on U (\<lambda>x. (x, One /\<^sub>R setdist {x} (- U)))"
- by (auto simp: Ucomp continuous_intros continuous_on_setdist)
+ apply (intro continuous_intros continuous_on_setdist)
+ by (simp add: Ucomp setdist_eq_0_sing_1)
then have homU: "homeomorphism U (f`U) f fst"
by (auto simp: f_def homeomorphism_def image_iff continuous_intros)
have cloS: "closedin (subtopology euclidean U) S"
@@ -945,9 +946,9 @@
have *: "r *\<^sub>R b = One \<Longrightarrow> b = (1 / r) *\<^sub>R One" for r and b::'b
by (metis One_non_0 nonzero_divide_eq_eq real_vector.scale_eq_0_iff real_vector.scale_scale scaleR_one)
have "f ` U = {z. (setdist {fst z} (- U) *\<^sub>R snd z) \<in> {One}}"
- apply (auto simp: f_def field_simps Ucomp)
+ apply (auto simp: f_def setdist_eq_0_sing_1 field_simps Ucomp)
apply (rule_tac x=a in image_eqI)
- apply (auto simp: * dest: setdist1D)
+ apply (auto simp: * setdist_eq_0_sing_1 dest: setdist1D)
done
then have clfU: "closed (f ` U)"
apply (rule ssubst)
@@ -1103,4 +1104,176 @@
using assms
by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
+subsection\<open>Covering spaces and lifting results for them\<close>
+
+definition covering_space
+ :: "'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
+ where
+ "covering_space c p s \<equiv>
+ continuous_on c p \<and> p ` c = s \<and>
+ (\<forall>x \<in> s. \<exists>t. x \<in> t \<and> openin (subtopology euclidean s) t \<and>
+ (\<exists>v. \<Union>v = {x. x \<in> c \<and> p x \<in> t} \<and>
+ (\<forall>u \<in> v. openin (subtopology euclidean c) u) \<and>
+ pairwise disjnt v \<and>
+ (\<forall>u \<in> v. \<exists>q. homeomorphism u t p q)))"
+
+lemma covering_space_imp_continuous: "covering_space c p s \<Longrightarrow> continuous_on c p"
+ by (simp add: covering_space_def)
+
+lemma covering_space_imp_surjective: "covering_space c p s \<Longrightarrow> p ` c = s"
+ by (simp add: covering_space_def)
+
+lemma homeomorphism_imp_covering_space: "homeomorphism s t f g \<Longrightarrow> covering_space s f t"
+ apply (simp add: homeomorphism_def covering_space_def, clarify)
+ apply (rule_tac x=t in exI, simp)
+ apply (rule_tac x="{s}" in exI, auto)
+ done
+
+lemma covering_space_local_homeomorphism:
+ assumes "covering_space c p s" "x \<in> c"
+ obtains t u q where "x \<in> t" "openin (subtopology euclidean c) t"
+ "p x \<in> u" "openin (subtopology euclidean s) u"
+ "homeomorphism t u p q"
+using assms
+apply (simp add: covering_space_def, clarify)
+apply (drule_tac x="p x" in bspec, force)
+by (metis (no_types, lifting) Union_iff mem_Collect_eq)
+
+
+lemma covering_space_local_homeomorphism_alt:
+ assumes p: "covering_space c p s" and "y \<in> s"
+ obtains x t u q where "p x = y"
+ "x \<in> t" "openin (subtopology euclidean c) t"
+ "y \<in> u" "openin (subtopology euclidean s) u"
+ "homeomorphism t u p q"
+proof -
+ obtain x where "p x = y" "x \<in> c"
+ using assms covering_space_imp_surjective by blast
+ show ?thesis
+ apply (rule covering_space_local_homeomorphism [OF p \<open>x \<in> c\<close>])
+ using that \<open>p x = y\<close> by blast
+qed
+
+proposition covering_space_open_map:
+ fixes s :: "'a :: metric_space set" and t :: "'b :: metric_space set"
+ assumes p: "covering_space c p s" and t: "openin (subtopology euclidean c) t"
+ shows "openin (subtopology euclidean s) (p ` t)"
+proof -
+ have pce: "p ` c = s"
+ and covs:
+ "\<And>x. x \<in> s \<Longrightarrow>
+ \<exists>X VS. x \<in> X \<and> openin (subtopology euclidean s) X \<and>
+ \<Union>VS = {x. x \<in> c \<and> p x \<in> X} \<and>
+ (\<forall>u \<in> VS. openin (subtopology euclidean c) u) \<and>
+ pairwise disjnt VS \<and>
+ (\<forall>u \<in> VS. \<exists>q. homeomorphism u X p q)"
+ using p by (auto simp: covering_space_def)
+ have "t \<subseteq> c" by (metis openin_euclidean_subtopology_iff t)
+ have "\<exists>T. openin (subtopology euclidean s) T \<and> y \<in> T \<and> T \<subseteq> p ` t"
+ if "y \<in> p ` t" for y
+ proof -
+ have "y \<in> s" using \<open>t \<subseteq> c\<close> pce that by blast
+ obtain U VS where "y \<in> U" and U: "openin (subtopology euclidean s) U"
+ and VS: "\<Union>VS = {x. x \<in> c \<and> p x \<in> U}"
+ and openVS: "\<forall>V \<in> VS. openin (subtopology euclidean c) V"
+ and homVS: "\<And>V. V \<in> VS \<Longrightarrow> \<exists>q. homeomorphism V U p q"
+ using covs [OF \<open>y \<in> s\<close>] by auto
+ obtain x where "x \<in> c" "p x \<in> U" "x \<in> t" "p x = y"
+ apply simp
+ using t [unfolded openin_euclidean_subtopology_iff] \<open>y \<in> U\<close> \<open>y \<in> p ` t\<close> by blast
+ with VS obtain V where "x \<in> V" "V \<in> VS" by auto
+ then obtain q where q: "homeomorphism V U p q" using homVS by blast
+ then have ptV: "p ` (t \<inter> V) = U \<inter> {z. q z \<in> (t \<inter> V)}"
+ using VS \<open>V \<in> VS\<close> by (auto simp: homeomorphism_def)
+ have ocv: "openin (subtopology euclidean c) V"
+ by (simp add: \<open>V \<in> VS\<close> openVS)
+ have "openin (subtopology euclidean U) {z \<in> U. q z \<in> t \<inter> V}"
+ apply (rule continuous_on_open [THEN iffD1, rule_format])
+ using homeomorphism_def q apply blast
+ using openin_subtopology_Int_subset [of c] q t unfolding homeomorphism_def
+ by (metis inf.absorb_iff2 Int_commute ocv openin_euclidean_subtopology_iff)
+ then have os: "openin (subtopology euclidean s) (U \<inter> {z. q z \<in> t \<inter> V})"
+ using openin_trans [of U] by (simp add: Collect_conj_eq U)
+ show ?thesis
+ apply (rule_tac x = "p ` (t \<inter> V)" in exI)
+ apply (rule conjI)
+ apply (simp only: ptV os)
+ using \<open>p x = y\<close> \<open>x \<in> V\<close> \<open>x \<in> t\<close> apply blast
+ done
+ qed
+ with openin_subopen show ?thesis by blast
+qed
+
+lemma covering_space_lift_unique_gen:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
+ fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
+ assumes cov: "covering_space c p s"
+ and eq: "g1 a = g2 a"
+ and f: "continuous_on t f" "f ` t \<subseteq> s"
+ and g1: "continuous_on t g1" "g1 ` t \<subseteq> c"
+ and fg1: "\<And>x. x \<in> t \<Longrightarrow> f x = p(g1 x)"
+ and g2: "continuous_on t g2" "g2 ` t \<subseteq> c"
+ and fg2: "\<And>x. x \<in> t \<Longrightarrow> f x = p(g2 x)"
+ and u_compt: "u \<in> components t" and "a \<in> u" "x \<in> u"
+ shows "g1 x = g2 x"
+proof -
+ have "u \<subseteq> t" by (rule in_components_subset [OF u_compt])
+ def G12 \<equiv> "{x \<in> u. g1 x - g2 x = 0}"
+ have "connected u" by (rule in_components_connected [OF u_compt])
+ have contu: "continuous_on u g1" "continuous_on u g2"
+ using \<open>u \<subseteq> t\<close> continuous_on_subset g1 g2 by blast+
+ have o12: "openin (subtopology euclidean u) G12"
+ unfolding G12_def
+ proof (subst openin_subopen, clarify)
+ fix z
+ assume z: "z \<in> u" "g1 z - g2 z = 0"
+ obtain v w q where "g1 z \<in> v" and ocv: "openin (subtopology euclidean c) v"
+ and "p (g1 z) \<in> w" and osw: "openin (subtopology euclidean s) w"
+ and hom: "homeomorphism v w p q"
+ apply (rule_tac x = "g1 z" in covering_space_local_homeomorphism [OF cov])
+ using \<open>u \<subseteq> t\<close> \<open>z \<in> u\<close> g1(2) apply blast+
+ done
+ have "g2 z \<in> v" using \<open>g1 z \<in> v\<close> z by auto
+ have gg: "{x \<in> u. g x \<in> v} = {x \<in> u. g x \<in> (v \<inter> g ` u)}" for g
+ by auto
+ have "openin (subtopology euclidean (g1 ` u)) (v \<inter> g1 ` u)"
+ using ocv \<open>u \<subseteq> t\<close> g1 by (fastforce simp add: openin_open)
+ then have 1: "openin (subtopology euclidean u) {x \<in> u. g1 x \<in> v}"
+ unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
+ have "openin (subtopology euclidean (g2 ` u)) (v \<inter> g2 ` u)"
+ using ocv \<open>u \<subseteq> t\<close> g2 by (fastforce simp add: openin_open)
+ then have 2: "openin (subtopology euclidean u) {x \<in> u. g2 x \<in> v}"
+ unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
+ show "\<exists>T. openin (subtopology euclidean u) T \<and>
+ z \<in> T \<and> T \<subseteq> {z \<in> u. g1 z - g2 z = 0}"
+ using z
+ apply (rule_tac x = "{x. x \<in> u \<and> g1 x \<in> v} \<inter> {x. x \<in> u \<and> g2 x \<in> v}" in exI)
+ apply (intro conjI)
+ apply (rule openin_Int [OF 1 2])
+ using \<open>g1 z \<in> v\<close> \<open>g2 z \<in> v\<close> apply (force simp:, clarify)
+ apply (metis \<open>u \<subseteq> t\<close> subsetD eq_iff_diff_eq_0 fg1 fg2 hom homeomorphism_def)
+ done
+ qed
+ have c12: "closedin (subtopology euclidean u) G12"
+ unfolding G12_def
+ by (intro continuous_intros continuous_closedin_preimage_constant contu)
+ have "G12 = {} \<or> G12 = u"
+ by (intro connected_clopen [THEN iffD1, rule_format] \<open>connected u\<close> conjI o12 c12)
+ with eq \<open>a \<in> u\<close> have "\<And>x. x \<in> u \<Longrightarrow> g1 x - g2 x = 0" by (auto simp: G12_def)
+ then show ?thesis
+ using \<open>x \<in> u\<close> by force
+qed
+
+proposition covering_space_lift_unique:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
+ fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
+ assumes "covering_space c p s"
+ "g1 a = g2 a"
+ "continuous_on t f" "f ` t \<subseteq> s"
+ "continuous_on t g1" "g1 ` t \<subseteq> c" "\<And>x. x \<in> t \<Longrightarrow> f x = p(g1 x)"
+ "continuous_on t g2" "g2 ` t \<subseteq> c" "\<And>x. x \<in> t \<Longrightarrow> f x = p(g2 x)"
+ "connected t" "a \<in> t" "x \<in> t"
+ shows "g1 x = g2 x"
+using covering_space_lift_unique_gen [of c p s] in_components_self assms ex_in_conv by blast
+
end
--- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Jun 14 15:34:21 2016 +0100
@@ -11,6 +11,173 @@
"~~/src/HOL/Library/Indicator_Function"
begin
+(*FIXME: move elsewhere and use the existing locales*)
+
+subsection \<open>Using additivity of lifted function to encode definedness.\<close>
+
+definition "neutral opp = (SOME x. \<forall>y. opp x y = y \<and> opp y x = y)"
+
+fun lifted where
+ "lifted (opp :: 'a \<Rightarrow> 'a \<Rightarrow> 'b) (Some x) (Some y) = Some (opp x y)"
+| "lifted opp None _ = (None::'b option)"
+| "lifted opp _ None = None"
+
+lemma lifted_simp_1[simp]: "lifted opp v None = None"
+ by (induct v) auto
+
+definition "monoidal opp \<longleftrightarrow>
+ (\<forall>x y. opp x y = opp y x) \<and>
+ (\<forall>x y z. opp x (opp y z) = opp (opp x y) z) \<and>
+ (\<forall>x. opp (neutral opp) x = x)"
+
+lemma monoidalI:
+ assumes "\<And>x y. opp x y = opp y x"
+ and "\<And>x y z. opp x (opp y z) = opp (opp x y) z"
+ and "\<And>x. opp (neutral opp) x = x"
+ shows "monoidal opp"
+ unfolding monoidal_def using assms by fastforce
+
+lemma monoidal_ac:
+ assumes "monoidal opp"
+ shows [simp]: "opp (neutral opp) a = a"
+ and [simp]: "opp a (neutral opp) = a"
+ and "opp a b = opp b a"
+ and "opp (opp a b) c = opp a (opp b c)"
+ and "opp a (opp b c) = opp b (opp a c)"
+ using assms unfolding monoidal_def by metis+
+
+lemma neutral_lifted [cong]:
+ assumes "monoidal opp"
+ shows "neutral (lifted opp) = Some (neutral opp)"
+proof -
+ { fix x
+ assume "\<forall>y. lifted opp x y = y \<and> lifted opp y x = y"
+ then have "Some (neutral opp) = x"
+ apply (induct x)
+ apply force
+ by (metis assms lifted.simps(1) monoidal_ac(2) option.inject) }
+ note [simp] = this
+ show ?thesis
+ apply (subst neutral_def)
+ apply (intro some_equality allI)
+ apply (induct_tac y)
+ apply (auto simp add:monoidal_ac[OF assms])
+ done
+qed
+
+lemma monoidal_lifted[intro]:
+ assumes "monoidal opp"
+ shows "monoidal (lifted opp)"
+ unfolding monoidal_def split_option_all neutral_lifted[OF assms]
+ using monoidal_ac[OF assms]
+ by auto
+
+definition "support opp f s = {x. x\<in>s \<and> f x \<noteq> neutral opp}"
+definition "fold' opp e s = (if finite s then Finite_Set.fold opp e s else e)"
+definition "iterate opp s f = fold' (\<lambda>x a. opp (f x) a) (neutral opp) (support opp f s)"
+
+lemma support_subset[intro]: "support opp f s \<subseteq> s"
+ unfolding support_def by auto
+
+lemma support_empty[simp]: "support opp f {} = {}"
+ using support_subset[of opp f "{}"] by auto
+
+lemma comp_fun_commute_monoidal[intro]:
+ assumes "monoidal opp"
+ shows "comp_fun_commute opp"
+ unfolding comp_fun_commute_def
+ using monoidal_ac[OF assms]
+ by auto
+
+lemma support_clauses:
+ "\<And>f g s. support opp f {} = {}"
+ "\<And>f g s. support opp f (insert x s) =
+ (if f(x) = neutral opp then support opp f s else insert x (support opp f s))"
+ "\<And>f g s. support opp f (s - {x}) = (support opp f s) - {x}"
+ "\<And>f g s. support opp f (s \<union> t) = (support opp f s) \<union> (support opp f t)"
+ "\<And>f g s. support opp f (s \<inter> t) = (support opp f s) \<inter> (support opp f t)"
+ "\<And>f g s. support opp f (s - t) = (support opp f s) - (support opp f t)"
+ "\<And>f g s. support opp g (f ` s) = f ` (support opp (g \<circ> f) s)"
+ unfolding support_def by auto
+
+lemma finite_support[intro]: "finite s \<Longrightarrow> finite (support opp f s)"
+ unfolding support_def by auto
+
+lemma iterate_empty[simp]: "iterate opp {} f = neutral opp"
+ unfolding iterate_def fold'_def by auto
+
+lemma iterate_insert[simp]:
+ assumes "monoidal opp"
+ and "finite s"
+ shows "iterate opp (insert x s) f =
+ (if x \<in> s then iterate opp s f else opp (f x) (iterate opp s f))"
+proof (cases "x \<in> s")
+ case True
+ then show ?thesis by (auto simp: insert_absorb iterate_def)
+next
+ case False
+ note * = comp_fun_commute.comp_comp_fun_commute [OF comp_fun_commute_monoidal[OF assms(1)]]
+ show ?thesis
+ proof (cases "f x = neutral opp")
+ case True
+ then show ?thesis
+ using assms \<open>x \<notin> s\<close>
+ by (auto simp: iterate_def support_clauses)
+ next
+ case False
+ with \<open>x \<notin> s\<close> \<open>finite s\<close> support_subset show ?thesis
+ apply (simp add: iterate_def fold'_def support_clauses)
+ apply (subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def])
+ apply (force simp add: )+
+ done
+ qed
+qed
+
+lemma iterate_some:
+ "\<lbrakk>monoidal opp; finite s\<rbrakk> \<Longrightarrow> iterate (lifted opp) s (\<lambda>x. Some(f x)) = Some (iterate opp s f)"
+ by (erule finite_induct) (auto simp: monoidal_lifted)
+
+lemma neutral_add[simp]: "neutral op + = (0::'a::comm_monoid_add)"
+ unfolding neutral_def
+ by (force elim: allE [where x=0])
+
+lemma support_if: "a \<noteq> neutral opp \<Longrightarrow> support opp (\<lambda>x. if P x then a else neutral opp) A = {x \<in> A. P x}"
+unfolding support_def
+by (force intro: Collect_cong)
+
+lemma support_if_subset: "support opp (\<lambda>x. if P x then a else neutral opp) A \<subseteq> {x \<in> A. P x}"
+by (simp add: subset_iff support_def)
+
+definition supp_setsum where "supp_setsum f A \<equiv> setsum f (support op+ f A)"
+
+lemma supp_setsum_divide_distrib:
+ "supp_setsum f A / (r::'a::field) = supp_setsum (\<lambda>n. f n / r) A"
+apply (cases "r = 0")
+apply (simp add: supp_setsum_def)
+apply (simp add: supp_setsum_def setsum_divide_distrib support_def)
+done
+
+(*FIXME move up e.g. to Library/Convex.thy*)
+lemma convex_supp_setsum:
+ assumes "convex S" and 1: "supp_setsum u I = 1"
+ and "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> u i \<and> (u i = 0 \<or> f i \<in> S)"
+ shows "supp_setsum (\<lambda>i. u i *\<^sub>R f i) I \<in> S"
+proof -
+ have fin: "finite {i \<in> I. u i \<noteq> 0}"
+ using 1 setsum.infinite by (force simp: supp_setsum_def support_def)
+ then have eq: "supp_setsum(\<lambda>i. u i *\<^sub>R f i) I =
+ setsum (\<lambda>i. u i *\<^sub>R f i) {i \<in> I. u i \<noteq> 0}"
+ by (force intro: setsum.mono_neutral_left simp: supp_setsum_def support_def)
+ show ?thesis
+ apply (simp add: eq)
+ apply (rule convex_setsum [OF fin \<open>convex S\<close>])
+ using 1 assms apply (auto simp: supp_setsum_def support_def)
+ done
+qed
+
+(*END OF SUPPORT, ETC.*)
+
+
lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
@@ -3565,8 +3732,6 @@
subsection \<open>Generalized notion of additivity.\<close>
-definition "neutral opp = (SOME x. \<forall>y. opp x y = y \<and> opp y x = y)"
-
definition operative :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (('b::euclidean_space) set \<Rightarrow> 'a) \<Rightarrow> bool"
where "operative opp f \<longleftrightarrow>
(\<forall>a b. content (cbox a b) = 0 \<longrightarrow> f (cbox a b) = neutral opp) \<and>
@@ -3587,135 +3752,8 @@
unfolding operative_def by (rule property_empty_interval) auto
-subsection \<open>Using additivity of lifted function to encode definedness.\<close>
-
-fun lifted where
- "lifted (opp :: 'a \<Rightarrow> 'a \<Rightarrow> 'b) (Some x) (Some y) = Some (opp x y)"
-| "lifted opp None _ = (None::'b option)"
-| "lifted opp _ None = None"
-
-lemma lifted_simp_1[simp]: "lifted opp v None = None"
- by (induct v) auto
-
-definition "monoidal opp \<longleftrightarrow>
- (\<forall>x y. opp x y = opp y x) \<and>
- (\<forall>x y z. opp x (opp y z) = opp (opp x y) z) \<and>
- (\<forall>x. opp (neutral opp) x = x)"
-
-lemma monoidalI:
- assumes "\<And>x y. opp x y = opp y x"
- and "\<And>x y z. opp x (opp y z) = opp (opp x y) z"
- and "\<And>x. opp (neutral opp) x = x"
- shows "monoidal opp"
- unfolding monoidal_def using assms by fastforce
-
-lemma monoidal_ac:
- assumes "monoidal opp"
- shows [simp]: "opp (neutral opp) a = a"
- and [simp]: "opp a (neutral opp) = a"
- and "opp a b = opp b a"
- and "opp (opp a b) c = opp a (opp b c)"
- and "opp a (opp b c) = opp b (opp a c)"
- using assms unfolding monoidal_def by metis+
-
-lemma neutral_lifted [cong]:
- assumes "monoidal opp"
- shows "neutral (lifted opp) = Some (neutral opp)"
-proof -
- { fix x
- assume "\<forall>y. lifted opp x y = y \<and> lifted opp y x = y"
- then have "Some (neutral opp) = x"
- apply (induct x)
- apply force
- by (metis assms lifted.simps(1) monoidal_ac(2) option.inject) }
- note [simp] = this
- show ?thesis
- apply (subst neutral_def)
- apply (intro some_equality allI)
- apply (induct_tac y)
- apply (auto simp add:monoidal_ac[OF assms])
- done
-qed
-
-lemma monoidal_lifted[intro]:
- assumes "monoidal opp"
- shows "monoidal (lifted opp)"
- unfolding monoidal_def split_option_all neutral_lifted[OF assms]
- using monoidal_ac[OF assms]
- by auto
-
-definition "support opp f s = {x. x\<in>s \<and> f x \<noteq> neutral opp}"
-definition "fold' opp e s = (if finite s then Finite_Set.fold opp e s else e)"
-definition "iterate opp s f = fold' (\<lambda>x a. opp (f x) a) (neutral opp) (support opp f s)"
-
-lemma support_subset[intro]: "support opp f s \<subseteq> s"
- unfolding support_def by auto
-
-lemma support_empty[simp]: "support opp f {} = {}"
- using support_subset[of opp f "{}"] by auto
-
-lemma comp_fun_commute_monoidal[intro]:
- assumes "monoidal opp"
- shows "comp_fun_commute opp"
- unfolding comp_fun_commute_def
- using monoidal_ac[OF assms]
- by auto
-
-lemma support_clauses:
- "\<And>f g s. support opp f {} = {}"
- "\<And>f g s. support opp f (insert x s) =
- (if f(x) = neutral opp then support opp f s else insert x (support opp f s))"
- "\<And>f g s. support opp f (s - {x}) = (support opp f s) - {x}"
- "\<And>f g s. support opp f (s \<union> t) = (support opp f s) \<union> (support opp f t)"
- "\<And>f g s. support opp f (s \<inter> t) = (support opp f s) \<inter> (support opp f t)"
- "\<And>f g s. support opp f (s - t) = (support opp f s) - (support opp f t)"
- "\<And>f g s. support opp g (f ` s) = f ` (support opp (g \<circ> f) s)"
- unfolding support_def by auto
-
-lemma finite_support[intro]: "finite s \<Longrightarrow> finite (support opp f s)"
- unfolding support_def by auto
-
-lemma iterate_empty[simp]: "iterate opp {} f = neutral opp"
- unfolding iterate_def fold'_def by auto
-
-lemma iterate_insert[simp]:
- assumes "monoidal opp"
- and "finite s"
- shows "iterate opp (insert x s) f =
- (if x \<in> s then iterate opp s f else opp (f x) (iterate opp s f))"
-proof (cases "x \<in> s")
- case True
- then show ?thesis by (auto simp: insert_absorb iterate_def)
-next
- case False
- note * = comp_fun_commute.comp_comp_fun_commute [OF comp_fun_commute_monoidal[OF assms(1)]]
- show ?thesis
- proof (cases "f x = neutral opp")
- case True
- then show ?thesis
- using assms \<open>x \<notin> s\<close>
- by (auto simp: iterate_def support_clauses)
- next
- case False
- with \<open>x \<notin> s\<close> \<open>finite s\<close> support_subset show ?thesis
- apply (simp add: iterate_def fold'_def support_clauses)
- apply (subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def])
- apply (force simp add: )+
- done
- qed
-qed
-
-lemma iterate_some:
- "\<lbrakk>monoidal opp; finite s\<rbrakk> \<Longrightarrow> iterate (lifted opp) s (\<lambda>x. Some(f x)) = Some (iterate opp s f)"
- by (erule finite_induct) (auto simp: monoidal_lifted)
-
-
subsection \<open>Two key instances of additivity.\<close>
-lemma neutral_add[simp]: "neutral op + = (0::'a::comm_monoid_add)"
- unfolding neutral_def
- by (force elim: allE [where x=0])
-
lemma operative_content[intro]: "operative (op +) content"
by (force simp add: operative_def content_split[symmetric])
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Tue Jun 14 15:34:21 2016 +0100
@@ -1433,8 +1433,8 @@
ultimately show False
using *[unfolded connected_local not_ex, rule_format,
of "{x\<in>{0..1}. g x \<in> e1}" "{x\<in>{0..1}. g x \<in> e2}"]
- using continuous_openin_preimage[OF g(1)[unfolded path_def] as(1)]
- using continuous_openin_preimage[OF g(1)[unfolded path_def] as(2)]
+ using continuous_openin_preimage_gen[OF g(1)[unfolded path_def] as(1)]
+ using continuous_openin_preimage_gen[OF g(1)[unfolded path_def] as(2)]
by auto
qed
@@ -4605,6 +4605,24 @@
using eq homeomorphism_sym homeomorphism_symD [OF hom] apply blast+
done
+lemma homeomorphic_locally:
+ fixes S:: "'a::metric_space set" and T:: "'b::metric_space set"
+ assumes hom: "S homeomorphic T"
+ and iff: "\<And>X Y. X homeomorphic Y \<Longrightarrow> (P X \<longleftrightarrow> Q Y)"
+ shows "locally P S \<longleftrightarrow> locally Q T"
+proof -
+ obtain f g where hom: "homeomorphism S T f g"
+ using assms by (force simp: homeomorphic_def)
+ then show ?thesis
+ using homeomorphic_def local.iff
+ by (blast intro!: homeomorphism_locally)
+qed
+
+lemma homeomorphic_local_compactness:
+ fixes S:: "'a::metric_space set" and T:: "'b::metric_space set"
+ shows "S homeomorphic T \<Longrightarrow> locally compact S \<longleftrightarrow> locally compact T"
+by (simp add: homeomorphic_compactness homeomorphic_locally)
+
lemma locally_translation:
fixes P :: "'a :: real_normed_vector set \<Rightarrow> bool"
shows
@@ -4651,6 +4669,107 @@
done
qed
+subsection\<open>Sort of induction principle for connected sets\<close>
+
+lemma connected_induction:
+ assumes "connected S"
+ and opD: "\<And>T a. \<lbrakk>openin (subtopology euclidean S) T; a \<in> T\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> T \<and> P z"
+ and opI: "\<And>a. a \<in> S
+ \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and>
+ (\<forall>x \<in> T. \<forall>y \<in> T. P x \<and> P y \<and> Q x \<longrightarrow> Q y)"
+ and etc: "a \<in> S" "b \<in> S" "P a" "P b" "Q a"
+ shows "Q b"
+proof -
+ have 1: "openin (subtopology euclidean S)
+ {b. \<exists>T. openin (subtopology euclidean S) T \<and>
+ b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> Q x)}"
+ apply (subst openin_subopen, clarify)
+ apply (rule_tac x=T in exI, auto)
+ done
+ have 2: "openin (subtopology euclidean S)
+ {b. \<exists>T. openin (subtopology euclidean S) T \<and>
+ b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> ~ Q x)}"
+ apply (subst openin_subopen, clarify)
+ apply (rule_tac x=T in exI, auto)
+ done
+ show ?thesis
+ using \<open>connected S\<close>
+ apply (simp only: connected_openin HOL.not_ex HOL.de_Morgan_conj)
+ apply (elim disjE allE)
+ apply (blast intro: 1)
+ apply (blast intro: 2, simp_all)
+ apply clarify apply (metis opI)
+ using opD apply (blast intro: etc elim: dest:)
+ using opI etc apply meson+
+ done
+qed
+
+lemma connected_equivalence_relation_gen:
+ assumes "connected S"
+ and etc: "a \<in> S" "b \<in> S" "P a" "P b"
+ and trans: "\<And>x y z. \<lbrakk>R x y; R y z\<rbrakk> \<Longrightarrow> R x z"
+ and opD: "\<And>T a. \<lbrakk>openin (subtopology euclidean S) T; a \<in> T\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> T \<and> P z"
+ and opI: "\<And>a. a \<in> S
+ \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and>
+ (\<forall>x \<in> T. \<forall>y \<in> T. P x \<and> P y \<longrightarrow> R x y)"
+ shows "R a b"
+proof -
+ have "\<And>a b c. \<lbrakk>a \<in> S; P a; b \<in> S; c \<in> S; P b; P c; R a b\<rbrakk> \<Longrightarrow> R a c"
+ apply (rule connected_induction [OF \<open>connected S\<close> opD], simp_all)
+ by (meson trans opI)
+ then show ?thesis by (metis etc opI)
+qed
+
+lemma connected_induction_simple:
+ assumes "connected S"
+ and etc: "a \<in> S" "b \<in> S" "P a"
+ and opI: "\<And>a. a \<in> S
+ \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and>
+ (\<forall>x \<in> T. \<forall>y \<in> T. P x \<longrightarrow> P y)"
+ shows "P b"
+apply (rule connected_induction [OF \<open>connected S\<close> _, where P = "\<lambda>x. True"], blast)
+apply (frule opI)
+using etc apply simp_all
+done
+
+lemma connected_equivalence_relation:
+ assumes "connected S"
+ and etc: "a \<in> S" "b \<in> S"
+ and sym: "\<And>x y z. R x y \<Longrightarrow> R y x"
+ and trans: "\<And>x y z. R x y \<and> R y z \<Longrightarrow> R x z"
+ and opI: "\<And>a. a \<in> S
+ \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and> (\<forall>x \<in> T. R a x)"
+ shows "R a b"
+proof -
+ have "\<And>a b c. \<lbrakk>a \<in> S; b \<in> S; c \<in> S; R a b\<rbrakk> \<Longrightarrow> R a c"
+ apply (rule connected_induction_simple [OF \<open>connected S\<close>], simp_all)
+ by (meson local.sym local.trans opI)
+ then show ?thesis by (metis etc opI)
+qed
+
+
+lemma locally_constant_imp_constant:
+ assumes "connected S"
+ and opI: "\<And>a. a \<in> S
+ \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and> (\<forall>x \<in> T. f x = f a)"
+ shows "f constant_on S"
+proof -
+ have "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> f x = f y"
+ apply (rule connected_equivalence_relation [OF \<open>connected S\<close>], simp_all)
+ by (metis opI)
+ then show ?thesis
+ by (metis constant_on_def)
+qed
+
+lemma locally_constant:
+ "connected S \<Longrightarrow> locally (\<lambda>U. f constant_on U) S \<longleftrightarrow> f constant_on S"
+apply (simp add: locally_def)
+apply (rule iffI)
+ apply (rule locally_constant_imp_constant, assumption)
+ apply (metis (mono_tags, hide_lams) constant_on_def constant_on_subset openin_subtopology_self)
+by (meson constant_on_subset openin_imp_subset order_refl)
+
+
subsection\<open>Basic properties of local compactness\<close>
lemma locally_compact:
@@ -5145,7 +5264,7 @@
lemma continuous_openin_preimage_eq:
"continuous_on S f \<longleftrightarrow>
(\<forall>t. open t \<longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
-apply (auto simp: continuous_openin_preimage)
+apply (auto simp: continuous_openin_preimage_gen)
apply (fastforce simp add: continuous_on_open openin_open)
done
@@ -5171,7 +5290,7 @@
using Union_components by blast
then show "openin (subtopology euclidean S) {x \<in> S. f x \<in> t}"
using \<open>open t\<close> assms
- by (fastforce intro: openin_trans continuous_openin_preimage)
+ by (fastforce intro: openin_trans continuous_openin_preimage_gen)
qed
lemma continuous_on_components:
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Jun 14 15:34:21 2016 +0100
@@ -1906,12 +1906,12 @@
lemma islimpt_in_closure: "(x islimpt S) = (x:closure(S-{x}))"
unfolding closure_def using islimpt_punctured by blast
-lemma connected_imp_connected_closure: "connected s \<Longrightarrow> connected (closure s)"
+lemma connected_imp_connected_closure: "connected S \<Longrightarrow> connected (closure S)"
by (rule connectedI) (meson closure_subset open_Int open_Int_closure_eq_empty subset_trans connectedD)
lemma limpt_of_limpts:
fixes x :: "'a::metric_space"
- shows "x islimpt {y. y islimpt s} \<Longrightarrow> x islimpt s"
+ shows "x islimpt {y. y islimpt S} \<Longrightarrow> x islimpt S"
apply (clarsimp simp add: islimpt_approachable)
apply (drule_tac x="e/2" in spec)
apply (auto simp: simp del: less_divide_eq_numeral1)
@@ -1920,27 +1920,37 @@
apply (erule rev_bexI)
by (metis dist_commute dist_triangle_half_r less_trans less_irrefl)
-lemma closed_limpts: "closed {x::'a::metric_space. x islimpt s}"
+lemma closed_limpts: "closed {x::'a::metric_space. x islimpt S}"
using closed_limpt limpt_of_limpts by blast
lemma limpt_of_closure:
fixes x :: "'a::metric_space"
- shows "x islimpt closure s \<longleftrightarrow> x islimpt s"
+ shows "x islimpt closure S \<longleftrightarrow> x islimpt S"
by (auto simp: closure_def islimpt_Un dest: limpt_of_limpts)
lemma closedin_limpt:
- "closedin (subtopology euclidean t) s \<longleftrightarrow> s \<subseteq> t \<and> (\<forall>x. x islimpt s \<and> x \<in> t \<longrightarrow> x \<in> s)"
+ "closedin (subtopology euclidean T) S \<longleftrightarrow> S \<subseteq> T \<and> (\<forall>x. x islimpt S \<and> x \<in> T \<longrightarrow> x \<in> S)"
apply (simp add: closedin_closed, safe)
apply (simp add: closed_limpt islimpt_subset)
- apply (rule_tac x="closure s" in exI)
+ apply (rule_tac x="closure S" in exI)
apply simp
apply (force simp: closure_def)
done
lemma closedin_closed_eq:
- "closed s \<Longrightarrow> (closedin (subtopology euclidean s) t \<longleftrightarrow> closed t \<and> t \<subseteq> s)"
+ "closed S \<Longrightarrow> (closedin (subtopology euclidean S) T \<longleftrightarrow> closed T \<and> T \<subseteq> S)"
by (meson closedin_limpt closed_subset closedin_closed_trans)
+lemma closedin_subset_trans:
+ "\<lbrakk>closedin (subtopology euclidean U) S; S \<subseteq> T; T \<subseteq> U\<rbrakk>
+ \<Longrightarrow> closedin (subtopology euclidean T) S"
+by (meson closedin_limpt subset_iff)
+
+lemma closedin_Times:
+ "\<lbrakk>closedin (subtopology euclidean S) S'; closedin (subtopology euclidean T) T'\<rbrakk>
+ \<Longrightarrow> closedin (subtopology euclidean (S \<times> T)) (S' \<times> T')"
+unfolding closedin_closed using closed_Times by blast
+
lemma bdd_below_closure:
fixes A :: "real set"
assumes "bdd_below A"
@@ -2438,14 +2448,13 @@
by (rule topological_tendstoI, auto elim: eventually_mono)
lemma Lim_transform_within_set:
- fixes a l :: "'a::real_normed_vector"
- shows "\<lbrakk>(f \<longlongrightarrow> l) (at a within s); eventually (\<lambda>x. x \<in> s \<longleftrightarrow> x \<in> t) (at a)\<rbrakk>
- \<Longrightarrow> (f \<longlongrightarrow> l) (at a within t)"
+ fixes a :: "'a::metric_space" and l :: "'b::metric_space"
+ shows "\<lbrakk>(f \<longlongrightarrow> l) (at a within S); eventually (\<lambda>x. x \<in> S \<longleftrightarrow> x \<in> T) (at a)\<rbrakk>
+ \<Longrightarrow> (f \<longlongrightarrow> l) (at a within T)"
apply (clarsimp simp: eventually_at Lim_within)
apply (drule_tac x=e in spec, clarify)
apply (rename_tac k)
-apply (rule_tac x="min d k" in exI)
-apply (simp add:)
+apply (rule_tac x="min d k" in exI, simp)
done
lemma Lim_transform_within_set_eq:
@@ -2454,6 +2463,31 @@
\<Longrightarrow> ((f \<longlongrightarrow> l) (at a within s) \<longleftrightarrow> (f \<longlongrightarrow> l) (at a within t))"
by (force intro: Lim_transform_within_set elim: eventually_mono)
+lemma Lim_transform_within_openin:
+ fixes a :: "'a::metric_space"
+ assumes f: "(f \<longlongrightarrow> l) (at a within T)"
+ and "openin (subtopology euclidean T) S" "a \<in> S"
+ and eq: "\<And>x. \<lbrakk>x \<in> S; x \<noteq> a\<rbrakk> \<Longrightarrow> f x = g x"
+ shows "(g \<longlongrightarrow> l) (at a within T)"
+proof -
+ obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "ball a \<epsilon> \<inter> T \<subseteq> S"
+ using assms by (force simp: openin_contains_ball)
+ then have "a \<in> ball a \<epsilon>"
+ by force
+ show ?thesis
+ apply (rule Lim_transform_within [OF f \<open>0 < \<epsilon>\<close> eq])
+ using \<epsilon> apply (auto simp: dist_commute subset_iff)
+ done
+qed
+
+lemma continuous_transform_within_openin:
+ fixes a :: "'a::metric_space"
+ assumes "continuous (at a within T) f"
+ and "openin (subtopology euclidean T) S" "a \<in> S"
+ and eq: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
+ shows "continuous (at a within T) g"
+using assms by (simp add: Lim_transform_within_openin continuous_within)
+
text\<open>The expected monotonicity property.\<close>
lemma Lim_Un:
@@ -2544,6 +2578,72 @@
text\<open>Another limit point characterization.\<close>
+lemma limpt_sequential_inj:
+ fixes x :: "'a::metric_space"
+ shows "x islimpt S \<longleftrightarrow>
+ (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> inj f \<and> (f \<longlongrightarrow> x) sequentially)"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then have "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"
+ by (force simp: islimpt_approachable)
+ then obtain y where y: "\<And>e. e>0 \<Longrightarrow> y e \<in> S \<and> y e \<noteq> x \<and> dist (y e) x < e"
+ by metis
+ define f where "f \<equiv> rec_nat (y 1) (\<lambda>n fn. y (min (inverse(2 ^ (Suc n))) (dist fn x)))"
+ have [simp]: "f 0 = y 1"
+ "f(Suc n) = y (min (inverse(2 ^ (Suc n))) (dist (f n) x))" for n
+ by (simp_all add: f_def)
+ have f: "f n \<in> S \<and> (f n \<noteq> x) \<and> dist (f n) x < inverse(2 ^ n)" for n
+ proof (induction n)
+ case 0 show ?case
+ by (simp add: y)
+ next
+ case (Suc n) then show ?case
+ apply (auto simp: y)
+ by (metis half_gt_zero_iff inverse_positive_iff_positive less_divide_eq_numeral1(1) min_less_iff_conj y zero_less_dist_iff zero_less_numeral zero_less_power)
+ qed
+ show ?rhs
+ proof (rule_tac x=f in exI, intro conjI allI)
+ show "\<And>n. f n \<in> S - {x}"
+ using f by blast
+ have "dist (f n) x < dist (f m) x" if "m < n" for m n
+ using that
+ proof (induction n)
+ case 0 then show ?case by simp
+ next
+ case (Suc n)
+ then consider "m < n" | "m = n" using less_Suc_eq by blast
+ then show ?case
+ proof cases
+ assume "m < n"
+ have "dist (f(Suc n)) x = dist (y (min (inverse(2 ^ (Suc n))) (dist (f n) x))) x"
+ by simp
+ also have "... < dist (f n) x"
+ by (metis dist_pos_lt f min.strict_order_iff min_less_iff_conj y)
+ also have "... < dist (f m) x"
+ using Suc.IH \<open>m < n\<close> by blast
+ finally show ?thesis .
+ next
+ assume "m = n" then show ?case
+ by simp (metis dist_pos_lt f half_gt_zero_iff inverse_positive_iff_positive min_less_iff_conj y zero_less_numeral zero_less_power)
+ qed
+ qed
+ then show "inj f"
+ by (metis less_irrefl linorder_injI)
+ show "f \<longlonglongrightarrow> x"
+ apply (rule tendstoI)
+ apply (rule_tac c="nat (ceiling(1/e))" in eventually_sequentiallyI)
+ apply (rule less_trans [OF f [THEN conjunct2, THEN conjunct2]])
+ apply (simp add: field_simps)
+ by (meson le_less_trans mult_less_cancel_left not_le of_nat_less_two_power)
+ qed
+next
+ assume ?rhs
+ then show ?lhs
+ by (fastforce simp add: islimpt_approachable lim_sequentially)
+qed
+
+(*could prove directly from islimpt_sequential_inj, but only for metric spaces*)
lemma islimpt_sequential:
fixes x :: "'a::first_countable_topology"
shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> (f \<longlongrightarrow> x) sequentially)"
@@ -5822,6 +5922,36 @@
unfolding continuous_on_open_invariant openin_open Int_def vimage_def Int_commute
by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
+lemma continuous_on_open_gen:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ assumes "f ` S \<subseteq> T"
+ shows "continuous_on S f \<longleftrightarrow>
+ (\<forall>U. openin (subtopology euclidean T) U
+ \<longrightarrow> openin (subtopology euclidean S) {x \<in> S. f x \<in> U})"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ apply (auto simp: openin_euclidean_subtopology_iff continuous_on_iff)
+ by (metis assms image_subset_iff)
+next
+ have ope: "openin (subtopology euclidean T) (ball y e \<inter> T)" for y e
+ by (simp add: Int_commute openin_open_Int)
+ assume ?rhs
+ then show ?lhs
+ apply (clarsimp simp add: continuous_on_iff)
+ apply (drule_tac x = "ball (f x) e \<inter> T" in spec)
+ apply (clarsimp simp add: ope openin_euclidean_subtopology_iff [of S])
+ by (metis (no_types, hide_lams) assms dist_commute dist_self image_subset_iff)
+qed
+
+lemma continuous_openin_preimage:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ shows
+ "\<lbrakk>continuous_on S f; f ` S \<subseteq> T; openin (subtopology euclidean T) U\<rbrakk>
+ \<Longrightarrow> openin (subtopology euclidean S) {x \<in> S. f x \<in> U}"
+by (simp add: continuous_on_open_gen)
+
text \<open>Similarly in terms of closed sets.\<close>
lemma continuous_on_closed:
@@ -5831,9 +5961,37 @@
unfolding continuous_on_closed_invariant closedin_closed Int_def vimage_def Int_commute
by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
+lemma continuous_on_closed_gen:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ assumes "f ` S \<subseteq> T"
+ shows "continuous_on S f \<longleftrightarrow>
+ (\<forall>U. closedin (subtopology euclidean T) U
+ \<longrightarrow> closedin (subtopology euclidean S) {x \<in> S. f x \<in> U})"
+proof -
+ have *: "U \<subseteq> T \<Longrightarrow> {x \<in> S. f x \<in> T \<and> f x \<notin> U} = S - {x \<in> S. f x \<in> U}" for U
+ using assms by blast
+ show ?thesis
+ apply (simp add: continuous_on_open_gen [OF assms], safe)
+ apply (drule_tac [!] x="T-U" in spec)
+ apply (force simp: closedin_def *)
+ apply (force simp: openin_closedin_eq *)
+ done
+qed
+
+lemma continuous_closedin_preimage_gen:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ assumes "continuous_on S f" "f ` S \<subseteq> T" "closedin (subtopology euclidean T) U"
+ shows "closedin (subtopology euclidean S) {x \<in> S. f x \<in> U}"
+using assms continuous_on_closed_gen by blast
+
+lemma continuous_on_imp_closedin:
+ assumes "continuous_on S f" "closedin (subtopology euclidean (f ` S)) T"
+ shows "closedin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> T}"
+using assms continuous_on_closed by blast
+
subsection \<open>Half-global and completely global cases.\<close>
-lemma continuous_openin_preimage:
+lemma continuous_openin_preimage_gen:
assumes "continuous_on s f" "open t"
shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
proof -
@@ -5867,7 +6025,7 @@
shows "open {x \<in> s. f x \<in> t}"
proof-
obtain T where T: "open T" "{x \<in> s. f x \<in> t} = s \<inter> T"
- using continuous_openin_preimage[OF assms(1,3)] unfolding openin_open by auto
+ using continuous_openin_preimage_gen[OF assms(1,3)] unfolding openin_open by auto
then show ?thesis
using open_Int[of s T, OF assms(2)] by auto
qed
@@ -6753,7 +6911,7 @@
proof safe
fix y
assume "y \<in> s"
- from continuous_openin_preimage[OF f open_ball]
+ from continuous_openin_preimage_gen[OF f open_ball]
obtain T where "open T" and T: "{x \<in> s. f x \<in> ball (f y) (e/2)} = T \<inter> s"
unfolding openin_subtopology open_openin by metis
then obtain d where "ball y d \<subseteq> T" "0 < d"
@@ -9257,12 +9415,12 @@
assumes "open S" "finite X" "p \<in> S"
shows "\<exists>e>0. \<forall>w\<in>ball p e. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
proof -
- obtain e1 where "0 < e1" and e1_b:"ball p e1 \<subseteq> S"
+ obtain e1 where "0 < e1" and e1_b:"ball p e1 \<subseteq> S"
using open_contains_ball_eq[OF \<open>open S\<close>] assms by auto
- obtain e2 where "0 < e2" and "\<forall>x\<in>X. x \<noteq> p \<longrightarrow> e2 \<le> dist p x"
+ obtain e2 where "0 < e2" and "\<forall>x\<in>X. x \<noteq> p \<longrightarrow> e2 \<le> dist p x"
using finite_set_avoid[OF \<open>finite X\<close>,of p] by auto
hence "\<forall>w\<in>ball p (min e1 e2). w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)" using e1_b by auto
- thus "\<exists>e>0. \<forall>w\<in>ball p e. w \<in> S \<and> (w \<noteq> p \<longrightarrow> w \<notin> X)" using \<open>e2>0\<close> \<open>e1>0\<close>
+ thus "\<exists>e>0. \<forall>w\<in>ball p e. w \<in> S \<and> (w \<noteq> p \<longrightarrow> w \<notin> X)" using \<open>e2>0\<close> \<open>e1>0\<close>
apply (rule_tac x="min e1 e2" in exI)
by auto
qed
@@ -9272,7 +9430,7 @@
assumes "open S" "finite X" "p \<in> S"
shows "\<exists>e>0. \<forall>w\<in>cball p e. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
proof -
- obtain e1 where "e1>0" and e1: "\<forall>w\<in>ball p e1. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
+ obtain e1 where "e1>0" and e1: "\<forall>w\<in>ball p e1. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
using finite_ball_avoid[OF assms] by auto
define e2 where "e2 \<equiv> e1/2"
have "e2>0" and "e2 < e1" unfolding e2_def using \<open>e1>0\<close> by auto
@@ -9280,6 +9438,180 @@
then show "\<exists>e>0. \<forall>w\<in>cball p e. w \<in> S \<and> (w \<noteq> p \<longrightarrow> w \<notin> X)" using \<open>e2>0\<close> e1 by auto
qed
+subsection\<open>Various separability-type properties\<close>
+
+lemma univ_second_countable:
+ obtains \<B> :: "'a::euclidean_space set set"
+ where "countable \<B>" "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
+ "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
+by (metis ex_countable_basis topological_basis_def)
+
+lemma univ_second_countable_sequence:
+ obtains B :: "nat \<Rightarrow> 'a::euclidean_space set"
+ where "inj B" "\<And>n. open(B n)" "\<And>S. open S \<Longrightarrow> \<exists>k. S = \<Union>{B n |n. n \<in> k}"
+proof -
+ obtain \<B> :: "'a set set"
+ where "countable \<B>"
+ and op: "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
+ and Un: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
+ using univ_second_countable by blast
+ have *: "infinite (range (\<lambda>n. ball (0::'a) (inverse(Suc n))))"
+ apply (rule Infinite_Set.range_inj_infinite)
+ apply (simp add: inj_on_def ball_eq_ball_iff)
+ done
+ have "infinite \<B>"
+ proof
+ assume "finite \<B>"
+ then have "finite (Union ` (Pow \<B>))"
+ by simp
+ then have "finite (range (\<lambda>n. ball (0::'a) (inverse(Suc n))))"
+ apply (rule rev_finite_subset)
+ by (metis (no_types, lifting) PowI image_eqI image_subset_iff Un [OF open_ball])
+ with * show False by simp
+ qed
+ obtain f :: "nat \<Rightarrow> 'a set" where "\<B> = range f" "inj f"
+ by (blast intro: countable_as_injective_image [OF \<open>countable \<B>\<close> \<open>infinite \<B>\<close>])
+ have *: "\<exists>k. S = \<Union>{f n |n. n \<in> k}" if "open S" for S
+ using Un [OF that]
+ apply clarify
+ apply (rule_tac x="f-`U" in exI)
+ using \<open>inj f\<close> \<open>\<B> = range f\<close> apply force
+ done
+ show ?thesis
+ apply (rule that [OF \<open>inj f\<close> _ *])
+ apply (auto simp: \<open>\<B> = range f\<close> op)
+ done
+qed
+
+proposition Lindelof:
+ fixes \<F> :: "'a::euclidean_space set set"
+ assumes \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> open S"
+ obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
+proof -
+ obtain \<B> :: "'a set set"
+ where "countable \<B>" "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
+ and \<B>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
+ using univ_second_countable by blast
+ define \<D> where "\<D> \<equiv> {S. S \<in> \<B> \<and> (\<exists>U. U \<in> \<F> \<and> S \<subseteq> U)}"
+ have "countable \<D>"
+ apply (rule countable_subset [OF _ \<open>countable \<B>\<close>])
+ apply (force simp: \<D>_def)
+ done
+ have "\<And>S. \<exists>U. S \<in> \<D> \<longrightarrow> U \<in> \<F> \<and> S \<subseteq> U"
+ by (simp add: \<D>_def)
+ then obtain G where G: "\<And>S. S \<in> \<D> \<longrightarrow> G S \<in> \<F> \<and> S \<subseteq> G S"
+ by metis
+ have "\<Union>\<F> \<subseteq> \<Union>\<D>"
+ unfolding \<D>_def by (blast dest: \<F> \<B>)
+ moreover have "\<Union>\<D> \<subseteq> \<Union>\<F>"
+ using \<D>_def by blast
+ ultimately have eq1: "\<Union>\<F> = \<Union>\<D>" ..
+ have eq2: "\<Union>\<D> = UNION \<D> G"
+ using G eq1 by auto
+ show ?thesis
+ apply (rule_tac \<F>' = "G ` \<D>" in that)
+ using G \<open>countable \<D>\<close> apply (auto simp: eq1 eq2)
+ done
+qed
+
+lemma Lindelof_openin:
+ fixes \<F> :: "'a::euclidean_space set set"
+ assumes "\<And>S. S \<in> \<F> \<Longrightarrow> openin (subtopology euclidean U) S"
+ obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
+proof -
+ have "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>T. open T \<and> S = U \<inter> T"
+ using assms by (simp add: openin_open)
+ then obtain tf where tf: "\<And>S. S \<in> \<F> \<Longrightarrow> open (tf S) \<and> (S = U \<inter> tf S)"
+ by metis
+ have [simp]: "\<And>\<F>'. \<F>' \<subseteq> \<F> \<Longrightarrow> \<Union>\<F>' = U \<inter> \<Union>(tf ` \<F>')"
+ using tf by fastforce
+ obtain \<G> where "countable \<G> \<and> \<G> \<subseteq> tf ` \<F>" "\<Union>\<G> = UNION \<F> tf"
+ using tf by (force intro: Lindelof [of "tf ` \<F>"])
+ then obtain \<F>' where \<F>': "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
+ by (clarsimp simp add: countable_subset_image)
+ then show ?thesis ..
+qed
+
+lemma countable_disjoint_open_subsets:
+ fixes \<F> :: "'a::euclidean_space set set"
+ assumes "\<And>S. S \<in> \<F> \<Longrightarrow> open S" and pw: "pairwise disjnt \<F>"
+ shows "countable \<F>"
+proof -
+ obtain \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
+ by (meson assms Lindelof)
+ with pw have "\<F> \<subseteq> insert {} \<F>'"
+ by (fastforce simp add: pairwise_def disjnt_iff)
+ then show ?thesis
+ by (simp add: \<open>countable \<F>'\<close> countable_subset)
+qed
+
+lemma closedin_compact:
+ "\<lbrakk>compact S; closedin (subtopology euclidean S) T\<rbrakk> \<Longrightarrow> compact T"
+by (metis closedin_closed compact_Int_closed)
+
+lemma closedin_compact_eq:
+ fixes S :: "'a::t2_space set"
+ shows
+ "compact S
+ \<Longrightarrow> (closedin (subtopology euclidean S) T \<longleftrightarrow>
+ compact T \<and> T \<subseteq> S)"
+by (metis closedin_imp_subset closedin_compact closed_subset compact_imp_closed)
+
+subsection\<open> Finite intersection property\<close>
+
+text\<open>Also developed in HOL's toplogical spaces theory, but the Heine-Borel type class isn't available there.\<close>
+
+lemma closed_imp_fip:
+ fixes S :: "'a::heine_borel set"
+ assumes "closed S"
+ and T: "T \<in> \<F>" "bounded T"
+ and clof: "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
+ and none: "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> S \<inter> \<Inter>\<F>' \<noteq> {}"
+ shows "S \<inter> \<Inter>\<F> \<noteq> {}"
+proof -
+ have "compact (S \<inter> T)"
+ using \<open>closed S\<close> clof compact_eq_bounded_closed T by blast
+ then have "(S \<inter> T) \<inter> \<Inter>\<F> \<noteq> {}"
+ apply (rule compact_imp_fip)
+ apply (simp add: clof)
+ by (metis Int_assoc complete_lattice_class.Inf_insert finite_insert insert_subset none \<open>T \<in> \<F>\<close>)
+ then show ?thesis by blast
+qed
+
+lemma closed_imp_fip_compact:
+ fixes S :: "'a::heine_borel set"
+ shows
+ "\<lbrakk>closed S; \<And>T. T \<in> \<F> \<Longrightarrow> compact T;
+ \<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> S \<inter> \<Inter>\<F>' \<noteq> {}\<rbrakk>
+ \<Longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}"
+by (metis Inf_greatest closed_imp_fip compact_eq_bounded_closed empty_subsetI finite.emptyI inf.orderE)
+
+lemma closed_fip_heine_borel:
+ fixes \<F> :: "'a::heine_borel set set"
+ assumes "closed S" "T \<in> \<F>" "bounded T"
+ and "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
+ and "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> \<Inter>\<F>' \<noteq> {}"
+ shows "\<Inter>\<F> \<noteq> {}"
+proof -
+ have "UNIV \<inter> \<Inter>\<F> \<noteq> {}"
+ using assms closed_imp_fip [OF closed_UNIV] by auto
+ then show ?thesis by simp
+qed
+
+lemma compact_fip_heine_borel:
+ fixes \<F> :: "'a::heine_borel set set"
+ assumes clof: "\<And>T. T \<in> \<F> \<Longrightarrow> compact T"
+ and none: "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> \<Inter>\<F>' \<noteq> {}"
+ shows "\<Inter>\<F> \<noteq> {}"
+by (metis InterI all_not_in_conv clof closed_fip_heine_borel compact_eq_bounded_closed none)
+
+lemma compact_sequence_with_limit:
+ fixes f :: "nat \<Rightarrow> 'a::heine_borel"
+ shows "(f \<longlongrightarrow> l) sequentially \<Longrightarrow> compact (insert l (range f))"
+apply (simp add: compact_eq_bounded_closed, auto)
+apply (simp add: convergent_imp_bounded)
+by (simp add: closed_limpt islimpt_insert sequence_unique_limpt)
+
no_notation
eucl_less (infix "<e" 50)
--- a/src/HOL/Set.thy Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Set.thy Tue Jun 14 15:34:21 2016 +0100
@@ -1928,6 +1928,9 @@
definition disjnt where "disjnt A B \<equiv> A \<inter> B = {}"
+lemma disjnt_iff: "disjnt A B \<longleftrightarrow> (\<forall>x. ~ (x \<in> A \<and> x \<in> B))"
+ by (force simp: disjnt_def)
+
lemma pairwise_empty [simp]: "pairwise P {}"
by (simp add: pairwise_def)
--- a/src/HOL/Topological_Spaces.thy Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Topological_Spaces.thy Tue Jun 14 15:34:21 2016 +0100
@@ -146,7 +146,7 @@
shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U)"
using t1_space[of x y] by blast
-lemma closed_singleton:
+lemma closed_singleton [iff]:
fixes a :: "'a::t1_space"
shows "closed {a}"
proof -
@@ -1610,6 +1610,9 @@
lemma continuous_on_id[continuous_intros]: "continuous_on s (\<lambda>x. x)"
unfolding continuous_on_def by fast
+lemma continuous_on_id'[continuous_intros]: "continuous_on s id"
+ unfolding continuous_on_def id_def by fast
+
lemma continuous_on_const[continuous_intros]: "continuous_on s (\<lambda>x. c)"
unfolding continuous_on_def by auto
@@ -1841,6 +1844,8 @@
lemma inj_setminus: "inj_on uminus (A::'a set set)"
by (auto simp: inj_on_def)
+subsection\<open> Finite intersection property\<close>
+
lemma compact_fip:
"compact U \<longleftrightarrow>
(\<forall>A. (\<forall>a\<in>A. closed a) \<longrightarrow> (\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}) \<longrightarrow> U \<inter> \<Inter>A \<noteq> {})"