--- a/src/HOL/Analysis/Abstract_Topology.thy Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy Tue May 02 15:17:39 2023 +0100
@@ -297,6 +297,10 @@
unfolding closedin_def topspace_subtopology
by (auto simp: openin_subtopology)
+lemma closedin_relative_to:
+ "(closedin X relative_to S) = closedin (subtopology X S)"
+ by (force simp: relative_to_def closedin_subtopology)
+
lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U"
unfolding openin_subtopology
by auto (metis IntD1 in_mono openin_subset)
@@ -1879,6 +1883,250 @@
by (metis \<open>closedin X T\<close> closed_map_def closedin_subtopology f)
qed
+lemma closed_map_closure_of_image:
+ "closed_map X Y f \<longleftrightarrow>
+ f ` topspace X \<subseteq> topspace Y \<and>
+ (\<forall>S. S \<subseteq> topspace X \<longrightarrow> Y closure_of (f ` S) \<subseteq> image f (X closure_of S))" (is "?lhs=?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ by (simp add: closed_map_def closed_map_imp_subset_topspace closure_of_minimal closure_of_subset image_mono)
+next
+ assume ?rhs
+ then show ?lhs
+ by (metis closed_map_def closed_map_into_discrete_topology closure_of_eq
+ closure_of_subset_eq topspace_discrete_topology)
+qed
+
+lemma open_map_interior_of_image_subset:
+ "open_map X Y f \<longleftrightarrow> (\<forall>S. image f (X interior_of S) \<subseteq> Y interior_of (f ` S))"
+ by (metis image_mono interior_of_eq interior_of_maximal interior_of_subset open_map_def openin_interior_of subset_antisym)
+
+lemma open_map_interior_of_image_subset_alt:
+ "open_map X Y f \<longleftrightarrow> (\<forall>S\<subseteq>topspace X. f ` (X interior_of S) \<subseteq> Y interior_of f ` S)"
+ by (metis interior_of_eq open_map_def open_map_interior_of_image_subset openin_subset subset_interior_of_eq)
+
+lemma open_map_interior_of_image_subset_gen:
+ "open_map X Y f \<longleftrightarrow>
+ (f ` topspace X \<subseteq> topspace Y \<and> (\<forall>S. f ` (X interior_of S) \<subseteq> Y interior_of f ` S))"
+ by (meson open_map_imp_subset_topspace open_map_interior_of_image_subset)
+
+lemma open_map_preimage_neighbourhood:
+ "open_map X Y f \<longleftrightarrow>
+ (f ` topspace X \<subseteq> topspace Y \<and>
+ (\<forall>U T. closedin X U \<and> T \<subseteq> topspace Y \<and>
+ {x \<in> topspace X. f x \<in> T} \<subseteq> U \<longrightarrow>
+ (\<exists>V. closedin Y V \<and> T \<subseteq> V \<and> {x \<in> topspace X. f x \<in> V} \<subseteq> U)))" (is "?lhs=?rhs")
+proof
+ assume L: ?lhs
+ show ?rhs
+ proof (intro conjI strip)
+ show "f ` topspace X \<subseteq> topspace Y"
+ by (simp add: \<open>open_map X Y f\<close> open_map_imp_subset_topspace)
+ next
+ fix U T
+ assume UT: "closedin X U \<and> T \<subseteq> topspace Y \<and> {x \<in> topspace X. f x \<in> T} \<subseteq> U"
+ have "closedin Y (topspace Y - f ` (topspace X - U))"
+ by (meson UT L open_map_def openin_closedin_eq openin_diff openin_topspace)
+ with UT
+ show "\<exists>V. closedin Y V \<and> T \<subseteq> V \<and> {x \<in> topspace X. f x \<in> V} \<subseteq> U"
+ using image_iff by auto
+ qed
+next
+ assume R: ?rhs
+ show ?lhs
+ unfolding open_map_def
+ proof (intro strip)
+ fix U assume "openin X U"
+ have "{x \<in> topspace X. f x \<in> topspace Y - f ` U} \<subseteq> topspace X - U"
+ by blast
+ then obtain V where V: "closedin Y V"
+ and sub: "topspace Y - f ` U \<subseteq> V" "{x \<in> topspace X. f x \<in> V} \<subseteq> topspace X - U"
+ using R \<open>openin X U\<close> by (meson Diff_subset openin_closedin_eq)
+ then have "f ` U \<subseteq> topspace Y - V"
+ using R \<open>openin X U\<close> openin_subset by fastforce
+ with sub have "f ` U = topspace Y - V"
+ by auto
+ then show "openin Y (f ` U)"
+ using V(1) by auto
+ qed
+qed
+
+
+lemma closed_map_preimage_neighbourhood:
+ "closed_map X Y f \<longleftrightarrow>
+ image f (topspace X) \<subseteq> topspace Y \<and>
+ (\<forall>U T. openin X U \<and> T \<subseteq> topspace Y \<and>
+ {x \<in> topspace X. f x \<in> T} \<subseteq> U
+ \<longrightarrow> (\<exists>V. openin Y V \<and> T \<subseteq> V \<and>
+ {x \<in> topspace X. f x \<in> V} \<subseteq> U))" (is "?lhs=?rhs")
+proof
+ assume L: ?lhs
+ show ?rhs
+ proof (intro conjI strip)
+ show "f ` topspace X \<subseteq> topspace Y"
+ by (simp add: L closed_map_imp_subset_topspace)
+ next
+ fix U T
+ assume UT: "openin X U \<and> T \<subseteq> topspace Y \<and> {x \<in> topspace X. f x \<in> T} \<subseteq> U"
+ then have "openin Y (topspace Y - f ` (topspace X - U))"
+ by (meson L closed_map_def closedin_def closedin_diff closedin_topspace)
+ then show "\<exists>V. openin Y V \<and> T \<subseteq> V \<and> {x \<in> topspace X. f x \<in> V} \<subseteq> U"
+ using UT image_iff by auto
+ qed
+next
+ assume R: ?rhs
+ show ?lhs
+ unfolding closed_map_def
+ proof (intro strip)
+ fix U assume "closedin X U"
+ have "{x \<in> topspace X. f x \<in> topspace Y - f ` U} \<subseteq> topspace X - U"
+ by blast
+ then obtain V where V: "openin Y V"
+ and sub: "topspace Y - f ` U \<subseteq> V" "{x \<in> topspace X. f x \<in> V} \<subseteq> topspace X - U"
+ using R Diff_subset \<open>closedin X U\<close> unfolding closedin_def
+ by (smt (verit, ccfv_threshold) Collect_mem_eq Collect_mono_iff)
+ then have "f ` U \<subseteq> topspace Y - V"
+ using R \<open>closedin X U\<close> closedin_subset by fastforce
+ with sub have "f ` U = topspace Y - V"
+ by auto
+ with V show "closedin Y (f ` U)"
+ by auto
+ qed
+qed
+
+lemma closed_map_fibre_neighbourhood:
+ "closed_map X Y f \<longleftrightarrow>
+ f ` (topspace X) \<subseteq> topspace Y \<and>
+ (\<forall>U y. openin X U \<and> y \<in> topspace Y \<and> {x \<in> topspace X. f x = y} \<subseteq> U
+ \<longrightarrow> (\<exists>V. openin Y V \<and> y \<in> V \<and> {x \<in> topspace X. f x \<in> V} \<subseteq> U))"
+ unfolding closed_map_preimage_neighbourhood
+proof (intro conj_cong refl all_cong1)
+ fix U
+ assume "f ` topspace X \<subseteq> topspace Y"
+ show "(\<forall>T. openin X U \<and> T \<subseteq> topspace Y \<and> {x \<in> topspace X. f x \<in> T} \<subseteq> U
+ \<longrightarrow> (\<exists>V. openin Y V \<and> T \<subseteq> V \<and> {x \<in> topspace X. f x \<in> V} \<subseteq> U))
+ = (\<forall>y. openin X U \<and> y \<in> topspace Y \<and> {x \<in> topspace X. f x = y} \<subseteq> U
+ \<longrightarrow> (\<exists>V. openin Y V \<and> y \<in> V \<and> {x \<in> topspace X. f x \<in> V} \<subseteq> U))"
+ (is "(\<forall>T. ?P T) \<longleftrightarrow> (\<forall>y. ?Q y)")
+ proof
+ assume L [rule_format]: "\<forall>T. ?P T"
+ show "\<forall>y. ?Q y"
+ proof
+ fix y show "?Q y"
+ using L [of "{y}"] by blast
+ qed
+ next
+ assume R: "\<forall>y. ?Q y"
+ show "\<forall>T. ?P T"
+ proof (cases "openin X U")
+ case True
+ note [[unify_search_bound=3]]
+ obtain V where V: "\<And>y. \<lbrakk>y \<in> topspace Y; {x \<in> topspace X. f x = y} \<subseteq> U\<rbrakk> \<Longrightarrow>
+ openin Y (V y) \<and> y \<in> V y \<and> {x \<in> topspace X. f x \<in> V y} \<subseteq> U"
+ using R by (simp add: True) meson
+ show ?thesis
+ proof clarify
+ fix T
+ assume "openin X U" and "T \<subseteq> topspace Y" and "{x \<in> topspace X. f x \<in> T} \<subseteq> U"
+ with V show "\<exists>V. openin Y V \<and> T \<subseteq> V \<and> {x \<in> topspace X. f x \<in> V} \<subseteq> U"
+ by (rule_tac x="\<Union>y\<in>T. V y" in exI) fastforce
+ qed
+ qed auto
+ qed
+qed
+
+lemma open_map_in_subtopology:
+ "openin Y S
+ \<Longrightarrow> (open_map X (subtopology Y S) f \<longleftrightarrow> open_map X Y f \<and> f ` (topspace X) \<subseteq> S)"
+ by (metis le_inf_iff open_map_def open_map_imp_subset_topspace open_map_into_subtopology openin_trans_full topspace_subtopology)
+
+lemma open_map_from_open_subtopology:
+ "\<lbrakk>openin Y S; open_map X (subtopology Y S) f\<rbrakk> \<Longrightarrow> open_map X Y f"
+ using open_map_in_subtopology by blast
+
+lemma closed_map_in_subtopology:
+ "closedin Y S
+ \<Longrightarrow> closed_map X (subtopology Y S) f \<longleftrightarrow> (closed_map X Y f \<and> f ` topspace X \<subseteq> S)"
+ by (metis closed_map_def closed_map_imp_subset_topspace closed_map_into_subtopology
+ closedin_closed_subtopology closedin_subset topspace_subtopology_subset)
+
+lemma closed_map_from_closed_subtopology:
+ "\<lbrakk>closedin Y S; closed_map X (subtopology Y S) f\<rbrakk> \<Longrightarrow> closed_map X Y f"
+ using closed_map_in_subtopology by blast
+
+lemma closed_map_from_composition_left:
+ assumes cmf: "closed_map X Z (g \<circ> f)" and contf: "continuous_map X Y f" and fim: "f ` topspace X = topspace Y"
+ shows "closed_map Y Z g"
+ unfolding closed_map_def
+proof (intro strip)
+ fix U assume "closedin Y U"
+ then have "closedin X {x \<in> topspace X. f x \<in> U}"
+ using contf closedin_continuous_map_preimage by blast
+ then have "closedin Z ((g \<circ> f) ` {x \<in> topspace X. f x \<in> U})"
+ using cmf closed_map_def by blast
+ moreover
+ have "\<And>y. y \<in> U \<Longrightarrow> \<exists>x \<in> topspace X. f x \<in> U \<and> g y = g (f x)"
+ by (smt (verit, ccfv_SIG) \<open>closedin Y U\<close> closedin_subset fim image_iff subsetD)
+ then have "(g \<circ> f) ` {x \<in> topspace X. f x \<in> U} = g`U" by auto
+ ultimately show "closedin Z (g ` U)"
+ by metis
+qed
+
+text \<open>identical proof as the above\<close>
+lemma open_map_from_composition_left:
+ assumes cmf: "open_map X Z (g \<circ> f)" and contf: "continuous_map X Y f" and fim: "f ` topspace X = topspace Y"
+ shows "open_map Y Z g"
+ unfolding open_map_def
+proof (intro strip)
+ fix U assume "openin Y U"
+ then have "openin X {x \<in> topspace X. f x \<in> U}"
+ using contf openin_continuous_map_preimage by blast
+ then have "openin Z ((g \<circ> f) ` {x \<in> topspace X. f x \<in> U})"
+ using cmf open_map_def by blast
+ moreover
+ have "\<And>y. y \<in> U \<Longrightarrow> \<exists>x \<in> topspace X. f x \<in> U \<and> g y = g (f x)"
+ by (smt (verit, ccfv_SIG) \<open>openin Y U\<close> openin_subset fim image_iff subsetD)
+ then have "(g \<circ> f) ` {x \<in> topspace X. f x \<in> U} = g`U" by auto
+ ultimately show "openin Z (g ` U)"
+ by metis
+qed
+
+lemma closed_map_from_composition_right:
+ assumes cmf: "closed_map X Z (g \<circ> f)" "f ` topspace X \<subseteq> topspace Y" "continuous_map Y Z g" "inj_on g (topspace Y)"
+ shows "closed_map X Y f"
+ unfolding closed_map_def
+proof (intro strip)
+ fix C assume "closedin X C"
+ have "\<And>y c. \<lbrakk>y \<in> topspace Y; g y = g (f c); c \<in> C\<rbrakk> \<Longrightarrow> y \<in> f ` C"
+ using \<open>closedin X C\<close> assms closedin_subset inj_onD by fastforce
+ then
+ have "f ` C = {x \<in> topspace Y. g x \<in> (g \<circ> f) ` C}"
+ using \<open>closedin X C\<close> assms(2) closedin_subset by fastforce
+ moreover have "closedin Z ((g \<circ> f) ` C)"
+ using \<open>closedin X C\<close> cmf closed_map_def by blast
+ ultimately show "closedin Y (f ` C)"
+ using assms(3) closedin_continuous_map_preimage by fastforce
+qed
+
+text \<open>identical proof as the above\<close>
+lemma open_map_from_composition_right:
+ assumes "open_map X Z (g \<circ> f)" "f ` topspace X \<subseteq> topspace Y" "continuous_map Y Z g" "inj_on g (topspace Y)"
+ shows "open_map X Y f"
+ unfolding open_map_def
+proof (intro strip)
+ fix C assume "openin X C"
+ have "\<And>y c. \<lbrakk>y \<in> topspace Y; g y = g (f c); c \<in> C\<rbrakk> \<Longrightarrow> y \<in> f ` C"
+ using \<open>openin X C\<close> assms openin_subset inj_onD by fastforce
+ then
+ have "f ` C = {x \<in> topspace Y. g x \<in> (g \<circ> f) ` C}"
+ using \<open>openin X C\<close> assms(2) openin_subset by fastforce
+ moreover have "openin Z ((g \<circ> f) ` C)"
+ using \<open>openin X C\<close> assms(1) open_map_def by blast
+ ultimately show "openin Y (f ` C)"
+ using assms(3) openin_continuous_map_preimage by fastforce
+qed
+
subsection\<open>Quotient maps\<close>
definition quotient_map where
@@ -2163,6 +2411,84 @@
qed
qed
+lemma quotient_map_saturated_closed:
+ "quotient_map X Y f \<longleftrightarrow>
+ continuous_map X Y f \<and> f ` (topspace X) = topspace Y \<and>
+ (\<forall>U. closedin X U \<and> {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U \<longrightarrow> closedin Y (f ` U))"
+ (is "?lhs = ?rhs")
+proof
+ assume L: ?lhs
+ then obtain fim: "f ` topspace X = topspace Y"
+ and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> closedin Y U = closedin X {x \<in> topspace X. f x \<in> U}"
+ by (simp add: quotient_map_closedin)
+ show ?rhs
+ proof (intro conjI allI impI)
+ show "continuous_map X Y f"
+ by (simp add: L quotient_imp_continuous_map)
+ show "f ` topspace X = topspace Y"
+ by (simp add: fim)
+ next
+ fix U :: "'a set"
+ assume U: "closedin X U \<and> {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U"
+ then have sub: "f ` U \<subseteq> topspace Y" and eq: "{x \<in> topspace X. f x \<in> f ` U} = U"
+ using fim closedin_subset by fastforce+
+ show "closedin Y (f ` U)"
+ by (simp add: sub Y eq U)
+ qed
+next
+ assume ?rhs
+ then obtain YX: "\<And>U. closedin Y U \<Longrightarrow> closedin X {x \<in> topspace X. f x \<in> U}"
+ and fim: "f ` topspace X = topspace Y"
+ and XY: "\<And>U. \<lbrakk>closedin X U; {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U\<rbrakk> \<Longrightarrow> closedin Y (f ` U)"
+ by (simp add: continuous_map_closedin)
+ show ?lhs
+ proof (simp add: quotient_map_closedin fim, intro allI impI iffI)
+ fix U :: "'b set"
+ assume "U \<subseteq> topspace Y" and X: "closedin X {x \<in> topspace X. f x \<in> U}"
+ have feq: "f ` {x \<in> topspace X. f x \<in> U} = U"
+ using \<open>U \<subseteq> topspace Y\<close> fim by auto
+ show "closedin Y U"
+ using XY [OF X] by (simp add: feq)
+ next
+ fix U :: "'b set"
+ assume "U \<subseteq> topspace Y" and Y: "closedin Y U"
+ show "closedin X {x \<in> topspace X. f x \<in> U}"
+ by (metis YX [OF Y])
+ qed
+qed
+
+lemma quotient_map_onto_image:
+ assumes "f ` topspace X \<subseteq> topspace Y" and U: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U} = openin Y U"
+ shows "quotient_map X (subtopology Y (f ` topspace X)) f"
+ unfolding quotient_map_def topspace_subtopology
+proof (intro conjI strip)
+ fix U
+ assume "U \<subseteq> topspace Y \<inter> f ` topspace X"
+ with U have "openin X {x \<in> topspace X. f x \<in> U} \<Longrightarrow> \<exists>x. openin Y x \<and> U = f ` topspace X \<inter> x"
+ by fastforce
+ moreover have "\<exists>x. openin Y x \<and> U = f ` topspace X \<inter> x \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U}"
+ by (metis (mono_tags, lifting) Collect_cong IntE IntI U image_eqI openin_subset)
+ ultimately show "openin X {x \<in> topspace X. f x \<in> U} = openin (subtopology Y (f ` topspace X)) U"
+ by (force simp: openin_subtopology_alt image_iff)
+qed (use assms in auto)
+
+lemma quotient_map_lift_exists:
+ assumes f: "quotient_map X Y f" and h: "continuous_map X Z h"
+ and "\<And>x y. \<lbrakk>x \<in> topspace X; y \<in> topspace X; f x = f y\<rbrakk> \<Longrightarrow> h x = h y"
+ obtains g where "continuous_map Y Z g" "g ` topspace Y = h ` topspace X"
+ "\<And>x. x \<in> topspace X \<Longrightarrow> g(f x) = h x"
+proof -
+ obtain g where g: "\<And>x. x \<in> topspace X \<Longrightarrow> h x = g(f x)"
+ using function_factors_left_gen[of "\<lambda>x. x \<in> topspace X" f h] assms by blast
+ show ?thesis
+ proof
+ show "g ` topspace Y = h ` topspace X"
+ using f g by (force dest!: quotient_imp_surjective_map)
+ show "continuous_map Y Z g"
+ by (smt (verit) f g h continuous_compose_quotient_map_eq continuous_map_eq o_def)
+ qed (simp add: g)
+qed
+
subsection\<open> Separated Sets\<close>
definition separatedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
@@ -2257,6 +2583,11 @@
unfolding openin_closedin_eq topspace_subtopology separation_closedin_Un_gen disjnt_def
by (auto simp: Diff_triv Int_commute Un_Diff inf_absorb1 topspace_def)
+lemma separatedin_full:
+ "S \<union> T = topspace X
+ \<Longrightarrow> separatedin X S T \<longleftrightarrow> disjnt S T \<and> closedin X S \<and> openin X S \<and> closedin X T \<and> openin X T"
+ by (metis separatedin_open_sets separation_closedin_Un_gen separation_openin_Un_gen subtopology_topspace)
+
subsection\<open>Homeomorphisms\<close>
text\<open>(1-way and 2-way versions may be useful in places)\<close>
@@ -2778,6 +3109,10 @@
by (intro conj_cong arg_cong [where f=Not] ex_cong1; blast dest!: openin_subset)
qed
+lemma connectedinD:
+ "\<lbrakk>connectedin X S; openin X E1; openin X E2; S \<subseteq> E1 \<union> E2; E1 \<inter> E2 \<inter> S = {}; E1 \<inter> S \<noteq> {}; E2 \<inter> S \<noteq> {}\<rbrakk> \<Longrightarrow> False"
+ by (meson connectedin)
+
lemma connectedin_iff_connected [simp]: "connectedin euclidean S \<longleftrightarrow> connected S"
by (simp add: connected_def connectedin)
@@ -3080,7 +3415,7 @@
moreover have "connectedin (discrete_topology U) S \<longleftrightarrow> (\<exists>a. S = {a})"
proof
show "connectedin (discrete_topology U) S \<Longrightarrow> \<exists>a. S = {a}"
- using False connectedin_inter_frontier_of insert_Diff by fastforce
+ using False connectedin_Int_frontier_of insert_Diff by fastforce
qed (use True in auto)
ultimately show ?thesis
by auto
@@ -3568,6 +3903,10 @@
unfolding closed_map_def
by (auto simp: closedin_closed_subtopology embedding_map_def homeomorphic_map_closedness_eq)
+lemma embedding_imp_closed_map_eq:
+ "embedding_map X Y f \<Longrightarrow> (closed_map X Y f \<longleftrightarrow> closedin Y (f ` topspace X))"
+ using closed_map_def embedding_imp_closed_map by blast
+
subsection\<open>Retraction and section maps\<close>
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue May 02 15:17:39 2023 +0100
@@ -1716,6 +1716,11 @@
shows "connected S \<longleftrightarrow> convex S"
by (metis is_interval_convex convex_connected is_interval_connected_1)
+lemma connected_space_iff_is_interval_1 [iff]:
+ fixes S :: "real set"
+ shows "connected_space (top_of_set S) \<longleftrightarrow> is_interval S"
+ using connectedin_topspace is_interval_connected_1 by force
+
lemma connected_convex_1_gen:
fixes S :: "'a :: euclidean_space set"
assumes "DIM('a) = 1"
--- a/src/HOL/Analysis/Further_Topology.thy Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy Tue May 02 15:17:39 2023 +0100
@@ -969,9 +969,6 @@
subsection\<open> Special cases and corollaries involving spheres\<close>
-lemma disjnt_Diff1: "X \<subseteq> Y' \<Longrightarrow> disjnt (X - Y) (X' - Y')"
- by (auto simp: disjnt_def)
-
proposition extend_map_affine_to_sphere_cofinite_simple:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "compact S" "convex U" "bounded U"
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Tue May 02 15:17:39 2023 +0100
@@ -2,7 +2,7 @@
theory Ordered_Euclidean_Space
imports
- Convex_Euclidean_Space
+ Convex_Euclidean_Space Abstract_Limits
"HOL-Library.Product_Order"
begin
@@ -157,6 +157,32 @@
shows "((\<lambda>i. inf (X i) (Y i)) \<longlongrightarrow> inf x y) net"
unfolding inf_min eucl_inf by (intro assms tendsto_intros)
+lemma tendsto_Inf:
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::ordered_euclidean_space"
+ assumes "finite K" "\<And>i. i \<in> K \<Longrightarrow> ((\<lambda>x. f x i) \<longlongrightarrow> l i) F"
+ shows "((\<lambda>x. Inf (f x ` K)) \<longlongrightarrow> Inf (l ` K)) F"
+ using assms
+ by (induction K rule: finite_induct) (auto simp: cInf_insert_If tendsto_inf)
+
+lemma tendsto_Sup:
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::ordered_euclidean_space"
+ assumes "finite K" "\<And>i. i \<in> K \<Longrightarrow> ((\<lambda>x. f x i) \<longlongrightarrow> l i) F"
+ shows "((\<lambda>x. Sup (f x ` K)) \<longlongrightarrow> Sup (l ` K)) F"
+ using assms
+ by (induction K rule: finite_induct) (auto simp: cSup_insert_If tendsto_sup)
+
+lemma continuous_map_Inf:
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::ordered_euclidean_space"
+ assumes "finite K" "\<And>i. i \<in> K \<Longrightarrow> continuous_map X euclidean (\<lambda>x. f x i)"
+ shows "continuous_map X euclidean (\<lambda>x. INF i\<in>K. f x i)"
+ using assms by (simp add: continuous_map_atin tendsto_Inf)
+
+lemma continuous_map_Sup:
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::ordered_euclidean_space"
+ assumes "finite K" "\<And>i. i \<in> K \<Longrightarrow> continuous_map X euclidean (\<lambda>x. f x i)"
+ shows "continuous_map X euclidean (\<lambda>x. SUP i\<in>K. f x i)"
+ using assms by (simp add: continuous_map_atin tendsto_Sup)
+
lemma tendsto_componentwise_max:
assumes f: "(f \<longlongrightarrow> l) F" and g: "(g \<longlongrightarrow> m) F"
shows "((\<lambda>x. (\<Sum>i\<in>Basis. max (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i)) \<longlongrightarrow> (\<Sum>i\<in>Basis. max (l \<bullet> i) (m \<bullet> i) *\<^sub>R i)) F"
@@ -167,10 +193,6 @@
shows "((\<lambda>x. (\<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i)) \<longlongrightarrow> (\<Sum>i\<in>Basis. min (l \<bullet> i) (m \<bullet> i) *\<^sub>R i)) F"
by (intro tendsto_intros assms)
-lemma (in order) atLeastatMost_empty'[simp]:
- "(\<not> a \<le> b) \<Longrightarrow> {a..b} = {}"
- by (auto)
-
instance real :: ordered_euclidean_space
by standard auto
--- a/src/HOL/Analysis/Product_Topology.thy Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Analysis/Product_Topology.thy Tue May 02 15:17:39 2023 +0100
@@ -464,6 +464,10 @@
"homeomorphic_map (prod_topology X Y) (prod_topology Y X) (\<lambda>(x,y). (y,x))"
using homeomorphic_map_maps homeomorphic_maps_swap by metis
+lemma homeomorphic_space_prod_topology_swap:
+ "(prod_topology X Y) homeomorphic_space (prod_topology Y X)"
+ using homeomorphic_map_swap homeomorphic_space by blast
+
lemma embedding_map_graph:
"embedding_map X (prod_topology X Y) (\<lambda>x. (x, f x)) \<longleftrightarrow> continuous_map X Y f"
(is "?lhs = ?rhs")
@@ -472,8 +476,7 @@
have "snd \<circ> (\<lambda>x. (x, f x)) = f"
by force
moreover have "continuous_map X Y (snd \<circ> (\<lambda>x. (x, f x)))"
- using L
- unfolding embedding_map_def
+ using L unfolding embedding_map_def
by (meson continuous_map_in_subtopology continuous_map_snd_of homeomorphic_imp_continuous_map)
ultimately show ?rhs
by simp
--- a/src/HOL/Analysis/T1_Spaces.thy Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Analysis/T1_Spaces.thy Tue May 02 15:17:39 2023 +0100
@@ -380,8 +380,7 @@
lemma Hausdorff_space_discrete_topology [simp]:
"Hausdorff_space (discrete_topology U)"
unfolding Hausdorff_space_def
- apply safe
- by (metis discrete_topology_unique_alt disjnt_empty2 disjnt_insert2 insert_iff mk_disjoint_insert topspace_discrete_topology)
+ by (metis Hausdorff_space_compact_sets Hausdorff_space_def compactin_discrete_topology equalityE openin_discrete_topology)
lemma compactin_Int:
"\<lbrakk>Hausdorff_space X; compactin X S; compactin X T\<rbrakk> \<Longrightarrow> compactin X (S \<inter> T)"
@@ -395,6 +394,10 @@
"\<lbrakk>Hausdorff_space X; finite S\<rbrakk> \<Longrightarrow> X derived_set_of S = {}"
using Hausdorff_imp_t1_space t1_space_derived_set_of_finite by auto
+lemma infinite_perfect_set:
+ "\<lbrakk>Hausdorff_space X; S \<subseteq> X derived_set_of S; S \<noteq> {}\<rbrakk> \<Longrightarrow> infinite S"
+ using derived_set_of_finite by blast
+
lemma derived_set_of_singleton:
"Hausdorff_space X \<Longrightarrow> X derived_set_of {x} = {}"
by (simp add: derived_set_of_finite)
@@ -698,4 +701,47 @@
qed
qed
+lemma Hausdorff_space_closed_neighbourhood:
+ "Hausdorff_space X \<longleftrightarrow>
+ (\<forall>x \<in> topspace X. \<exists>U C. openin X U \<and> closedin X C \<and>
+ Hausdorff_space(subtopology X C) \<and> x \<in> U \<and> U \<subseteq> C)" (is "_ = ?rhs")
+proof
+ assume R: ?rhs
+ show "Hausdorff_space X"
+ unfolding Hausdorff_space_def
+ proof clarify
+ fix x y
+ assume x: "x \<in> topspace X" and y: "y \<in> topspace X" and "x \<noteq> y"
+ obtain T C where *: "openin X T" "closedin X C" "x \<in> T" "T \<subseteq> C"
+ and C: "Hausdorff_space (subtopology X C)"
+ by (meson R \<open>x \<in> topspace X\<close>)
+ show "\<exists>U V. openin X U \<and> openin X V \<and> x \<in> U \<and> y \<in> V \<and> disjnt U V"
+ proof (cases "y \<in> C")
+ case True
+ with * C obtain U V where U: "openin (subtopology X C) U"
+ and V: "openin (subtopology X C) V"
+ and "x \<in> U" "y \<in> V" "disjnt U V"
+ unfolding Hausdorff_space_def
+ by (smt (verit, best) \<open>x \<noteq> y\<close> closedin_subset subsetD topspace_subtopology_subset)
+ then obtain U' V' where UV': "U = U' \<inter> C" "openin X U'" "V = V' \<inter> C" "openin X V'"
+ by (meson openin_subtopology)
+ have "disjnt (T \<inter> U') V'"
+ using \<open>disjnt U V\<close> UV' \<open>T \<subseteq> C\<close> by (force simp: disjnt_iff)
+ with \<open>T \<subseteq> C\<close> have "disjnt (T \<inter> U') (V' \<union> (topspace X - C))"
+ unfolding disjnt_def by blast
+ moreover
+ have "openin X (T \<inter> U')"
+ by (simp add: \<open>openin X T\<close> \<open>openin X U'\<close> openin_Int)
+ moreover have "openin X (V' \<union> (topspace X - C))"
+ using \<open>closedin X C\<close> \<open>openin X V'\<close> by auto
+ ultimately show ?thesis
+ using UV' \<open>x \<in> T\<close> \<open>x \<in> U\<close> \<open>y \<in> V\<close> by blast
+ next
+ case False
+ with * y show ?thesis
+ by (force simp: closedin_def disjnt_def)
+ qed
+ qed
+qed fastforce
+
end
--- a/src/HOL/Library/Set_Idioms.thy Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Library/Set_Idioms.thy Tue May 02 15:17:39 2023 +0100
@@ -557,4 +557,162 @@
by blast
qed
+lemma countable_union_of_empty [simp]: "(countable union_of P) {}"
+ by (simp add: union_of_empty)
+
+lemma countable_intersection_of_empty [simp]: "(countable intersection_of P) UNIV"
+ by (simp add: intersection_of_empty)
+
+lemma countable_union_of_inc: "P S \<Longrightarrow> (countable union_of P) S"
+ by (simp add: union_of_inc)
+
+lemma countable_intersection_of_inc: "P S \<Longrightarrow> (countable intersection_of P) S"
+ by (simp add: intersection_of_inc)
+
+lemma countable_union_of_complement:
+ "(countable union_of P) S \<longleftrightarrow> (countable intersection_of (\<lambda>S. P(-S))) (-S)"
+ (is "?lhs=?rhs")
+proof
+ assume ?lhs
+ then obtain \<U> where "countable \<U>" and \<U>: "\<U> \<subseteq> Collect P" "\<Union>\<U> = S"
+ by (metis union_of_def)
+ define \<U>' where "\<U>' \<equiv> (\<lambda>C. -C) ` \<U>"
+ have "\<U>' \<subseteq> {S. P (- S)}" "\<Inter>\<U>' = -S"
+ using \<U>'_def \<U> by auto
+ then show ?rhs
+ unfolding intersection_of_def by (metis \<U>'_def \<open>countable \<U>\<close> countable_image)
+next
+ assume ?rhs
+ then obtain \<U> where "countable \<U>" and \<U>: "\<U> \<subseteq> {S. P (- S)}" "\<Inter>\<U> = -S"
+ by (metis intersection_of_def)
+ define \<U>' where "\<U>' \<equiv> (\<lambda>C. -C) ` \<U>"
+ have "\<U>' \<subseteq> Collect P" "\<Union> \<U>' = S"
+ using \<U>'_def \<U> by auto
+ then show ?lhs
+ unfolding union_of_def
+ by (metis \<U>'_def \<open>countable \<U>\<close> countable_image)
+qed
+
+lemma countable_intersection_of_complement:
+ "(countable intersection_of P) S \<longleftrightarrow> (countable union_of (\<lambda>S. P(- S))) (- S)"
+ by (simp add: countable_union_of_complement)
+
+lemma countable_union_of_explicit:
+ assumes "P {}"
+ shows "(countable union_of P) S \<longleftrightarrow>
+ (\<exists>T. (\<forall>n::nat. P(T n)) \<and> \<Union>(range T) = S)" (is "?lhs=?rhs")
+proof
+ assume ?lhs
+ then obtain \<U> where "countable \<U>" and \<U>: "\<U> \<subseteq> Collect P" "\<Union>\<U> = S"
+ by (metis union_of_def)
+ then show ?rhs
+ by (metis SUP_bot Sup_empty assms from_nat_into mem_Collect_eq range_from_nat_into subsetD)
+next
+ assume ?rhs
+ then show ?lhs
+ by (metis countableI_type countable_image image_subset_iff mem_Collect_eq union_of_def)
+qed
+
+lemma countable_union_of_ascending:
+ assumes empty: "P {}" and Un: "\<And>T U. \<lbrakk>P T; P U\<rbrakk> \<Longrightarrow> P(T \<union> U)"
+ shows "(countable union_of P) S \<longleftrightarrow>
+ (\<exists>T. (\<forall>n. P(T n)) \<and> (\<forall>n. T n \<subseteq> T(Suc n)) \<and> \<Union>(range T) = S)" (is "?lhs=?rhs")
+proof
+ assume ?lhs
+ then obtain T where T: "\<And>n::nat. P(T n)" "\<Union>(range T) = S"
+ by (meson empty countable_union_of_explicit)
+ have "P (\<Union> (T ` {..n}))" for n
+ by (induction n) (auto simp: atMost_Suc Un T)
+ with T show ?rhs
+ by (rule_tac x="\<lambda>n. \<Union>k\<le>n. T k" in exI) force
+next
+ assume ?rhs
+ then show ?lhs
+ using empty countable_union_of_explicit by auto
+qed
+
+lemma countable_union_of_idem [simp]:
+ "countable union_of countable union_of P = countable union_of P" (is "?lhs=?rhs")
+proof
+ fix S
+ show "(countable union_of countable union_of P) S = (countable union_of P) S"
+ proof
+ assume L: "?lhs S"
+ then obtain \<U> where "countable \<U>" and \<U>: "\<U> \<subseteq> Collect (countable union_of P)" "\<Union>\<U> = S"
+ by (metis union_of_def)
+ then have "\<forall>U \<in> \<U>. \<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> Collect P \<and> U = \<Union>\<V>"
+ by (metis Ball_Collect union_of_def)
+ then obtain \<F> where \<F>: "\<forall>U \<in> \<U>. countable (\<F> U) \<and> \<F> U \<subseteq> Collect P \<and> U = \<Union>(\<F> U)"
+ by metis
+ have "countable (\<Union> (\<F> ` \<U>))"
+ using \<F> \<open>countable \<U>\<close> by blast
+ moreover have "\<Union> (\<F> ` \<U>) \<subseteq> Collect P"
+ by (simp add: Sup_le_iff \<F>)
+ moreover have "\<Union> (\<Union> (\<F> ` \<U>)) = S"
+ by auto (metis Union_iff \<F> \<U>(2))+
+ ultimately show "?rhs S"
+ by (meson union_of_def)
+ qed (simp add: countable_union_of_inc)
+qed
+
+lemma countable_intersection_of_idem [simp]:
+ "countable intersection_of countable intersection_of P =
+ countable intersection_of P"
+ by (force simp: countable_intersection_of_complement)
+
+lemma countable_union_of_Union:
+ "\<lbrakk>countable \<U>; \<And>S. S \<in> \<U> \<Longrightarrow> (countable union_of P) S\<rbrakk>
+ \<Longrightarrow> (countable union_of P) (\<Union> \<U>)"
+ by (metis Ball_Collect countable_union_of_idem union_of_def)
+
+lemma countable_union_of_UN:
+ "\<lbrakk>countable I; \<And>i. i \<in> I \<Longrightarrow> (countable union_of P) (U i)\<rbrakk>
+ \<Longrightarrow> (countable union_of P) (\<Union>i\<in>I. U i)"
+ by (metis (mono_tags, lifting) countable_image countable_union_of_Union imageE)
+
+lemma countable_union_of_Un:
+ "\<lbrakk>(countable union_of P) S; (countable union_of P) T\<rbrakk>
+ \<Longrightarrow> (countable union_of P) (S \<union> T)"
+ by (smt (verit) Union_Un_distrib countable_Un le_sup_iff union_of_def)
+
+lemma countable_intersection_of_Inter:
+ "\<lbrakk>countable \<U>; \<And>S. S \<in> \<U> \<Longrightarrow> (countable intersection_of P) S\<rbrakk>
+ \<Longrightarrow> (countable intersection_of P) (\<Inter> \<U>)"
+ by (metis countable_intersection_of_idem intersection_of_def mem_Collect_eq subsetI)
+
+lemma countable_intersection_of_INT:
+ "\<lbrakk>countable I; \<And>i. i \<in> I \<Longrightarrow> (countable intersection_of P) (U i)\<rbrakk>
+ \<Longrightarrow> (countable intersection_of P) (\<Inter>i\<in>I. U i)"
+ by (metis (mono_tags, lifting) countable_image countable_intersection_of_Inter imageE)
+
+lemma countable_intersection_of_inter:
+ "\<lbrakk>(countable intersection_of P) S; (countable intersection_of P) T\<rbrakk>
+ \<Longrightarrow> (countable intersection_of P) (S \<inter> T)"
+ by (simp add: countable_intersection_of_complement countable_union_of_Un)
+
+lemma countable_union_of_Int:
+ assumes S: "(countable union_of P) S" and T: "(countable union_of P) T"
+ and Int: "\<And>S T. P S \<and> P T \<Longrightarrow> P(S \<inter> T)"
+ shows "(countable union_of P) (S \<inter> T)"
+proof -
+ obtain \<U> where "countable \<U>" and \<U>: "\<U> \<subseteq> Collect P" "\<Union>\<U> = S"
+ using S by (metis union_of_def)
+ obtain \<V> where "countable \<V>" and \<V>: "\<V> \<subseteq> Collect P" "\<Union>\<V> = T"
+ using T by (metis union_of_def)
+ have "\<And>U V. \<lbrakk>U \<in> \<U>; V \<in> \<V>\<rbrakk> \<Longrightarrow> (countable union_of P) (U \<inter> V)"
+ using \<U> \<V> by (metis Ball_Collect countable_union_of_inc local.Int)
+ then have "(countable union_of P) (\<Union>U\<in>\<U>. \<Union>V\<in>\<V>. U \<inter> V)"
+ by (meson \<open>countable \<U>\<close> \<open>countable \<V>\<close> countable_union_of_UN)
+ moreover have "S \<inter> T = (\<Union>U\<in>\<U>. \<Union>V\<in>\<V>. U \<inter> V)"
+ by (simp add: \<U> \<V>)
+ ultimately show ?thesis
+ by presburger
+qed
+
+lemma countable_intersection_of_union:
+ assumes S: "(countable intersection_of P) S" and T: "(countable intersection_of P) T"
+ and Un: "\<And>S T. P S \<and> P T \<Longrightarrow> P(S \<union> T)"
+ shows "(countable intersection_of P) (S \<union> T)"
+ by (metis (mono_tags, lifting) Compl_Int S T Un compl_sup countable_intersection_of_complement countable_union_of_Int)
+
end
--- a/src/HOL/Set.thy Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Set.thy Tue May 02 15:17:39 2023 +0100
@@ -1946,6 +1946,9 @@
lemma disjnt_Un2 [simp]: "disjnt C (A \<union> B) \<longleftrightarrow> disjnt C A \<and> disjnt C B"
by (auto simp: disjnt_def)
+lemma disjnt_Diff1: "disjnt (X-Y) (U-V)" and disjnt_Diff2: "disjnt (U-V) (X-Y)" if "X \<subseteq> V"
+ using that by (auto simp: disjnt_def)
+
lemma disjoint_image_subset: "\<lbrakk>pairwise disjnt \<A>; \<And>X. X \<in> \<A> \<Longrightarrow> f X \<subseteq> X\<rbrakk> \<Longrightarrow> pairwise disjnt (f `\<A>)"
unfolding disjnt_def pairwise_def by fast
--- a/src/HOL/Set_Interval.thy Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Set_Interval.thy Tue May 02 15:17:39 2023 +0100
@@ -280,8 +280,8 @@
context order
begin
-lemma atLeastatMost_empty[simp]:
- "b < a \<Longrightarrow> {a..b} = {}"
+lemma atLeastatMost_empty[simp]: "b < a \<Longrightarrow> {a..b} = {}"
+ and atLeastatMost_empty'[simp]: "\<not> a \<le> b \<Longrightarrow> {a..b} = {}"
by(auto simp: atLeastAtMost_def atLeast_def atMost_def)
lemma atLeastLessThan_empty[simp]: