--- a/src/HOL/Analysis/Connected.thy Mon Jan 07 11:51:18 2019 +0100
+++ b/src/HOL/Analysis/Connected.thy Mon Jan 07 12:31:08 2019 +0100
@@ -494,118 +494,8 @@
using closedin_connected_component componentsE by blast
-subsection%unimportant\<open>Quotient maps\<close>
-
-lemma quotient_map_imp_continuous_open:
- assumes T: "f ` S \<subseteq> T"
- and ope: "\<And>U. U \<subseteq> T
- \<Longrightarrow> (openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
- openin (subtopology euclidean T) U)"
- shows "continuous_on S f"
-proof -
- have [simp]: "S \<inter> f -` f ` S = S" by auto
- show ?thesis
- using ope [OF T]
- apply (simp add: continuous_on_open)
- by (meson ope openin_imp_subset openin_trans)
-qed
-
-lemma quotient_map_imp_continuous_closed:
- assumes T: "f ` S \<subseteq> T"
- and ope: "\<And>U. U \<subseteq> T
- \<Longrightarrow> (closedin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
- closedin (subtopology euclidean T) U)"
- shows "continuous_on S f"
-proof -
- have [simp]: "S \<inter> f -` f ` S = S" by auto
- show ?thesis
- using ope [OF T]
- apply (simp add: continuous_on_closed)
- by (metis (no_types, lifting) ope closedin_imp_subset closedin_trans)
-qed
-
-lemma open_map_imp_quotient_map:
- assumes contf: "continuous_on S f"
- and T: "T \<subseteq> f ` S"
- and ope: "\<And>T. openin (subtopology euclidean S) T
- \<Longrightarrow> openin (subtopology euclidean (f ` S)) (f ` T)"
- shows "openin (subtopology euclidean S) (S \<inter> f -` T) =
- openin (subtopology euclidean (f ` S)) T"
-proof -
- have "T = f ` (S \<inter> f -` T)"
- using T by blast
- then show ?thesis
- using "ope" contf continuous_on_open by metis
-qed
-
-lemma closed_map_imp_quotient_map:
- assumes contf: "continuous_on S f"
- and T: "T \<subseteq> f ` S"
- and ope: "\<And>T. closedin (subtopology euclidean S) T
- \<Longrightarrow> closedin (subtopology euclidean (f ` S)) (f ` T)"
- shows "openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow>
- openin (subtopology euclidean (f ` S)) T"
- (is "?lhs = ?rhs")
-proof
- assume ?lhs
- then have *: "closedin (subtopology euclidean S) (S - (S \<inter> f -` T))"
- using closedin_diff by fastforce
- have [simp]: "(f ` S - f ` (S - (S \<inter> f -` T))) = T"
- using T by blast
- show ?rhs
- using ope [OF *, unfolded closedin_def] by auto
-next
- assume ?rhs
- with contf show ?lhs
- by (auto simp: continuous_on_open)
-qed
-
-lemma continuous_right_inverse_imp_quotient_map:
- assumes contf: "continuous_on S f" and imf: "f ` S \<subseteq> T"
- and contg: "continuous_on T g" and img: "g ` T \<subseteq> S"
- and fg [simp]: "\<And>y. y \<in> T \<Longrightarrow> f(g y) = y"
- and U: "U \<subseteq> T"
- shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
- openin (subtopology euclidean T) U"
- (is "?lhs = ?rhs")
-proof -
- have f: "\<And>Z. openin (subtopology euclidean (f ` S)) Z \<Longrightarrow>
- openin (subtopology euclidean S) (S \<inter> f -` Z)"
- and g: "\<And>Z. openin (subtopology euclidean (g ` T)) Z \<Longrightarrow>
- openin (subtopology euclidean T) (T \<inter> g -` Z)"
- using contf contg by (auto simp: continuous_on_open)
- show ?thesis
- proof
- have "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = {x \<in> T. f (g x) \<in> U}"
- using imf img by blast
- also have "... = U"
- using U by auto
- finally have eq: "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = U" .
- assume ?lhs
- then have *: "openin (subtopology euclidean (g ` T)) (g ` T \<inter> (S \<inter> f -` U))"
- by (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self)
- show ?rhs
- using g [OF *] eq by auto
- next
- assume rhs: ?rhs
- show ?lhs
- by (metis f fg image_eqI image_subset_iff imf img openin_subopen openin_subtopology_self openin_trans rhs)
- qed
-qed
-
-lemma continuous_left_inverse_imp_quotient_map:
- assumes "continuous_on S f"
- and "continuous_on (f ` S) g"
- and "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
- and "U \<subseteq> f ` S"
- shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
- openin (subtopology euclidean (f ` S)) U"
-apply (rule continuous_right_inverse_imp_quotient_map)
-using assms apply force+
-done
-
-
-subsection%unimportant \<open>Proving a function is constant by proving that a level set is open\<close>
+subsection%unimportant \<open>Proving a function is constant on a connected set
+ by proving that a level set is open\<close>
lemma continuous_levelset_openin_cases:
fixes f :: "_ \<Rightarrow> 'b::t1_space"
@@ -635,273 +525,13 @@
by fast
-subsection%unimportant \<open>Connectedness is invariant under homeomorphisms.\<close>
+subsection%unimportant \<open>Preservation of Connectedness\<close>
lemma homeomorphic_connectedness:
assumes "s homeomorphic t"
shows "connected s \<longleftrightarrow> connected t"
using assms unfolding homeomorphic_def homeomorphism_def by (metis connected_continuous_image)
-
-subsection\<open>Various separability-type properties\<close>
-
-lemma univ_second_countable:
- obtains \<B> :: "'a::second_countable_topology 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 subset_second_countable:
- obtains \<B> :: "'a:: second_countable_topology set set"
- where "countable \<B>"
- "{} \<notin> \<B>"
- "\<And>C. C \<in> \<B> \<Longrightarrow> openin(subtopology euclidean S) C"
- "\<And>T. openin(subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
-proof -
- obtain \<B> :: "'a set set"
- where "countable \<B>"
- and opeB: "\<And>C. C \<in> \<B> \<Longrightarrow> openin(subtopology euclidean S) C"
- and \<B>: "\<And>T. openin(subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
- proof -
- obtain \<C> :: "'a set set"
- where "countable \<C>" and ope: "\<And>C. C \<in> \<C> \<Longrightarrow> open C"
- and \<C>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<C> \<and> S = \<Union>U"
- by (metis univ_second_countable that)
- show ?thesis
- proof
- show "countable ((\<lambda>C. S \<inter> C) ` \<C>)"
- by (simp add: \<open>countable \<C>\<close>)
- show "\<And>C. C \<in> (\<inter>) S ` \<C> \<Longrightarrow> openin (subtopology euclidean S) C"
- using ope by auto
- show "\<And>T. openin (subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>\<subseteq>(\<inter>) S ` \<C>. T = \<Union>\<U>"
- by (metis \<C> image_mono inf_Sup openin_open)
- qed
- qed
- show ?thesis
- proof
- show "countable (\<B> - {{}})"
- using \<open>countable \<B>\<close> by blast
- show "\<And>C. \<lbrakk>C \<in> \<B> - {{}}\<rbrakk> \<Longrightarrow> openin (subtopology euclidean S) C"
- by (simp add: \<open>\<And>C. C \<in> \<B> \<Longrightarrow> openin (subtopology euclidean S) C\<close>)
- show "\<exists>\<U>\<subseteq>\<B> - {{}}. T = \<Union>\<U>" if "openin (subtopology euclidean S) T" for T
- using \<B> [OF that]
- apply clarify
- apply (rule_tac x="\<U> - {{}}" in exI, auto)
- done
- qed auto
-qed
-
-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 opn: "\<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> opn)
- done
-qed
-
-proposition separable:
- fixes S :: "'a::{metric_space, second_countable_topology} set"
- obtains T where "countable T" "T \<subseteq> S" "S \<subseteq> closure T"
-proof -
- obtain \<B> :: "'a set set"
- where "countable \<B>"
- and "{} \<notin> \<B>"
- and ope: "\<And>C. C \<in> \<B> \<Longrightarrow> openin(subtopology euclidean S) C"
- and if_ope: "\<And>T. openin(subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
- by (meson subset_second_countable)
- then obtain f where f: "\<And>C. C \<in> \<B> \<Longrightarrow> f C \<in> C"
- by (metis equals0I)
- show ?thesis
- proof
- show "countable (f ` \<B>)"
- by (simp add: \<open>countable \<B>\<close>)
- show "f ` \<B> \<subseteq> S"
- using ope f openin_imp_subset by blast
- show "S \<subseteq> closure (f ` \<B>)"
- proof (clarsimp simp: closure_approachable)
- fix x and e::real
- assume "x \<in> S" "0 < e"
- have "openin (subtopology euclidean S) (S \<inter> ball x e)"
- by (simp add: openin_Int_open)
- with if_ope obtain \<U> where \<U>: "\<U> \<subseteq> \<B>" "S \<inter> ball x e = \<Union>\<U>"
- by meson
- show "\<exists>C \<in> \<B>. dist (f C) x < e"
- proof (cases "\<U> = {}")
- case True
- then show ?thesis
- using \<open>0 < e\<close> \<U> \<open>x \<in> S\<close> by auto
- next
- case False
- then obtain C where "C \<in> \<U>" by blast
- show ?thesis
- proof
- show "dist (f C) x < e"
- by (metis Int_iff Union_iff \<U> \<open>C \<in> \<U>\<close> dist_commute f mem_ball subsetCE)
- show "C \<in> \<B>"
- using \<open>\<U> \<subseteq> \<B>\<close> \<open>C \<in> \<U>\<close> by blast
- qed
- qed
- qed
- qed
-qed
-
-proposition Lindelof:
- fixes \<F> :: "'a::second_countable_topology 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> (G ` \<D>)"
- 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::second_countable_topology 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>(tf ` \<F>)"
- 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::second_countable_topology 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 countable_disjoint_nonempty_interior_subsets:
- fixes \<F> :: "'a::second_countable_topology set set"
- assumes pw: "pairwise disjnt \<F>" and int: "\<And>S. \<lbrakk>S \<in> \<F>; interior S = {}\<rbrakk> \<Longrightarrow> S = {}"
- shows "countable \<F>"
-proof (rule countable_image_inj_on)
- have "disjoint (interior ` \<F>)"
- using pw by (simp add: disjoint_image_subset interior_subset)
- then show "countable (interior ` \<F>)"
- by (auto intro: countable_disjoint_open_subsets)
- show "inj_on interior \<F>"
- using pw apply (clarsimp simp: inj_on_def pairwise_def)
- apply (metis disjnt_def disjnt_subset1 inf.orderE int interior_subset)
- done
-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)
-
-lemma continuous_imp_closed_map:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
- assumes "closedin (subtopology euclidean S) U"
- "continuous_on S f" "f ` S = T" "compact S"
- shows "closedin (subtopology euclidean T) (f ` U)"
- by (metis assms closedin_compact_eq compact_continuous_image continuous_on_subset subset_image_iff)
-
-lemma continuous_imp_quotient_map:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
- assumes "continuous_on S f" "f ` S = T" "compact S" "U \<subseteq> T"
- shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
- openin (subtopology euclidean T) U"
- by (metis (no_types, lifting) assms closed_map_imp_quotient_map continuous_imp_closed_map)
-
-
-lemma open_map_restrict:
- assumes opeU: "openin (subtopology euclidean (S \<inter> f -` T')) U"
- and oo: "\<And>U. openin (subtopology euclidean S) U \<Longrightarrow> openin (subtopology euclidean T) (f ` U)"
- and "T' \<subseteq> T"
- shows "openin (subtopology euclidean T') (f ` U)"
-proof -
- obtain V where "open V" "U = S \<inter> f -` T' \<inter> V"
- using opeU by (auto simp: openin_open)
- with oo [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
- by (fastforce simp add: openin_open)
-qed
-
-lemma closed_map_restrict:
- assumes cloU: "closedin (subtopology euclidean (S \<inter> f -` T')) U"
- and cc: "\<And>U. closedin (subtopology euclidean S) U \<Longrightarrow> closedin (subtopology euclidean T) (f ` U)"
- and "T' \<subseteq> T"
- shows "closedin (subtopology euclidean T') (f ` U)"
-proof -
- obtain V where "closed V" "U = S \<inter> f -` T' \<inter> V"
- using cloU by (auto simp: closedin_closed)
- with cc [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
- by (fastforce simp add: closedin_closed)
-qed
-
lemma connected_monotone_quotient_preimage:
assumes "connected T"
and contf: "continuous_on S f" and fim: "f ` S = T"
@@ -1124,348 +754,6 @@
by auto
qed
-subsection%unimportant\<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)
-
-
-subsection%unimportant\<open>Componentwise limits and continuity\<close>
-
-text\<open>But is the premise really necessary? Need to generalise @{thm euclidean_dist_l2}\<close>
-lemma Euclidean_dist_upper: "i \<in> Basis \<Longrightarrow> dist (x \<bullet> i) (y \<bullet> i) \<le> dist x y"
- by (metis (no_types) member_le_L2_set euclidean_dist_l2 finite_Basis)
-
-text\<open>But is the premise \<^term>\<open>i \<in> Basis\<close> really necessary?\<close>
-lemma open_preimage_inner:
- assumes "open S" "i \<in> Basis"
- shows "open {x. x \<bullet> i \<in> S}"
-proof (rule openI, simp)
- fix x
- assume x: "x \<bullet> i \<in> S"
- with assms obtain e where "0 < e" and e: "ball (x \<bullet> i) e \<subseteq> S"
- by (auto simp: open_contains_ball_eq)
- have "\<exists>e>0. ball (y \<bullet> i) e \<subseteq> S" if dxy: "dist x y < e / 2" for y
- proof (intro exI conjI)
- have "dist (x \<bullet> i) (y \<bullet> i) < e / 2"
- by (meson \<open>i \<in> Basis\<close> dual_order.trans Euclidean_dist_upper not_le that)
- then have "dist (x \<bullet> i) z < e" if "dist (y \<bullet> i) z < e / 2" for z
- by (metis dist_commute dist_triangle_half_l that)
- then have "ball (y \<bullet> i) (e / 2) \<subseteq> ball (x \<bullet> i) e"
- using mem_ball by blast
- with e show "ball (y \<bullet> i) (e / 2) \<subseteq> S"
- by (metis order_trans)
- qed (simp add: \<open>0 < e\<close>)
- then show "\<exists>e>0. ball x e \<subseteq> {s. s \<bullet> i \<in> S}"
- by (metis (no_types, lifting) \<open>0 < e\<close> \<open>open S\<close> half_gt_zero_iff mem_Collect_eq mem_ball open_contains_ball_eq subsetI)
-qed
-
-proposition tendsto_componentwise_iff:
- fixes f :: "_ \<Rightarrow> 'b::euclidean_space"
- shows "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>i \<in> Basis. ((\<lambda>x. (f x \<bullet> i)) \<longlongrightarrow> (l \<bullet> i)) F)"
- (is "?lhs = ?rhs")
-proof
- assume ?lhs
- then show ?rhs
- unfolding tendsto_def
- apply clarify
- apply (drule_tac x="{s. s \<bullet> i \<in> S}" in spec)
- apply (auto simp: open_preimage_inner)
- done
-next
- assume R: ?rhs
- then have "\<And>e. e > 0 \<Longrightarrow> \<forall>i\<in>Basis. \<forall>\<^sub>F x in F. dist (f x \<bullet> i) (l \<bullet> i) < e"
- unfolding tendsto_iff by blast
- then have R': "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F x in F. \<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e"
- by (simp add: eventually_ball_finite_distrib [symmetric])
- show ?lhs
- unfolding tendsto_iff
- proof clarify
- fix e::real
- assume "0 < e"
- have *: "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e"
- if "\<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / real DIM('b)" for x
- proof -
- have "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis \<le> sum (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis"
- by (simp add: L2_set_le_sum)
- also have "... < DIM('b) * (e / real DIM('b))"
- apply (rule sum_bounded_above_strict)
- using that by auto
- also have "... = e"
- by (simp add: field_simps)
- finally show "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e" .
- qed
- have "\<forall>\<^sub>F x in F. \<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / DIM('b)"
- apply (rule R')
- using \<open>0 < e\<close> by simp
- then show "\<forall>\<^sub>F x in F. dist (f x) l < e"
- apply (rule eventually_mono)
- apply (subst euclidean_dist_l2)
- using * by blast
- qed
-qed
-
-
-corollary continuous_componentwise:
- "continuous F f \<longleftrightarrow> (\<forall>i \<in> Basis. continuous F (\<lambda>x. (f x \<bullet> i)))"
-by (simp add: continuous_def tendsto_componentwise_iff [symmetric])
-
-corollary continuous_on_componentwise:
- fixes S :: "'a :: t2_space set"
- shows "continuous_on S f \<longleftrightarrow> (\<forall>i \<in> Basis. continuous_on S (\<lambda>x. (f x \<bullet> i)))"
- apply (simp add: continuous_on_eq_continuous_within)
- using continuous_componentwise by blast
-
-lemma linear_componentwise_iff:
- "(linear f') \<longleftrightarrow> (\<forall>i\<in>Basis. linear (\<lambda>x. f' x \<bullet> i))"
- apply (auto simp: linear_iff inner_left_distrib)
- apply (metis inner_left_distrib euclidean_eq_iff)
- by (metis euclidean_eqI inner_scaleR_left)
-
-lemma bounded_linear_componentwise_iff:
- "(bounded_linear f') \<longleftrightarrow> (\<forall>i\<in>Basis. bounded_linear (\<lambda>x. f' x \<bullet> i))"
- (is "?lhs = ?rhs")
-proof
- assume ?lhs then show ?rhs
- by (simp add: bounded_linear_inner_left_comp)
-next
- assume ?rhs
- then have "(\<forall>i\<in>Basis. \<exists>K. \<forall>x. \<bar>f' x \<bullet> i\<bar> \<le> norm x * K)" "linear f'"
- by (auto simp: bounded_linear_def bounded_linear_axioms_def linear_componentwise_iff [symmetric] ball_conj_distrib)
- then obtain F where F: "\<And>i x. i \<in> Basis \<Longrightarrow> \<bar>f' x \<bullet> i\<bar> \<le> norm x * F i"
- by metis
- have "norm (f' x) \<le> norm x * sum F Basis" for x
- proof -
- have "norm (f' x) \<le> (\<Sum>i\<in>Basis. \<bar>f' x \<bullet> i\<bar>)"
- by (rule norm_le_l1)
- also have "... \<le> (\<Sum>i\<in>Basis. norm x * F i)"
- by (metis F sum_mono)
- also have "... = norm x * sum F Basis"
- by (simp add: sum_distrib_left)
- finally show ?thesis .
- qed
- then show ?lhs
- by (force simp: bounded_linear_def bounded_linear_axioms_def \<open>linear f'\<close>)
-qed
-
-subsection%unimportant\<open>Pasting functions together\<close>
-
-subsubsection%unimportant\<open>on open sets\<close>
-
-lemma pasting_lemma:
- fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
- assumes clo: "\<And>i. i \<in> I \<Longrightarrow> openin (subtopology euclidean S) (T i)"
- and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
- and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
- and g: "\<And>x. x \<in> S \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
- shows "continuous_on S g"
-proof (clarsimp simp: continuous_openin_preimage_eq)
- fix U :: "'b set"
- assume "open U"
- have S: "\<And>i. i \<in> I \<Longrightarrow> (T i) \<subseteq> S"
- using clo openin_imp_subset by blast
- have *: "(S \<inter> g -` U) = (\<Union>i \<in> I. T i \<inter> f i -` U)"
- using S f g by fastforce
- show "openin (subtopology euclidean S) (S \<inter> g -` U)"
- apply (subst *)
- apply (rule openin_Union, clarify)
- using \<open>open U\<close> clo cont continuous_openin_preimage_gen openin_trans by blast
-qed
-
-lemma pasting_lemma_exists:
- fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
- assumes S: "S \<subseteq> (\<Union>i \<in> I. T i)"
- and clo: "\<And>i. i \<in> I \<Longrightarrow> openin (subtopology euclidean S) (T i)"
- and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
- and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
- obtains g where "continuous_on S g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> S \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x"
-proof
- show "continuous_on S (\<lambda>x. f (SOME i. i \<in> I \<and> x \<in> T i) x)"
- apply (rule pasting_lemma [OF clo cont])
- apply (blast intro: f)+
- apply (metis (mono_tags, lifting) S UN_iff subsetCE someI)
- done
-next
- fix x i
- assume "i \<in> I" "x \<in> S \<inter> T i"
- then show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
- by (metis (no_types, lifting) IntD2 IntI f someI_ex)
-qed
-
-subsubsection%unimportant\<open>Likewise on closed sets, with a finiteness assumption\<close>
-
-lemma pasting_lemma_closed:
- fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
- assumes "finite I"
- and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin (subtopology euclidean S) (T i)"
- and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
- and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
- and g: "\<And>x. x \<in> S \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
- shows "continuous_on S g"
-proof (clarsimp simp: continuous_closedin_preimage_eq)
- fix U :: "'b set"
- assume "closed U"
- have S: "\<And>i. i \<in> I \<Longrightarrow> (T i) \<subseteq> S"
- using clo closedin_imp_subset by blast
- have *: "(S \<inter> g -` U) = (\<Union>i \<in> I. T i \<inter> f i -` U)"
- using S f g by fastforce
- show "closedin (subtopology euclidean S) (S \<inter> g -` U)"
- apply (subst *)
- apply (rule closedin_Union)
- using \<open>finite I\<close> apply simp
- apply (blast intro: \<open>closed U\<close> continuous_closedin_preimage cont clo closedin_trans)
- done
-qed
-
-lemma pasting_lemma_exists_closed:
- fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
- assumes "finite I"
- and S: "S \<subseteq> (\<Union>i \<in> I. T i)"
- and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin (subtopology euclidean S) (T i)"
- and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
- and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
- obtains g where "continuous_on S g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> S \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x"
-proof
- show "continuous_on S (\<lambda>x. f (SOME i. i \<in> I \<and> x \<in> T i) x)"
- apply (rule pasting_lemma_closed [OF \<open>finite I\<close> clo cont])
- apply (blast intro: f)+
- apply (metis (mono_tags, lifting) S UN_iff subsetCE someI)
- done
-next
- fix x i
- assume "i \<in> I" "x \<in> S \<inter> T i"
- then show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
- by (metis (no_types, lifting) IntD2 IntI f someI_ex)
-qed
-
-lemma tube_lemma:
- assumes "compact K"
- assumes "open W"
- assumes "{x0} \<times> K \<subseteq> W"
- shows "\<exists>X0. x0 \<in> X0 \<and> open X0 \<and> X0 \<times> K \<subseteq> W"
-proof -
- {
- fix y assume "y \<in> K"
- then have "(x0, y) \<in> W" using assms by auto
- with \<open>open W\<close>
- have "\<exists>X0 Y. open X0 \<and> open Y \<and> x0 \<in> X0 \<and> y \<in> Y \<and> X0 \<times> Y \<subseteq> W"
- by (rule open_prod_elim) blast
- }
- then obtain X0 Y where
- *: "\<forall>y \<in> K. open (X0 y) \<and> open (Y y) \<and> x0 \<in> X0 y \<and> y \<in> Y y \<and> X0 y \<times> Y y \<subseteq> W"
- by metis
- from * have "\<forall>t\<in>Y ` K. open t" "K \<subseteq> \<Union>(Y ` K)" by auto
- with \<open>compact K\<close> obtain CC where CC: "CC \<subseteq> Y ` K" "finite CC" "K \<subseteq> \<Union>CC"
- by (meson compactE)
- then obtain c where c: "\<And>C. C \<in> CC \<Longrightarrow> c C \<in> K \<and> C = Y (c C)"
- by (force intro!: choice)
- with * CC show ?thesis
- by (force intro!: exI[where x="\<Inter>C\<in>CC. X0 (c C)"]) (* SLOW *)
-qed
-
-lemma continuous_on_prod_compactE:
- fixes fx::"'a::topological_space \<times> 'b::topological_space \<Rightarrow> 'c::metric_space"
- and e::real
- assumes cont_fx: "continuous_on (U \<times> C) fx"
- assumes "compact C"
- assumes [intro]: "x0 \<in> U"
- notes [continuous_intros] = continuous_on_compose2[OF cont_fx]
- assumes "e > 0"
- obtains X0 where "x0 \<in> X0" "open X0"
- "\<forall>x\<in>X0 \<inter> U. \<forall>t \<in> C. dist (fx (x, t)) (fx (x0, t)) \<le> e"
-proof -
- define psi where "psi = (\<lambda>(x, t). dist (fx (x, t)) (fx (x0, t)))"
- define W0 where "W0 = {(x, t) \<in> U \<times> C. psi (x, t) < e}"
- have W0_eq: "W0 = psi -` {..<e} \<inter> U \<times> C"
- by (auto simp: vimage_def W0_def)
- have "open {..<e}" by simp
- have "continuous_on (U \<times> C) psi"
- by (auto intro!: continuous_intros simp: psi_def split_beta')
- from this[unfolded continuous_on_open_invariant, rule_format, OF \<open>open {..<e}\<close>]
- obtain W where W: "open W" "W \<inter> U \<times> C = W0 \<inter> U \<times> C"
- unfolding W0_eq by blast
- have "{x0} \<times> C \<subseteq> W \<inter> U \<times> C"
- unfolding W
- by (auto simp: W0_def psi_def \<open>0 < e\<close>)
- then have "{x0} \<times> C \<subseteq> W" by blast
- from tube_lemma[OF \<open>compact C\<close> \<open>open W\<close> this]
- obtain X0 where X0: "x0 \<in> X0" "open X0" "X0 \<times> C \<subseteq> W"
- by blast
-
- have "\<forall>x\<in>X0 \<inter> U. \<forall>t \<in> C. dist (fx (x, t)) (fx (x0, t)) \<le> e"
- proof safe
- fix x assume x: "x \<in> X0" "x \<in> U"
- fix t assume t: "t \<in> C"
- have "dist (fx (x, t)) (fx (x0, t)) = psi (x, t)"
- by (auto simp: psi_def)
- also
- {
- have "(x, t) \<in> X0 \<times> C"
- using t x
- by auto
- also note \<open>\<dots> \<subseteq> W\<close>
- finally have "(x, t) \<in> W" .
- with t x have "(x, t) \<in> W \<inter> U \<times> C"
- by blast
- also note \<open>W \<inter> U \<times> C = W0 \<inter> U \<times> C\<close>
- finally have "psi (x, t) < e"
- by (auto simp: W0_def)
- }
- finally show "dist (fx (x, t)) (fx (x0, t)) \<le> e" by simp
- qed
- from X0(1,2) this show ?thesis ..
-qed
-
subsection%unimportant\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
@@ -1523,33 +811,6 @@
by blast
qed
-lemma finite_implies_discrete:
- fixes S :: "'a::topological_space set"
- assumes "finite (f ` S)"
- shows "(\<forall>x \<in> S. \<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x))"
-proof -
- have "\<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" if "x \<in> S" for x
- proof (cases "f ` S - {f x} = {}")
- case True
- with zero_less_numeral show ?thesis
- by (fastforce simp add: Set.image_subset_iff cong: conj_cong)
- next
- case False
- then obtain z where z: "z \<in> S" "f z \<noteq> f x"
- by blast
- have finn: "finite {norm (z - f x) |z. z \<in> f ` S - {f x}}"
- using assms by simp
- then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` S - {f x}}"
- apply (rule finite_imp_less_Inf)
- using z apply force+
- done
- show ?thesis
- by (force intro!: * cInf_le_finite [OF finn])
- qed
- with assms show ?thesis
- by blast
-qed
-
text\<open>This proof requires the existence of two separate values of the range type.\<close>
lemma finite_range_constant_imp_connected:
assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
@@ -1624,108 +885,4 @@
shows "f constant_on S"
using assms continuous_finite_range_constant_eq by blast
-
-
-subsection%unimportant \<open>Continuous Extension\<close>
-
-definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
- "clamp a b x = (if (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)
- then (\<Sum>i\<in>Basis. (if x\<bullet>i < a\<bullet>i then a\<bullet>i else if x\<bullet>i \<le> b\<bullet>i then x\<bullet>i else b\<bullet>i) *\<^sub>R i)
- else a)"
-
-lemma clamp_in_interval[simp]:
- assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
- shows "clamp a b x \<in> cbox a b"
- unfolding clamp_def
- using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)
-
-lemma clamp_cancel_cbox[simp]:
- fixes x a b :: "'a::euclidean_space"
- assumes x: "x \<in> cbox a b"
- shows "clamp a b x = x"
- using assms
- by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a])
-
-lemma clamp_empty_interval:
- assumes "i \<in> Basis" "a \<bullet> i > b \<bullet> i"
- shows "clamp a b = (\<lambda>_. a)"
- using assms
- by (force simp: clamp_def[abs_def] split: if_splits intro!: ext)
-
-lemma dist_clamps_le_dist_args:
- fixes x :: "'a::euclidean_space"
- shows "dist (clamp a b y) (clamp a b x) \<le> dist y x"
-proof cases
- assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
- then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le>
- (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
- by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
- then show ?thesis
- by (auto intro: real_sqrt_le_mono
- simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] L2_set_def)
-qed (auto simp: clamp_def)
-
-lemma clamp_continuous_at:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
- and x :: 'a
- assumes f_cont: "continuous_on (cbox a b) f"
- shows "continuous (at x) (\<lambda>x. f (clamp a b x))"
-proof cases
- assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
- show ?thesis
- unfolding continuous_at_eps_delta
- proof safe
- fix x :: 'a
- fix e :: real
- assume "e > 0"
- moreover have "clamp a b x \<in> cbox a b"
- by (simp add: clamp_in_interval le)
- moreover note f_cont[simplified continuous_on_iff]
- ultimately
- obtain d where d: "0 < d"
- "\<And>x'. x' \<in> cbox a b \<Longrightarrow> dist x' (clamp a b x) < d \<Longrightarrow> dist (f x') (f (clamp a b x)) < e"
- by force
- show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow>
- dist (f (clamp a b x')) (f (clamp a b x)) < e"
- using le
- by (auto intro!: d clamp_in_interval dist_clamps_le_dist_args[THEN le_less_trans])
- qed
-qed (auto simp: clamp_empty_interval)
-
-lemma clamp_continuous_on:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
- assumes f_cont: "continuous_on (cbox a b) f"
- shows "continuous_on S (\<lambda>x. f (clamp a b x))"
- using assms
- by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)
-
-lemma clamp_bounded:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
- assumes bounded: "bounded (f ` (cbox a b))"
- shows "bounded (range (\<lambda>x. f (clamp a b x)))"
-proof cases
- assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
- from bounded obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. dist undefined x \<le> c"
- by (auto simp: bounded_any_center[where a=undefined])
- then show ?thesis
- by (auto intro!: exI[where x=c] clamp_in_interval[OF le[rule_format]]
- simp: bounded_any_center[where a=undefined])
-qed (auto simp: clamp_empty_interval image_def)
-
-
-definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
- where "ext_cont f a b = (\<lambda>x. f (clamp a b x))"
-
-lemma ext_cont_cancel_cbox[simp]:
- fixes x a b :: "'a::euclidean_space"
- assumes x: "x \<in> cbox a b"
- shows "ext_cont f a b x = f x"
- using assms
- unfolding ext_cont_def
- by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a] arg_cong[where f=f])
-
-lemma continuous_on_ext_cont[continuous_intros]:
- "continuous_on (cbox a b) f \<Longrightarrow> continuous_on S (ext_cont f a b)"
- by (auto intro!: clamp_continuous_on simp: ext_cont_def)
-
end
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Mon Jan 07 11:51:18 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Mon Jan 07 12:31:08 2019 +0100
@@ -85,6 +85,18 @@
openin (subtopology euclidean (S \<times> T)) (S' \<times> T')"
unfolding openin_open using open_Times by blast
+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)
+
subsubsection \<open>Closure\<close>
@@ -395,6 +407,310 @@
by (simp add: continuous_on_closed oo)
qed
+subsubsection%unimportant \<open>Seperability\<close>
+
+lemma subset_second_countable:
+ obtains \<B> :: "'a:: second_countable_topology set set"
+ where "countable \<B>"
+ "{} \<notin> \<B>"
+ "\<And>C. C \<in> \<B> \<Longrightarrow> openin(subtopology euclidean S) C"
+ "\<And>T. openin(subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
+proof -
+ obtain \<B> :: "'a set set"
+ where "countable \<B>"
+ and opeB: "\<And>C. C \<in> \<B> \<Longrightarrow> openin(subtopology euclidean S) C"
+ and \<B>: "\<And>T. openin(subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
+ proof -
+ obtain \<C> :: "'a set set"
+ where "countable \<C>" and ope: "\<And>C. C \<in> \<C> \<Longrightarrow> open C"
+ and \<C>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<C> \<and> S = \<Union>U"
+ by (metis univ_second_countable that)
+ show ?thesis
+ proof
+ show "countable ((\<lambda>C. S \<inter> C) ` \<C>)"
+ by (simp add: \<open>countable \<C>\<close>)
+ show "\<And>C. C \<in> (\<inter>) S ` \<C> \<Longrightarrow> openin (subtopology euclidean S) C"
+ using ope by auto
+ show "\<And>T. openin (subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>\<subseteq>(\<inter>) S ` \<C>. T = \<Union>\<U>"
+ by (metis \<C> image_mono inf_Sup openin_open)
+ qed
+ qed
+ show ?thesis
+ proof
+ show "countable (\<B> - {{}})"
+ using \<open>countable \<B>\<close> by blast
+ show "\<And>C. \<lbrakk>C \<in> \<B> - {{}}\<rbrakk> \<Longrightarrow> openin (subtopology euclidean S) C"
+ by (simp add: \<open>\<And>C. C \<in> \<B> \<Longrightarrow> openin (subtopology euclidean S) C\<close>)
+ show "\<exists>\<U>\<subseteq>\<B> - {{}}. T = \<Union>\<U>" if "openin (subtopology euclidean S) T" for T
+ using \<B> [OF that]
+ apply clarify
+ apply (rule_tac x="\<U> - {{}}" in exI, auto)
+ done
+ qed auto
+qed
+
+lemma Lindelof_openin:
+ fixes \<F> :: "'a::second_countable_topology 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>(tf ` \<F>)"
+ 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
+
+
+subsubsection%unimportant\<open>Closed Maps\<close>
+
+lemma continuous_imp_closed_map:
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::t2_space"
+ assumes "closedin (subtopology euclidean S) U"
+ "continuous_on S f" "f ` S = T" "compact S"
+ shows "closedin (subtopology euclidean T) (f ` U)"
+ by (metis assms closedin_compact_eq compact_continuous_image continuous_on_subset subset_image_iff)
+
+lemma closed_map_restrict:
+ assumes cloU: "closedin (subtopology euclidean (S \<inter> f -` T')) U"
+ and cc: "\<And>U. closedin (subtopology euclidean S) U \<Longrightarrow> closedin (subtopology euclidean T) (f ` U)"
+ and "T' \<subseteq> T"
+ shows "closedin (subtopology euclidean T') (f ` U)"
+proof -
+ obtain V where "closed V" "U = S \<inter> f -` T' \<inter> V"
+ using cloU by (auto simp: closedin_closed)
+ with cc [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
+ by (fastforce simp add: closedin_closed)
+qed
+
+subsubsection%unimportant\<open>Open Maps\<close>
+
+lemma open_map_restrict:
+ assumes opeU: "openin (subtopology euclidean (S \<inter> f -` T')) U"
+ and oo: "\<And>U. openin (subtopology euclidean S) U \<Longrightarrow> openin (subtopology euclidean T) (f ` U)"
+ and "T' \<subseteq> T"
+ shows "openin (subtopology euclidean T') (f ` U)"
+proof -
+ obtain V where "open V" "U = S \<inter> f -` T' \<inter> V"
+ using opeU by (auto simp: openin_open)
+ with oo [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
+ by (fastforce simp add: openin_open)
+qed
+
+
+subsubsection%unimportant\<open>Quotient maps\<close>
+
+lemma quotient_map_imp_continuous_open:
+ assumes T: "f ` S \<subseteq> T"
+ and ope: "\<And>U. U \<subseteq> T
+ \<Longrightarrow> (openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+ openin (subtopology euclidean T) U)"
+ shows "continuous_on S f"
+proof -
+ have [simp]: "S \<inter> f -` f ` S = S" by auto
+ show ?thesis
+ using ope [OF T]
+ apply (simp add: continuous_on_open)
+ by (meson ope openin_imp_subset openin_trans)
+qed
+
+lemma quotient_map_imp_continuous_closed:
+ assumes T: "f ` S \<subseteq> T"
+ and ope: "\<And>U. U \<subseteq> T
+ \<Longrightarrow> (closedin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+ closedin (subtopology euclidean T) U)"
+ shows "continuous_on S f"
+proof -
+ have [simp]: "S \<inter> f -` f ` S = S" by auto
+ show ?thesis
+ using ope [OF T]
+ apply (simp add: continuous_on_closed)
+ by (metis (no_types, lifting) ope closedin_imp_subset closedin_trans)
+qed
+
+lemma open_map_imp_quotient_map:
+ assumes contf: "continuous_on S f"
+ and T: "T \<subseteq> f ` S"
+ and ope: "\<And>T. openin (subtopology euclidean S) T
+ \<Longrightarrow> openin (subtopology euclidean (f ` S)) (f ` T)"
+ shows "openin (subtopology euclidean S) (S \<inter> f -` T) =
+ openin (subtopology euclidean (f ` S)) T"
+proof -
+ have "T = f ` (S \<inter> f -` T)"
+ using T by blast
+ then show ?thesis
+ using "ope" contf continuous_on_open by metis
+qed
+
+lemma closed_map_imp_quotient_map:
+ assumes contf: "continuous_on S f"
+ and T: "T \<subseteq> f ` S"
+ and ope: "\<And>T. closedin (subtopology euclidean S) T
+ \<Longrightarrow> closedin (subtopology euclidean (f ` S)) (f ` T)"
+ shows "openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow>
+ openin (subtopology euclidean (f ` S)) T"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then have *: "closedin (subtopology euclidean S) (S - (S \<inter> f -` T))"
+ using closedin_diff by fastforce
+ have [simp]: "(f ` S - f ` (S - (S \<inter> f -` T))) = T"
+ using T by blast
+ show ?rhs
+ using ope [OF *, unfolded closedin_def] by auto
+next
+ assume ?rhs
+ with contf show ?lhs
+ by (auto simp: continuous_on_open)
+qed
+
+lemma continuous_right_inverse_imp_quotient_map:
+ assumes contf: "continuous_on S f" and imf: "f ` S \<subseteq> T"
+ and contg: "continuous_on T g" and img: "g ` T \<subseteq> S"
+ and fg [simp]: "\<And>y. y \<in> T \<Longrightarrow> f(g y) = y"
+ and U: "U \<subseteq> T"
+ shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+ openin (subtopology euclidean T) U"
+ (is "?lhs = ?rhs")
+proof -
+ have f: "\<And>Z. openin (subtopology euclidean (f ` S)) Z \<Longrightarrow>
+ openin (subtopology euclidean S) (S \<inter> f -` Z)"
+ and g: "\<And>Z. openin (subtopology euclidean (g ` T)) Z \<Longrightarrow>
+ openin (subtopology euclidean T) (T \<inter> g -` Z)"
+ using contf contg by (auto simp: continuous_on_open)
+ show ?thesis
+ proof
+ have "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = {x \<in> T. f (g x) \<in> U}"
+ using imf img by blast
+ also have "... = U"
+ using U by auto
+ finally have eq: "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = U" .
+ assume ?lhs
+ then have *: "openin (subtopology euclidean (g ` T)) (g ` T \<inter> (S \<inter> f -` U))"
+ by (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self)
+ show ?rhs
+ using g [OF *] eq by auto
+ next
+ assume rhs: ?rhs
+ show ?lhs
+ by (metis f fg image_eqI image_subset_iff imf img openin_subopen openin_subtopology_self openin_trans rhs)
+ qed
+qed
+
+lemma continuous_left_inverse_imp_quotient_map:
+ assumes "continuous_on S f"
+ and "continuous_on (f ` S) g"
+ and "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
+ and "U \<subseteq> f ` S"
+ shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+ openin (subtopology euclidean (f ` S)) U"
+apply (rule continuous_right_inverse_imp_quotient_map)
+using assms apply force+
+done
+
+lemma continuous_imp_quotient_map:
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::t2_space"
+ assumes "continuous_on S f" "f ` S = T" "compact S" "U \<subseteq> T"
+ shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+ openin (subtopology euclidean T) U"
+ by (metis (no_types, lifting) assms closed_map_imp_quotient_map continuous_imp_closed_map)
+
+subsubsection%unimportant\<open>Pasting functions together\<close>
+
+text\<open>on open sets\<close>
+
+lemma pasting_lemma:
+ fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
+ assumes clo: "\<And>i. i \<in> I \<Longrightarrow> openin (subtopology euclidean S) (T i)"
+ and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
+ and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
+ and g: "\<And>x. x \<in> S \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
+ shows "continuous_on S g"
+proof (clarsimp simp: continuous_openin_preimage_eq)
+ fix U :: "'b set"
+ assume "open U"
+ have S: "\<And>i. i \<in> I \<Longrightarrow> (T i) \<subseteq> S"
+ using clo openin_imp_subset by blast
+ have *: "(S \<inter> g -` U) = (\<Union>i \<in> I. T i \<inter> f i -` U)"
+ using S f g by fastforce
+ show "openin (subtopology euclidean S) (S \<inter> g -` U)"
+ apply (subst *)
+ apply (rule openin_Union, clarify)
+ using \<open>open U\<close> clo cont continuous_openin_preimage_gen openin_trans by blast
+qed
+
+lemma pasting_lemma_exists:
+ fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
+ assumes S: "S \<subseteq> (\<Union>i \<in> I. T i)"
+ and clo: "\<And>i. i \<in> I \<Longrightarrow> openin (subtopology euclidean S) (T i)"
+ and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
+ and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
+ obtains g where "continuous_on S g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> S \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x"
+proof
+ show "continuous_on S (\<lambda>x. f (SOME i. i \<in> I \<and> x \<in> T i) x)"
+ apply (rule pasting_lemma [OF clo cont])
+ apply (blast intro: f)+
+ apply (metis (mono_tags, lifting) S UN_iff subsetCE someI)
+ done
+next
+ fix x i
+ assume "i \<in> I" "x \<in> S \<inter> T i"
+ then show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
+ by (metis (no_types, lifting) IntD2 IntI f someI_ex)
+qed
+
+text\<open>Likewise on closed sets, with a finiteness assumption\<close>
+
+lemma pasting_lemma_closed:
+ fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
+ assumes "finite I"
+ and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin (subtopology euclidean S) (T i)"
+ and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
+ and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
+ and g: "\<And>x. x \<in> S \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
+ shows "continuous_on S g"
+proof (clarsimp simp: continuous_closedin_preimage_eq)
+ fix U :: "'b set"
+ assume "closed U"
+ have S: "\<And>i. i \<in> I \<Longrightarrow> (T i) \<subseteq> S"
+ using clo closedin_imp_subset by blast
+ have *: "(S \<inter> g -` U) = (\<Union>i \<in> I. T i \<inter> f i -` U)"
+ using S f g by fastforce
+ show "closedin (subtopology euclidean S) (S \<inter> g -` U)"
+ apply (subst *)
+ apply (rule closedin_Union)
+ using \<open>finite I\<close> apply simp
+ apply (blast intro: \<open>closed U\<close> continuous_closedin_preimage cont clo closedin_trans)
+ done
+qed
+
+lemma pasting_lemma_exists_closed:
+ fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
+ assumes "finite I"
+ and S: "S \<subseteq> (\<Union>i \<in> I. T i)"
+ and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin (subtopology euclidean S) (T i)"
+ and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
+ and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
+ obtains g where "continuous_on S g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> S \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x"
+proof
+ show "continuous_on S (\<lambda>x. f (SOME i. i \<in> I \<and> x \<in> T i) x)"
+ apply (rule pasting_lemma_closed [OF \<open>finite I\<close> clo cont])
+ apply (blast intro: f)+
+ apply (metis (mono_tags, lifting) S UN_iff subsetCE someI)
+ done
+next
+ fix x i
+ assume "i \<in> I" "x \<in> S \<inter> T i"
+ then show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
+ by (metis (no_types, lifting) IntD2 IntI f someI_ex)
+qed
+
subsection \<open>Open and closed balls\<close>
@@ -2227,6 +2543,62 @@
by auto
+subsection%unimportant\<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)
+
+
subsection \<open>Properties of Balls and Spheres\<close>
lemma compact_cball[simp]:
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy Mon Jan 07 11:51:18 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Mon Jan 07 12:31:08 2019 +0100
@@ -1573,6 +1573,36 @@
using assms homeomorphic_ball01_UNIV homeomorphic_balls(1) homeomorphic_trans zero_less_one by blast
+subsection%unimportant \<open>Discrete\<close>
+
+lemma finite_implies_discrete:
+ fixes S :: "'a::topological_space set"
+ assumes "finite (f ` S)"
+ shows "(\<forall>x \<in> S. \<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x))"
+proof -
+ have "\<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" if "x \<in> S" for x
+ proof (cases "f ` S - {f x} = {}")
+ case True
+ with zero_less_numeral show ?thesis
+ by (fastforce simp add: Set.image_subset_iff cong: conj_cong)
+ next
+ case False
+ then obtain z where z: "z \<in> S" "f z \<noteq> f x"
+ by blast
+ have finn: "finite {norm (z - f x) |z. z \<in> f ` S - {f x}}"
+ using assms by simp
+ then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` S - {f x}}"
+ apply (rule finite_imp_less_Inf)
+ using z apply force+
+ done
+ show ?thesis
+ by (force intro!: * cInf_le_finite [OF finn])
+ qed
+ with assms show ?thesis
+ by blast
+qed
+
+
subsection%unimportant \<open>Completeness of "Isometry" (up to constant bounds)\<close>
lemma cauchy_isometric:\<comment> \<open>TODO: rename lemma to \<open>Cauchy_isometric\<close>\<close>
--- a/src/HOL/Analysis/Elementary_Topology.thy Mon Jan 07 11:51:18 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy Mon Jan 07 12:31:08 2019 +0100
@@ -9,6 +9,7 @@
theory Elementary_Topology
imports
"HOL-Library.Set_Idioms"
+ "HOL-Library.Disjoint_Sets"
Product_Vector
begin
@@ -463,13 +464,65 @@
qed
qed
+
end
+lemma univ_second_countable:
+ obtains \<B> :: "'a::second_countable_topology 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)
+
+proposition Lindelof:
+ fixes \<F> :: "'a::second_countable_topology 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> (G ` \<D>)"
+ using G eq1 by auto
+ show ?thesis
+ apply (rule_tac \<F>' = "G ` \<D>" in that)
+ using G \<open>countable \<D>\<close>
+ by (auto simp: eq1 eq2)
+qed
+
+lemma countable_disjoint_open_subsets:
+ fixes \<F> :: "'a::second_countable_topology 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
+
sublocale second_countable_topology <
countable_basis "SOME B. countable B \<and> topological_basis B"
using someI_ex[OF ex_countable_basis]
by unfold_locales safe
+
instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology
proof
obtain A :: "'a set set" where "countable A" "topological_basis A"
@@ -594,6 +647,7 @@
then show ?thesis using B(1) by auto
qed
+
subsection%important \<open>Polish spaces\<close>
text \<open>Textbooks define Polish spaces as completely metrizable.
@@ -966,6 +1020,20 @@
by (auto simp: subset_eq less_le)
qed auto
+lemma countable_disjoint_nonempty_interior_subsets:
+ fixes \<F> :: "'a::second_countable_topology set set"
+ assumes pw: "pairwise disjnt \<F>" and int: "\<And>S. \<lbrakk>S \<in> \<F>; interior S = {}\<rbrakk> \<Longrightarrow> S = {}"
+ shows "countable \<F>"
+proof (rule countable_image_inj_on)
+ have "disjoint (interior ` \<F>)"
+ using pw by (simp add: disjoint_image_subset interior_subset)
+ then show "countable (interior ` \<F>)"
+ by (auto intro: countable_disjoint_open_subsets)
+ show "inj_on interior \<F>"
+ using pw apply (clarsimp simp: inj_on_def pairwise_def)
+ apply (metis disjnt_def disjnt_subset1 inf.orderE int interior_subset)
+ done
+qed
subsection \<open>Closure of a Set\<close>
@@ -2172,6 +2240,85 @@
qed
+lemma tube_lemma:
+ assumes "compact K"
+ assumes "open W"
+ assumes "{x0} \<times> K \<subseteq> W"
+ shows "\<exists>X0. x0 \<in> X0 \<and> open X0 \<and> X0 \<times> K \<subseteq> W"
+proof -
+ {
+ fix y assume "y \<in> K"
+ then have "(x0, y) \<in> W" using assms by auto
+ with \<open>open W\<close>
+ have "\<exists>X0 Y. open X0 \<and> open Y \<and> x0 \<in> X0 \<and> y \<in> Y \<and> X0 \<times> Y \<subseteq> W"
+ by (rule open_prod_elim) blast
+ }
+ then obtain X0 Y where
+ *: "\<forall>y \<in> K. open (X0 y) \<and> open (Y y) \<and> x0 \<in> X0 y \<and> y \<in> Y y \<and> X0 y \<times> Y y \<subseteq> W"
+ by metis
+ from * have "\<forall>t\<in>Y ` K. open t" "K \<subseteq> \<Union>(Y ` K)" by auto
+ with \<open>compact K\<close> obtain CC where CC: "CC \<subseteq> Y ` K" "finite CC" "K \<subseteq> \<Union>CC"
+ by (meson compactE)
+ then obtain c where c: "\<And>C. C \<in> CC \<Longrightarrow> c C \<in> K \<and> C = Y (c C)"
+ by (force intro!: choice)
+ with * CC show ?thesis
+ by (force intro!: exI[where x="\<Inter>C\<in>CC. X0 (c C)"]) (* SLOW *)
+qed
+
+lemma continuous_on_prod_compactE:
+ fixes fx::"'a::topological_space \<times> 'b::topological_space \<Rightarrow> 'c::metric_space"
+ and e::real
+ assumes cont_fx: "continuous_on (U \<times> C) fx"
+ assumes "compact C"
+ assumes [intro]: "x0 \<in> U"
+ notes [continuous_intros] = continuous_on_compose2[OF cont_fx]
+ assumes "e > 0"
+ obtains X0 where "x0 \<in> X0" "open X0"
+ "\<forall>x\<in>X0 \<inter> U. \<forall>t \<in> C. dist (fx (x, t)) (fx (x0, t)) \<le> e"
+proof -
+ define psi where "psi = (\<lambda>(x, t). dist (fx (x, t)) (fx (x0, t)))"
+ define W0 where "W0 = {(x, t) \<in> U \<times> C. psi (x, t) < e}"
+ have W0_eq: "W0 = psi -` {..<e} \<inter> U \<times> C"
+ by (auto simp: vimage_def W0_def)
+ have "open {..<e}" by simp
+ have "continuous_on (U \<times> C) psi"
+ by (auto intro!: continuous_intros simp: psi_def split_beta')
+ from this[unfolded continuous_on_open_invariant, rule_format, OF \<open>open {..<e}\<close>]
+ obtain W where W: "open W" "W \<inter> U \<times> C = W0 \<inter> U \<times> C"
+ unfolding W0_eq by blast
+ have "{x0} \<times> C \<subseteq> W \<inter> U \<times> C"
+ unfolding W
+ by (auto simp: W0_def psi_def \<open>0 < e\<close>)
+ then have "{x0} \<times> C \<subseteq> W" by blast
+ from tube_lemma[OF \<open>compact C\<close> \<open>open W\<close> this]
+ obtain X0 where X0: "x0 \<in> X0" "open X0" "X0 \<times> C \<subseteq> W"
+ by blast
+
+ have "\<forall>x\<in>X0 \<inter> U. \<forall>t \<in> C. dist (fx (x, t)) (fx (x0, t)) \<le> e"
+ proof safe
+ fix x assume x: "x \<in> X0" "x \<in> U"
+ fix t assume t: "t \<in> C"
+ have "dist (fx (x, t)) (fx (x0, t)) = psi (x, t)"
+ by (auto simp: psi_def)
+ also
+ {
+ have "(x, t) \<in> X0 \<times> C"
+ using t x
+ by auto
+ also note \<open>\<dots> \<subseteq> W\<close>
+ finally have "(x, t) \<in> W" .
+ with t x have "(x, t) \<in> W \<inter> U \<times> C"
+ by blast
+ also note \<open>W \<inter> U \<times> C = W0 \<inter> U \<times> C\<close>
+ finally have "psi (x, t) < e"
+ by (auto simp: W0_def)
+ }
+ finally show "dist (fx (x, t)) (fx (x0, t)) \<le> e" by simp
+ qed
+ from X0(1,2) this show ?thesis ..
+qed
+
+
subsection \<open>Continuity\<close>
lemma continuous_at_imp_continuous_within:
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Jan 07 11:51:18 2019 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Jan 07 12:31:08 2019 +0100
@@ -1586,6 +1586,313 @@
qed
+subsection%unimportant\<open>Componentwise limits and continuity\<close>
+
+text\<open>But is the premise really necessary? Need to generalise @{thm euclidean_dist_l2}\<close>
+lemma Euclidean_dist_upper: "i \<in> Basis \<Longrightarrow> dist (x \<bullet> i) (y \<bullet> i) \<le> dist x y"
+ by (metis (no_types) member_le_L2_set euclidean_dist_l2 finite_Basis)
+
+text\<open>But is the premise \<^term>\<open>i \<in> Basis\<close> really necessary?\<close>
+lemma open_preimage_inner:
+ assumes "open S" "i \<in> Basis"
+ shows "open {x. x \<bullet> i \<in> S}"
+proof (rule openI, simp)
+ fix x
+ assume x: "x \<bullet> i \<in> S"
+ with assms obtain e where "0 < e" and e: "ball (x \<bullet> i) e \<subseteq> S"
+ by (auto simp: open_contains_ball_eq)
+ have "\<exists>e>0. ball (y \<bullet> i) e \<subseteq> S" if dxy: "dist x y < e / 2" for y
+ proof (intro exI conjI)
+ have "dist (x \<bullet> i) (y \<bullet> i) < e / 2"
+ by (meson \<open>i \<in> Basis\<close> dual_order.trans Euclidean_dist_upper not_le that)
+ then have "dist (x \<bullet> i) z < e" if "dist (y \<bullet> i) z < e / 2" for z
+ by (metis dist_commute dist_triangle_half_l that)
+ then have "ball (y \<bullet> i) (e / 2) \<subseteq> ball (x \<bullet> i) e"
+ using mem_ball by blast
+ with e show "ball (y \<bullet> i) (e / 2) \<subseteq> S"
+ by (metis order_trans)
+ qed (simp add: \<open>0 < e\<close>)
+ then show "\<exists>e>0. ball x e \<subseteq> {s. s \<bullet> i \<in> S}"
+ by (metis (no_types, lifting) \<open>0 < e\<close> \<open>open S\<close> half_gt_zero_iff mem_Collect_eq mem_ball open_contains_ball_eq subsetI)
+qed
+
+proposition tendsto_componentwise_iff:
+ fixes f :: "_ \<Rightarrow> 'b::euclidean_space"
+ shows "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>i \<in> Basis. ((\<lambda>x. (f x \<bullet> i)) \<longlongrightarrow> (l \<bullet> i)) F)"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ unfolding tendsto_def
+ apply clarify
+ apply (drule_tac x="{s. s \<bullet> i \<in> S}" in spec)
+ apply (auto simp: open_preimage_inner)
+ done
+next
+ assume R: ?rhs
+ then have "\<And>e. e > 0 \<Longrightarrow> \<forall>i\<in>Basis. \<forall>\<^sub>F x in F. dist (f x \<bullet> i) (l \<bullet> i) < e"
+ unfolding tendsto_iff by blast
+ then have R': "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F x in F. \<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e"
+ by (simp add: eventually_ball_finite_distrib [symmetric])
+ show ?lhs
+ unfolding tendsto_iff
+ proof clarify
+ fix e::real
+ assume "0 < e"
+ have *: "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e"
+ if "\<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / real DIM('b)" for x
+ proof -
+ have "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis \<le> sum (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis"
+ by (simp add: L2_set_le_sum)
+ also have "... < DIM('b) * (e / real DIM('b))"
+ apply (rule sum_bounded_above_strict)
+ using that by auto
+ also have "... = e"
+ by (simp add: field_simps)
+ finally show "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e" .
+ qed
+ have "\<forall>\<^sub>F x in F. \<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / DIM('b)"
+ apply (rule R')
+ using \<open>0 < e\<close> by simp
+ then show "\<forall>\<^sub>F x in F. dist (f x) l < e"
+ apply (rule eventually_mono)
+ apply (subst euclidean_dist_l2)
+ using * by blast
+ qed
+qed
+
+
+corollary continuous_componentwise:
+ "continuous F f \<longleftrightarrow> (\<forall>i \<in> Basis. continuous F (\<lambda>x. (f x \<bullet> i)))"
+by (simp add: continuous_def tendsto_componentwise_iff [symmetric])
+
+corollary continuous_on_componentwise:
+ fixes S :: "'a :: t2_space set"
+ shows "continuous_on S f \<longleftrightarrow> (\<forall>i \<in> Basis. continuous_on S (\<lambda>x. (f x \<bullet> i)))"
+ apply (simp add: continuous_on_eq_continuous_within)
+ using continuous_componentwise by blast
+
+lemma linear_componentwise_iff:
+ "(linear f') \<longleftrightarrow> (\<forall>i\<in>Basis. linear (\<lambda>x. f' x \<bullet> i))"
+ apply (auto simp: linear_iff inner_left_distrib)
+ apply (metis inner_left_distrib euclidean_eq_iff)
+ by (metis euclidean_eqI inner_scaleR_left)
+
+lemma bounded_linear_componentwise_iff:
+ "(bounded_linear f') \<longleftrightarrow> (\<forall>i\<in>Basis. bounded_linear (\<lambda>x. f' x \<bullet> i))"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs then show ?rhs
+ by (simp add: bounded_linear_inner_left_comp)
+next
+ assume ?rhs
+ then have "(\<forall>i\<in>Basis. \<exists>K. \<forall>x. \<bar>f' x \<bullet> i\<bar> \<le> norm x * K)" "linear f'"
+ by (auto simp: bounded_linear_def bounded_linear_axioms_def linear_componentwise_iff [symmetric] ball_conj_distrib)
+ then obtain F where F: "\<And>i x. i \<in> Basis \<Longrightarrow> \<bar>f' x \<bullet> i\<bar> \<le> norm x * F i"
+ by metis
+ have "norm (f' x) \<le> norm x * sum F Basis" for x
+ proof -
+ have "norm (f' x) \<le> (\<Sum>i\<in>Basis. \<bar>f' x \<bullet> i\<bar>)"
+ by (rule norm_le_l1)
+ also have "... \<le> (\<Sum>i\<in>Basis. norm x * F i)"
+ by (metis F sum_mono)
+ also have "... = norm x * sum F Basis"
+ by (simp add: sum_distrib_left)
+ finally show ?thesis .
+ qed
+ then show ?lhs
+ by (force simp: bounded_linear_def bounded_linear_axioms_def \<open>linear f'\<close>)
+qed
+
+subsection%unimportant \<open>Continuous Extension\<close>
+
+definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
+ "clamp a b x = (if (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)
+ then (\<Sum>i\<in>Basis. (if x\<bullet>i < a\<bullet>i then a\<bullet>i else if x\<bullet>i \<le> b\<bullet>i then x\<bullet>i else b\<bullet>i) *\<^sub>R i)
+ else a)"
+
+lemma clamp_in_interval[simp]:
+ assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
+ shows "clamp a b x \<in> cbox a b"
+ unfolding clamp_def
+ using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)
+
+lemma clamp_cancel_cbox[simp]:
+ fixes x a b :: "'a::euclidean_space"
+ assumes x: "x \<in> cbox a b"
+ shows "clamp a b x = x"
+ using assms
+ by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a])
+
+lemma clamp_empty_interval:
+ assumes "i \<in> Basis" "a \<bullet> i > b \<bullet> i"
+ shows "clamp a b = (\<lambda>_. a)"
+ using assms
+ by (force simp: clamp_def[abs_def] split: if_splits intro!: ext)
+
+lemma dist_clamps_le_dist_args:
+ fixes x :: "'a::euclidean_space"
+ shows "dist (clamp a b y) (clamp a b x) \<le> dist y x"
+proof cases
+ assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
+ then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le>
+ (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
+ by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
+ then show ?thesis
+ by (auto intro: real_sqrt_le_mono
+ simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] L2_set_def)
+qed (auto simp: clamp_def)
+
+lemma clamp_continuous_at:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
+ and x :: 'a
+ assumes f_cont: "continuous_on (cbox a b) f"
+ shows "continuous (at x) (\<lambda>x. f (clamp a b x))"
+proof cases
+ assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
+ show ?thesis
+ unfolding continuous_at_eps_delta
+ proof safe
+ fix x :: 'a
+ fix e :: real
+ assume "e > 0"
+ moreover have "clamp a b x \<in> cbox a b"
+ by (simp add: clamp_in_interval le)
+ moreover note f_cont[simplified continuous_on_iff]
+ ultimately
+ obtain d where d: "0 < d"
+ "\<And>x'. x' \<in> cbox a b \<Longrightarrow> dist x' (clamp a b x) < d \<Longrightarrow> dist (f x') (f (clamp a b x)) < e"
+ by force
+ show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow>
+ dist (f (clamp a b x')) (f (clamp a b x)) < e"
+ using le
+ by (auto intro!: d clamp_in_interval dist_clamps_le_dist_args[THEN le_less_trans])
+ qed
+qed (auto simp: clamp_empty_interval)
+
+lemma clamp_continuous_on:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
+ assumes f_cont: "continuous_on (cbox a b) f"
+ shows "continuous_on S (\<lambda>x. f (clamp a b x))"
+ using assms
+ by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)
+
+lemma clamp_bounded:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
+ assumes bounded: "bounded (f ` (cbox a b))"
+ shows "bounded (range (\<lambda>x. f (clamp a b x)))"
+proof cases
+ assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
+ from bounded obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. dist undefined x \<le> c"
+ by (auto simp: bounded_any_center[where a=undefined])
+ then show ?thesis
+ by (auto intro!: exI[where x=c] clamp_in_interval[OF le[rule_format]]
+ simp: bounded_any_center[where a=undefined])
+qed (auto simp: clamp_empty_interval image_def)
+
+
+definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
+ where "ext_cont f a b = (\<lambda>x. f (clamp a b x))"
+
+lemma ext_cont_cancel_cbox[simp]:
+ fixes x a b :: "'a::euclidean_space"
+ assumes x: "x \<in> cbox a b"
+ shows "ext_cont f a b x = f x"
+ using assms
+ unfolding ext_cont_def
+ by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a] arg_cong[where f=f])
+
+lemma continuous_on_ext_cont[continuous_intros]:
+ "continuous_on (cbox a b) f \<Longrightarrow> continuous_on S (ext_cont f a b)"
+ by (auto intro!: clamp_continuous_on simp: ext_cont_def)
+
+
+subsection \<open>Separability\<close>
+
+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 opn: "\<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> opn)
+ done
+qed
+
+proposition separable:
+ fixes S :: "'a::{metric_space, second_countable_topology} set"
+ obtains T where "countable T" "T \<subseteq> S" "S \<subseteq> closure T"
+proof -
+ obtain \<B> :: "'a set set"
+ where "countable \<B>"
+ and "{} \<notin> \<B>"
+ and ope: "\<And>C. C \<in> \<B> \<Longrightarrow> openin(subtopology euclidean S) C"
+ and if_ope: "\<And>T. openin(subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
+ by (meson subset_second_countable)
+ then obtain f where f: "\<And>C. C \<in> \<B> \<Longrightarrow> f C \<in> C"
+ by (metis equals0I)
+ show ?thesis
+ proof
+ show "countable (f ` \<B>)"
+ by (simp add: \<open>countable \<B>\<close>)
+ show "f ` \<B> \<subseteq> S"
+ using ope f openin_imp_subset by blast
+ show "S \<subseteq> closure (f ` \<B>)"
+ proof (clarsimp simp: closure_approachable)
+ fix x and e::real
+ assume "x \<in> S" "0 < e"
+ have "openin (subtopology euclidean S) (S \<inter> ball x e)"
+ by (simp add: openin_Int_open)
+ with if_ope obtain \<U> where \<U>: "\<U> \<subseteq> \<B>" "S \<inter> ball x e = \<Union>\<U>"
+ by meson
+ show "\<exists>C \<in> \<B>. dist (f C) x < e"
+ proof (cases "\<U> = {}")
+ case True
+ then show ?thesis
+ using \<open>0 < e\<close> \<U> \<open>x \<in> S\<close> by auto
+ next
+ case False
+ then obtain C where "C \<in> \<U>" by blast
+ show ?thesis
+ proof
+ show "dist (f C) x < e"
+ by (metis Int_iff Union_iff \<U> \<open>C \<in> \<U>\<close> dist_commute f mem_ball subsetCE)
+ show "C \<in> \<B>"
+ using \<open>\<U> \<subseteq> \<B>\<close> \<open>C \<in> \<U>\<close> by blast
+ qed
+ qed
+ qed
+ qed
+qed
+
+
subsection%unimportant \<open>Diameter\<close>
lemma diameter_cball [simp]: