--- a/NEWS Mon Jul 10 22:06:31 2023 +0200
+++ b/NEWS Mon Jul 10 22:06:42 2023 +0200
@@ -322,7 +322,7 @@
* Session "HOL-Analysis":
- Imported the HOL Light abstract metric space library and numerous
- associated topological developments.
+ results in abstract topology (1200+ lemmas).
- New material on infinite sums and integration, due to Manuel Eberl
and Wenda Li.
--- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy Mon Jul 10 22:06:31 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy Mon Jul 10 22:06:42 2023 +0200
@@ -3401,7 +3401,7 @@
strict_mono_iff_mono top_greatest topspace_euclidean topspace_euclidean_subtopology)
-subsection\<open>Normal spaces including Urysohn's lemma and the Tietze extension theorem\<close>
+subsection\<open>Normal spaces\<close>
definition normal_space
where "normal_space X \<equiv>
--- a/src/HOL/Analysis/Continuous_Extension.thy Mon Jul 10 22:06:31 2023 +0200
+++ b/src/HOL/Analysis/Continuous_Extension.thy Mon Jul 10 22:06:42 2023 +0200
@@ -5,7 +5,7 @@
section \<open>Continuous Extensions of Functions\<close>
theory Continuous_Extension
-imports Starlike
+imports Starlike
begin
subsection\<open>Partitions of unity subordinate to locally finite open coverings\<close>
@@ -152,9 +152,7 @@
proof -
have "f x = b \<longleftrightarrow> (setdist {x} S / (setdist {x} S + setdist {x} T)) = 1"
unfolding f_def
- apply (rule iffI)
- apply (metis \<open>a \<noteq> b\<close> add_diff_cancel_left' eq_iff_diff_eq_0 pth_1 real_vector.scale_right_imp_eq, force)
- done
+ by (metis add_diff_cancel_left' \<open>a \<noteq> b\<close> diff_add_cancel eq_iff_diff_eq_0 scaleR_cancel_right scaleR_one)
also have "... \<longleftrightarrow> setdist {x} T = 0 \<and> setdist {x} S \<noteq> 0"
using sdpos that
by (simp add: field_split_simps) linarith
@@ -166,6 +164,47 @@
qed
qed
+lemma Urysohn_local_strong_aux:
+ assumes US: "closedin (top_of_set U) S"
+ and UT: "closedin (top_of_set U) T"
+ and "S \<inter> T = {}" "a \<noteq> b" "S \<noteq> {}"
+ obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ where "continuous_on U f"
+ "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b"
+ "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"
+ "\<And>x. x \<in> U \<Longrightarrow> (f x = b \<longleftrightarrow> x \<in> T)"
+proof (cases "T = {}")
+ case True show ?thesis
+ proof (cases "S = U")
+ case True with \<open>T = {}\<close> \<open>a \<noteq> b\<close> show ?thesis
+ by (rule_tac f = "\<lambda>x. a" in that) (auto)
+ next
+ case False
+ with US closedin_subset obtain c where c: "c \<in> U" "c \<notin> S"
+ by fastforce
+ obtain f where f: "continuous_on U f"
+ "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a (midpoint a b)"
+ "\<And>x. x \<in> U \<Longrightarrow> (f x = midpoint a b \<longleftrightarrow> x = c)"
+ "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"
+ apply (rule Urysohn_both_ne [of U S "{c}" a "midpoint a b"])
+ using c \<open>S \<noteq> {}\<close> assms apply simp_all
+ apply (metis midpoint_eq_endpoint)
+ done
+ show ?thesis
+ apply (rule_tac f=f in that)
+ using \<open>S \<noteq> {}\<close> \<open>T = {}\<close> f \<open>a \<noteq> b\<close>
+ apply simp_all
+ apply (metis (no_types) closed_segment_commute csegment_midpoint_subset midpoint_sym subset_iff)
+ apply (metis closed_segment_commute midpoint_sym notin_segment_midpoint)
+ done
+ qed
+next
+ case False
+ show ?thesis
+ using Urysohn_both_ne [OF US UT \<open>S \<inter> T = {}\<close> \<open>S \<noteq> {}\<close> \<open>T \<noteq> {}\<close> \<open>a \<noteq> b\<close>] that
+ by blast
+qed
+
proposition Urysohn_local_strong:
assumes US: "closedin (top_of_set U) S"
and UT: "closedin (top_of_set U) T"
@@ -191,62 +230,13 @@
qed
next
case False
- show ?thesis
- proof (cases "T = U")
- case True with \<open>S = {}\<close> \<open>a \<noteq> b\<close> show ?thesis
- by (rule_tac f = "\<lambda>x. b" in that) (auto)
- next
- case False
- with UT closedin_subset obtain c where c: "c \<in> U" "c \<notin> T"
- by fastforce
- obtain f where f: "continuous_on U f"
- "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment (midpoint a b) b"
- "\<And>x. x \<in> U \<Longrightarrow> (f x = midpoint a b \<longleftrightarrow> x = c)"
- "\<And>x. x \<in> U \<Longrightarrow> (f x = b \<longleftrightarrow> x \<in> T)"
- apply (rule Urysohn_both_ne [of U "{c}" T "midpoint a b" "b"])
- using c \<open>T \<noteq> {}\<close> assms apply simp_all
- done
- show ?thesis
- apply (rule_tac f=f in that)
- using \<open>S = {}\<close> \<open>T \<noteq> {}\<close> f csegment_midpoint_subset notin_segment_midpoint [OF \<open>a \<noteq> b\<close>]
- apply force+
- done
- qed
+ with Urysohn_local_strong_aux [OF UT US] assms show ?thesis
+ by (smt (verit) True closed_segment_commute inf_bot_right that)
qed
next
case False
- show ?thesis
- proof (cases "T = {}")
- case True show ?thesis
- proof (cases "S = U")
- case True with \<open>T = {}\<close> \<open>a \<noteq> b\<close> show ?thesis
- by (rule_tac f = "\<lambda>x. a" in that) (auto)
- next
- case False
- with US closedin_subset obtain c where c: "c \<in> U" "c \<notin> S"
- by fastforce
- obtain f where f: "continuous_on U f"
- "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a (midpoint a b)"
- "\<And>x. x \<in> U \<Longrightarrow> (f x = midpoint a b \<longleftrightarrow> x = c)"
- "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"
- apply (rule Urysohn_both_ne [of U S "{c}" a "midpoint a b"])
- using c \<open>S \<noteq> {}\<close> assms apply simp_all
- apply (metis midpoint_eq_endpoint)
- done
- show ?thesis
- apply (rule_tac f=f in that)
- using \<open>S \<noteq> {}\<close> \<open>T = {}\<close> f \<open>a \<noteq> b\<close>
- apply simp_all
- apply (metis (no_types) closed_segment_commute csegment_midpoint_subset midpoint_sym subset_iff)
- apply (metis closed_segment_commute midpoint_sym notin_segment_midpoint)
- done
- qed
- next
- case False
- show ?thesis
- using Urysohn_both_ne [OF US UT \<open>S \<inter> T = {}\<close> \<open>S \<noteq> {}\<close> \<open>T \<noteq> {}\<close> \<open>a \<noteq> b\<close>] that
- by blast
- qed
+ with Urysohn_local_strong_aux [OF assms] show ?thesis
+ using that by blast
qed
lemma Urysohn_local:
@@ -263,12 +253,8 @@
by (rule_tac f = "\<lambda>x. b" in that) (auto)
next
case False
- then show ?thesis
- apply (rule Urysohn_local_strong [OF assms])
- apply (erule that, assumption)
- apply (meson US closedin_singleton closedin_trans)
- apply (meson UT closedin_singleton closedin_trans)
- done
+ with Urysohn_local_strong [OF assms] show ?thesis
+ by (smt (verit) US UT closedin_imp_subset subset_eq that)
qed
lemma Urysohn_strong:
@@ -298,20 +284,6 @@
text \<open>See \<^cite>\<open>"dugundji"\<close>.\<close>
-lemma convex_supp_sum:
- assumes "convex S" and 1: "supp_sum u I = 1"
- and "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> u i \<and> (u i = 0 \<or> f i \<in> S)"
- shows "supp_sum (\<lambda>i. u i *\<^sub>R f i) I \<in> S"
-proof -
- have fin: "finite {i \<in> I. u i \<noteq> 0}"
- using 1 sum.infinite by (force simp: supp_sum_def support_on_def)
- then have "supp_sum (\<lambda>i. u i *\<^sub>R f i) I = sum (\<lambda>i. u i *\<^sub>R f i) {i \<in> I. u i \<noteq> 0}"
- by (force intro: sum.mono_neutral_left simp: supp_sum_def support_on_def)
- also have "... \<in> S"
- using 1 assms by (force simp: supp_sum_def support_on_def intro: convex_sum [OF fin \<open>convex S\<close>])
- finally show ?thesis .
-qed
-
theorem Dugundji:
fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::real_inner"
assumes "convex C" "C \<noteq> {}"
@@ -320,11 +292,13 @@
obtains g where "continuous_on U g" "g ` U \<subseteq> C"
"\<And>x. x \<in> S \<Longrightarrow> g x = f x"
proof (cases "S = {}")
- case True then show thesis
- apply (rule_tac g="\<lambda>x. SOME y. y \<in> C" in that)
- apply (rule continuous_intros)
- apply (meson all_not_in_conv \<open>C \<noteq> {}\<close> image_subsetI someI_ex, simp)
- done
+ case True show thesis
+ proof
+ show "continuous_on U (\<lambda>x. SOME y. y \<in> C)"
+ by (rule continuous_intros)
+ show "(\<lambda>x. SOME y. y \<in> C) ` U \<subseteq> C"
+ by (simp add: \<open>C \<noteq> {}\<close> image_subsetI some_in_eq)
+ qed (use True in auto)
next
case False
then have sd_pos: "\<And>x. \<lbrakk>x \<in> U; x \<notin> S\<rbrakk> \<Longrightarrow> 0 < setdist {x} S"
@@ -348,9 +322,7 @@
using setdist_ltE [of "{v}" S "2 * setdist {v} S"]
using False sd_pos by force
with v show ?thesis
- apply (rule_tac x=v in exI)
- apply (rule_tac x=a in exI, auto)
- done
+ by force
qed
then obtain \<V> \<A> where
VA: "\<And>T. T \<in> \<C> \<Longrightarrow> \<V> T \<in> U \<and> \<V> T \<notin> S \<and> \<A> T \<in> S \<and>
--- a/src/HOL/Analysis/Urysohn.thy Mon Jul 10 22:06:31 2023 +0200
+++ b/src/HOL/Analysis/Urysohn.thy Mon Jul 10 22:06:42 2023 +0200
@@ -10,7 +10,7 @@
subsection \<open>Urysohn lemma and Tietze's theorem\<close>
-lemma Urysohn_lemma:
+proposition Urysohn_lemma:
fixes a b :: real
assumes "normal_space X" "closedin X S" "closedin X T" "disjnt S T" "a \<le> b"
obtains f where "continuous_map X (top_of_set {a..b}) f" "f ` S \<subseteq> {a}" "f ` T \<subseteq> {b}"
@@ -333,7 +333,7 @@
qed
qed
-lemma Tietze_extension_closed_real_interval:
+theorem Tietze_extension_closed_real_interval:
assumes "normal_space X" and "closedin X S"
and contf: "continuous_map (subtopology X S) euclideanreal f"
and fim: "f ` S \<subseteq> {a..b}" and "a \<le> b"
@@ -498,7 +498,7 @@
qed
-lemma Tietze_extension_realinterval:
+theorem Tietze_extension_realinterval:
assumes XS: "normal_space X" "closedin X S" and T: "is_interval T" "T \<noteq> {}"
and contf: "continuous_map (subtopology X S) euclideanreal f"
and "f ` S \<subseteq> T"
@@ -665,8 +665,7 @@
qed
qed
-subsection \<open>random metric space stuff\<close>
-
+subsection \<open>Random metric space stuff\<close>
lemma metrizable_imp_k_space:
assumes "metrizable_space X"
@@ -1085,7 +1084,7 @@
qed
-lemma locally_compact_regular_imp_completely_regular_space:
+proposition locally_compact_regular_imp_completely_regular_space:
assumes "locally_compact_space X" "Hausdorff_space X \<or> regular_space X"
shows "completely_regular_space X"
unfolding completely_regular_space_def
@@ -1205,7 +1204,7 @@
qed
-lemma completely_regular_space_product_topology:
+proposition completely_regular_space_product_topology:
"completely_regular_space (product_topology X I) \<longleftrightarrow>
(\<Pi>\<^sub>E i\<in>I. topspace(X i)) = {} \<or> (\<forall>i \<in> I. completely_regular_space (X i))"
(is "?lhs \<longleftrightarrow> ?rhs")
@@ -1492,7 +1491,7 @@
"\<lbrakk>compact_space X; \<not> compactin X (topspace X - {a})\<rbrakk> \<Longrightarrow> X interior_of {a} = {}"
by (simp add: interior_of_eq_empty_complement one_point_compactification_dense)
-lemma kc_space_one_point_compactification_gen:
+proposition kc_space_one_point_compactification_gen:
assumes "compact_space X"
shows "kc_space X \<longleftrightarrow>
openin X (topspace X - {a}) \<and> (\<forall>K. compactin X K \<and> a\<notin>K \<longrightarrow> closedin X K) \<and>
@@ -1624,7 +1623,7 @@
unfolding eq using Alexandroff_open.base by blast
qed
-lemma istopology_Alexandroff_open: "istopology (Alexandroff_open X)"
+proposition istopology_Alexandroff_open: "istopology (Alexandroff_open X)"
unfolding istopology_def
proof (intro conjI strip)
fix S T
@@ -1930,7 +1929,7 @@
qed
-lemma regular_space_one_point_compactification:
+proposition regular_space_one_point_compactification:
assumes "compact_space X" and ope: "openin X (topspace X - {a})"
and \<section>: "\<And>K. \<lbrakk>compactin (subtopology X (topspace X - {a})) K; closedin (subtopology X (topspace X - {a})) K\<rbrakk> \<Longrightarrow> closedin X K"
shows "regular_space X \<longleftrightarrow>
@@ -2036,7 +2035,7 @@
by (metis regular_space_Alexandroff_compactification completely_regular_eq_regular_space
compact_imp_locally_compact_space compact_space_Alexandroff_compactification)
-lemma Hausdorff_space_one_point_compactification_asymmetric_prod:
+proposition Hausdorff_space_one_point_compactification_asymmetric_prod:
assumes "compact_space X"
shows "Hausdorff_space X \<longleftrightarrow>
kc_space (prod_topology X (subtopology X (topspace X - {a}))) \<and>
@@ -5182,4 +5181,766 @@
\<Longrightarrow> gdelta_in X S \<longleftrightarrow> S \<subseteq> topspace X \<and> completely_metrizable_space (subtopology X S)"
by (metis completely_metrizable_space_eq_gdelta_in gdelta_in_alt)
+subsection\<open> Theorems from Kuratowski\<close>
+
+text\<open>Kuratowski, Remark on an Invariance Theorem, \emph{Fundamenta Mathematicae} \textbf{37} (1950), pp. 251-252.
+ The idea is that in suitable spaces, to show "number of components of the complement" (without
+ distinguishing orders of infinity) is a homeomorphic invariant, it
+ suffices to show it for closed subsets. Kuratowski states the main result
+ for a "locally connected continuum", and seems clearly to be implicitly
+ assuming that means metrizable. We call out the general topological
+ hypotheses more explicitly, which do not however include connectedness. \<close>
+
+lemma separation_by_closed_intermediates_count:
+ assumes X: "hereditarily normal_space X"
+ and "finite \<U>"
+ and pwU: "pairwise (separatedin X) \<U>"
+ and nonempty: "{} \<notin> \<U>"
+ and UU: "\<Union>\<U> = topspace X - S"
+ obtains C where "closedin X C" "C \<subseteq> S"
+ "\<And>D. \<lbrakk>closedin X D; C \<subseteq> D; D \<subseteq> S\<rbrakk>
+ \<Longrightarrow> \<exists>\<V>. \<V> \<approx> \<U> \<and> pairwise (separatedin X) \<V> \<and> {} \<notin> \<V> \<and> \<Union>\<V> = topspace X - D"
+proof -
+ obtain F where F: "\<And>S. S \<in> \<U> \<Longrightarrow> openin X (F S) \<and> S \<subseteq> F S"
+ and pwF: "pairwise (\<lambda>S T. disjnt (F S) (F T)) \<U>"
+ using assms by (smt (verit, best) Diff_subset Sup_le_iff hereditarily_normal_separation_pairwise)
+ show thesis
+ proof
+ show "closedin X (topspace X - \<Union>(F ` \<U>))"
+ using F by blast
+ show "topspace X - \<Union>(F ` \<U>) \<subseteq> S"
+ using UU F by auto
+ show "\<exists>\<V>. \<V> \<approx> \<U> \<and> pairwise (separatedin X) \<V> \<and> {} \<notin> \<V> \<and> \<Union>\<V> = topspace X - C"
+ if "closedin X C" "C \<subseteq> S" and C: "topspace X - \<Union>(F ` \<U>) \<subseteq> C" for C
+ proof (intro exI conjI strip)
+ have "inj_on (\<lambda>S. F S - C) \<U>"
+ using pwF F
+ unfolding inj_on_def pairwise_def disjnt_iff
+ by (metis Diff_iff UU UnionI nonempty subset_empty subset_eq \<open>C \<subseteq> S\<close>)
+ then show "(\<lambda>S. F S - C) ` \<U> \<approx> \<U>"
+ by simp
+ show "pairwise (separatedin X) ((\<lambda>S. F S - C) ` \<U>)"
+ using \<open>closedin X C\<close> F pwF by (force simp: pairwise_def openin_diff separatedin_open_sets disjnt_iff)
+ show "{} \<notin> (\<lambda>S. F S - C) ` \<U>"
+ using nonempty UU \<open>C \<subseteq> S\<close> F
+ by clarify (metis DiffD2 Diff_eq_empty_iff F UnionI subset_empty subset_eq)
+ show "(\<Union>S\<in>\<U>. F S - C) = topspace X - C"
+ using UU F C openin_subset by fastforce
+ qed
+ qed
+qed
+
+lemma separation_by_closed_intermediates_gen:
+ assumes X: "hereditarily normal_space X"
+ and discon: "\<not> connectedin X (topspace X - S)"
+ obtains C where "closedin X C" "C \<subseteq> S"
+ "\<And>D. \<lbrakk>closedin X D; C \<subseteq> D; D \<subseteq> S\<rbrakk> \<Longrightarrow> \<not> connectedin X (topspace X - D)"
+proof -
+ obtain C1 C2 where Ueq: "C1 \<union> C2 = topspace X - S" and "C1 \<noteq> {}" "C2 \<noteq> {}"
+ and sep: "separatedin X C1 C2" and "C1 \<noteq> C2"
+ by (metis Diff_subset connectedin_eq_not_separated discon separatedin_refl)
+ then obtain C where "closedin X C" "C \<subseteq> S"
+ and C: "\<And>D. \<lbrakk>closedin X D; C \<subseteq> D; D \<subseteq> S\<rbrakk>
+ \<Longrightarrow> \<exists>\<V>. \<V> \<approx> {C1,C2} \<and> pairwise (separatedin X) \<V> \<and> {} \<notin> \<V> \<and> \<Union>\<V> = topspace X - D"
+ using separation_by_closed_intermediates_count [of X "{C1,C2}" S] X
+ apply (simp add: pairwise_insert separatedin_sym)
+ by metis
+ have "\<not> connectedin X (topspace X - D)"
+ if D: "closedin X D" "C \<subseteq> D" "D \<subseteq> S" for D
+ proof -
+ obtain V1 V2 where *: "pairwise (separatedin X) {V1,V2}" "{} \<notin> {V1,V2}"
+ "\<Union>{V1,V2} = topspace X - D" "V1\<noteq>V2"
+ by (metis C [OF D] \<open>C1 \<noteq> C2\<close> eqpoll_doubleton_iff)
+ then have "disjnt V1 V2"
+ by (metis pairwise_insert separatedin_imp_disjoint singleton_iff)
+ with * show ?thesis
+ by (auto simp add: connectedin_eq_not_separated pairwise_insert)
+ qed
+ then show thesis
+ using \<open>C \<subseteq> S\<close> \<open>closedin X C\<close> that by auto
+qed
+
+lemma separation_by_closed_intermediates_eq_count:
+ fixes n::nat
+ assumes lcX: "locally_connected_space X" and hnX: "hereditarily normal_space X"
+ shows "(\<exists>\<U>. \<U> \<approx> {..<n} \<and> pairwise (separatedin X) \<U> \<and> {} \<notin> \<U> \<and> \<Union>\<U> = topspace X - S) \<longleftrightarrow>
+ (\<exists>C. closedin X C \<and> C \<subseteq> S \<and>
+ (\<forall>D. closedin X D \<and> C \<subseteq> D \<and> D \<subseteq> S
+ \<longrightarrow> (\<exists>\<U>. \<U> \<approx> {..<n} \<and> pairwise (separatedin X) \<U> \<and> {} \<notin> \<U> \<and> \<Union>\<U> = topspace X - D)))"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs then show ?rhs
+ by (smt (verit, best) hnX separation_by_closed_intermediates_count eqpoll_iff_finite_card eqpoll_trans)
+next
+ assume R: ?rhs
+ show ?lhs
+ proof (cases "n=0")
+ case True
+ with R show ?thesis
+ by fastforce
+ next
+ case False
+ obtain C where "closedin X C" "C \<subseteq> S"
+ and C: "\<And>D. \<lbrakk>closedin X D; C \<subseteq> D; D \<subseteq> S\<rbrakk>
+ \<Longrightarrow> \<exists>\<U>. \<U> \<approx> {..<n} \<and> pairwise (separatedin X) \<U> \<and> {} \<notin> \<U> \<and> \<Union>\<U> = topspace X - D"
+ using R by force
+ then have "C \<subseteq> topspace X"
+ by (simp add: closedin_subset)
+ define \<U> where "\<U> \<equiv> {D \<in> connected_components_of (subtopology X (topspace X - C)). D-S \<noteq> {}}"
+ have ope\<U>: "openin X U" if "U \<in> \<U>" for U
+ using that \<open>closedin X C\<close> lcX locally_connected_space_open_connected_components
+ by (fastforce simp add: closedin_def \<U>_def)
+ have "{} \<notin> \<U>"
+ by (auto simp: \<U>_def)
+ have "pairwise disjnt \<U>"
+ using connected_components_of_disjoint by (fastforce simp add: pairwise_def \<U>_def)
+ show ?lhs
+ proof (rule ccontr)
+ assume con: "\<nexists>\<U>. \<U> \<approx> {..<n} \<and> pairwise (separatedin X) \<U> \<and> {} \<notin> \<U> \<and> \<Union>\<U> = topspace X - S"
+ have card\<U>: "finite \<U> \<and> card \<U> < n"
+ proof (rule ccontr)
+ assume "\<not> (finite \<U> \<and> card \<U> < n)"
+ then obtain \<V> where "\<V> \<subseteq> \<U>" "finite \<V>" "card \<V> = n"
+ by (metis infinite_arbitrarily_large linorder_not_less obtain_subset_with_card_n)
+ then obtain T where "T \<in> \<V>"
+ using False by force
+ define \<W> where "\<W> \<equiv> insert (topspace X - S - \<Union>(\<V> - {T})) ((\<lambda>D. D - S) ` (\<V> - {T}))"
+ have "\<Union>\<W> = topspace X - S"
+ using \<open>\<And>U. U \<in> \<U> \<Longrightarrow> openin X U\<close> \<open>\<V> \<subseteq> \<U>\<close> topspace_def by (fastforce simp: \<W>_def)
+ moreover have "{} \<notin> \<W>"
+ proof -
+ obtain a where "a \<in> T" "a \<notin> S"
+ using \<U>_def \<open>T \<in> \<V>\<close> \<open>\<V> \<subseteq> \<U>\<close> by blast
+ then have "a \<in> topspace X"
+ using \<open>T \<in> \<V>\<close> ope\<U> \<open>\<V> \<subseteq> \<U>\<close> openin_subset by blast
+ moreover have "a \<notin> \<Union>(\<V> - {T})"
+ using diff_Union_pairwise_disjoint [of \<V> "{T}"] \<open>disjoint \<U>\<close> pairwise_subset \<open>T \<in> \<V>\<close> \<open>\<V> \<subseteq> \<U>\<close> \<open>a \<in> T\<close>
+ by auto
+ ultimately have "topspace X - S - \<Union>(\<V> - {T}) \<noteq> {}"
+ using \<open>a \<notin> S\<close> by blast
+ moreover have "\<And>V. V \<in> \<V> - {T} \<Longrightarrow> V - S \<noteq> {}"
+ using \<U>_def \<open>\<V> \<subseteq> \<U>\<close> by blast
+ ultimately show ?thesis
+ by (metis (no_types, lifting) \<W>_def image_iff insert_iff)
+ qed
+ moreover have "disjoint \<V>"
+ using \<open>\<V> \<subseteq> \<U>\<close> \<open>disjoint \<U>\<close> pairwise_subset by blast
+ then have inj: "inj_on (\<lambda>D. D - S) (\<V> - {T})"
+ unfolding inj_on_def using \<open>\<V> \<subseteq> \<U>\<close> disjointD \<U>_def inf_commute by blast
+ have "finite \<W>" "card \<W> = n"
+ using \<open>{} \<notin> \<W>\<close> \<open>n \<noteq> 0\<close> \<open>T \<in> \<V>\<close>
+ by (auto simp add: \<W>_def \<open>finite \<V>\<close> card_insert_if card_image inj \<open>card \<V> = n\<close>)
+ moreover have "pairwise (separatedin X) \<W>"
+ proof -
+ have "disjoint \<W>"
+ using \<open>disjoint \<V>\<close> by (auto simp: \<W>_def pairwise_def disjnt_iff)
+ have "pairwise (separatedin (subtopology X (topspace X - S))) \<W>"
+ proof (intro pairwiseI)
+ fix A B
+ assume \<section>: "A \<in> \<W>" "B \<in> \<W>" "A \<noteq> B"
+ then have "disjnt A B"
+ by (meson \<open>disjoint \<W>\<close> pairwiseD)
+ have "closedin (subtopology X (topspace X - C)) (\<Union>(\<V> - {T}))"
+ using \<U>_def \<open>\<V> \<subseteq> \<U>\<close> closedin_connected_components_of \<open>finite \<V>\<close>
+ by (force simp add: intro!: closedin_Union)
+ with \<open>C \<subseteq> S\<close> have "openin (subtopology X (topspace X - S)) (topspace X - S - \<Union>(\<V> - {T}))"
+ by (fastforce simp add: openin_closedin_eq closedin_subtopology Int_absorb1)
+ moreover have "\<And>V. V \<in> \<V> \<and> V\<noteq>T \<Longrightarrow> openin (subtopology X (topspace X - S)) (V - S)"
+ using \<open>\<V> \<subseteq> \<U>\<close> ope\<U>
+ by (metis IntD2 Int_Diff inf.orderE openin_subset openin_subtopology)
+ ultimately have "openin (subtopology X (topspace X - S)) A" "openin (subtopology X (topspace X - S)) B"
+ using \<section> \<W>_def by blast+
+ with \<open>disjnt A B\<close> show "separatedin (subtopology X (topspace X - S)) A B"
+ using separatedin_open_sets by blast
+ qed
+ then show ?thesis
+ by (simp add: pairwise_def separatedin_subtopology)
+ qed
+ ultimately show False
+ by (metis con eqpoll_iff_finite_card)
+ qed
+ obtain \<V> where "\<V> \<approx> {..<n} " "{} \<notin> \<V>"
+ and pw\<V>: "pairwise (separatedin X) \<V>" and UV: "\<Union>\<V> = topspace X - (topspace X - \<Union>\<U>)"
+ proof -
+ have "closedin X (topspace X - \<Union>\<U>)"
+ using ope\<U> by blast
+ moreover have "C \<subseteq> topspace X - \<Union>\<U>"
+ using \<open>C \<subseteq> topspace X\<close> connected_components_of_subset by (fastforce simp: \<U>_def)
+ moreover have "topspace X - \<Union>\<U> \<subseteq> S"
+ using Union_connected_components_of [of "subtopology X (topspace X - C)"] \<open>C \<subseteq> S\<close>
+ by (auto simp: \<U>_def)
+ ultimately show thesis
+ by (metis C that)
+ qed
+ have "\<V> \<lesssim> \<U>"
+ proof (rule lepoll_relational_full)
+ have "\<Union>\<V> = \<Union>\<U>"
+ by (simp add: Sup_le_iff UV double_diff ope\<U> openin_subset)
+ then show "\<exists>U. U \<in> \<U> \<and> \<not> disjnt U V" if "V \<in> \<V>" for V
+ using that
+ by (metis \<open>{} \<notin> \<V>\<close> disjnt_Union1 disjnt_self_iff_empty)
+ show "C1 = C2"
+ if "T \<in> \<U>" and "C1 \<in> \<V>" and "C2 \<in> \<V>" and "\<not> disjnt T C1" and "\<not> disjnt T C2" for T C1 C2
+ proof (cases "C1=C2")
+ case False
+ then have "connectedin X T"
+ using \<U>_def connectedin_connected_components_of connectedin_subtopology \<open>T \<in> \<U>\<close> by blast
+ have "T \<subseteq> C1 \<union> \<Union>(\<V> - {C1})"
+ using \<open>\<Union>\<V> = \<Union>\<U>\<close> \<open>T \<in> \<U>\<close> by auto
+ with \<open>connectedin X T\<close>
+ have "\<not> separatedin X C1 (\<Union>(\<V> - {C1}))"
+ unfolding connectedin_eq_not_separated_subset
+ by (smt (verit) that False disjnt_def UnionI disjnt_iff insertE insert_Diff)
+ with that show ?thesis
+ by (metis (no_types, lifting) \<open>\<V> \<approx> {..<n}\<close> eqpoll_iff_finite_card finite_Diff pairwiseD pairwise_alt pw\<V> separatedin_Union(1) separatedin_def)
+ qed auto
+ qed
+ then show False
+ by (metis \<open>\<V> \<approx> {..<n}\<close> card\<U> eqpoll_iff_finite_card leD lepoll_iff_card_le)
+ qed
+ qed
+qed
+
+lemma separation_by_closed_intermediates_eq_gen:
+ assumes "locally_connected_space X" "hereditarily normal_space X"
+ shows "\<not> connectedin X (topspace X - S) \<longleftrightarrow>
+ (\<exists>C. closedin X C \<and> C \<subseteq> S \<and>
+ (\<forall>D. closedin X D \<and> C \<subseteq> D \<and> D \<subseteq> S \<longrightarrow> \<not> connectedin X (topspace X - D)))"
+ (is "?lhs = ?rhs")
+proof -
+ have *: "(\<exists>\<U>::'a set set. \<U> \<approx> {..<Suc (Suc 0)} \<and> P \<U>) \<longleftrightarrow> (\<exists>A B. A\<noteq>B \<and> P{A,B})" for P
+ by (metis One_nat_def eqpoll_doubleton_iff lessThan_Suc lessThan_empty_iff zero_neq_one)
+ have *: "(\<exists>C1 C2. separatedin X C1 C2 \<and> C1\<noteq>C2 \<and> C1\<noteq>{} \<and> C2\<noteq>{} \<and> C1 \<union> C2 = topspace X - S) \<longleftrightarrow>
+ (\<exists>C. closedin X C \<and> C \<subseteq> S \<and>
+ (\<forall>D. closedin X D \<and> C \<subseteq> D \<and> D \<subseteq> S
+ \<longrightarrow> (\<exists>C1 C2. separatedin X C1 C2 \<and> C1\<noteq>C2 \<and> C1\<noteq>{} \<and> C2\<noteq>{} \<and> C1 \<union> C2 = topspace X - D)))"
+ using separation_by_closed_intermediates_eq_count [OF assms, of "Suc(Suc 0)" S]
+ apply (simp add: * pairwise_insert separatedin_sym cong: conj_cong)
+ apply (simp add: eq_sym_conv conj_ac)
+ done
+ with separatedin_refl
+ show ?thesis
+ apply (simp add: connectedin_eq_not_separated)
+ by (smt (verit, best) separatedin_refl)
+qed
+
+
+
+lemma lepoll_connnected_components_connectedin:
+ assumes "\<And>C. C \<in> \<U> \<Longrightarrow> connectedin X C" "\<Union>\<U> = topspace X"
+ shows "connected_components_of X \<lesssim> \<U>"
+proof -
+ have "connected_components_of X \<lesssim> \<U> - {{}}"
+ proof (rule lepoll_relational_full)
+ show "\<exists>U. U \<in> \<U> - {{}} \<and> U \<subseteq> V"
+ if "V \<in> connected_components_of X" for V
+ using that unfolding connected_components_of_def image_iff
+ by (metis Union_iff assms connected_component_of_maximal empty_iff insert_Diff_single insert_iff)
+ show "V = V'"
+ if "U \<in> \<U> - {{}}" "V \<in> connected_components_of X" "V' \<in> connected_components_of X" "U \<subseteq> V" "U \<subseteq> V'"
+ for U V V'
+ by (metis DiffD2 disjointD insertCI le_inf_iff pairwise_disjoint_connected_components_of subset_empty that)
+ qed
+ also have "\<dots> \<lesssim> \<U>"
+ by (simp add: subset_imp_lepoll)
+ finally show ?thesis .
+qed
+
+lemma lepoll_connected_components_alt:
+ "{..<n::nat} \<lesssim> connected_components_of X \<longleftrightarrow>
+ n = 0 \<or> (\<exists>\<U>. \<U> \<approx> {..<n} \<and> pairwise (separatedin X) \<U> \<and> {} \<notin> \<U> \<and> \<Union>\<U> = topspace X)"
+ (is "?lhs \<longleftrightarrow> ?rhs")
+proof (cases "n=0")
+next
+ case False
+ show ?thesis
+ proof
+ assume L: ?lhs
+ with False show ?rhs
+ proof (induction n rule: less_induct)
+ case (less n)
+ show ?case
+ proof (cases "n\<le>1")
+ case True
+ with less.prems connected_components_of_empty_space show ?thesis
+ by (force simp add: le_Suc_eq eqpoll_iff_finite_card card_Suc_eq simp flip: ex_simps)
+ next
+ case False
+ then have "n-1 \<noteq> 0"
+ by linarith
+ have n1_lesspoll: "{..<n-1} \<prec> {..<n}"
+ using False lesspoll_iff_finite_card by fastforce
+ also have "\<dots> \<lesssim> connected_components_of X"
+ using less by blast
+ finally have "{..<n-1} \<lesssim> connected_components_of X"
+ using lesspoll_imp_lepoll by blast
+ then obtain \<U> where Ueq: "\<U> \<approx> {..<n-1}" and "{} \<notin> \<U>"
+ and pwU: "pairwise (separatedin X) \<U>" and UU: "\<Union>\<U> = topspace X"
+ by (meson \<open>n - 1 \<noteq> 0\<close> diff_less gr0I less zero_less_one)
+ show ?thesis
+ proof (cases "\<forall>C \<in> \<U>. connectedin X C")
+ case True
+ then show ?thesis
+ using lepoll_connnected_components_connectedin [of \<U> X] less.prems
+ by (metis UU Ueq lepoll_antisym lepoll_trans lepoll_trans2 lesspoll_def n1_lesspoll)
+ next
+ case False
+ with UU obtain C A B where ABC: "C \<in> \<U>" "A \<union> B = C" "A \<noteq> {}" "B \<noteq> {}" and sep: "separatedin X A B"
+ by (fastforce simp add: connectedin_eq_not_separated)
+ define \<V> where "\<V> \<equiv> insert A (insert B (\<U> - {C}))"
+ have "\<V> \<approx> {..<n}"
+ proof -
+ have "A \<noteq> B"
+ using \<open>B \<noteq> {}\<close> sep by auto
+ moreover obtain "A \<notin> \<U>" "B \<notin> \<U>"
+ using pwU unfolding pairwise_def
+ by (metis ABC sep separatedin_Un(1) separatedin_refl separatedin_sym)
+ moreover have "card \<U> = n-1" "finite \<U>"
+ using Ueq eqpoll_iff_finite_card by blast+
+ ultimately
+ have "card (insert A (insert B (\<U> - {C}))) = n"
+ using \<open>C \<in> \<U>\<close> by (auto simp add: card_insert_if)
+ then show ?thesis
+ using \<V>_def \<open>finite \<U>\<close> eqpoll_iff_finite_card by blast
+ qed
+ moreover have "{} \<notin> \<V>"
+ using ABC \<V>_def \<open>{} \<notin> \<U>\<close> by blast
+ moreover have "\<Union>\<V> = topspace X"
+ using ABC UU \<V>_def by auto
+ moreover have "pairwise (separatedin X) \<V>"
+ using pwU sep ABC unfolding \<V>_def
+ apply (simp add: separatedin_sym pairwise_def)
+ by (metis member_remove remove_def separatedin_Un(1))
+ ultimately show ?thesis
+ by blast
+ qed
+ qed
+ qed
+ next
+ assume ?rhs
+ then obtain \<U> where "\<U> \<approx> {..<n}" "{} \<notin> \<U>" and pwU: "pairwise (separatedin X) \<U>" and UU: "\<Union>\<U> = topspace X"
+ using False by force
+ have "card (connected_components_of X) \<ge> n" if "finite (connected_components_of X)"
+ proof -
+ have "\<U> \<lesssim> connected_components_of X"
+ proof (rule lepoll_relational_full)
+ show "\<exists>T. T \<in> connected_components_of X \<and> \<not> disjnt T C" if "C \<in> \<U>" for C
+ by (metis that UU Union_connected_components_of Union_iff \<open>{} \<notin> \<U>\<close> disjnt_iff equals0I)
+ show "(C1::'a set) = C2"
+ if "T \<in> connected_components_of X" and "C1 \<in> \<U>" "C2 \<in> \<U>" "\<not> disjnt T C1" "\<not> disjnt T C2" for T C1 C2
+ proof (rule ccontr)
+ assume "C1 \<noteq> C2"
+ then have "connectedin X T"
+ by (simp add: connectedin_connected_components_of that(1))
+ moreover have "\<not> separatedin X C1 (\<Union>(\<U> - {C1}))"
+ using \<open>connectedin X T\<close> pwU unfolding pairwise_def
+ by (smt (verit) Sup_upper UU Union_connected_components_of \<open>C1 \<noteq> C2\<close> complete_lattice_class.Sup_insert connectedin_subset_separated_union disjnt_subset2 disjnt_sym insert_Diff separatedin_imp_disjoint that)
+ ultimately show False
+ using \<open>\<U> \<approx> {..<n}\<close>
+ apply (simp add: connectedin_eq_not_separated_subset eqpoll_iff_finite_card)
+ by (metis Sup_upper UU finite_Diff pairwise_alt pwU separatedin_Union(1) that(2))
+ qed
+ qed
+ then show ?thesis
+ by (metis \<open>\<U> \<approx> {..<n}\<close> eqpoll_iff_finite_card lepoll_iff_card_le that)
+ qed
+ then show ?lhs
+ by (metis card_lessThan finite_lepoll_infinite finite_lessThan lepoll_iff_card_le)
+ qed
+qed auto
+
+
+subsection\<open>A perfect set in common cases must have at least the cardinality of the continuum\<close>
+
+lemma (in Metric_space) lepoll_perfect_set:
+ assumes "mcomplete"
+ and "mtopology derived_set_of S = S" "S \<noteq> {}"
+ shows "(UNIV::real set) \<lesssim> S"
+proof -
+ have "S \<subseteq> M"
+ using assms(2) derived_set_of_infinite_mball by blast
+ have "(UNIV::real set) \<lesssim> (UNIV::nat set set)"
+ using eqpoll_imp_lepoll eqpoll_sym nat_sets_eqpoll_reals by blast
+ also have "\<dots> \<lesssim> S"
+ proof -
+ have "\<exists>y z \<delta>. y \<in> S \<and> z \<in> S \<and> 0 < \<delta> \<and> \<delta> < \<epsilon>/2 \<and>
+ mcball y \<delta> \<subseteq> mcball x \<epsilon> \<and> mcball z \<delta> \<subseteq> mcball x \<epsilon> \<and> disjnt (mcball y \<delta>) (mcball z \<delta>)"
+ if "x \<in> S" "0 < \<epsilon>" for x \<epsilon>
+ proof -
+ define S' where "S' \<equiv> S \<inter> mball x (\<epsilon>/4)"
+ have "infinite S'"
+ using derived_set_of_infinite_mball [of S] assms that S'_def
+ by (smt (verit, ccfv_SIG) mem_Collect_eq zero_less_divide_iff)
+ then have "\<And>x y z. \<not> (S' \<subseteq> {x,y,z})"
+ using finite_subset by auto
+ then obtain l r where lr: "l \<in> S'" "r \<in> S'" "l\<noteq>r" "l\<noteq>x" "r\<noteq>x"
+ by (metis insert_iff subsetI)
+ show ?thesis
+ proof (intro exI conjI)
+ show "l \<in> S" "r \<in> S" "d l r / 3 > 0"
+ using lr by (auto simp: S'_def)
+ show "d l r / 3 < \<epsilon>/2" "mcball l (d l r / 3) \<subseteq> mcball x \<epsilon>" "mcball r (d l r / 3) \<subseteq> mcball x \<epsilon>"
+ using lr by (clarsimp simp: S'_def, smt (verit) commute triangle'')+
+ show "disjnt (mcball l (d l r / 3)) (mcball r (d l r / 3))"
+ using lr by (simp add: S'_def disjnt_iff) (smt (verit, best) mdist_pos_less triangle')
+ qed
+ qed
+ then obtain l r \<delta>
+ where lrS: "\<And>x \<epsilon>. \<lbrakk>x \<in> S; 0 < \<epsilon>\<rbrakk> \<Longrightarrow> l x \<epsilon> \<in> S \<and> r x \<epsilon> \<in> S"
+ and \<delta>: "\<And>x \<epsilon>. \<lbrakk>x \<in> S; 0 < \<epsilon>\<rbrakk> \<Longrightarrow> 0 < \<delta> x \<epsilon> \<and> \<delta> x \<epsilon> < \<epsilon>/2"
+ and "\<And>x \<epsilon>. \<lbrakk>x \<in> S; 0 < \<epsilon>\<rbrakk> \<Longrightarrow> mcball (l x \<epsilon>) (\<delta> x \<epsilon>) \<subseteq> mcball x \<epsilon> \<and> mcball (r x \<epsilon>) (\<delta> x \<epsilon>) \<subseteq> mcball x \<epsilon> \<and>
+ disjnt (mcball (l x \<epsilon>) (\<delta> x \<epsilon>)) (mcball (r x \<epsilon>) (\<delta> x \<epsilon>))"
+ by metis
+ then have lr_mcball: "\<And>x \<epsilon>. \<lbrakk>x \<in> S; 0 < \<epsilon>\<rbrakk> \<Longrightarrow> mcball (l x \<epsilon>) (\<delta> x \<epsilon>) \<subseteq> mcball x \<epsilon> \<and> mcball (r x \<epsilon>) (\<delta> x \<epsilon>) \<subseteq> mcball x \<epsilon> "
+ and lr_disjnt: "\<And>x \<epsilon>. \<lbrakk>x \<in> S; 0 < \<epsilon>\<rbrakk> \<Longrightarrow> disjnt (mcball (l x \<epsilon>) (\<delta> x \<epsilon>)) (mcball (r x \<epsilon>) (\<delta> x \<epsilon>))"
+ by metis+
+ obtain a where "a \<in> S"
+ using \<open>S \<noteq> {}\<close> by blast
+ define xe where "xe \<equiv>
+ \<lambda>B. rec_nat (a,1) (\<lambda>n (x,\<gamma>). ((if n\<in>B then r else l) x \<gamma>, \<delta> x \<gamma>))"
+ have [simp]: "xe b 0 = (a,1)" for b
+ by (simp add: xe_def)
+ have "xe B (Suc n) = (let (x,\<gamma>) = xe B n in ((if n\<in>B then r else l) x \<gamma>, \<delta> x \<gamma>))" for B n
+ by (simp add: xe_def)
+ define x where "x \<equiv> \<lambda>B n. fst (xe B n)"
+ define \<gamma> where "\<gamma> \<equiv> \<lambda>B n. snd (xe B n)"
+ have [simp]: "x B 0 = a" "\<gamma> B 0 = 1" for B
+ by (simp_all add: x_def \<gamma>_def xe_def)
+ have x_Suc[simp]: "x B (Suc n) = ((if n\<in>B then r else l) (x B n) (\<gamma> B n))"
+ and \<gamma>_Suc[simp]: "\<gamma> B (Suc n) = \<delta> (x B n) (\<gamma> B n)" for B n
+ by (simp_all add: x_def \<gamma>_def xe_def split: prod.split)
+ interpret Submetric M d S
+ proof qed (use \<open>S \<subseteq> M\<close> in metis)
+ have "closedin mtopology S"
+ by (metis assms(2) closure_of closure_of_eq inf.absorb_iff2 subset subset_Un_eq subset_refl topspace_mtopology)
+ with \<open>mcomplete\<close>
+ have "sub.mcomplete"
+ by (metis closedin_mcomplete_imp_mcomplete)
+ have *: "x B n \<in> S \<and> \<gamma> B n > 0" for B n
+ by (induction n) (auto simp: \<open>a \<in> S\<close> lrS \<delta>)
+ with subset have E: "x B n \<in> M" for B n
+ by blast
+ have \<gamma>_le: "\<gamma> B n \<le> (1/2)^n" for B n
+ proof(induction n)
+ case 0 then show ?case by auto
+ next
+ case (Suc n)
+ then show ?case
+ by simp (smt (verit) "*" \<delta> field_sum_of_halves)
+ qed
+ { fix B
+ have "\<And>n. sub.mcball (x B (Suc n)) (\<gamma> B (Suc n)) \<subseteq> sub.mcball (x B n) (\<gamma> B n)"
+ by (smt (verit, best) "*" Int_iff \<gamma>_Suc x_Suc in_mono lr_mcball mcball_submetric_eq subsetI)
+ then have mon: "monotone (\<le>) (\<lambda>x y. y \<subseteq> x) (\<lambda>n. sub.mcball (x B n) (\<gamma> B n))"
+ by (simp add: decseq_SucI)
+ have "\<exists>n a. sub.mcball (x B n) (\<gamma> B n) \<subseteq> sub.mcball a \<epsilon>" if "\<epsilon>>0" for \<epsilon>
+ proof -
+ obtain n where "(1/2)^n < \<epsilon>"
+ using \<open>0 < \<epsilon>\<close> real_arch_pow_inv by force
+ with \<gamma>_le have \<epsilon>: "\<gamma> B n \<le> \<epsilon>"
+ by (smt (verit))
+ show ?thesis
+ proof (intro exI)
+ show "sub.mcball (x B n) (\<gamma> B n) \<subseteq> sub.mcball (x B n) \<epsilon>"
+ by (simp add: \<epsilon> sub.mcball_subset_concentric)
+ qed
+ qed
+ then have "\<exists>l. l \<in> S \<and> (\<Inter>n. sub.mcball (x B n) (\<gamma> B n)) = {l}"
+ using \<open>sub.mcomplete\<close> mon
+ unfolding sub.mcomplete_nest_sing
+ apply (drule_tac x="\<lambda>n. sub.mcball (x B n) (\<gamma> B n)" in spec)
+ by (meson * order.asym sub.closedin_mcball sub.mcball_eq_empty)
+ }
+ then obtain z where z: "\<And>B. z B \<in> S \<and> (\<Inter>n. sub.mcball (x B n) (\<gamma> B n)) = {z B}"
+ by metis
+ show ?thesis
+ unfolding lepoll_def
+ proof (intro exI conjI)
+ show "inj z"
+ proof (rule inj_onCI)
+ fix B C
+ assume eq: "z B = z C" and "B \<noteq> C"
+ then have ne: "sym_diff B C \<noteq> {}"
+ by blast
+ define n where "n \<equiv> LEAST k. k \<in> (sym_diff B C)"
+ with ne have n: "n \<in> sym_diff B C"
+ by (metis Inf_nat_def1 LeastI)
+ then have non: "n \<in> B \<longleftrightarrow> n \<notin> C"
+ by blast
+ have H: "z C \<in> sub.mcball (x B (Suc n)) (\<gamma> B (Suc n)) \<and> z C \<in> sub.mcball (x C (Suc n)) (\<gamma> C (Suc n))"
+ using z [of B] z [of C] apply (simp add: lrS set_eq_iff non *)
+ by (smt (verit, best) \<gamma>_Suc eq non x_Suc)
+ have "k \<in> B \<longleftrightarrow> k \<in> C" if "k<n" for k
+ using that unfolding n_def by (meson DiffI UnCI not_less_Least)
+ moreover have "(\<forall>m. m < p \<longrightarrow> (m \<in> B \<longleftrightarrow> m \<in> C)) \<Longrightarrow> x B p = x C p \<and> \<gamma> B p = \<gamma> C p" for p
+ by (induction p) auto
+ ultimately have "x B n = x C n" "\<gamma> B n = \<gamma> C n"
+ by blast+
+ then show False
+ using lr_disjnt * H non
+ by (smt (verit) IntD2 \<gamma>_Suc disjnt_iff mcball_submetric_eq x_Suc)
+ qed
+ show "range z \<subseteq> S"
+ using z by blast
+ qed
+ qed
+ finally show ?thesis .
+qed
+
+lemma lepoll_perfect_set_aux:
+ assumes lcX: "locally_compact_space X" and hsX: "Hausdorff_space X"
+ and eq: "X derived_set_of topspace X = topspace X" and "topspace X \<noteq> {}"
+ shows "(UNIV::real set) \<lesssim> topspace X"
+proof -
+ have "(UNIV::real set) \<lesssim> (UNIV::nat set set)"
+ using eqpoll_imp_lepoll eqpoll_sym nat_sets_eqpoll_reals by blast
+ also have "\<dots> \<lesssim> topspace X"
+ proof -
+ obtain z where z: "z \<in> topspace X"
+ using assms by blast
+ then obtain U K where "openin X U" "compactin X K" "U \<noteq> {}" "U \<subseteq> K"
+ by (metis emptyE lcX locally_compact_space_def)
+ then have "closedin X K"
+ by (simp add: compactin_imp_closedin hsX)
+ have intK_ne: "X interior_of K \<noteq> {}"
+ using \<open>U \<noteq> {}\<close> \<open>U \<subseteq> K\<close> \<open>openin X U\<close> interior_of_eq_empty by blast
+ have "\<exists>D E. closedin X D \<and> D \<subseteq> K \<and> X interior_of D \<noteq> {} \<and>
+ closedin X E \<and> E \<subseteq> K \<and> X interior_of E \<noteq> {} \<and>
+ disjnt D E \<and> D \<subseteq> C \<and> E \<subseteq> C"
+ if "closedin X C" "C \<subseteq> K" and C: "X interior_of C \<noteq> {}" for C
+ proof -
+ obtain z where z: "z \<in> X interior_of C" "z \<in> topspace X"
+ using C interior_of_subset_topspace by fastforce
+ obtain x y where "x \<in> X interior_of C" "y \<in> X interior_of C" "x\<noteq>y"
+ by (metis z eq in_derived_set_of openin_interior_of)
+ then have "x \<in> topspace X" "y \<in> topspace X"
+ using interior_of_subset_topspace by force+
+ with hsX obtain V W where "openin X V" "openin X W" "x \<in> V" "y \<in> W" "disjnt V W"
+ by (metis Hausdorff_space_def \<open>x \<noteq> y\<close>)
+ have *: "\<And>W x. openin X W \<and> x \<in> W
+ \<Longrightarrow> \<exists>U V. openin X U \<and> closedin X V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W"
+ using lcX hsX locally_compact_Hausdorff_imp_regular_space neighbourhood_base_of_closedin neighbourhood_base_of
+ by metis
+ obtain M D where MD: "openin X M" "closedin X D" "y \<in> M" "M \<subseteq> D" "D \<subseteq> X interior_of C \<inter> W"
+ using * [of "X interior_of C \<inter> W" y]
+ using \<open>openin X W\<close> \<open>y \<in> W\<close> \<open>y \<in> X interior_of C\<close> by fastforce
+ obtain N E where NE: "openin X N" "closedin X E" "x \<in> N" "N \<subseteq> E" "E \<subseteq> X interior_of C \<inter> V"
+ using * [of "X interior_of C \<inter> V" x]
+ using \<open>openin X V\<close> \<open>x \<in> V\<close> \<open>x \<in> X interior_of C\<close> by fastforce
+ show ?thesis
+ proof (intro exI conjI)
+ show "X interior_of D \<noteq> {}" "X interior_of E \<noteq> {}"
+ using MD NE by (fastforce simp: interior_of_def)+
+ show "disjnt D E"
+ by (meson MD(5) NE(5) \<open>disjnt V W\<close> disjnt_subset1 disjnt_sym le_inf_iff)
+ qed (use MD NE \<open>C \<subseteq> K\<close> interior_of_subset in force)+
+ qed
+ then obtain L R where
+ LR: "\<And>C. \<lbrakk>closedin X C; C \<subseteq> K; X interior_of C \<noteq> {}\<rbrakk>
+ \<Longrightarrow> closedin X (L C) \<and> (L C) \<subseteq> K \<and> X interior_of (L C) \<noteq> {} \<and>
+ closedin X (R C) \<and> (R C) \<subseteq> K \<and> X interior_of (R C) \<noteq> {}"
+ and disjLR: "\<And>C. \<lbrakk>closedin X C; C \<subseteq> K; X interior_of C \<noteq> {}\<rbrakk>
+ \<Longrightarrow> disjnt (L C) (R C) \<and> (L C) \<subseteq> C \<and> (R C) \<subseteq> C"
+ by metis
+ define d where "d \<equiv> \<lambda>B. rec_nat K (\<lambda>n. if n \<in> B then R else L)"
+ have d0[simp]: "d B 0 = K" for B
+ by (simp add: d_def)
+ have [simp]: "d B (Suc n) = (if n \<in> B then R else L) (d B n)" for B n
+ by (simp add: d_def)
+ have d_correct: "closedin X (d B n) \<and> d B n \<subseteq> K \<and> X interior_of (d B n) \<noteq> {}" for B n
+ proof (induction n)
+ case 0
+ then show ?case by (auto simp: \<open>closedin X K\<close> intK_ne)
+ next
+ case (Suc n) with LR show ?case by auto
+ qed
+ have "(\<Inter>n. d B n) \<noteq> {}" for B
+ proof (rule compact_space_imp_nest)
+ show "compact_space (subtopology X K)"
+ by (simp add: \<open>compactin X K\<close> compact_space_subtopology)
+ show "closedin (subtopology X K) (d B n)" for n :: nat
+ by (simp add: closedin_subset_topspace d_correct)
+ show "d B n \<noteq> {}" for n :: nat
+ by (metis d_correct interior_of_empty)
+ show "antimono (d B)"
+ proof (rule antimonoI [OF transitive_stepwise_le])
+ fix n
+ show "d B (Suc n) \<subseteq> d B n"
+ by (simp add: d_correct disjLR)
+ qed auto
+ qed
+ then obtain x where x: "\<And>B. x B \<in> (\<Inter>n. d B n)"
+ unfolding set_eq_iff by (metis empty_iff)
+ show ?thesis
+ unfolding lepoll_def
+ proof (intro exI conjI)
+ show "inj x"
+ proof (rule inj_onCI)
+ fix B C
+ assume eq: "x B = x C" and "B\<noteq>C"
+ then have ne: "sym_diff B C \<noteq> {}"
+ by blast
+ define n where "n \<equiv> LEAST k. k \<in> (sym_diff B C)"
+ with ne have n: "n \<in> sym_diff B C"
+ by (metis Inf_nat_def1 LeastI)
+ then have non: "n \<in> B \<longleftrightarrow> n \<notin> C"
+ by blast
+ have "k \<in> B \<longleftrightarrow> k \<in> C" if "k<n" for k
+ using that unfolding n_def by (meson DiffI UnCI not_less_Least)
+ moreover have "(\<forall>m. m < p \<longrightarrow> (m \<in> B \<longleftrightarrow> m \<in> C)) \<Longrightarrow> d B p = d C p" for p
+ by (induction p) auto
+ ultimately have "d B n = d C n"
+ by blast
+ then have "disjnt (d B (Suc n)) (d C (Suc n))"
+ by (simp add: d_correct disjLR disjnt_sym non)
+ then show False
+ by (metis InterE disjnt_iff eq rangeI x)
+ qed
+ show "range x \<subseteq> topspace X"
+ using x d0 \<open>compactin X K\<close> compactin_subset_topspace d_correct by fastforce
+ qed
+ qed
+ finally show ?thesis .
+qed
+
+lemma lepoll_perfect_set:
+ assumes X: "completely_metrizable_space X \<or> locally_compact_space X \<and> Hausdorff_space X"
+ and S: "X derived_set_of S = S" "S \<noteq> {}"
+ shows "(UNIV::real set) \<lesssim> S"
+ using X
+proof
+ assume "completely_metrizable_space X"
+ with assms show "(UNIV::real set) \<lesssim> S"
+ by (metis Metric_space.lepoll_perfect_set completely_metrizable_space_def)
+next
+ assume "locally_compact_space X \<and> Hausdorff_space X"
+ then show "(UNIV::real set) \<lesssim> S"
+ using lepoll_perfect_set_aux [of "subtopology X S"]
+ by (metis Hausdorff_space_subtopology S closedin_derived_set_of closedin_subset derived_set_of_subtopology
+ locally_compact_space_closed_subset subtopology_topspace topspace_subtopology topspace_subtopology_subset)
+qed
+
+
+
+
+lemma Kuratowski_aux1:
+ assumes "\<And>S T. R S T \<Longrightarrow> R T S"
+ shows "(\<forall>S T n. R S T \<longrightarrow> (f S \<approx> {..<n::nat} \<longleftrightarrow> f T \<approx> {..<n::nat})) \<longleftrightarrow>
+ (\<forall>n S T. R S T \<longrightarrow> {..<n::nat} \<lesssim> f S \<longrightarrow> {..<n::nat} \<lesssim> f T)"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs then show ?rhs
+ by (meson eqpoll_iff_finite_card eqpoll_sym finite_lepoll_infinite finite_lessThan lepoll_trans2)
+next
+ assume ?rhs then show ?lhs
+ by (smt (verit, best) lepoll_iff_finite_card assms eqpoll_iff_finite_card finite_lepoll_infinite
+ finite_lessThan le_Suc_eq lepoll_antisym lepoll_iff_card_le not_less_eq_eq)
+qed
+
+lemma Kuratowski_aux2:
+ "pairwise (separatedin (subtopology X (topspace X - S))) \<U> \<and> {} \<notin> \<U> \<and>
+ \<Union>\<U> = topspace(subtopology X (topspace X - S)) \<longleftrightarrow>
+ pairwise (separatedin X) \<U> \<and> {} \<notin> \<U> \<and> \<Union>\<U> = topspace X - S"
+ by (auto simp: pairwise_def separatedin_subtopology)
+
+proposition Kuratowski_component_number_invariance_aux:
+ assumes "compact_space X" and HsX: "Hausdorff_space X"
+ and lcX: "locally_connected_space X" and hnX: "hereditarily normal_space X"
+ and hom: "(subtopology X S) homeomorphic_space (subtopology X T)"
+ and leXS: "{..<n::nat} \<lesssim> connected_components_of (subtopology X (topspace X - S))"
+ assumes \<section>: "\<And>S T.
+ \<lbrakk>closedin X S; closedin X T; (subtopology X S) homeomorphic_space (subtopology X T);
+ {..<n::nat} \<lesssim> connected_components_of (subtopology X (topspace X - S))\<rbrakk>
+ \<Longrightarrow> {..<n::nat} \<lesssim> connected_components_of (subtopology X (topspace X - T))"
+ shows "{..<n::nat} \<lesssim> connected_components_of (subtopology X (topspace X - T))"
+proof (cases "n=0")
+ case False
+ obtain f g where homf: "homeomorphic_map (subtopology X S) (subtopology X T) f"
+ and homg: "homeomorphic_map (subtopology X T) (subtopology X S) g"
+ and gf: "\<And>x. x \<in> topspace (subtopology X S) \<Longrightarrow> g(f x) = x"
+ and fg: "\<And>y. y \<in> topspace (subtopology X T) \<Longrightarrow> f(g y) = y"
+ and f: "f \<in> topspace (subtopology X S) \<rightarrow> topspace (subtopology X T)"
+ and g: "g \<in> topspace (subtopology X T) \<rightarrow> topspace (subtopology X S)"
+ using homeomorphic_space_unfold hom by metis
+ obtain C where "closedin X C" "C \<subseteq> S"
+ and C: "\<And>D. \<lbrakk>closedin X D; C \<subseteq> D; D \<subseteq> S\<rbrakk>
+ \<Longrightarrow> \<exists>\<U>. \<U> \<approx> {..<n} \<and> pairwise (separatedin X) \<U> \<and> {} \<notin> \<U> \<and> \<Union>\<U> = topspace X - D"
+ using separation_by_closed_intermediates_eq_count [of X n S] assms
+ by (smt (verit, ccfv_threshold) False Kuratowski_aux2 lepoll_connected_components_alt)
+ have "\<exists>C. closedin X C \<and> C \<subseteq> T \<and>
+ (\<forall>D. closedin X D \<and> C \<subseteq> D \<and> D \<subseteq> T
+ \<longrightarrow> (\<exists>\<U>. \<U> \<approx> {..<n} \<and> pairwise (separatedin X) \<U> \<and>
+ {} \<notin> \<U> \<and> \<Union>\<U> = topspace X - D))"
+ proof (intro exI, intro conjI strip)
+ have "compactin X (f ` C)"
+ by (meson \<open>C \<subseteq> S\<close> \<open>closedin X C\<close> assms(1) closedin_compact_space compactin_subtopology homeomorphic_map_compactness_eq homf)
+ then show "closedin X (f ` C)"
+ using \<open>Hausdorff_space X\<close> compactin_imp_closedin by blast
+ show "f ` C \<subseteq> T"
+ by (meson \<open>C \<subseteq> S\<close> \<open>closedin X C\<close> closedin_imp_subset closedin_subset_topspace homeomorphic_map_closedness_eq homf)
+ fix D'
+ assume D': "closedin X D' \<and> f ` C \<subseteq> D' \<and> D' \<subseteq> T"
+ define D where "D \<equiv> g ` D'"
+ have "compactin X D"
+ unfolding D_def
+ by (meson D' \<open>compact_space X\<close> closedin_compact_space compactin_subtopology homeomorphic_map_compactness_eq homg)
+ then have "closedin X D"
+ by (simp add: assms(2) compactin_imp_closedin)
+ moreover have "C \<subseteq> D"
+ using D' D_def \<open>C \<subseteq> S\<close> \<open>closedin X C\<close> closedin_subset gf image_iff by fastforce
+ moreover have "D \<subseteq> S"
+ by (metis D' D_def assms(1) closedin_compact_space compactin_subtopology homeomorphic_map_compactness_eq homg)
+ ultimately obtain \<U> where "\<U> \<approx> {..<n}" "pairwise (separatedin X) \<U>" "{} \<notin> \<U>" "\<Union>\<U> = topspace X - D"
+ using C by meson
+ moreover have "(subtopology X D) homeomorphic_space (subtopology X D')"
+ unfolding homeomorphic_space_def
+ proof (intro exI)
+ have "subtopology X D = subtopology (subtopology X S) D"
+ by (simp add: \<open>D \<subseteq> S\<close> inf.absorb2 subtopology_subtopology)
+ moreover have "subtopology X D' = subtopology (subtopology X T) D'"
+ by (simp add: D' inf.absorb2 subtopology_subtopology)
+ moreover have "homeomorphic_maps (subtopology X T) (subtopology X S) g f"
+ by (simp add: fg gf homeomorphic_maps_map homf homg)
+ ultimately
+ have "homeomorphic_maps (subtopology X D') (subtopology X D) g f"
+ by (metis D' D_def \<open>closedin X D\<close> closedin_subset homeomorphic_maps_subtopologies topspace_subtopology Int_absorb1)
+ then show "homeomorphic_maps (subtopology X D) (subtopology X D') f g"
+ using homeomorphic_maps_sym by blast
+ qed
+ ultimately show "\<exists>\<U>. \<U> \<approx> {..<n} \<and> pairwise (separatedin X) \<U> \<and> {} \<notin> \<U> \<and> \<Union> \<U> = topspace X - D'"
+ by (smt (verit, ccfv_SIG) \<section> D' False \<open>closedin X D\<close> Kuratowski_aux2 lepoll_connected_components_alt)
+ qed
+ then have "\<exists>\<U>. \<U> \<approx> {..<n} \<and>
+ pairwise (separatedin (subtopology X (topspace X - T))) \<U> \<and> {} \<notin> \<U> \<and> \<Union>\<U> = topspace X - T"
+ using separation_by_closed_intermediates_eq_count [of X n T] Kuratowski_aux2 lcX hnX by auto
+ with False show ?thesis
+ using lepoll_connected_components_alt by fastforce
+qed auto
+
+
+theorem Kuratowski_component_number_invariance:
+ assumes "compact_space X" "Hausdorff_space X" "locally_connected_space X" "hereditarily normal_space X"
+ shows "((\<forall>S T n.
+ closedin X S \<and> closedin X T \<and>
+ (subtopology X S) homeomorphic_space (subtopology X T)
+ \<longrightarrow> (connected_components_of
+ (subtopology X (topspace X - S)) \<approx> {..<n::nat} \<longleftrightarrow>
+ connected_components_of
+ (subtopology X (topspace X - T)) \<approx> {..<n::nat})) \<longleftrightarrow>
+ (\<forall>S T n.
+ (subtopology X S) homeomorphic_space (subtopology X T)
+ \<longrightarrow> (connected_components_of
+ (subtopology X (topspace X - S)) \<approx> {..<n::nat} \<longleftrightarrow>
+ connected_components_of
+ (subtopology X (topspace X - T)) \<approx> {..<n::nat})))"
+ (is "?lhs = ?rhs")
+proof
+ assume L: ?lhs
+ then show ?rhs
+ apply (subst (asm) Kuratowski_aux1, use homeomorphic_space_sym in blast)
+ apply (subst Kuratowski_aux1, use homeomorphic_space_sym in blast)
+ apply (blast intro: Kuratowski_component_number_invariance_aux assms)
+ done
+qed blast
+
end
--- a/src/HOL/Library/Equipollence.thy Mon Jul 10 22:06:31 2023 +0200
+++ b/src/HOL/Library/Equipollence.thy Mon Jul 10 22:06:42 2023 +0200
@@ -15,9 +15,18 @@
definition lesspoll :: "'a set \<Rightarrow> 'b set \<Rightarrow> bool" (infixl \<open>\<prec>\<close> 50)
where "A \<prec> B == A \<lesssim> B \<and> ~(A \<approx> B)"
+lemma lepoll_def': "lepoll A B \<equiv> \<exists>f. inj_on f A \<and> f \<in> A \<rightarrow> B"
+ by (simp add: Pi_iff image_subset_iff lepoll_def)
+
+lemma eqpoll_empty_iff_empty [simp]: "A \<approx> {} \<longleftrightarrow> A={}"
+ by (simp add: bij_betw_iff_bijections eqpoll_def)
+
lemma lepoll_empty_iff_empty [simp]: "A \<lesssim> {} \<longleftrightarrow> A = {}"
by (auto simp: lepoll_def)
+lemma not_lesspoll_empty: "\<not> A \<prec> {}"
+ by (simp add: lesspoll_def)
+
(*The HOL Light CARD_LE_RELATIONAL_FULL*)
lemma lepoll_relational_full:
assumes "\<And>y. y \<in> B \<Longrightarrow> \<exists>x. x \<in> A \<and> R x y"
@@ -46,16 +55,36 @@
shows "A \<approx> B \<longleftrightarrow> card A = card B"
using assms by (auto simp: bij_betw_iff_card eqpoll_def)
+lemma eqpoll_singleton_iff: "A \<approx> {x} \<longleftrightarrow> (\<exists>u. A = {u})"
+ by (metis card.infinite card_1_singleton_iff eqpoll_finite_iff eqpoll_iff_card not_less_eq_eq)
+
+lemma eqpoll_doubleton_iff: "A \<approx> {x,y} \<longleftrightarrow> (\<exists>u v. A = {u,v} \<and> (u=v \<longleftrightarrow> x=y))"
+proof (cases "x=y")
+ case True
+ then show ?thesis
+ by (simp add: eqpoll_singleton_iff)
+next
+ case False
+ then show ?thesis
+ by (smt (verit, ccfv_threshold) card_1_singleton_iff card_Suc_eq_finite eqpoll_finite_iff
+ eqpoll_iff_card finite.insertI singleton_iff)
+qed
+
lemma lepoll_antisym:
assumes "A \<lesssim> B" "B \<lesssim> A" shows "A \<approx> B"
using assms unfolding eqpoll_def lepoll_def by (metis Schroeder_Bernstein)
-lemma lepoll_trans [trans]: "\<lbrakk>A \<lesssim> B; B \<lesssim> C\<rbrakk> \<Longrightarrow> A \<lesssim> C"
- apply (clarsimp simp: lepoll_def)
- apply (rename_tac f g)
- apply (rule_tac x="g \<circ> f" in exI)
- apply (auto simp: image_subset_iff inj_on_def)
- done
+lemma lepoll_trans [trans]:
+ assumes "A \<lesssim> B" " B \<lesssim> C" shows "A \<lesssim> C"
+proof -
+ obtain f g where fg: "inj_on f A" "inj_on g B" and "f : A \<rightarrow> B" "g \<in> B \<rightarrow> C"
+ by (metis assms lepoll_def')
+ then have "g \<circ> f \<in> A \<rightarrow> C"
+ by auto
+ with fg show ?thesis
+ unfolding lepoll_def
+ by (metis \<open>f \<in> A \<rightarrow> B\<close> comp_inj_on image_subset_iff_funcset inj_on_subset)
+qed
lemma lepoll_trans1 [trans]: "\<lbrakk>A \<approx> B; B \<lesssim> C\<rbrakk> \<Longrightarrow> A \<lesssim> C"
by (meson card_of_ordLeq eqpoll_iff_card_of_ordIso lepoll_def lepoll_trans ordIso_iff_ordLeq)
@@ -716,8 +745,7 @@
corollary finite_funcset_iff:
"finite(I \<rightarrow>\<^sub>E S) \<longleftrightarrow> (\<exists>a. S \<subseteq> {a}) \<or> I = {} \<or> finite I \<and> finite S"
- apply (auto simp: finite_PiE_iff PiE_eq_empty_iff dest: not_finite_existsD)
- using finite.simps by auto
+ by (fastforce simp: finite_PiE_iff PiE_eq_empty_iff dest: subset_singletonD)
lemma lists_lepoll_mono:
assumes "A \<lesssim> B" shows "lists A \<lesssim> lists B"
--- a/src/HOL/Transcendental.thy Mon Jul 10 22:06:31 2023 +0200
+++ b/src/HOL/Transcendental.thy Mon Jul 10 22:06:42 2023 +0200
@@ -2716,9 +2716,6 @@
lemma floor_log_eq_powr_iff: "x > 0 \<Longrightarrow> b > 1 \<Longrightarrow> \<lfloor>log b x\<rfloor> = k \<longleftrightarrow> b powr k \<le> x \<and> x < b powr (k + 1)"
by (auto simp: floor_eq_iff powr_le_iff less_powr_iff)
-lemma power_of_nat_log_ge: "b > 1 \<Longrightarrow> b ^ nat \<lceil>log b x\<rceil> \<ge> x"
- by (smt (verit) less_log_of_power of_nat_ceiling)
-
lemma floor_log_nat_eq_powr_iff:
fixes b n k :: nat
shows "\<lbrakk> b \<ge> 2; k > 0 \<rbrakk> \<Longrightarrow> floor (log b (real k)) = n \<longleftrightarrow> b^n \<le> k \<and> k < b^(n+1)"
@@ -2806,6 +2803,19 @@
shows "x powr i = (if i \<ge> 0 then x ^ nat i else 1 / x ^ nat (-i))"
by (simp add: assms inverse_eq_divide powr_real_of_int)
+lemma power_of_nat_log_ge: "b > 1 \<Longrightarrow> b ^ nat \<lceil>log b x\<rceil> \<ge> x"
+ by (smt (verit) less_log_of_power of_nat_ceiling)
+
+lemma power_of_nat_log_le:
+ assumes "b > 1" "x\<ge>1"
+ shows "b ^ nat \<lfloor>log b x\<rfloor> \<le> x"
+proof -
+ have "\<lfloor>log b x\<rfloor> \<ge> 0"
+ using assms by auto
+ then show ?thesis
+ by (smt (verit) assms le_log_iff of_int_floor_le powr_int)
+qed
+
definition powr_real :: "real \<Rightarrow> real \<Rightarrow> real"
where [code_abbrev, simp]: "powr_real = Transcendental.powr"