--- a/src/HOL/Analysis/Abstract_Limits.thy Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Analysis/Abstract_Limits.thy Wed May 03 10:35:20 2023 +0100
@@ -47,6 +47,9 @@
definition limitin :: "'a topology \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" where
"limitin X f l F \<equiv> l \<in> topspace X \<and> (\<forall>U. openin X U \<and> l \<in> U \<longrightarrow> eventually (\<lambda>x. f x \<in> U) F)"
+lemma limitinD: "\<lbrakk>limitin X f l F; openin X U; l \<in> U\<rbrakk> \<Longrightarrow> eventually (\<lambda>x. f x \<in> U) F"
+ by (simp add: limitin_def)
+
lemma limitin_canonical_iff [simp]: "limitin euclidean f l F \<longleftrightarrow> (f \<longlongrightarrow> l) F"
by (auto simp: limitin_def tendsto_def)
--- a/src/HOL/Analysis/Abstract_Topology.thy Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Analysis/Abstract_Topology.thy Wed May 03 10:35:20 2023 +0100
@@ -174,6 +174,18 @@
shows "closedin U (S - T)"
by (metis Int_Diff cT closedin_Int closedin_subset inf.orderE oS openin_closedin_eq)
+lemma all_openin: "(\<forall>U. openin X U \<longrightarrow> P U) \<longleftrightarrow> (\<forall>U. closedin X U \<longrightarrow> P (topspace X - U))"
+ by (metis Diff_Diff_Int closedin_def inf.absorb_iff2 openin_closedin_eq)
+
+lemma all_closedin: "(\<forall>U. closedin X U \<longrightarrow> P U) \<longleftrightarrow> (\<forall>U. openin X U \<longrightarrow> P (topspace X - U))"
+ by (metis Diff_Diff_Int closedin_subset inf.absorb_iff2 openin_closedin_eq)
+
+lemma ex_openin: "(\<exists>U. openin X U \<and> P U) \<longleftrightarrow> (\<exists>U. closedin X U \<and> P (topspace X - U))"
+ by (metis Diff_Diff_Int closedin_def inf.absorb_iff2 openin_closedin_eq)
+
+lemma ex_closedin: "(\<exists>U. closedin X U \<and> P U) \<longleftrightarrow> (\<exists>U. openin X U \<and> P (topspace X - U))"
+ by (metis Diff_Diff_Int closedin_subset inf.absorb_iff2 openin_closedin_eq)
+
subsection\<open>The discrete topology\<close>
@@ -285,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)
@@ -1371,7 +1387,7 @@
by (metis (mono_tags) closedin_closure_of closedin_locally_finite_Union imageE locally_finite_in_closure)
lemma closure_of_Union_subset: "\<Union>((\<lambda>S. X closure_of S) ` \<A>) \<subseteq> X closure_of (\<Union>\<A>)"
- by clarify (meson Union_upper closure_of_mono subsetD)
+ by (simp add: SUP_le_iff Sup_upper closure_of_mono)
lemma closure_of_locally_finite_Union:
assumes "locally_finite_in X \<A>"
@@ -1867,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
@@ -2151,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"
@@ -2245,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>
@@ -2766,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)
@@ -2966,7 +3313,7 @@
by (metis closure_of_eq)
qed
-lemma connectedin_inter_frontier_of:
+lemma connectedin_Int_frontier_of:
assumes "connectedin X S" "S \<inter> T \<noteq> {}" "S - T \<noteq> {}"
shows "S \<inter> X frontier_of T \<noteq> {}"
proof -
@@ -3068,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
@@ -3360,7 +3707,7 @@
corollary compact_space_imp_nest:
fixes C :: "nat \<Rightarrow> 'a set"
assumes "compact_space X" and clo: "\<And>n. closedin X (C n)"
- and ne: "\<And>n. C n \<noteq> {}" and inc: "\<And>m n. m \<le> n \<Longrightarrow> C n \<subseteq> C m"
+ and ne: "\<And>n. C n \<noteq> {}" and dec: "decseq C"
shows "(\<Inter>n. C n) \<noteq> {}"
proof -
let ?\<U> = "range (\<lambda>n. \<Inter>m \<le> n. C m)"
@@ -3370,8 +3717,8 @@
proof -
obtain n where "\<And>k. k \<in> K \<Longrightarrow> k \<le> n"
using Max.coboundedI \<open>finite K\<close> by blast
- with inc have "C n \<subseteq> (\<Inter>n\<in>K. \<Inter>m \<le> n. C m)"
- by blast
+ with dec have "C n \<subseteq> (\<Inter>n\<in>K. \<Inter>m \<le> n. C m)"
+ unfolding decseq_def by blast
with ne [of n] show ?thesis
by blast
qed
@@ -3556,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/Abstract_Topology_2.thy Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy Wed May 03 10:35:20 2023 +0100
@@ -1138,6 +1138,20 @@
by (force simp: retract_of_space_def)
qed
+lemma retract_of_space_trans:
+ assumes "S retract_of_space X" "T retract_of_space subtopology X S"
+ shows "T retract_of_space X"
+ using assms
+ apply (simp add: retract_of_space_retraction_maps)
+ by (metis id_comp inf.absorb_iff2 retraction_maps_compose subtopology_subtopology)
+
+lemma retract_of_space_subtopology:
+ assumes "S retract_of_space X" "S \<subseteq> U"
+ shows "S retract_of_space subtopology X U"
+ using assms
+ apply (clarsimp simp: retract_of_space_def)
+ by (metis continuous_map_from_subtopology inf.absorb2 subtopology_subtopology)
+
lemma retract_of_space_clopen:
assumes "openin X S" "closedin X S" "S = {} \<Longrightarrow> topspace X = {}"
shows "S retract_of_space X"
@@ -1194,6 +1208,13 @@
using embedding_map_imp_homeomorphic_space homeomorphic_space_sym section_imp_embedding_map
section_map_def by blast
+lemma hereditary_imp_retractive_property:
+ assumes "\<And>X S. P X \<Longrightarrow> P(subtopology X S)"
+ "\<And>X X'. X homeomorphic_space X' \<Longrightarrow> (P X \<longleftrightarrow> Q X')"
+ assumes "retraction_map X X' r" "P X"
+ shows "Q X'"
+ by (meson assms retraction_map_def retraction_maps_section_image2)
+
subsection\<open>Paths and path-connectedness\<close>
definition pathin :: "'a topology \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool" where
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed May 03 10:35:20 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 08:39:48 2023 +0000
+++ b/src/HOL/Analysis/Further_Topology.thy Wed May 03 10:35:20 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/Homotopy.thy Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Analysis/Homotopy.thy Wed May 03 10:35:20 2023 +0100
@@ -156,7 +156,7 @@
qed
show ?thesis
using assms
- apply (clarsimp simp add: homotopic_with_def)
+ apply (clarsimp simp: homotopic_with_def)
subgoal for h
by (rule_tac x="h \<circ> (\<lambda>y. (1 - fst y, snd y))" in exI) (simp add: continuous_map_compose [OF *])
done
@@ -211,7 +211,7 @@
show "\<forall>t\<in>{0..1}. P (\<lambda>x. k (t, x))"
proof
fix t show "t\<in>{0..1} \<Longrightarrow> P (\<lambda>x. k (t, x))"
- by (cases "t \<le> 1/2") (auto simp add: k_def P)
+ by (cases "t \<le> 1/2") (auto simp: k_def P)
qed
qed
qed
@@ -578,7 +578,7 @@
proposition homotopic_paths_join:
"\<lbrakk>homotopic_paths S p p'; homotopic_paths S q q'; pathfinish p = pathstart q\<rbrakk> \<Longrightarrow> homotopic_paths S (p +++ q) (p' +++ q')"
- apply (clarsimp simp add: homotopic_paths_def homotopic_with_def)
+ apply (clarsimp simp: homotopic_paths_def homotopic_with_def)
apply (rename_tac k1 k2)
apply (rule_tac x="(\<lambda>y. ((k1 \<circ> Pair (fst y)) +++ (k2 \<circ> Pair (fst y))) (snd y))" in exI)
apply (intro conjI continuous_intros continuous_on_homotopic_join_lemma; force simp: joinpaths_def pathstart_def pathfinish_def path_image_def)
@@ -639,8 +639,8 @@
show "continuous_on {x \<in> ?A. snd x \<le> 1/2} (\<lambda>t. p (fst t * (2 * snd t)))"
"continuous_on {x \<in> ?A. 1/2 \<le> snd x} (\<lambda>t. p (fst t * (1 - (2 * snd t - 1))))"
"continuous_on ?A snd"
- by (intro continuous_on_compose2 [OF p] continuous_intros; auto simp add: mult_le_one)+
- qed (auto simp add: algebra_simps)
+ by (intro continuous_on_compose2 [OF p] continuous_intros; auto simp: mult_le_one)+
+ qed (auto simp: algebra_simps)
then show ?thesis
using assms
apply (subst homotopic_paths_sym_eq)
@@ -1004,7 +1004,7 @@
by (force simp: field_simps not_le mult_left_mono affine_ineq dest!: 1 2)
show "(subpath u v g +++ subpath v w g) t = subpath u w g (?f t)" if "t \<in> {0..1}" for t
using assms
- unfolding joinpaths_def subpath_def by (auto simp add: divide_simps add.commute mult.commute mult.left_commute)
+ unfolding joinpaths_def subpath_def by (auto simp: divide_simps add.commute mult.commute mult.left_commute)
qed (use False in auto)
qed
then show ?thesis
@@ -1062,26 +1062,24 @@
then have "continuous_on ({0..1} \<times> {0..1}) (g \<circ> fst)"
by (fastforce intro!: continuous_intros)+
with g show ?thesis
- by (auto simp add: homotopic_loops_def homotopic_with_def path_defs image_subset_iff)
+ by (auto simp: homotopic_loops_def homotopic_with_def path_defs image_subset_iff)
qed
lemma homotopic_loops_imp_path_component_value:
- "\<lbrakk>homotopic_loops S p q; 0 \<le> t; t \<le> 1\<rbrakk>
- \<Longrightarrow> path_component S (p t) (q t)"
-apply (clarsimp simp add: homotopic_loops_def homotopic_with_def path_defs)
+ "\<lbrakk>homotopic_loops S p q; 0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> path_component S (p t) (q t)"
+apply (clarsimp simp: homotopic_loops_def homotopic_with_def path_defs)
apply (rule_tac x="h \<circ> (\<lambda>u. (u, t))" in exI)
apply (fastforce elim!: continuous_on_subset intro!: continuous_intros)
done
lemma homotopic_points_eq_path_component:
"homotopic_loops S (linepath a a) (linepath b b) \<longleftrightarrow> path_component S a b"
-by (auto simp: path_component_imp_homotopic_points
- dest: homotopic_loops_imp_path_component_value [where t=1])
+ using homotopic_loops_imp_path_component_value path_component_imp_homotopic_points by fastforce
lemma path_connected_eq_homotopic_points:
- "path_connected S \<longleftrightarrow>
+ "path_connected S \<longleftrightarrow>
(\<forall>a b. a \<in> S \<and> b \<in> S \<longrightarrow> homotopic_loops S (linepath a a) (linepath b b))"
-by (auto simp: path_connected_def path_component_def homotopic_points_eq_path_component)
+ by (auto simp: path_connected_def path_component_def homotopic_points_eq_path_component)
subsection\<open>Simply connected sets\<close>
@@ -1134,16 +1132,9 @@
then show ?rhs
using simply_connected_eq_contractible_loop_any by (blast intro: simply_connected_imp_path_connected)
next
- assume r: ?rhs
- note pa = r [THEN conjunct2, rule_format]
- show ?lhs
- proof (clarsimp simp add: simply_connected_eq_contractible_loop_any)
- fix p a
- assume "path p" and "path_image p \<subseteq> S" "pathfinish p = pathstart p"
- and "a \<in> S"
- with pa [of p] show "homotopic_loops S p (linepath a a)"
- using homotopic_loops_trans path_connected_eq_homotopic_points r by blast
- qed
+ assume ?rhs
+ then show ?lhs
+ by (meson homotopic_loops_trans path_connected_eq_homotopic_points simply_connected_eq_contractible_loop_any)
qed
lemma simply_connected_eq_contractible_loop_all:
@@ -1158,19 +1149,8 @@
next
case False
then obtain a where "a \<in> S" by blast
- show ?thesis
- proof
- assume "simply_connected S"
- then show ?rhs
- using \<open>a \<in> S\<close> \<open>simply_connected S\<close> simply_connected_eq_contractible_loop_any
- by blast
- next
- assume ?rhs
- then show "simply_connected S"
- unfolding simply_connected_eq_contractible_loop_any
- by (meson False homotopic_loops_refl homotopic_loops_sym homotopic_loops_trans
- path_component_imp_homotopic_points path_component_refl)
- qed
+ then show ?thesis
+ by (meson False homotopic_loops_sym homotopic_loops_trans simply_connected_def simply_connected_eq_contractible_loop_any)
qed
lemma simply_connected_eq_contractible_path:
@@ -1212,19 +1192,17 @@
"path_image q \<subseteq> S" "pathstart q = pathstart p"
"pathfinish q = pathfinish p" for p q
proof -
- have "homotopic_paths S p (p +++ linepath (pathfinish p) (pathfinish p))"
- by (simp add: homotopic_paths_rid homotopic_paths_sym that)
- also have "homotopic_paths S (p +++ linepath (pathfinish p) (pathfinish p))
- (p +++ reversepath q +++ q)"
+ have "homotopic_paths S p (p +++ reversepath q +++ q)"
using that
- by (metis homotopic_paths_join homotopic_paths_linv homotopic_paths_refl homotopic_paths_sym_eq pathstart_linepath)
+ by (smt (verit, best) homotopic_paths_join homotopic_paths_linv homotopic_paths_rid homotopic_paths_sym
+ homotopic_paths_trans pathstart_linepath)
also have "homotopic_paths S (p +++ reversepath q +++ q)
((p +++ reversepath q) +++ q)"
by (simp add: that homotopic_paths_assoc)
also have "homotopic_paths S ((p +++ reversepath q) +++ q)
(linepath (pathstart q) (pathstart q) +++ q)"
using * [of "p +++ reversepath q"] that
- by (simp add: homotopic_paths_join path_image_join)
+ by (simp add: homotopic_paths_assoc homotopic_paths_join path_image_join)
also have "homotopic_paths S (linepath (pathstart q) (pathstart q) +++ q) q"
using that homotopic_paths_lid by blast
finally show ?thesis .
@@ -1291,12 +1269,12 @@
have "\<forall>p. path p \<and>
path_image p \<subseteq> S \<and> pathfinish p = pathstart p \<longrightarrow>
homotopic_loops S p (linepath a a)"
- using a apply (clarsimp simp add: homotopic_loops_def homotopic_with_def path_defs)
+ using a apply (clarsimp simp: homotopic_loops_def homotopic_with_def path_defs)
apply (rule_tac x="(h \<circ> (\<lambda>y. (fst y, (p \<circ> snd) y)))" in exI)
apply (intro conjI continuous_on_compose continuous_intros; force elim: continuous_on_subset)
done
with \<open>a \<in> S\<close> show ?thesis
- by (auto simp add: simply_connected_eq_contractible_loop_all False)
+ by (auto simp: simply_connected_eq_contractible_loop_all False)
qed
corollary contractible_imp_connected:
@@ -1369,20 +1347,20 @@
lemma homotopic_into_contractible:
fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set"
assumes f: "continuous_on S f" "f ` S \<subseteq> T"
- and g: "continuous_on S g" "g ` S \<subseteq> T"
- and T: "contractible T"
- shows "homotopic_with_canon (\<lambda>h. True) S T f g"
-using homotopic_through_contractible [of S f T id T g id]
-by (simp add: assms contractible_imp_path_connected)
+ and g: "continuous_on S g" "g ` S \<subseteq> T"
+ and T: "contractible T"
+ shows "homotopic_with_canon (\<lambda>h. True) S T f g"
+ using homotopic_through_contractible [of S f T id T g id]
+ by (simp add: assms contractible_imp_path_connected)
lemma homotopic_from_contractible:
fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set"
assumes f: "continuous_on S f" "f ` S \<subseteq> T"
- and g: "continuous_on S g" "g ` S \<subseteq> T"
- and "contractible S" "path_connected T"
- shows "homotopic_with_canon (\<lambda>h. True) S T f g"
-using homotopic_through_contractible [of S id S f T id g]
-by (simp add: assms contractible_imp_path_connected)
+ and g: "continuous_on S g" "g ` S \<subseteq> T"
+ and "contractible S" "path_connected T"
+ shows "homotopic_with_canon (\<lambda>h. True) S T f g"
+ using homotopic_through_contractible [of S id S f T id g]
+ by (simp add: assms contractible_imp_path_connected)
subsection\<open>Starlike sets\<close>
@@ -1402,8 +1380,7 @@
proof -
have "rel_interior S \<noteq> {}"
by (simp add: assms rel_interior_eq_empty)
- then obtain a where a: "a \<in> rel_interior S" by blast
- with ST have "a \<in> T" by blast
+ with ST obtain a where a: "a \<in> rel_interior S" and "a \<in> T" by blast
have "\<And>x. x \<in> T \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
by (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> a]) (use assms in auto)
then have "\<forall>x\<in>T. a \<in> T \<and> open_segment a x \<subseteq> T"
@@ -1439,7 +1416,7 @@
lemma starlike_imp_contractible:
fixes S :: "'a::real_normed_vector set"
shows "starlike S \<Longrightarrow> contractible S"
-using starlike_imp_contractible_gen contractible_def by (fastforce simp: id_def)
+ using starlike_imp_contractible_gen contractible_def by (fastforce simp: id_def)
lemma contractible_UNIV [simp]: "contractible (UNIV :: 'a::real_normed_vector set)"
by (simp add: starlike_imp_contractible)
@@ -1447,27 +1424,27 @@
lemma starlike_imp_simply_connected:
fixes S :: "'a::real_normed_vector set"
shows "starlike S \<Longrightarrow> simply_connected S"
-by (simp add: contractible_imp_simply_connected starlike_imp_contractible)
+ by (simp add: contractible_imp_simply_connected starlike_imp_contractible)
lemma convex_imp_simply_connected:
fixes S :: "'a::real_normed_vector set"
shows "convex S \<Longrightarrow> simply_connected S"
-using convex_imp_starlike starlike_imp_simply_connected by blast
+ using convex_imp_starlike starlike_imp_simply_connected by blast
lemma starlike_imp_path_connected:
fixes S :: "'a::real_normed_vector set"
shows "starlike S \<Longrightarrow> path_connected S"
-by (simp add: simply_connected_imp_path_connected starlike_imp_simply_connected)
+ by (simp add: simply_connected_imp_path_connected starlike_imp_simply_connected)
lemma starlike_imp_connected:
fixes S :: "'a::real_normed_vector set"
shows "starlike S \<Longrightarrow> connected S"
-by (simp add: path_connected_imp_connected starlike_imp_path_connected)
+ by (simp add: path_connected_imp_connected starlike_imp_path_connected)
lemma is_interval_simply_connected_1:
fixes S :: "real set"
shows "is_interval S \<longleftrightarrow> simply_connected S"
-using convex_imp_simply_connected is_interval_convex_1 is_interval_path_connected_1 simply_connected_imp_path_connected by auto
+ by (meson convex_imp_simply_connected is_interval_connected_1 is_interval_convex_1 simply_connected_imp_connected)
lemma contractible_empty [simp]: "contractible {}"
by (simp add: contractible_def homotopic_on_emptyI)
@@ -1476,15 +1453,8 @@
fixes S :: "'a::euclidean_space set"
assumes "convex S" and TS: "rel_interior S \<subseteq> T" "T \<subseteq> closure S"
shows "contractible T"
-proof (cases "S = {}")
- case True
- with assms show ?thesis
- by (simp add: subsetCE)
-next
- case False
- show ?thesis
- by (meson False assms starlike_convex_tweak_boundary_points starlike_imp_contractible)
-qed
+ by (metis assms closure_eq_empty contractible_empty empty_subsetI
+ starlike_convex_tweak_boundary_points starlike_imp_contractible subset_antisym)
lemma convex_imp_contractible:
fixes S :: "'a::real_normed_vector set"
@@ -1494,13 +1464,13 @@
lemma contractible_sing [simp]:
fixes a :: "'a::real_normed_vector"
shows "contractible {a}"
-by (rule convex_imp_contractible [OF convex_singleton])
+ by (rule convex_imp_contractible [OF convex_singleton])
lemma is_interval_contractible_1:
fixes S :: "real set"
shows "is_interval S \<longleftrightarrow> contractible S"
-using contractible_imp_simply_connected convex_imp_contractible is_interval_convex_1
- is_interval_simply_connected_1 by auto
+ using contractible_imp_simply_connected convex_imp_contractible is_interval_convex_1
+ is_interval_simply_connected_1 by auto
lemma contractible_Times:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
@@ -1556,9 +1526,7 @@
lemma locally_open_subset:
assumes "locally P S" "openin (top_of_set S) t"
shows "locally P t"
- using assms
- unfolding locally_def
- by (elim all_forward) (meson dual_order.trans openin_imp_subset openin_subset_trans openin_trans)
+ by (smt (verit, ccfv_SIG) assms order.trans locally_def openin_imp_subset openin_subset_trans openin_trans)
lemma locally_diff_closed:
"\<lbrakk>locally P S; closedin (top_of_set S) t\<rbrakk> \<Longrightarrow> locally P (S - t)"
@@ -1575,16 +1543,13 @@
using zero_less_one by blast
then show ?thesis
unfolding locally_def
- by (auto simp add: openin_euclidean_subtopology_iff subset_singleton_iff conj_disj_distribR)
+ by (auto simp: openin_euclidean_subtopology_iff subset_singleton_iff conj_disj_distribR)
qed
lemma locally_iff:
"locally P S \<longleftrightarrow>
(\<forall>T x. open T \<and> x \<in> S \<inter> T \<longrightarrow> (\<exists>U. open U \<and> (\<exists>V. P V \<and> x \<in> S \<inter> U \<and> S \<inter> U \<subseteq> V \<and> V \<subseteq> S \<inter> T)))"
- apply (simp add: le_inf_iff locally_def openin_open, safe)
- apply (metis IntE IntI le_inf_iff)
- apply (metis IntI Int_subset_iff)
- done
+ by (smt (verit) locally_def openin_open)
lemma locally_Int:
assumes S: "locally P S" and T: "locally P T"
@@ -1649,34 +1614,29 @@
using hom by (auto simp: homeomorphism_def)
have gw: "g ` W = S \<inter> f -` W"
using \<open>W \<subseteq> T\<close> g by force
- have \<circ>: "openin (top_of_set S) (g ` W)"
- proof -
- have "continuous_on S f"
- using f(3) by blast
- then show "openin (top_of_set S) (g ` W)"
- by (simp add: gw Collect_conj_eq \<open>openin (top_of_set T) W\<close> continuous_on_open f(2))
- qed
+ have "openin (top_of_set S) (g ` W)"
+ using \<open>openin (top_of_set T) W\<close> continuous_on_open f gw by auto
then obtain U V
where osu: "openin (top_of_set S) U" and uv: "P V" "g y \<in> U" "U \<subseteq> V" "V \<subseteq> g ` W"
- using S [unfolded locally_def, rule_format, of "g ` W" "g y"] \<open>y \<in> W\<close> by force
+ by (metis S \<open>y \<in> W\<close> image_eqI locallyE)
have "V \<subseteq> S" using uv by (simp add: gw)
have fv: "f ` V = T \<inter> {x. g x \<in> V}"
using \<open>f ` S = T\<close> f \<open>V \<subseteq> S\<close> by auto
+ have contvf: "continuous_on V f"
+ using \<open>V \<subseteq> S\<close> continuous_on_subset f(3) by blast
have "f ` V \<subseteq> W"
using uv using Int_lower2 gw image_subsetI mem_Collect_eq subset_iff by auto
- have contvf: "continuous_on V f"
- using \<open>V \<subseteq> S\<close> continuous_on_subset f(3) by blast
- have contvg: "continuous_on (f ` V) g"
- using \<open>f ` V \<subseteq> W\<close> \<open>W \<subseteq> T\<close> continuous_on_subset [OF g(3)] by blast
+ then have contvg: "continuous_on (f ` V) g"
+ using \<open>W \<subseteq> T\<close> continuous_on_subset [OF g(3)] by blast
have "V \<subseteq> g ` f ` V"
by (metis \<open>V \<subseteq> S\<close> hom homeomorphism_def homeomorphism_of_subsets order_refl)
then have homv: "homeomorphism V (f ` V) f g"
- using \<open>V \<subseteq> S\<close> f by (auto simp add: homeomorphism_def contvf contvg)
+ using \<open>V \<subseteq> S\<close> f by (auto simp: homeomorphism_def contvf contvg)
have "openin (top_of_set (g ` T)) U"
using \<open>g ` T = S\<close> by (simp add: osu)
- then have 1: "openin (top_of_set T) (T \<inter> g -` U)"
+ then have "openin (top_of_set T) (T \<inter> g -` U)"
using \<open>continuous_on T g\<close> continuous_on_open [THEN iffD1] by blast
- have 2: "\<exists>V. Q V \<and> y \<in> (T \<inter> g -` U) \<and> (T \<inter> g -` U) \<subseteq> V \<and> V \<subseteq> W"
+ moreover have "\<exists>V. Q V \<and> y \<in> (T \<inter> g -` U) \<and> (T \<inter> g -` U) \<subseteq> V \<and> V \<subseteq> W"
proof (intro exI conjI)
show "Q (f ` V)"
using Q homv \<open>P V\<close> by blast
@@ -1687,44 +1647,28 @@
show "f ` V \<subseteq> W"
using \<open>f ` V \<subseteq> W\<close> by blast
qed
- show "\<exists>U. openin (top_of_set T) U \<and> (\<exists>v. Q v \<and> y \<in> U \<and> U \<subseteq> v \<and> v \<subseteq> W)"
- by (meson 1 2)
+ ultimately show "\<exists>U. openin (top_of_set T) U \<and> (\<exists>v. Q v \<and> y \<in> U \<and> U \<subseteq> v \<and> v \<subseteq> W)"
+ by meson
qed
lemma homeomorphism_locally:
fixes f:: "'a::metric_space \<Rightarrow> 'b::metric_space"
- assumes hom: "homeomorphism S T f g"
- and eq: "\<And>S T. homeomorphism S T f g \<Longrightarrow> (P S \<longleftrightarrow> Q T)"
+ assumes "homeomorphism S T f g"
+ and "\<And>S T. homeomorphism S T f g \<Longrightarrow> (P S \<longleftrightarrow> Q T)"
shows "locally P S \<longleftrightarrow> locally Q T"
- (is "?lhs = ?rhs")
-proof
- assume ?lhs
- then show ?rhs
- using eq hom homeomorphism_locally_imp by blast
-next
- assume ?rhs
- then show ?lhs
- using eq homeomorphism_sym homeomorphism_symD [OF hom]
- by (blast intro: homeomorphism_locally_imp)
-qed
+ by (smt (verit) assms homeomorphism_locally_imp homeomorphism_symD)
lemma homeomorphic_locally:
fixes S:: "'a::metric_space set" and T:: "'b::metric_space set"
assumes hom: "S homeomorphic T"
and iff: "\<And>X Y. X homeomorphic Y \<Longrightarrow> (P X \<longleftrightarrow> Q Y)"
shows "locally P S \<longleftrightarrow> locally Q T"
-proof -
- obtain f g where hom: "homeomorphism S T f g"
- using assms by (force simp: homeomorphic_def)
- then show ?thesis
- using homeomorphic_def local.iff
- by (blast intro!: homeomorphism_locally)
-qed
+ by (smt (verit, ccfv_SIG) hom homeomorphic_def homeomorphism_locally homeomorphism_locally_imp iff)
lemma homeomorphic_local_compactness:
fixes S:: "'a::metric_space set" and T:: "'b::metric_space set"
shows "S homeomorphic T \<Longrightarrow> locally compact S \<longleftrightarrow> locally compact T"
-by (simp add: homeomorphic_compactness homeomorphic_locally)
+ by (simp add: homeomorphic_compactness homeomorphic_locally)
lemma locally_translation:
fixes P :: "'a :: real_normed_vector set \<Rightarrow> bool"
@@ -1746,7 +1690,7 @@
and oo: "\<And>T. openin (top_of_set S) T \<Longrightarrow> openin (top_of_set (f ` S)) (f ` T)"
and Q: "\<And>T. \<lbrakk>T \<subseteq> S; P T\<rbrakk> \<Longrightarrow> Q(f ` T)"
shows "locally Q (f ` S)"
-proof (clarsimp simp add: locally_def)
+proof (clarsimp simp: locally_def)
fix W y
assume oiw: "openin (top_of_set (f ` S)) W" and "y \<in> W"
then have "W \<subseteq> f ` S" by (simp add: openin_euclidean_subtopology_iff)
@@ -1756,8 +1700,7 @@
using \<open>W \<subseteq> f ` S\<close> \<open>y \<in> W\<close> by blast
then obtain U V
where "openin (top_of_set S) U" "P V" "x \<in> U" "U \<subseteq> V" "V \<subseteq> S \<inter> f -` W"
- using P [unfolded locally_def, rule_format, of "(S \<inter> f -` W)" x] oivf \<open>y \<in> W\<close>
- by auto
+ by (metis IntI P \<open>y \<in> W\<close> locallyE oivf vimageI)
then have "openin (top_of_set (f ` S)) (f ` U)"
by (simp add: oo)
then show "\<exists>X. openin (top_of_set (f ` S)) X \<and> (\<exists>Y. Q Y \<and> y \<in> X \<and> X \<subseteq> Y \<and> Y \<subseteq> W)"
@@ -1778,17 +1721,16 @@
proof -
let ?A = "{b. \<exists>T. openin (top_of_set S) T \<and> b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> Q x)}"
let ?B = "{b. \<exists>T. openin (top_of_set S) T \<and> b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> \<not> Q x)}"
- have 1: "openin (top_of_set S) ?A"
- by (subst openin_subopen, blast)
- have 2: "openin (top_of_set S) ?B"
- by (subst openin_subopen, blast)
- have \<section>: "?A \<inter> ?B = {}"
+ have "?A \<inter> ?B = {}"
by (clarsimp simp: set_eq_iff) (metis (no_types, opaque_lifting) Int_iff opD openin_Int)
- have *: "S \<subseteq> ?A \<union> ?B"
+ moreover have "S \<subseteq> ?A \<union> ?B"
by clarsimp (meson opI)
- have "?A = {} \<or> ?B = {}"
- using \<open>connected S\<close> [unfolded connected_openin, simplified, rule_format, OF 1 \<section> * 2]
- by blast
+ moreover have "openin (top_of_set S) ?A"
+ by (subst openin_subopen, blast)
+ moreover have "openin (top_of_set S) ?B"
+ by (subst openin_subopen, blast)
+ ultimately have "?A = {} \<or> ?B = {}"
+ by (metis (no_types, lifting) \<open>connected S\<close> connected_openin)
then show ?thesis
by clarsimp (meson opI etc)
qed
@@ -1851,15 +1793,11 @@
shows "locally (\<lambda>U. f constant_on U) S \<longleftrightarrow> f constant_on S" (is "?lhs = ?rhs")
proof
assume ?lhs
- then have "\<And>a. a \<in> S \<Longrightarrow> \<exists>T. openin (top_of_set S) T \<and> a \<in> T \<and> (\<forall>x\<in>T. f x = f a)"
- unfolding locally_def
- by (metis (mono_tags, opaque_lifting) constant_on_def constant_on_subset openin_subtopology_self)
then show ?rhs
- using assms
- by (simp add: locally_constant_imp_constant)
+ by (smt (verit, del_insts) assms constant_on_def locally_constant_imp_constant locally_def openin_subtopology_self subset_iff)
next
assume ?rhs then show ?lhs
- using assms by (metis constant_on_subset locallyI openin_imp_subset order_refl)
+ by (metis constant_on_subset locallyI openin_imp_subset order_refl)
qed
@@ -1938,10 +1876,8 @@
proof
fix x
assume "x \<in> S"
- then obtain e where "e>0" and e: "closed (cball x e \<inter> S)"
- using R by blast
- then have "compact (cball x e \<inter> S)"
- by (simp add: bounded_Int compact_eq_bounded_closed)
+ then obtain e where "e>0" and "compact (cball x e \<inter> S)"
+ by (metis Int_commute compact_Int_closed compact_cball inf.right_idem R)
moreover have "\<forall>y\<in>ball x e \<inter> S. \<exists>\<epsilon>>0. cball y \<epsilon> \<inter> S \<subseteq> ball x e"
by (meson Elementary_Metric_Spaces.open_ball IntD1 le_infI1 open_contains_cball_eq)
moreover have "openin (top_of_set S) (ball x e \<inter> S)"
@@ -1984,10 +1920,8 @@
have "openin (top_of_set S) (\<Union> (u ` T))"
using T that uv by fastforce
moreover
- have "compact (\<Union> (v ` T))"
- by (meson T compact_UN subset_eq that(1) uv)
- moreover have "\<Union> (v ` T) \<subseteq> S"
- by (metis SUP_least T(1) subset_eq that(1) uv)
+ obtain "compact (\<Union> (v ` T))" "\<Union> (v ` T) \<subseteq> S"
+ by (metis T UN_subset_iff \<open>K \<subseteq> S\<close> compact_UN subset_iff uv)
ultimately show ?thesis
using T by auto
qed
@@ -1996,7 +1930,7 @@
next
assume ?rhs
then show ?lhs
- apply (clarsimp simp add: locally_compact)
+ apply (clarsimp simp: locally_compact)
apply (drule_tac x="{x}" in spec, simp)
done
qed
@@ -2014,14 +1948,7 @@
have ope: "openin (top_of_set S) (ball x e)"
by (meson e open_ball ball_subset_cball dual_order.trans open_subset)
show ?thesis
- proof (intro exI conjI)
- let ?U = "ball x e"
- let ?V = "cball x e"
- show "x \<in> ?U" "?U \<subseteq> ?V" "?V \<subseteq> S" "compact ?V"
- using \<open>e > 0\<close> e by auto
- show "openin (top_of_set S) ?U"
- using ope by blast
- qed
+ by (meson \<open>0 < e\<close> ball_subset_cball centre_in_ball compact_cball e ope)
qed
show ?thesis
unfolding locally_compact by (blast intro: *)
@@ -2045,13 +1972,13 @@
lemma locally_compact_Int:
fixes S :: "'a :: t2_space set"
- shows "\<lbrakk>locally compact S; locally compact t\<rbrakk> \<Longrightarrow> locally compact (S \<inter> t)"
-by (simp add: compact_Int locally_Int)
+ shows "\<lbrakk>locally compact S; locally compact T\<rbrakk> \<Longrightarrow> locally compact (S \<inter> T)"
+ by (simp add: compact_Int locally_Int)
lemma locally_compact_closedin:
fixes S :: "'a :: heine_borel set"
- shows "\<lbrakk>closedin (top_of_set S) t; locally compact S\<rbrakk>
- \<Longrightarrow> locally compact t"
+ shows "\<lbrakk>closedin (top_of_set S) T; locally compact S\<rbrakk>
+ \<Longrightarrow> locally compact T"
unfolding closedin_closed
using closed_imp_locally_compact locally_compact_Int by blast
@@ -2130,12 +2057,7 @@
obtain e2 where "e2 > 0" and e2: "closed (cball x e2 \<inter> T)"
using LCT \<open>x \<in> T\<close> unfolding locally_compact_Int_cball by blast
moreover have "closed (cball x (min e1 e2) \<inter> (S \<union> T))"
- proof -
- have "closed (cball x e1 \<inter> (cball x e2 \<inter> S))"
- by (metis closed_Int closed_cball e1 inf_left_commute)
- then show ?thesis
- by (simp add: Int_Un_distrib cball_min_Int closed_Int closed_Un e2 inf_assoc)
- qed
+ by (smt (verit) Int_Un_distrib2 Int_commute cball_min_Int closed_Int closed_Un closed_cball e1 e2 inf_left_commute)
ultimately show ?thesis
by (rule_tac x="min e1 e2" in exI) linarith
qed
@@ -2298,7 +2220,7 @@
by (simp_all add: closedin_closed_Int)
moreover have "D \<inter> closure V1 = D \<inter> V1" "D \<inter> closure V2 = D \<inter> V2"
using \<open>D \<subseteq> V1 \<union> V2\<close> \<open>open V1\<close> \<open>open V2\<close> V12
- by (auto simp add: closure_subset [THEN subsetD] closure_iff_nhds_not_empty, blast+)
+ by (auto simp: closure_subset [THEN subsetD] closure_iff_nhds_not_empty, blast+)
ultimately have cloDV1: "closedin (top_of_set D) (D \<inter> V1)"
and cloDV2: "closedin (top_of_set D) (D \<inter> V2)"
by metis+
@@ -2721,7 +2643,7 @@
fixes S :: "'a:: real_normed_vector set"
assumes "convex S"
shows "locally path_connected S"
-proof (clarsimp simp add: locally_path_connected)
+proof (clarsimp simp: locally_path_connected)
fix V x
assume "openin (top_of_set S) V" and "x \<in> V"
then obtain T e where "V = S \<inter> T" "x \<in> S" "0 < e" "ball x e \<subseteq> T"
@@ -3824,7 +3746,7 @@
show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set S)) (top_of_set S)
(\<lambda>(t,x). (1 - t) * x + t * z)"
using \<open>z \<in> S\<close>
- by (auto simp add: case_prod_unfold intro!: continuous_intros \<section>)
+ by (auto simp: case_prod_unfold intro!: continuous_intros \<section>)
qed auto
qed (simp add: contractible_space_empty)
qed
@@ -3946,7 +3868,7 @@
by (rule homotopic_with_compose_continuous_right [where X=S]) (use k in auto)
moreover have "homotopic_with_canon (\<lambda>x. True) T U (f \<circ> id) (f \<circ> (h \<circ> k))"
by (rule homotopic_with_compose_continuous_left [where Y=T])
- (use f in \<open>auto simp add: hom homotopic_with_symD\<close>)
+ (use f in \<open>auto simp: hom homotopic_with_symD\<close>)
ultimately show ?thesis
using that homotopic_with_trans by (fastforce simp add: o_def)
qed
@@ -3987,7 +3909,7 @@
by (rule homotopic_with_compose_continuous_left [where Y=S]) (use h in auto)
moreover have "homotopic_with_canon (\<lambda>x. True) U T (id \<circ> f) ((h \<circ> k) \<circ> f)"
by (rule homotopic_with_compose_continuous_right [where X=T])
- (use f in \<open>auto simp add: hom homotopic_with_symD\<close>)
+ (use f in \<open>auto simp: hom homotopic_with_symD\<close>)
ultimately show ?thesis
using homotopic_with_trans by (fastforce simp add: o_def)
qed
@@ -4123,7 +4045,7 @@
fixes U :: "'a::euclidean_space set"
assumes "convex U" "\<not> collinear U" "countable S"
shows "path_connected(U - S)"
-proof (clarsimp simp add: path_connected_def)
+proof (clarsimp simp: path_connected_def)
fix a b
assume "a \<in> U" "a \<notin> S" "b \<in> U" "b \<notin> S"
let ?m = "midpoint a b"
@@ -4245,7 +4167,7 @@
next
assume ge2: "aff_dim S \<ge> 2"
then have "\<not> collinear S"
- proof (clarsimp simp add: collinear_affine_hull)
+ proof (clarsimp simp: collinear_affine_hull)
fix u v
assume "S \<subseteq> affine hull {u, v}"
then have "aff_dim S \<le> aff_dim {u, v}"
@@ -4282,7 +4204,7 @@
assumes "connected S" and ope: "openin (top_of_set (affine hull S)) S"
and "\<not> collinear S" "countable T"
shows "path_connected(S - T)"
-proof (clarsimp simp add: path_connected_component)
+proof (clarsimp simp: path_connected_component)
fix x y
assume xy: "x \<in> S" "x \<notin> T" "y \<in> S" "y \<notin> T"
show "path_component (S - T) x y"
@@ -4483,7 +4405,7 @@
by blast
next
show "cball a r \<inter> T \<subseteq> f ` (cball a r \<inter> T)"
- proof (clarsimp simp add: dist_norm norm_minus_commute)
+ proof (clarsimp simp: dist_norm norm_minus_commute)
fix x
assume x: "norm (x - a) \<le> r" and "x \<in> T"
have "\<exists>v \<in> {0..1}. ((1 - v) * r - norm ((x - a) - v *\<^sub>R (u - a))) \<bullet> 1 = 0"
@@ -4575,7 +4497,7 @@
then show "continuous_on S gg"
by (rule continuous_on_subset) (use ST in auto)
show "ff ` S \<subseteq> S"
- proof (clarsimp simp add: ff_def)
+ proof (clarsimp simp: ff_def)
fix x
assume "x \<in> S" and x: "dist a x < r" and "x \<in> T"
then have "f x \<in> cball a r \<inter> T"
@@ -4584,7 +4506,7 @@
using ST(1) \<open>x \<in> T\<close> gid hom homeomorphism_def x by fastforce
qed
show "gg ` S \<subseteq> S"
- proof (clarsimp simp add: gg_def)
+ proof (clarsimp simp: gg_def)
fix x
assume "x \<in> S" and x: "dist a x < r" and "x \<in> T"
then have "g x \<in> cball a r \<inter> T"
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Wed May 03 10:35:20 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 08:39:48 2023 +0000
+++ b/src/HOL/Analysis/Product_Topology.thy Wed May 03 10:35:20 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 08:39:48 2023 +0000
+++ b/src/HOL/Analysis/T1_Spaces.thy Wed May 03 10:35:20 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/Archimedean_Field.thy Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Archimedean_Field.thy Wed May 03 10:35:20 2023 +0100
@@ -16,15 +16,10 @@
proof -
have "Sup (uminus ` S) = - (Inf S)"
proof (rule antisym)
- show "- (Inf S) \<le> Sup (uminus ` S)"
- apply (subst minus_le_iff)
- apply (rule cInf_greatest [OF \<open>S \<noteq> {}\<close>])
- apply (subst minus_le_iff)
- apply (rule cSup_upper)
- apply force
- using bdd
- apply (force simp: abs_le_iff bdd_above_def)
- done
+ have "\<And>x. x \<in> S \<Longrightarrow> bdd_above (uminus ` S)"
+ using bdd by (force simp: abs_le_iff bdd_above_def)
+ then show "- (Inf S) \<le> Sup (uminus ` S)"
+ by (meson cInf_greatest [OF \<open>S \<noteq> {}\<close>] cSUP_upper minus_le_iff)
next
have *: "\<And>x. x \<in> S \<Longrightarrow> Inf S \<le> x"
by (meson abs_le_iff bdd bdd_below_def cInf_lower minus_le_iff)
--- a/src/HOL/Conditionally_Complete_Lattices.thy Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Wed May 03 10:35:20 2023 +0100
@@ -481,6 +481,12 @@
assume "X = {}" with lt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
qed (intro cSup_eq_non_empty assms)
+lemma cSup_unique:
+ fixes b :: "'a :: {conditionally_complete_lattice, no_bot}"
+ assumes "\<And>c. (\<forall>x \<in> s. x \<le> c) \<longleftrightarrow> b \<le> c"
+ shows "Sup s = b"
+ by (metis assms cSup_eq order.refl)
+
lemma cInf_eq:
fixes a :: "'a :: {conditionally_complete_lattice, no_top}"
assumes upper: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
@@ -490,6 +496,12 @@
assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
qed (intro cInf_eq_non_empty assms)
+lemma cInf_unique:
+ fixes b :: "'a :: {conditionally_complete_lattice, no_top}"
+ assumes "\<And>c. (\<forall>x \<in> s. x \<ge> c) \<longleftrightarrow> b \<ge> c"
+ shows "Inf s = b"
+ by (meson assms cInf_eq order.refl)
+
class conditionally_complete_linorder = conditionally_complete_lattice + linorder
begin
--- a/src/HOL/Fun.thy Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Fun.thy Wed May 03 10:35:20 2023 +0100
@@ -1031,6 +1031,12 @@
abbreviation strict_mono_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
where "strict_mono_on A \<equiv> monotone_on A (<) (<)"
+abbreviation antimono_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
+ where "antimono_on A \<equiv> monotone_on A (\<le>) (\<ge>)"
+
+abbreviation strict_antimono_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
+ where "strict_antimono_on A \<equiv> monotone_on A (<) (>)"
+
lemma mono_on_def[no_atp]: "mono_on A f \<longleftrightarrow> (\<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s)"
by (auto simp add: monotone_on_def)
@@ -1265,6 +1271,32 @@
"strict_mono_on A (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) \<Longrightarrow> mono_on A f"
by (rule mono_onI, rule strict_mono_on_leD)
+lemma mono_imp_strict_mono:
+ fixes f :: "'a::order \<Rightarrow> 'b::order"
+ shows "\<lbrakk>mono_on S f; inj_on f S\<rbrakk> \<Longrightarrow> strict_mono_on S f"
+ by (auto simp add: monotone_on_def order_less_le inj_on_eq_iff)
+
+lemma strict_mono_iff_mono:
+ fixes f :: "'a::linorder \<Rightarrow> 'b::order"
+ shows "strict_mono_on S f \<longleftrightarrow> mono_on S f \<and> inj_on f S"
+proof
+ show "strict_mono_on S f \<Longrightarrow> mono_on S f \<and> inj_on f S"
+ by (simp add: strict_mono_on_imp_inj_on strict_mono_on_imp_mono_on)
+qed (auto intro: mono_imp_strict_mono)
+
+lemma antimono_imp_strict_antimono:
+ fixes f :: "'a::order \<Rightarrow> 'b::order"
+ shows "\<lbrakk>antimono_on S f; inj_on f S\<rbrakk> \<Longrightarrow> strict_antimono_on S f"
+ by (auto simp add: monotone_on_def order_less_le inj_on_eq_iff)
+
+lemma strict_antimono_iff_antimono:
+ fixes f :: "'a::linorder \<Rightarrow> 'b::order"
+ shows "strict_antimono_on S f \<longleftrightarrow> antimono_on S f \<and> inj_on f S"
+proof
+ show "strict_antimono_on S f \<Longrightarrow> antimono_on S f \<and> inj_on f S"
+ by (force simp add: monotone_on_def intro: linorder_inj_onI)
+qed (auto intro: antimono_imp_strict_antimono)
+
lemma mono_compose: "mono Q \<Longrightarrow> mono (\<lambda>i x. Q i (f x))"
unfolding mono_def le_fun_def by auto
--- a/src/HOL/Library/Set_Idioms.thy Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Library/Set_Idioms.thy Wed May 03 10:35:20 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/Real.thy Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Real.thy Wed May 03 10:35:20 2023 +0100
@@ -1096,6 +1096,27 @@
by (metis reals_Archimedean3 dual_order.order_iff_strict le0 le_less_trans not_le x0 xc)
+lemma inverse_Suc: "inverse (Suc n) > 0"
+ using of_nat_0_less_iff positive_imp_inverse_positive zero_less_Suc by blast
+
+lemma Archimedean_eventually_inverse:
+ fixes \<epsilon>::real shows "(\<forall>\<^sub>F n in sequentially. inverse (real (Suc n)) < \<epsilon>) \<longleftrightarrow> 0 < \<epsilon>"
+ (is "?lhs=?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ unfolding eventually_at_top_dense using inverse_Suc order_less_trans by blast
+next
+ assume ?rhs
+ then obtain N where "inverse (Suc N) < \<epsilon>"
+ using reals_Archimedean by blast
+ moreover have "inverse (Suc n) \<le> inverse (Suc N)" if "n \<ge> N" for n
+ using inverse_Suc that by fastforce
+ ultimately show ?lhs
+ unfolding eventually_sequentially
+ using order_le_less_trans by blast
+qed
+
subsection \<open>Rationals\<close>
lemma Rats_abs_iff[simp]:
--- a/src/HOL/Set.thy Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Set.thy Wed May 03 10:35:20 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 08:39:48 2023 +0000
+++ b/src/HOL/Set_Interval.thy Wed May 03 10:35:20 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]: