First tranche of the Homology development: Simplices
[dummy commit to run testboard again]
(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr with additions from LCP
License: BSD
*)
theory Function_Topology
imports Topology_Euclidean_Space Abstract_Limits
begin
section \<open>Function Topology\<close>
text \<open>We want to define the general product topology.
The product topology on a product of topological spaces is generated by
the sets which are products of open sets along finitely many coordinates, and the whole
space along the other coordinates. This is the coarsest topology for which the projection
to each factor is continuous.
To form a product of objects in Isabelle/HOL, all these objects should be subsets of a common type
'a. The product is then \<^term>\<open>Pi\<^sub>E I X\<close>, the set of elements from \<open>'i\<close> to \<open>'a\<close> such that the \<open>i\<close>-th
coordinate belongs to \<open>X i\<close> for all \<open>i \<in> I\<close>.
Hence, to form a product of topological spaces, all these spaces should be subsets of a common type.
This means that type classes can not be used to define such a product if one wants to take the
product of different topological spaces (as the type 'a can only be given one structure of
topological space using type classes). On the other hand, one can define different topologies (as
introduced in \<open>thy\<close>) on one type, and these topologies do not need to
share the same maximal open set. Hence, one can form a product of topologies in this sense, and
this works well. The big caveat is that it does not interact well with the main body of
topology in Isabelle/HOL defined in terms of type classes... For instance, continuity of maps
is not defined in this setting.
As the product of different topological spaces is very important in several areas of
mathematics (for instance adeles), I introduce below the product topology in terms of topologies,
and reformulate afterwards the consequences in terms of type classes (which are of course very
handy for applications).
Given this limitation, it looks to me that it would be very beneficial to revamp the theory
of topological spaces in Isabelle/HOL in terms of topologies, and keep the statements involving
type classes as consequences of more general statements in terms of topologies (but I am
probably too naive here).
Here is an example of a reformulation using topologies. Let
@{text [display]
\<open>continuous_map T1 T2 f =
((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
\<and> (f`(topspace T1) \<subseteq> (topspace T2)))\<close>}
be the natural continuity definition of a map from the topology \<open>T1\<close> to the topology \<open>T2\<close>. Then
the current \<open>continuous_on\<close> (with type classes) can be redefined as
@{text [display] \<open>continuous_on s f =
continuous_map (top_of_set s) (topology euclidean) f\<close>}
In fact, I need \<open>continuous_map\<close> to express the continuity of the projection on subfactors
for the product topology, in Lemma~\<open>continuous_on_restrict_product_topology\<close>, and I show
the above equivalence in Lemma~\<open>continuous_map_iff_continuous\<close>.
I only develop the basics of the product topology in this theory. The most important missing piece
is Tychonov theorem, stating that a product of compact spaces is always compact for the product
topology, even when the product is not finite (or even countable).
I realized afterwards that this theory has a lot in common with \<^file>\<open>~~/src/HOL/Library/Finite_Map.thy\<close>.
\<close>
subsection \<open>The product topology\<close>
text \<open>We can now define the product topology, as generated by
the sets which are products of open sets along finitely many coordinates, and the whole
space along the other coordinates. Equivalently, it is generated by sets which are one open
set along one single coordinate, and the whole space along other coordinates. In fact, this is only
equivalent for nonempty products, but for the empty product the first formulation is better
(the second one gives an empty product space, while an empty product should have exactly one
point, equal to \<open>undefined\<close> along all coordinates.
So, we use the first formulation, which moreover seems to give rise to more straightforward proofs.
\<close>
definition%important product_topology::"('i \<Rightarrow> ('a topology)) \<Rightarrow> ('i set) \<Rightarrow> (('i \<Rightarrow> 'a) topology)"
where "product_topology T I =
topology_generated_by {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
abbreviation powertop_real :: "'a set \<Rightarrow> ('a \<Rightarrow> real) topology"
where "powertop_real \<equiv> product_topology (\<lambda>i. euclideanreal)"
text \<open>The total set of the product topology is the product of the total sets
along each coordinate.\<close>
proposition product_topology:
"product_topology X I =
topology
(arbitrary union_of
((finite intersection_of
(\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))
relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i))))"
(is "_ = topology (_ union_of ((_ intersection_of ?\<Psi>) relative_to ?TOP))")
proof -
let ?\<Omega> = "(\<lambda>F. \<exists>Y. F = Pi\<^sub>E I Y \<and> (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)})"
have *: "(finite' intersection_of ?\<Omega>) A = (finite intersection_of ?\<Psi> relative_to ?TOP) A" for A
proof -
have 1: "\<exists>U. (\<exists>\<U>. finite \<U> \<and> \<U> \<subseteq> Collect ?\<Psi> \<and> \<Inter>\<U> = U) \<and> ?TOP \<inter> U = \<Inter>\<U>"
if \<U>: "\<U> \<subseteq> Collect ?\<Omega>" and "finite' \<U>" "A = \<Inter>\<U>" "\<U> \<noteq> {}" for \<U>
proof -
have "\<forall>U \<in> \<U>. \<exists>Y. U = Pi\<^sub>E I Y \<and> (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)}"
using \<U> by auto
then obtain Y where Y: "\<And>U. U \<in> \<U> \<Longrightarrow> U = Pi\<^sub>E I (Y U) \<and> (\<forall>i. openin (X i) (Y U i)) \<and> finite {i. (Y U) i \<noteq> topspace (X i)}"
by metis
obtain U where "U \<in> \<U>"
using \<open>\<U> \<noteq> {}\<close> by blast
let ?F = "\<lambda>U. (\<lambda>i. {f. f i \<in> Y U i}) ` {i \<in> I. Y U i \<noteq> topspace (X i)}"
show ?thesis
proof (intro conjI exI)
show "finite (\<Union>U\<in>\<U>. ?F U)"
using Y \<open>finite' \<U>\<close> by auto
show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) = \<Inter>\<U>"
proof
have *: "f \<in> U"
if "U \<in> \<U>" and "\<forall>V\<in>\<U>. \<forall>i. i \<in> I \<and> Y V i \<noteq> topspace (X i) \<longrightarrow> f i \<in> Y V i"
and "\<forall>i\<in>I. f i \<in> topspace (X i)" and "f \<in> extensional I" for f U
proof -
have "Pi\<^sub>E I (Y U) = U"
using Y \<open>U \<in> \<U>\<close> by blast
then show "f \<in> U"
using that unfolding PiE_def Pi_def by blast
qed
show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) \<subseteq> \<Inter>\<U>"
by (auto simp: PiE_iff *)
show "\<Inter>\<U> \<subseteq> ?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U)"
using Y openin_subset \<open>finite' \<U>\<close> by fastforce
qed
qed (use Y openin_subset in \<open>blast+\<close>)
qed
have 2: "\<exists>\<U>'. finite' \<U>' \<and> \<U>' \<subseteq> Collect ?\<Omega> \<and> \<Inter>\<U>' = ?TOP \<inter> \<Inter>\<U>"
if \<U>: "\<U> \<subseteq> Collect ?\<Psi>" and "finite \<U>" for \<U>
proof (cases "\<U>={}")
case True
then show ?thesis
apply (rule_tac x="{?TOP}" in exI, simp)
apply (rule_tac x="\<lambda>i. topspace (X i)" in exI)
apply force
done
next
case False
then obtain U where "U \<in> \<U>"
by blast
have "\<forall>U \<in> \<U>. \<exists>i Y. U = {f. f i \<in> Y} \<and> i \<in> I \<and> openin (X i) Y"
using \<U> by auto
then obtain J Y where
Y: "\<And>U. U \<in> \<U> \<Longrightarrow> U = {f. f (J U) \<in> Y U} \<and> J U \<in> I \<and> openin (X (J U)) (Y U)"
by metis
let ?G = "\<lambda>U. \<Pi>\<^sub>E i\<in>I. if i = J U then Y U else topspace (X i)"
show ?thesis
proof (intro conjI exI)
show "finite (?G ` \<U>)" "?G ` \<U> \<noteq> {}"
using \<open>finite \<U>\<close> \<open>U \<in> \<U>\<close> by blast+
have *: "\<And>U. U \<in> \<U> \<Longrightarrow> openin (X (J U)) (Y U)"
using Y by force
show "?G ` \<U> \<subseteq> {Pi\<^sub>E I Y |Y. (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)}}"
apply clarsimp
apply (rule_tac x=" (\<lambda>i. if i = J U then Y U else topspace (X i))" in exI)
apply (auto simp: *)
done
next
show "(\<Inter>U\<in>\<U>. ?G U) = ?TOP \<inter> \<Inter>\<U>"
proof
have "(\<Pi>\<^sub>E i\<in>I. if i = J U then Y U else topspace (X i)) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
apply (clarsimp simp: PiE_iff Ball_def all_conj_distrib split: if_split_asm)
using Y \<open>U \<in> \<U>\<close> openin_subset by blast+
then have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP"
using \<open>U \<in> \<U>\<close>
by fastforce
moreover have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> \<Inter>\<U>"
using PiE_mem Y by fastforce
ultimately show "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP \<inter> \<Inter>\<U>"
by auto
qed (use Y in fastforce)
qed
qed
show ?thesis
unfolding relative_to_def intersection_of_def
by (safe; blast dest!: 1 2)
qed
show ?thesis
unfolding product_topology_def generate_topology_on_eq
apply (rule arg_cong [where f = topology])
apply (rule arg_cong [where f = "(union_of)arbitrary"])
apply (force simp: *)
done
qed
lemma topspace_product_topology [simp]:
"topspace (product_topology T I) = (\<Pi>\<^sub>E i\<in>I. topspace(T i))"
proof
show "topspace (product_topology T I) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
unfolding product_topology_def topology_generated_by_topspace
unfolding topspace_def by auto
have "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<in> {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
using openin_topspace not_finite_existsD by auto
then show "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<subseteq> topspace (product_topology T I)"
unfolding product_topology_def using PiE_def by (auto simp add: topology_generated_by_topspace)
qed
lemma product_topology_basis:
assumes "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"
shows "openin (product_topology T I) (\<Pi>\<^sub>E i\<in>I. X i)"
unfolding product_topology_def
by (rule topology_generated_by_Basis) (use assms in auto)
proposition product_topology_open_contains_basis:
assumes "openin (product_topology T I) U" "x \<in> U"
shows "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
proof -
have "generate_topology_on {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}} U"
using assms unfolding product_topology_def by (intro openin_topology_generated_by) auto
then have "\<And>x. x\<in>U \<Longrightarrow> \<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
proof induction
case (Int U V x)
then obtain XU XV where H:
"x \<in> Pi\<^sub>E I XU" "(\<forall>i. openin (T i) (XU i))" "finite {i. XU i \<noteq> topspace (T i)}" "Pi\<^sub>E I XU \<subseteq> U"
"x \<in> Pi\<^sub>E I XV" "(\<forall>i. openin (T i) (XV i))" "finite {i. XV i \<noteq> topspace (T i)}" "Pi\<^sub>E I XV \<subseteq> V"
by auto meson
define X where "X = (\<lambda>i. XU i \<inter> XV i)"
have "Pi\<^sub>E I X \<subseteq> Pi\<^sub>E I XU \<inter> Pi\<^sub>E I XV"
unfolding X_def by (auto simp add: PiE_iff)
then have "Pi\<^sub>E I X \<subseteq> U \<inter> V" using H by auto
moreover have "\<forall>i. openin (T i) (X i)"
unfolding X_def using H by auto
moreover have "finite {i. X i \<noteq> topspace (T i)}"
apply (rule rev_finite_subset[of "{i. XU i \<noteq> topspace (T i)} \<union> {i. XV i \<noteq> topspace (T i)}"])
unfolding X_def using H by auto
moreover have "x \<in> Pi\<^sub>E I X"
unfolding X_def using H by auto
ultimately show ?case
by auto
next
case (UN K x)
then obtain k where "k \<in> K" "x \<in> k" by auto
with UN have "\<exists>X. x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> k"
by simp
then obtain X where "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> k"
by blast
then have "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> (\<Union>K)"
using \<open>k \<in> K\<close> by auto
then show ?case
by auto
qed auto
then show ?thesis using \<open>x \<in> U\<close> by auto
qed
lemma product_topology_empty_discrete:
"product_topology T {} = discrete_topology {(\<lambda>x. undefined)}"
by (simp add: subtopology_eq_discrete_topology_sing)
lemma openin_product_topology:
"openin (product_topology X I) =
arbitrary union_of
((finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)))
relative_to topspace (product_topology X I))"
apply (subst product_topology)
apply (simp add: topology_inverse' [OF istopology_subbase])
done
lemma subtopology_PiE:
"subtopology (product_topology X I) (\<Pi>\<^sub>E i\<in>I. (S i)) = product_topology (\<lambda>i. subtopology (X i) (S i)) I"
proof -
let ?P = "\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U"
let ?X = "\<Pi>\<^sub>E i\<in>I. topspace (X i)"
have "finite intersection_of ?P relative_to ?X \<inter> Pi\<^sub>E I S =
finite intersection_of (?P relative_to ?X \<inter> Pi\<^sub>E I S) relative_to ?X \<inter> Pi\<^sub>E I S"
by (rule finite_intersection_of_relative_to)
also have "\<dots> = finite intersection_of
((\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> (openin (X i) relative_to S i) U)
relative_to ?X \<inter> Pi\<^sub>E I S)
relative_to ?X \<inter> Pi\<^sub>E I S"
apply (rule arg_cong2 [where f = "(relative_to)"])
apply (rule arg_cong [where f = "(intersection_of)finite"])
apply (rule ext)
apply (auto simp: relative_to_def intersection_of_def)
done
finally
have "finite intersection_of ?P relative_to ?X \<inter> Pi\<^sub>E I S =
finite intersection_of
(\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> (openin (X i) relative_to S i) U)
relative_to ?X \<inter> Pi\<^sub>E I S"
by (metis finite_intersection_of_relative_to)
then show ?thesis
unfolding topology_eq
apply clarify
apply (simp add: openin_product_topology flip: openin_relative_to)
apply (simp add: arbitrary_union_of_relative_to topspace_product_topology topspace_subtopology flip: PiE_Int)
done
qed
lemma product_topology_base_alt:
"finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))
relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i)) =
(\<lambda>F. (\<exists>U. F = Pi\<^sub>E I U \<and> finite {i \<in> I. U i \<noteq> topspace(X i)} \<and> (\<forall>i \<in> I. openin (X i) (U i))))"
(is "?lhs = ?rhs")
proof -
have "(\<forall>F. ?lhs F \<longrightarrow> ?rhs F)"
unfolding all_relative_to all_intersection_of topspace_product_topology
proof clarify
fix \<F>
assume "finite \<F>" and "\<F> \<subseteq> {{f. f i \<in> U} |i U. i \<in> I \<and> openin (X i) U}"
then show "\<exists>U. (\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>\<F> = Pi\<^sub>E I U \<and>
finite {i \<in> I. U i \<noteq> topspace (X i)} \<and> (\<forall>i\<in>I. openin (X i) (U i))"
proof (induction)
case (insert F \<F>)
then obtain U where eq: "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>\<F> = Pi\<^sub>E I U"
and fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}"
and ope: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (U i)"
by auto
obtain i V where "F = {f. f i \<in> V}" "i \<in> I" "openin (X i) V"
using insert by auto
let ?U = "\<lambda>j. U j \<inter> (if j = i then V else topspace(X j))"
show ?case
proof (intro exI conjI)
show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>(insert F \<F>) = Pi\<^sub>E I ?U"
using eq PiE_mem \<open>i \<in> I\<close> by (auto simp: \<open>F = {f. f i \<in> V}\<close>) fastforce
next
show "finite {i \<in> I. ?U i \<noteq> topspace (X i)}"
by (rule rev_finite_subset [OF finite.insertI [OF fin]]) auto
next
show "\<forall>i\<in>I. openin (X i) (?U i)"
by (simp add: \<open>openin (X i) V\<close> ope openin_Int)
qed
qed (auto intro: dest: not_finite_existsD)
qed
moreover have "(\<forall>F. ?rhs F \<longrightarrow> ?lhs F)"
proof clarify
fix U :: "'a \<Rightarrow> 'b set"
assume fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}" and ope: "\<forall>i\<in>I. openin (X i) (U i)"
let ?U = "\<Inter>i\<in>{i \<in> I. U i \<noteq> topspace (X i)}. {x. x i \<in> U i}"
show "?lhs (Pi\<^sub>E I U)"
unfolding relative_to_def topspace_product_topology
proof (intro exI conjI)
show "(finite intersection_of (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)) ?U"
using fin ope by (intro finite_intersection_of_Inter finite_intersection_of_inc) auto
show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> ?U = Pi\<^sub>E I U"
using ope openin_subset by fastforce
qed
qed
ultimately show ?thesis
by meson
qed
corollary openin_product_topology_alt:
"openin (product_topology X I) S \<longleftrightarrow>
(\<forall>x \<in> S. \<exists>U. finite {i \<in> I. U i \<noteq> topspace(X i)} \<and>
(\<forall>i \<in> I. openin (X i) (U i)) \<and> x \<in> Pi\<^sub>E I U \<and> Pi\<^sub>E I U \<subseteq> S)"
unfolding openin_product_topology arbitrary_union_of_alt product_topology_base_alt topspace_product_topology
apply safe
apply (drule bspec; blast)+
done
lemma closure_of_product_topology:
"(product_topology X I) closure_of (PiE I S) = PiE I (\<lambda>i. (X i) closure_of (S i))"
proof -
have *: "(\<forall>T. f \<in> T \<and> openin (product_topology X I) T \<longrightarrow> (\<exists>y\<in>Pi\<^sub>E I S. y \<in> T))
\<longleftrightarrow> (\<forall>i \<in> I. \<forall>T. f i \<in> T \<and> openin (X i) T \<longrightarrow> S i \<inter> T \<noteq> {})"
(is "?lhs = ?rhs")
if top: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> topspace (X i)" and ext: "f \<in> extensional I" for f
proof
assume L[rule_format]: ?lhs
show ?rhs
proof clarify
fix i T
assume "i \<in> I" "f i \<in> T" "openin (X i) T" "S i \<inter> T = {}"
then have "openin (product_topology X I) ((\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> {x. x i \<in> T})"
by (force simp: openin_product_topology intro: arbitrary_union_of_inc relative_to_inc finite_intersection_of_inc)
then show "False"
using L [of "topspace (product_topology X I) \<inter> {f. f i \<in> T}"] \<open>S i \<inter> T = {}\<close> \<open>f i \<in> T\<close> \<open>i \<in> I\<close>
by (auto simp: top ext PiE_iff)
qed
next
assume R [rule_format]: ?rhs
show ?lhs
proof (clarsimp simp: openin_product_topology union_of_def arbitrary_def)
fix \<U> U
assume
\<U>: "\<U> \<subseteq> Collect
(finite intersection_of (\<lambda>F. \<exists>i U. F = {x. x i \<in> U} \<and> i \<in> I \<and> openin (X i) U) relative_to
(\<Pi>\<^sub>E i\<in>I. topspace (X i)))" and
"f \<in> U" "U \<in> \<U>"
then have "(finite intersection_of (\<lambda>F. \<exists>i U. F = {x. x i \<in> U} \<and> i \<in> I \<and> openin (X i) U)
relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i))) U"
by blast
with \<open>f \<in> U\<close> \<open>U \<in> \<U>\<close>
obtain \<T> where "finite \<T>"
and \<T>: "\<And>C. C \<in> \<T> \<Longrightarrow> \<exists>i \<in> I. \<exists>V. openin (X i) V \<and> C = {x. x i \<in> V}"
and "topspace (product_topology X I) \<inter> \<Inter> \<T> \<subseteq> U" "f \<in> topspace (product_topology X I) \<inter> \<Inter> \<T>"
apply (clarsimp simp add: relative_to_def intersection_of_def)
apply (rule that, auto dest!: subsetD)
done
then have "f \<in> PiE I (topspace \<circ> X)" "f \<in> \<Inter>\<T>" and subU: "PiE I (topspace \<circ> X) \<inter> \<Inter>\<T> \<subseteq> U"
by (auto simp: PiE_iff)
have *: "f i \<in> topspace (X i) \<inter> \<Inter>{U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>}
\<and> openin (X i) (topspace (X i) \<inter> \<Inter>{U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>})"
if "i \<in> I" for i
proof -
have "finite ((\<lambda>U. {x. x i \<in> U}) -` \<T>)"
proof (rule finite_vimageI [OF \<open>finite \<T>\<close>])
show "inj (\<lambda>U. {x. x i \<in> U})"
by (auto simp: inj_on_def)
qed
then have fin: "finite {U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>}"
by (rule rev_finite_subset) auto
have "openin (X i) (\<Inter> (insert (topspace (X i)) {U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>}))"
by (rule openin_Inter) (auto simp: fin)
then show ?thesis
using \<open>f \<in> \<Inter> \<T>\<close> by (fastforce simp: that top)
qed
define \<Phi> where "\<Phi> \<equiv> \<lambda>i. topspace (X i) \<inter> \<Inter>{U. openin (X i) U \<and> {f. f i \<in> U} \<in> \<T>}"
have "\<forall>i \<in> I. \<exists>x. x \<in> S i \<inter> \<Phi> i"
using R [OF _ *] unfolding \<Phi>_def by blast
then obtain \<theta> where \<theta> [rule_format]: "\<forall>i \<in> I. \<theta> i \<in> S i \<inter> \<Phi> i"
by metis
show "\<exists>y\<in>Pi\<^sub>E I S. \<exists>x\<in>\<U>. y \<in> x"
proof
show "\<exists>U \<in> \<U>. (\<lambda>i \<in> I. \<theta> i) \<in> U"
proof
have "restrict \<theta> I \<in> PiE I (topspace \<circ> X) \<inter> \<Inter>\<T>"
using \<T> by (fastforce simp: \<Phi>_def PiE_def dest: \<theta>)
then show "restrict \<theta> I \<in> U"
using subU by blast
qed (rule \<open>U \<in> \<U>\<close>)
next
show "(\<lambda>i \<in> I. \<theta> i) \<in> Pi\<^sub>E I S"
using \<theta> by simp
qed
qed
qed
show ?thesis
apply (simp add: * closure_of_def PiE_iff set_eq_iff cong: conj_cong)
by metis
qed
corollary closedin_product_topology:
"closedin (product_topology X I) (PiE I S) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. closedin (X i) (S i))"
apply (simp add: PiE_eq PiE_eq_empty_iff closure_of_product_topology flip: closure_of_eq)
apply (metis closure_of_empty)
done
corollary closedin_product_topology_singleton:
"f \<in> extensional I \<Longrightarrow> closedin (product_topology X I) {f} \<longleftrightarrow> (\<forall>i \<in> I. closedin (X i) {f i})"
using PiE_singleton closedin_product_topology [of X I]
by (metis (no_types, lifting) all_not_in_conv insertI1)
lemma product_topology_empty:
"product_topology X {} = topology (\<lambda>S. S \<in> {{},{\<lambda>k. undefined}})"
unfolding product_topology union_of_def intersection_of_def arbitrary_def relative_to_def
by (auto intro: arg_cong [where f=topology])
lemma openin_product_topology_empty: "openin (product_topology X {}) S \<longleftrightarrow> S \<in> {{},{\<lambda>k. undefined}}"
unfolding union_of_def intersection_of_def arbitrary_def relative_to_def openin_product_topology
by auto
subsubsection \<open>The basic property of the product topology is the continuity of projections:\<close>
lemma continuous_map_product_coordinates [simp]:
assumes "i \<in> I"
shows "continuous_map (product_topology T I) (T i) (\<lambda>x. x i)"
proof -
{
fix U assume "openin (T i) U"
define X where "X = (\<lambda>j. if j = i then U else topspace (T j))"
then have *: "(\<lambda>x. x i) -` U \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (T i)) = (\<Pi>\<^sub>E j\<in>I. X j)"
unfolding X_def using assms openin_subset[OF \<open>openin (T i) U\<close>]
by (auto simp add: PiE_iff, auto, metis subsetCE)
have **: "(\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}"
unfolding X_def using \<open>openin (T i) U\<close> by auto
have "openin (product_topology T I) ((\<lambda>x. x i) -` U \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (T i)))"
unfolding product_topology_def
apply (rule topology_generated_by_Basis)
apply (subst *)
using ** by auto
}
then show ?thesis unfolding continuous_map_alt
by (auto simp add: assms PiE_iff)
qed
lemma continuous_map_coordinatewise_then_product [intro]:
assumes "\<And>i. i \<in> I \<Longrightarrow> continuous_map T1 (T i) (\<lambda>x. f x i)"
"\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
shows "continuous_map T1 (product_topology T I) f"
unfolding product_topology_def
proof (rule continuous_on_generated_topo)
fix U assume "U \<in> {Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
then obtain X where H: "U = Pi\<^sub>E I X" "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"
by blast
define J where "J = {i \<in> I. X i \<noteq> topspace (T i)}"
have "finite J" "J \<subseteq> I" unfolding J_def using H(3) by auto
have "(\<lambda>x. f x i)-`(topspace(T i)) \<inter> topspace T1 = topspace T1" if "i \<in> I" for i
using that assms(1) by (simp add: continuous_map_preimage_topspace)
then have *: "(\<lambda>x. f x i)-`(X i) \<inter> topspace T1 = topspace T1" if "i \<in> I-J" for i
using that unfolding J_def by auto
have "f-`U \<inter> topspace T1 = (\<Inter>i\<in>I. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
by (subst H(1), auto simp add: PiE_iff assms)
also have "... = (\<Inter>i\<in>J. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
using * \<open>J \<subseteq> I\<close> by auto
also have "openin T1 (...)"
apply (rule openin_INT)
apply (simp add: \<open>finite J\<close>)
using H(2) assms(1) \<open>J \<subseteq> I\<close> by auto
ultimately show "openin T1 (f-`U \<inter> topspace T1)" by simp
next
show "f `topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
apply (subst topology_generated_by_topspace[symmetric])
apply (subst product_topology_def[symmetric])
apply (simp only: topspace_product_topology)
apply (auto simp add: PiE_iff)
using assms unfolding continuous_map_def by auto
qed
lemma continuous_map_product_then_coordinatewise [intro]:
assumes "continuous_map T1 (product_topology T I) f"
shows "\<And>i. i \<in> I \<Longrightarrow> continuous_map T1 (T i) (\<lambda>x. f x i)"
"\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
proof -
fix i assume "i \<in> I"
have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f" by auto
also have "continuous_map T1 (T i) (...)"
apply (rule continuous_map_compose[of _ "product_topology T I"])
using assms \<open>i \<in> I\<close> by auto
ultimately show "continuous_map T1 (T i) (\<lambda>x. f x i)"
by simp
next
fix i x assume "i \<notin> I" "x \<in> topspace T1"
have "f x \<in> topspace (product_topology T I)"
using assms \<open>x \<in> topspace T1\<close> unfolding continuous_map_def by auto
then have "f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
using topspace_product_topology by metis
then show "f x i = undefined"
using \<open>i \<notin> I\<close> by (auto simp add: PiE_iff extensional_def)
qed
lemma continuous_on_restrict:
assumes "J \<subseteq> I"
shows "continuous_map (product_topology T I) (product_topology T J) (\<lambda>x. restrict x J)"
proof (rule continuous_map_coordinatewise_then_product)
fix i assume "i \<in> J"
then have "(\<lambda>x. restrict x J i) = (\<lambda>x. x i)" unfolding restrict_def by auto
then show "continuous_map (product_topology T I) (T i) (\<lambda>x. restrict x J i)"
using \<open>i \<in> J\<close> \<open>J \<subseteq> I\<close> by auto
next
fix i assume "i \<notin> J"
then show "restrict x J i = undefined" for x::"'a \<Rightarrow> 'b"
unfolding restrict_def by auto
qed
subsubsection%important \<open>Powers of a single topological space as a topological space, using type classes\<close>
instantiation "fun" :: (type, topological_space) topological_space
begin
definition%important open_fun_def:
"open U = openin (product_topology (\<lambda>i. euclidean) UNIV) U"
instance proof
have "topspace (product_topology (\<lambda>(i::'a). euclidean::('b topology)) UNIV) = UNIV"
unfolding topspace_product_topology topspace_euclidean by auto
then show "open (UNIV::('a \<Rightarrow> 'b) set)"
unfolding open_fun_def by (metis openin_topspace)
qed (auto simp add: open_fun_def)
end
lemma open_PiE [intro?]:
fixes X::"'i \<Rightarrow> ('b::topological_space) set"
assumes "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
shows "open (Pi\<^sub>E UNIV X)"
by (simp add: assms open_fun_def product_topology_basis)
lemma euclidean_product_topology:
"product_topology (\<lambda>i. euclidean::('b::topological_space) topology) UNIV = euclidean"
by (metis open_openin topology_eq open_fun_def)
proposition product_topology_basis':
fixes x::"'i \<Rightarrow> 'a" and U::"'i \<Rightarrow> ('b::topological_space) set"
assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
shows "open {f. \<forall>i\<in>I. f (x i) \<in> U i}"
proof -
define J where "J = x`I"
define V where "V = (\<lambda>y. if y \<in> J then \<Inter>{U i|i. i\<in>I \<and> x i = y} else UNIV)"
define X where "X = (\<lambda>y. if y \<in> J then V y else UNIV)"
have *: "open (X i)" for i
unfolding X_def V_def using assms by auto
have **: "finite {i. X i \<noteq> UNIV}"
unfolding X_def V_def J_def using assms(1) by auto
have "open (Pi\<^sub>E UNIV X)"
by (simp add: "*" "**" open_PiE)
moreover have "Pi\<^sub>E UNIV X = {f. \<forall>i\<in>I. f (x i) \<in> U i}"
apply (auto simp add: PiE_iff) unfolding X_def V_def J_def
proof (auto)
fix f :: "'a \<Rightarrow> 'b" and i :: 'i
assume a1: "i \<in> I"
assume a2: "\<forall>i. f i \<in> (if i \<in> x`I then if i \<in> x`I then \<Inter>{U ia |ia. ia \<in> I \<and> x ia = i} else UNIV else UNIV)"
have f3: "x i \<in> x`I"
using a1 by blast
have "U i \<in> {U ia |ia. ia \<in> I \<and> x ia = x i}"
using a1 by blast
then show "f (x i) \<in> U i"
using f3 a2 by (meson Inter_iff)
qed
ultimately show ?thesis by simp
qed
text \<open>The results proved in the general situation of products of possibly different
spaces have their counterparts in this simpler setting.\<close>
lemma continuous_on_product_coordinates [simp]:
"continuous_on UNIV (\<lambda>x. x i::('b::topological_space))"
using continuous_map_product_coordinates [of _ UNIV "\<lambda>i. euclidean"]
by (metis (no_types) continuous_map_iff_continuous euclidean_product_topology iso_tuple_UNIV_I subtopology_UNIV)
lemma continuous_on_coordinatewise_then_product [continuous_intros]:
fixes f :: "'a::topological_space \<Rightarrow> 'b \<Rightarrow> 'c::topological_space"
assumes "\<And>i. continuous_on S (\<lambda>x. f x i)"
shows "continuous_on S f"
using continuous_map_coordinatewise_then_product [of UNIV, where T = "\<lambda>i. euclidean"]
by (metis UNIV_I assms continuous_map_iff_continuous euclidean_product_topology)
lemma continuous_on_product_then_coordinatewise_UNIV:
assumes "continuous_on UNIV f"
shows "continuous_on UNIV (\<lambda>x. f x i)"
unfolding continuous_map_iff_continuous2 [symmetric]
by (rule continuous_map_product_then_coordinatewise [where I=UNIV]) (use assms in \<open>auto simp: euclidean_product_topology\<close>)
lemma continuous_on_product_then_coordinatewise:
assumes "continuous_on S f"
shows "continuous_on S (\<lambda>x. f x i)"
proof -
have "continuous_on S ((\<lambda>q. q i) \<circ> f)"
by (metis assms continuous_on_compose continuous_on_id
continuous_on_product_then_coordinatewise_UNIV continuous_on_subset subset_UNIV)
then show ?thesis
by auto
qed
lemma continuous_on_coordinatewise_iff:
fixes f :: "('a \<Rightarrow> real) \<Rightarrow> 'b \<Rightarrow> real"
shows "continuous_on (A \<inter> S) f \<longleftrightarrow> (\<forall>i. continuous_on (A \<inter> S) (\<lambda>x. f x i))"
by (auto simp: continuous_on_product_then_coordinatewise continuous_on_coordinatewise_then_product)
lemma continuous_map_span_sum:
fixes B :: "'a::real_inner set"
assumes biB: "\<And>i. i \<in> I \<Longrightarrow> b i \<in> B"
shows "continuous_map euclidean (top_of_set (span B)) (\<lambda>x. \<Sum>i\<in>I. x i *\<^sub>R b i)"
proof (rule continuous_map_euclidean_top_of_set)
show "(\<lambda>x. \<Sum>i\<in>I. x i *\<^sub>R b i) -` span B = UNIV"
by auto (meson biB lessThan_iff span_base span_scale span_sum)
show "continuous_on UNIV (\<lambda>x. \<Sum>i\<in> I. x i *\<^sub>R b i)"
by (intro continuous_intros) auto
qed
subsubsection%important \<open>Topological countability for product spaces\<close>
text \<open>The next two lemmas are useful to prove first or second countability
of product spaces, but they have more to do with countability and could
be put in the corresponding theory.\<close>
lemma countable_nat_product_event_const:
fixes F::"'a set" and a::'a
assumes "a \<in> F" "countable F"
shows "countable {x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}"
proof -
have *: "{x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}
\<subseteq> (\<Union>N. {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)})"
using infinite_nat_iff_unbounded_le by fastforce
have "countable {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)}" for N::nat
proof (induction N)
case 0
have "{x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>(0::nat). x i = a)} = {(\<lambda>i. a)}"
using \<open>a \<in> F\<close> by auto
then show ?case by auto
next
case (Suc N)
define f::"((nat \<Rightarrow> 'a) \<times> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)"
where "f = (\<lambda>(x, b). (\<lambda>i. if i = N then b else x i))"
have "{x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>Suc N. x i = a)} \<subseteq> f`({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
proof (auto)
fix x assume H: "\<forall>i::nat. x i \<in> F" "\<forall>i\<ge>Suc N. x i = a"
define y where "y = (\<lambda>i. if i = N then a else x i)"
have "f (y, x N) = x"
unfolding f_def y_def by auto
moreover have "(y, x N) \<in> {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F"
unfolding y_def using H \<open>a \<in> F\<close> by auto
ultimately show "x \<in> f`({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
by (metis (no_types, lifting) image_eqI)
qed
moreover have "countable ({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
using Suc.IH assms(2) by auto
ultimately show ?case
by (meson countable_image countable_subset)
qed
then show ?thesis using countable_subset[OF *] by auto
qed
lemma countable_product_event_const:
fixes F::"('a::countable) \<Rightarrow> 'b set" and b::'b
assumes "\<And>i. countable (F i)"
shows "countable {f::('a \<Rightarrow> 'b). (\<forall>i. f i \<in> F i) \<and> (finite {i. f i \<noteq> b})}"
proof -
define G where "G = (\<Union>i. F i) \<union> {b}"
have "countable G" unfolding G_def using assms by auto
have "b \<in> G" unfolding G_def by auto
define pi where "pi = (\<lambda>(x::(nat \<Rightarrow> 'b)). (\<lambda> i::'a. x ((to_nat::('a \<Rightarrow> nat)) i)))"
have "{f::('a \<Rightarrow> 'b). (\<forall>i. f i \<in> F i) \<and> (finite {i. f i \<noteq> b})}
\<subseteq> pi`{g::(nat \<Rightarrow> 'b). (\<forall>j. g j \<in> G) \<and> (finite {j. g j \<noteq> b})}"
proof (auto)
fix f assume H: "\<forall>i. f i \<in> F i" "finite {i. f i \<noteq> b}"
define I where "I = {i. f i \<noteq> b}"
define g where "g = (\<lambda>j. if j \<in> to_nat`I then f (from_nat j) else b)"
have "{j. g j \<noteq> b} \<subseteq> to_nat`I" unfolding g_def by auto
then have "finite {j. g j \<noteq> b}"
unfolding I_def using H(2) using finite_surj by blast
moreover have "g j \<in> G" for j
unfolding g_def G_def using H by auto
ultimately have "g \<in> {g::(nat \<Rightarrow> 'b). (\<forall>j. g j \<in> G) \<and> (finite {j. g j \<noteq> b})}"
by auto
moreover have "f = pi g"
unfolding pi_def g_def I_def using H by fastforce
ultimately show "f \<in> pi`{g. (\<forall>j. g j \<in> G) \<and> finite {j. g j \<noteq> b}}"
by auto
qed
then show ?thesis
using countable_nat_product_event_const[OF \<open>b \<in> G\<close> \<open>countable G\<close>]
by (meson countable_image countable_subset)
qed
instance "fun" :: (countable, first_countable_topology) first_countable_topology
proof
fix x::"'a \<Rightarrow> 'b"
have "\<exists>A::('b \<Rightarrow> nat \<Rightarrow> 'b set). \<forall>x. (\<forall>i. x \<in> A x i \<and> open (A x i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A x i \<subseteq> S))"
apply (rule choice) using first_countable_basis by auto
then obtain A::"('b \<Rightarrow> nat \<Rightarrow> 'b set)" where A: "\<And>x i. x \<in> A x i"
"\<And>x i. open (A x i)"
"\<And>x S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>i. A x i \<subseteq> S)"
by metis
text \<open>\<open>B i\<close> is a countable basis of neighborhoods of \<open>x\<^sub>i\<close>.\<close>
define B where "B = (\<lambda>i. (A (x i))`UNIV \<union> {UNIV})"
have "countable (B i)" for i unfolding B_def by auto
have open_B: "\<And>X i. X \<in> B i \<Longrightarrow> open X"
by (auto simp: B_def A)
define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
have "Pi\<^sub>E UNIV (\<lambda>i. UNIV) \<in> K"
unfolding K_def B_def by auto
then have "K \<noteq> {}" by auto
have "countable {X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
apply (rule countable_product_event_const) using \<open>\<And>i. countable (B i)\<close> by auto
moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
unfolding K_def by auto
ultimately have "countable K" by auto
have "x \<in> k" if "k \<in> K" for k
using that unfolding K_def B_def apply auto using A(1) by auto
have "open k" if "k \<in> K" for k
using that unfolding K_def by (blast intro: open_B open_PiE elim: )
have Inc: "\<exists>k\<in>K. k \<subseteq> U" if "open U \<and> x \<in> U" for U
proof -
have "openin (product_topology (\<lambda>i. euclidean) UNIV) U" "x \<in> U"
using \<open>open U \<and> x \<in> U\<close> unfolding open_fun_def by auto
with product_topology_open_contains_basis[OF this]
have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
by simp
then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
"\<And>i. open (X i)"
"finite {i. X i \<noteq> UNIV}"
"(\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
by auto
define I where "I = {i. X i \<noteq> UNIV}"
define Y where "Y = (\<lambda>i. if i \<in> I then (SOME y. y \<in> B i \<and> y \<subseteq> X i) else UNIV)"
have *: "\<exists>y. y \<in> B i \<and> y \<subseteq> X i" for i
unfolding B_def using A(3)[OF H(2)] H(1) by (metis PiE_E UNIV_I UnCI image_iff)
have **: "Y i \<in> B i \<and> Y i \<subseteq> X i" for i
apply (cases "i \<in> I")
unfolding Y_def using * that apply (auto)
apply (metis (no_types, lifting) someI, metis (no_types, lifting) someI_ex subset_iff)
unfolding B_def apply simp
unfolding I_def apply auto
done
have "{i. Y i \<noteq> UNIV} \<subseteq> I"
unfolding Y_def by auto
then have ***: "finite {i. Y i \<noteq> UNIV}"
unfolding I_def using H(3) rev_finite_subset by blast
have "(\<forall>i. Y i \<in> B i) \<and> finite {i. Y i \<noteq> UNIV}"
using ** *** by auto
then have "Pi\<^sub>E UNIV Y \<in> K"
unfolding K_def by auto
have "Y i \<subseteq> X i" for i
apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
then show ?thesis using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> by auto
qed
show "\<exists>L. (\<forall>(i::nat). x \<in> L i \<and> open (L i)) \<and> (\<forall>U. open U \<and> x \<in> U \<longrightarrow> (\<exists>i. L i \<subseteq> U))"
apply (rule first_countableI[of K])
using \<open>countable K\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> x \<in> k\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> open k\<close> Inc by auto
qed
proposition product_topology_countable_basis:
shows "\<exists>K::(('a::countable \<Rightarrow> 'b::second_countable_topology) set set).
topological_basis K \<and> countable K \<and>
(\<forall>k\<in>K. \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV})"
proof -
obtain B::"'b set set" where B: "countable B \<and> topological_basis B"
using ex_countable_basis by auto
then have "B \<noteq> {}" by (meson UNIV_I empty_iff open_UNIV topological_basisE)
define B2 where "B2 = B \<union> {UNIV}"
have "countable B2"
unfolding B2_def using B by auto
have "open U" if "U \<in> B2" for U
using that unfolding B2_def using B topological_basis_open by auto
define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i::'a. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
have i: "\<forall>k\<in>K. \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
unfolding K_def using \<open>\<And>U. U \<in> B2 \<Longrightarrow> open U\<close> by auto
have "countable {X. (\<forall>(i::'a). X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
apply (rule countable_product_event_const) using \<open>countable B2\<close> by auto
moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
unfolding K_def by auto
ultimately have ii: "countable K" by auto
have iii: "topological_basis K"
proof (rule topological_basisI)
fix U and x::"'a\<Rightarrow>'b" assume "open U" "x \<in> U"
then have "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
unfolding open_fun_def by auto
with product_topology_open_contains_basis[OF this \<open>x \<in> U\<close>]
have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
by simp
then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
"\<And>i. open (X i)"
"finite {i. X i \<noteq> UNIV}"
"(\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
by auto
then have "x i \<in> X i" for i by auto
define I where "I = {i. X i \<noteq> UNIV}"
define Y where "Y = (\<lambda>i. if i \<in> I then (SOME y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y) else UNIV)"
have *: "\<exists>y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y" for i
unfolding B2_def using B \<open>open (X i)\<close> \<open>x i \<in> X i\<close> by (meson UnCI topological_basisE)
have **: "Y i \<in> B2 \<and> Y i \<subseteq> X i \<and> x i \<in> Y i" for i
using someI_ex[OF *]
apply (cases "i \<in> I")
unfolding Y_def using * apply (auto)
unfolding B2_def I_def by auto
have "{i. Y i \<noteq> UNIV} \<subseteq> I"
unfolding Y_def by auto
then have ***: "finite {i. Y i \<noteq> UNIV}"
unfolding I_def using H(3) rev_finite_subset by blast
have "(\<forall>i. Y i \<in> B2) \<and> finite {i. Y i \<noteq> UNIV}"
using ** *** by auto
then have "Pi\<^sub>E UNIV Y \<in> K"
unfolding K_def by auto
have "Y i \<subseteq> X i" for i
apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
have "x \<in> Pi\<^sub>E UNIV Y"
using ** by auto
show "\<exists>V\<in>K. x \<in> V \<and> V \<subseteq> U"
using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> \<open>Pi\<^sub>E UNIV Y \<subseteq> U\<close> \<open>x \<in> Pi\<^sub>E UNIV Y\<close> by auto
next
fix U assume "U \<in> K"
show "open U"
using \<open>U \<in> K\<close> unfolding open_fun_def K_def by clarify (metis \<open>U \<in> K\<close> i open_PiE open_fun_def)
qed
show ?thesis using i ii iii by auto
qed
instance "fun" :: (countable, second_countable_topology) second_countable_topology
apply standard
using product_topology_countable_basis topological_basis_imp_subbasis by auto
subsection \<open>Metrics on product spaces\<close>
text \<open>In general, the product topology is not metrizable, unless the index set is countable.
When the index set is countable, essentially any (convergent) combination of the metrics on the
factors will do. We use below the simplest one, based on \<open>L\<^sup>1\<close>, but \<open>L\<^sup>2\<close> would also work,
for instance.
What is not completely trivial is that the distance thus defined induces the same topology
as the product topology. This is what we have to prove to show that we have an instance
of \<^class>\<open>metric_space\<close>.
The proofs below would work verbatim for general countable products of metric spaces. However,
since distances are only implemented in terms of type classes, we only develop the theory
for countable products of the same space.\<close>
instantiation "fun" :: (countable, metric_space) metric_space
begin
definition%important dist_fun_def:
"dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
definition%important uniformity_fun_def:
"(uniformity::(('a \<Rightarrow> 'b) \<times> ('a \<Rightarrow> 'b)) filter) = (INF e\<in>{0<..}. principal {(x, y). dist (x::('a\<Rightarrow>'b)) y < e})"
text \<open>Except for the first one, the auxiliary lemmas below are only useful when proving the
instance: once it is proved, they become trivial consequences of the general theory of metric
spaces. It would thus be desirable to hide them once the instance is proved, but I do not know how
to do this.\<close>
lemma dist_fun_le_dist_first_terms:
"dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
proof -
have "(\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)
= (\<Sum>n. (1 / 2) ^ (Suc N) * ((1/2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1))"
by (rule suminf_cong, simp add: power_add)
also have "... = (1/2)^(Suc N) * (\<Sum>n. (1 / 2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)"
apply (rule suminf_mult)
by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
also have "... \<le> (1/2)^(Suc N) * (\<Sum>n. (1 / 2) ^ n)"
apply (simp, rule suminf_le, simp)
by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
also have "... = (1/2)^(Suc N) * 2"
using suminf_geometric[of "1/2"] by auto
also have "... = (1/2)^N"
by auto
finally have *: "(\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1) \<le> (1/2)^N"
by simp
define M where "M = Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N}"
have "dist (x (from_nat 0)) (y (from_nat 0)) \<le> M"
unfolding M_def by (rule Max_ge, auto)
then have [simp]: "M \<ge> 0" by (meson dual_order.trans zero_le_dist)
have "dist (x (from_nat n)) (y (from_nat n)) \<le> M" if "n\<le>N" for n
unfolding M_def apply (rule Max_ge) using that by auto
then have i: "min (dist (x (from_nat n)) (y (from_nat n))) 1 \<le> M" if "n\<le>N" for n
using that by force
have "(\<Sum>n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) \<le>
(\<Sum>n< Suc N. M * (1 / 2) ^ n)"
by (rule sum_mono, simp add: i)
also have "... = M * (\<Sum>n<Suc N. (1 / 2) ^ n)"
by (rule sum_distrib_left[symmetric])
also have "... \<le> M * (\<Sum>n. (1 / 2) ^ n)"
by (rule mult_left_mono, rule sum_le_suminf, auto simp add: summable_geometric_iff)
also have "... = M * 2"
using suminf_geometric[of "1/2"] by auto
finally have **: "(\<Sum>n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) \<le> 2 * M"
by simp
have "dist x y = (\<Sum>n. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
unfolding dist_fun_def by simp
also have "... = (\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)
+ (\<Sum>n<Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
apply (rule suminf_split_initial_segment)
by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
also have "... \<le> 2 * M + (1/2)^N"
using * ** by auto
finally show ?thesis unfolding M_def by simp
qed
lemma open_fun_contains_ball_aux:
assumes "open (U::(('a \<Rightarrow> 'b) set))"
"x \<in> U"
shows "\<exists>e>0. {y. dist x y < e} \<subseteq> U"
proof -
have *: "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
using open_fun_def assms by auto
obtain X where H: "Pi\<^sub>E UNIV X \<subseteq> U"
"\<And>i. openin euclidean (X i)"
"finite {i. X i \<noteq> topspace euclidean}"
"x \<in> Pi\<^sub>E UNIV X"
using product_topology_open_contains_basis[OF * \<open>x \<in> U\<close>] by auto
define I where "I = {i. X i \<noteq> topspace euclidean}"
have "finite I" unfolding I_def using H(3) by auto
{
fix i
have "x i \<in> X i" using \<open>x \<in> U\<close> H by auto
then have "\<exists>e. e>0 \<and> ball (x i) e \<subseteq> X i"
using \<open>openin euclidean (X i)\<close> open_openin open_contains_ball by blast
then obtain e where "e>0" "ball (x i) e \<subseteq> X i" by blast
define f where "f = min e (1/2)"
have "f>0" "f<1" unfolding f_def using \<open>e>0\<close> by auto
moreover have "ball (x i) f \<subseteq> X i" unfolding f_def using \<open>ball (x i) e \<subseteq> X i\<close> by auto
ultimately have "\<exists>f. f > 0 \<and> f < 1 \<and> ball (x i) f \<subseteq> X i" by auto
} note * = this
have "\<exists>e. \<forall>i. e i > 0 \<and> e i < 1 \<and> ball (x i) (e i) \<subseteq> X i"
by (rule choice, auto simp add: *)
then obtain e where "\<And>i. e i > 0" "\<And>i. e i < 1" "\<And>i. ball (x i) (e i) \<subseteq> X i"
by blast
define m where "m = Min {(1/2)^(to_nat i) * e i|i. i \<in> I}"
have "m > 0" if "I\<noteq>{}"
unfolding m_def Min_gr_iff using \<open>finite I\<close> \<open>I \<noteq> {}\<close> \<open>\<And>i. e i > 0\<close> by auto
moreover have "{y. dist x y < m} \<subseteq> U"
proof (auto)
fix y assume "dist x y < m"
have "y i \<in> X i" if "i \<in> I" for i
proof -
have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
define n where "n = to_nat i"
have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 < m"
using \<open>dist x y < m\<close> unfolding dist_fun_def using sum_le_suminf[OF *, of "{n}"] by auto
then have "(1/2)^(to_nat i) * min (dist (x i) (y i)) 1 < m"
using \<open>n = to_nat i\<close> by auto
also have "... \<le> (1/2)^(to_nat i) * e i"
unfolding m_def apply (rule Min_le) using \<open>finite I\<close> \<open>i \<in> I\<close> by auto
ultimately have "min (dist (x i) (y i)) 1 < e i"
by (auto simp add: divide_simps)
then have "dist (x i) (y i) < e i"
using \<open>e i < 1\<close> by auto
then show "y i \<in> X i" using \<open>ball (x i) (e i) \<subseteq> X i\<close> by auto
qed
then have "y \<in> Pi\<^sub>E UNIV X" using H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
then show "y \<in> U" using \<open>Pi\<^sub>E UNIV X \<subseteq> U\<close> by auto
qed
ultimately have *: "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I \<noteq> {}" using that by auto
have "U = UNIV" if "I = {}"
using that H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
then have "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I = {}" using that zero_less_one by blast
then show "\<exists>m>0. {y. dist x y < m} \<subseteq> U" using * by blast
qed
lemma ball_fun_contains_open_aux:
fixes x::"('a \<Rightarrow> 'b)" and e::real
assumes "e>0"
shows "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> {y. dist x y < e}"
proof -
have "\<exists>N::nat. 2^N > 8/e"
by (simp add: real_arch_pow)
then obtain N::nat where "2^N > 8/e" by auto
define f where "f = e/4"
have [simp]: "e>0" "f > 0" unfolding f_def using assms by auto
define X::"('a \<Rightarrow> 'b set)" where "X = (\<lambda>i. if (\<exists>n\<le>N. i = from_nat n) then {z. dist (x i) z < f} else UNIV)"
have "{i. X i \<noteq> UNIV} \<subseteq> from_nat`{0..N}"
unfolding X_def by auto
then have "finite {i. X i \<noteq> topspace euclidean}"
unfolding topspace_euclidean using finite_surj by blast
have "\<And>i. open (X i)"
unfolding X_def using metric_space_class.open_ball open_UNIV by auto
then have "\<And>i. openin euclidean (X i)"
using open_openin by auto
define U where "U = Pi\<^sub>E UNIV X"
have "open U"
unfolding open_fun_def product_topology_def apply (rule topology_generated_by_Basis)
unfolding U_def using \<open>\<And>i. openin euclidean (X i)\<close> \<open>finite {i. X i \<noteq> topspace euclidean}\<close>
by auto
moreover have "x \<in> U"
unfolding U_def X_def by (auto simp add: PiE_iff)
moreover have "dist x y < e" if "y \<in> U" for y
proof -
have *: "dist (x (from_nat n)) (y (from_nat n)) \<le> f" if "n \<le> N" for n
using \<open>y \<in> U\<close> unfolding U_def apply (auto simp add: PiE_iff)
unfolding X_def using that by (metis less_imp_le mem_Collect_eq)
have **: "Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} \<le> f"
apply (rule Max.boundedI) using * by auto
have "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
by (rule dist_fun_le_dist_first_terms)
also have "... \<le> 2 * f + e / 8"
apply (rule add_mono) using ** \<open>2^N > 8/e\<close> by(auto simp add: algebra_simps divide_simps)
also have "... \<le> e/2 + e/8"
unfolding f_def by auto
also have "... < e"
by auto
finally show "dist x y < e" by simp
qed
ultimately show ?thesis by auto
qed
lemma fun_open_ball_aux:
fixes U::"('a \<Rightarrow> 'b) set"
shows "open U \<longleftrightarrow> (\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U)"
proof (auto)
assume "open U"
fix x assume "x \<in> U"
then show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
using open_fun_contains_ball_aux[OF \<open>open U\<close> \<open>x \<in> U\<close>] by auto
next
assume H: "\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
define K where "K = {V. open V \<and> V \<subseteq> U}"
{
fix x assume "x \<in> U"
then obtain e where e: "e>0" "{y. dist x y < e} \<subseteq> U" using H by blast
then obtain V where V: "open V" "x \<in> V" "V \<subseteq> {y. dist x y < e}"
using ball_fun_contains_open_aux[OF \<open>e>0\<close>, of x] by auto
have "V \<in> K"
unfolding K_def using e(2) V(1) V(3) by auto
then have "x \<in> (\<Union>K)" using \<open>x \<in> V\<close> by auto
}
then have "(\<Union>K) = U"
unfolding K_def by auto
moreover have "open (\<Union>K)"
unfolding K_def by auto
ultimately show "open U" by simp
qed
instance proof
fix x y::"'a \<Rightarrow> 'b" show "(dist x y = 0) = (x = y)"
proof
assume "x = y"
then show "dist x y = 0" unfolding dist_fun_def using \<open>x = y\<close> by auto
next
assume "dist x y = 0"
have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 = 0" for n
using \<open>dist x y = 0\<close> unfolding dist_fun_def by (simp add: "*" suminf_eq_zero_iff)
then have "dist (x (from_nat n)) (y (from_nat n)) = 0" for n
by (metis div_0 min_def nonzero_mult_div_cancel_left power_eq_0_iff
zero_eq_1_divide_iff zero_neq_numeral)
then have "x (from_nat n) = y (from_nat n)" for n
by auto
then have "x i = y i" for i
by (metis from_nat_to_nat)
then show "x = y"
by auto
qed
next
text\<open>The proof of the triangular inequality is trivial, modulo the fact that we are dealing
with infinite series, hence we should justify the convergence at each step. In this
respect, the following simplification rule is extremely handy.\<close>
have [simp]: "summable (\<lambda>n. (1/2)^n * min (dist (u (from_nat n)) (v (from_nat n))) 1)" for u v::"'a \<Rightarrow> 'b"
by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
fix x y z::"'a \<Rightarrow> 'b"
{
fix n
have *: "dist (x (from_nat n)) (y (from_nat n)) \<le>
dist (x (from_nat n)) (z (from_nat n)) + dist (y (from_nat n)) (z (from_nat n))"
by (simp add: dist_triangle2)
have "0 \<le> dist (y (from_nat n)) (z (from_nat n))"
using zero_le_dist by blast
moreover
{
assume "min (dist (y (from_nat n)) (z (from_nat n))) 1 \<noteq> dist (y (from_nat n)) (z (from_nat n))"
then have "1 \<le> min (dist (x (from_nat n)) (z (from_nat n))) 1 + min (dist (y (from_nat n)) (z (from_nat n))) 1"
by (metis (no_types) diff_le_eq diff_self min_def zero_le_dist zero_le_one)
}
ultimately have "min (dist (x (from_nat n)) (y (from_nat n))) 1 \<le>
min (dist (x (from_nat n)) (z (from_nat n))) 1 + min (dist (y (from_nat n)) (z (from_nat n))) 1"
using * by linarith
} note ineq = this
have "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
unfolding dist_fun_def by simp
also have "... \<le> (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1
+ (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)"
apply (rule suminf_le)
using ineq apply (metis (no_types, hide_lams) add.right_neutral distrib_left
le_divide_eq_numeral1(1) mult_2_right mult_left_mono zero_le_one zero_le_power)
by (auto simp add: summable_add)
also have "... = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1)
+ (\<Sum>n. (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)"
by (rule suminf_add[symmetric], auto)
also have "... = dist x z + dist y z"
unfolding dist_fun_def by simp
finally show "dist x y \<le> dist x z + dist y z"
by simp
next
text\<open>Finally, we show that the topology generated by the distance and the product
topology coincide. This is essentially contained in Lemma \<open>fun_open_ball_aux\<close>,
except that the condition to prove is expressed with filters. To deal with this,
we copy some mumbo jumbo from Lemma \<open>eventually_uniformity_metric\<close> in
\<^file>\<open>~~/src/HOL/Real_Vector_Spaces.thy\<close>\<close>
fix U::"('a \<Rightarrow> 'b) set"
have "eventually P uniformity \<longleftrightarrow> (\<exists>e>0. \<forall>x (y::('a \<Rightarrow> 'b)). dist x y < e \<longrightarrow> P (x, y))" for P
unfolding uniformity_fun_def apply (subst eventually_INF_base)
by (auto simp: eventually_principal subset_eq intro: bexI[of _ "min _ _"])
then show "open U = (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)"
unfolding fun_open_ball_aux by simp
qed (simp add: uniformity_fun_def)
end
text \<open>Nice properties of spaces are preserved under countable products. In addition
to first countability, second countability and metrizability, as we have seen above,
completeness is also preserved, and therefore being Polish.\<close>
instance "fun" :: (countable, complete_space) complete_space
proof
fix u::"nat \<Rightarrow> ('a \<Rightarrow> 'b)" assume "Cauchy u"
have "Cauchy (\<lambda>n. u n i)" for i
unfolding cauchy_def proof (intro impI allI)
fix e assume "e>(0::real)"
obtain k where "i = from_nat k"
using from_nat_to_nat[of i] by metis
have "(1/2)^k * min e 1 > 0" using \<open>e>0\<close> by auto
then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"
using \<open>Cauchy u\<close> unfolding cauchy_def by blast
then obtain N::nat where C: "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"
by blast
have "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
proof (auto)
fix m n::nat assume "m \<ge> N" "n \<ge> N"
have "(1/2)^k * min (dist (u m i) (u n i)) 1
= sum (\<lambda>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1) {k}"
using \<open>i = from_nat k\<close> by auto
also have "... \<le> (\<Sum>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1)"
apply (rule sum_le_suminf)
by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
also have "... = dist (u m) (u n)"
unfolding dist_fun_def by auto
also have "... < (1/2)^k * min e 1"
using C \<open>m \<ge> N\<close> \<open>n \<ge> N\<close> by auto
finally have "min (dist (u m i) (u n i)) 1 < min e 1"
by (auto simp add: algebra_simps divide_simps)
then show "dist (u m i) (u n i) < e" by auto
qed
then show "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
by blast
qed
then have "\<exists>x. (\<lambda>n. u n i) \<longlonglongrightarrow> x" for i
using Cauchy_convergent convergent_def by auto
then have "\<exists>x. \<forall>i. (\<lambda>n. u n i) \<longlonglongrightarrow> x i"
using choice by force
then obtain x where *: "\<And>i. (\<lambda>n. u n i) \<longlonglongrightarrow> x i" by blast
have "u \<longlonglongrightarrow> x"
proof (rule metric_LIMSEQ_I)
fix e assume [simp]: "e>(0::real)"
have i: "\<exists>K. \<forall>n\<ge>K. dist (u n i) (x i) < e/4" for i
by (rule metric_LIMSEQ_D, auto simp add: *)
have "\<exists>K. \<forall>i. \<forall>n\<ge>K i. dist (u n i) (x i) < e/4"
apply (rule choice) using i by auto
then obtain K where K: "\<And>i n. n \<ge> K i \<Longrightarrow> dist (u n i) (x i) < e/4"
by blast
have "\<exists>N::nat. 2^N > 4/e"
by (simp add: real_arch_pow)
then obtain N::nat where "2^N > 4/e" by auto
define L where "L = Max {K (from_nat n)|n. n \<le> N}"
have "dist (u k) x < e" if "k \<ge> L" for k
proof -
have *: "dist (u k (from_nat n)) (x (from_nat n)) \<le> e / 4" if "n \<le> N" for n
proof -
have "K (from_nat n) \<le> L"
unfolding L_def apply (rule Max_ge) using \<open>n \<le> N\<close> by auto
then have "k \<ge> K (from_nat n)" using \<open>k \<ge> L\<close> by auto
then show ?thesis using K less_imp_le by auto
qed
have **: "Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n \<le> N} \<le> e/4"
apply (rule Max.boundedI) using * by auto
have "dist (u k) x \<le> 2 * Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n \<le> N} + (1/2)^N"
using dist_fun_le_dist_first_terms by auto
also have "... \<le> 2 * e/4 + e/4"
apply (rule add_mono)
using ** \<open>2^N > 4/e\<close> less_imp_le by (auto simp add: algebra_simps divide_simps)
also have "... < e" by auto
finally show ?thesis by simp
qed
then show "\<exists>L. \<forall>k\<ge>L. dist (u k) x < e" by blast
qed
then show "convergent u" using convergent_def by blast
qed
instance "fun" :: (countable, polish_space) polish_space
by standard
subsection\<open>The Alexander subbase theorem\<close>
theorem Alexander_subbase:
assumes X: "topology (arbitrary union_of (finite intersection_of (\<lambda>x. x \<in> \<B>) relative_to \<Union>\<B>)) = X"
and fin: "\<And>C. \<lbrakk>C \<subseteq> \<B>; \<Union>C = topspace X\<rbrakk> \<Longrightarrow> \<exists>C'. finite C' \<and> C' \<subseteq> C \<and> \<Union>C' = topspace X"
shows "compact_space X"
proof -
have U\<B>: "\<Union>\<B> = topspace X"
by (simp flip: X)
have False if \<U>: "\<forall>U\<in>\<U>. openin X U" and sub: "topspace X \<subseteq> \<Union>\<U>"
and neg: "\<And>\<F>. \<lbrakk>\<F> \<subseteq> \<U>; finite \<F>\<rbrakk> \<Longrightarrow> \<not> topspace X \<subseteq> \<Union>\<F>" for \<U>
proof -
define \<A> where "\<A> \<equiv> {\<C>. (\<forall>U \<in> \<C>. openin X U) \<and> topspace X \<subseteq> \<Union>\<C> \<and> (\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> \<C> \<longrightarrow> ~(topspace X \<subseteq> \<Union>\<F>))}"
have 1: "\<A> \<noteq> {}"
unfolding \<A>_def using sub \<U> neg by force
have 2: "\<Union>\<C> \<in> \<A>" if "\<C>\<noteq>{}" and \<C>: "subset.chain \<A> \<C>" for \<C>
unfolding \<A>_def
proof (intro CollectI conjI ballI allI impI notI)
show "openin X U" if U: "U \<in> \<Union>\<C>" for U
using U \<C> unfolding \<A>_def subset_chain_def by force
have "\<C> \<subseteq> \<A>"
using subset_chain_def \<C> by blast
with that \<A>_def show UUC: "topspace X \<subseteq> \<Union>(\<Union>\<C>)"
by blast
show "False" if "finite \<F>" and "\<F> \<subseteq> \<Union>\<C>" and "topspace X \<subseteq> \<Union>\<F>" for \<F>
proof -
obtain \<B> where "\<B> \<in> \<C>" "\<F> \<subseteq> \<B>"
by (metis Sup_empty \<C> \<open>\<F> \<subseteq> \<Union>\<C>\<close> \<open>finite \<F>\<close> UUC empty_subsetI finite.emptyI finite_subset_Union_chain neg)
then show False
using \<A>_def \<open>\<C> \<subseteq> \<A>\<close> \<open>finite \<F>\<close> \<open>topspace X \<subseteq> \<Union>\<F>\<close> by blast
qed
qed
obtain \<K> where "\<K> \<in> \<A>" and "\<And>X. \<lbrakk>X\<in>\<A>; \<K> \<subseteq> X\<rbrakk> \<Longrightarrow> X = \<K>"
using subset_Zorn_nonempty [OF 1 2] by metis
then have *: "\<And>\<W>. \<lbrakk>\<And>W. W\<in>\<W> \<Longrightarrow> openin X W; topspace X \<subseteq> \<Union>\<W>; \<K> \<subseteq> \<W>;
\<And>\<F>. \<lbrakk>finite \<F>; \<F> \<subseteq> \<W>; topspace X \<subseteq> \<Union>\<F>\<rbrakk> \<Longrightarrow> False\<rbrakk>
\<Longrightarrow> \<W> = \<K>"
and ope: "\<forall>U\<in>\<K>. openin X U" and top: "topspace X \<subseteq> \<Union>\<K>"
and non: "\<And>\<F>. \<lbrakk>finite \<F>; \<F> \<subseteq> \<K>; topspace X \<subseteq> \<Union>\<F>\<rbrakk> \<Longrightarrow> False"
unfolding \<A>_def by simp_all metis+
then obtain x where "x \<in> topspace X" "x \<notin> \<Union>(\<B> \<inter> \<K>)"
proof -
have "\<Union>(\<B> \<inter> \<K>) \<noteq> \<Union>\<B>"
by (metis \<open>\<Union>\<B> = topspace X\<close> fin inf.bounded_iff non order_refl)
then have "\<exists>a. a \<notin> \<Union>(\<B> \<inter> \<K>) \<and> a \<in> \<Union>\<B>"
by blast
then show ?thesis
using that by (metis U\<B>)
qed
obtain C where C: "openin X C" "C \<in> \<K>" "x \<in> C"
using \<open>x \<in> topspace X\<close> ope top by auto
then have "C \<subseteq> topspace X"
by (metis openin_subset)
then have "(arbitrary union_of (finite intersection_of (\<lambda>x. x \<in> \<B>) relative_to \<Union>\<B>)) C"
using openin_subbase C unfolding X [symmetric] by blast
moreover have "C \<noteq> topspace X"
using \<open>\<K> \<in> \<A>\<close> \<open>C \<in> \<K>\<close> unfolding \<A>_def by blast
ultimately obtain \<V> W where W: "(finite intersection_of (\<lambda>x. x \<in> \<B>) relative_to topspace X) W"
and "x \<in> W" "W \<in> \<V>" "\<Union>\<V> \<noteq> topspace X" "C = \<Union>\<V>"
using C by (auto simp: union_of_def U\<B>)
then have "\<Union>\<V> \<subseteq> topspace X"
by (metis \<open>C \<subseteq> topspace X\<close>)
then have "topspace X \<notin> \<V>"
using \<open>\<Union>\<V> \<noteq> topspace X\<close> by blast
then obtain \<B>' where \<B>': "finite \<B>'" "\<B>' \<subseteq> \<B>" "x \<in> \<Inter>\<B>'" "W = topspace X \<inter> \<Inter>\<B>'"
using W \<open>x \<in> W\<close> unfolding relative_to_def intersection_of_def by auto
then have "\<Inter>\<B>' \<subseteq> \<Union>\<B>"
using \<open>W \<in> \<V>\<close> \<open>\<Union>\<V> \<noteq> topspace X\<close> \<open>\<Union>\<V> \<subseteq> topspace X\<close> by blast
then have "\<Inter>\<B>' \<subseteq> C"
using U\<B> \<open>C = \<Union>\<V>\<close> \<open>W = topspace X \<inter> \<Inter>\<B>'\<close> \<open>W \<in> \<V>\<close> by auto
have "\<forall>b \<in> \<B>'. \<exists>C'. finite C' \<and> C' \<subseteq> \<K> \<and> topspace X \<subseteq> \<Union>(insert b C')"
proof
fix b
assume "b \<in> \<B>'"
have "insert b \<K> = \<K>" if neg: "\<not> (\<exists>C'. finite C' \<and> C' \<subseteq> \<K> \<and> topspace X \<subseteq> \<Union>(insert b C'))"
proof (rule *)
show "openin X W" if "W \<in> insert b \<K>" for W
using that
proof
have "b \<in> \<B>"
using \<open>b \<in> \<B>'\<close> \<open>\<B>' \<subseteq> \<B>\<close> by blast
then have "\<exists>\<U>. finite \<U> \<and> \<U> \<subseteq> \<B> \<and> \<Inter>\<U> = b"
by (rule_tac x="{b}" in exI) auto
moreover have "\<Union>\<B> \<inter> b = b"
using \<B>'(2) \<open>b \<in> \<B>'\<close> by auto
ultimately show "openin X W" if "W = b"
using that \<open>b \<in> \<B>'\<close>
apply (simp add: openin_subbase flip: X)
apply (auto simp: arbitrary_def intersection_of_def relative_to_def intro!: union_of_inc)
done
show "openin X W" if "W \<in> \<K>"
by (simp add: \<open>W \<in> \<K>\<close> ope)
qed
next
show "topspace X \<subseteq> \<Union> (insert b \<K>)"
using top by auto
next
show False if "finite \<F>" and "\<F> \<subseteq> insert b \<K>" "topspace X \<subseteq> \<Union>\<F>" for \<F>
proof -
have "insert b (\<F> \<inter> \<K>) = \<F>"
using non that by blast
then show False
by (metis Int_lower2 finite_insert neg that(1) that(3))
qed
qed auto
then show "\<exists>C'. finite C' \<and> C' \<subseteq> \<K> \<and> topspace X \<subseteq> \<Union>(insert b C')"
using \<open>b \<in> \<B>'\<close> \<open>x \<notin> \<Union>(\<B> \<inter> \<K>)\<close> \<B>'
by (metis IntI InterE Union_iff subsetD insertI1)
qed
then obtain F where F: "\<forall>b \<in> \<B>'. finite (F b) \<and> F b \<subseteq> \<K> \<and> topspace X \<subseteq> \<Union>(insert b (F b))"
by metis
let ?\<D> = "insert C (\<Union>(F ` \<B>'))"
show False
proof (rule non)
have "topspace X \<subseteq> (\<Inter>b \<in> \<B>'. \<Union>(insert b (F b)))"
using F by (simp add: INT_greatest)
also have "\<dots> \<subseteq> \<Union>?\<D>"
using \<open>\<Inter>\<B>' \<subseteq> C\<close> by force
finally show "topspace X \<subseteq> \<Union>?\<D>" .
show "?\<D> \<subseteq> \<K>"
using \<open>C \<in> \<K>\<close> F by auto
show "finite ?\<D>"
using \<open>finite \<B>'\<close> F by auto
qed
qed
then show ?thesis
by (force simp: compact_space_def compactin_def)
qed
corollary Alexander_subbase_alt:
assumes "U \<subseteq> \<Union>\<B>"
and fin: "\<And>C. \<lbrakk>C \<subseteq> \<B>; U \<subseteq> \<Union>C\<rbrakk> \<Longrightarrow> \<exists>C'. finite C' \<and> C' \<subseteq> C \<and> U \<subseteq> \<Union>C'"
and X: "topology
(arbitrary union_of
(finite intersection_of (\<lambda>x. x \<in> \<B>) relative_to U)) = X"
shows "compact_space X"
proof -
have "topspace X = U"
using X topspace_subbase by fastforce
have eq: "\<Union> (Collect ((\<lambda>x. x \<in> \<B>) relative_to U)) = U"
unfolding relative_to_def
using \<open>U \<subseteq> \<Union>\<B>\<close> by blast
have *: "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<C> \<and> \<Union>\<F> = topspace X"
if "\<C> \<subseteq> Collect ((\<lambda>x. x \<in> \<B>) relative_to topspace X)" and UC: "\<Union>\<C> = topspace X" for \<C>
proof -
have "\<C> \<subseteq> (\<lambda>U. topspace X \<inter> U) ` \<B>"
using that by (auto simp: relative_to_def)
then obtain \<B>' where "\<B>' \<subseteq> \<B>" and \<B>': "\<C> = (\<inter>) (topspace X) ` \<B>'"
by (auto simp: subset_image_iff)
moreover have "U \<subseteq> \<Union>\<B>'"
using \<B>' \<open>topspace X = U\<close> UC by auto
ultimately obtain \<C>' where "finite \<C>'" "\<C>' \<subseteq> \<B>'" "U \<subseteq> \<Union>\<C>'"
using fin [of \<B>'] \<open>topspace X = U\<close> \<open>U \<subseteq> \<Union>\<B>\<close> by blast
then show ?thesis
unfolding \<B>' exists_finite_subset_image \<open>topspace X = U\<close> by auto
qed
show ?thesis
apply (rule Alexander_subbase [where \<B> = "Collect ((\<lambda>x. x \<in> \<B>) relative_to (topspace X))"])
apply (simp flip: X)
apply (metis finite_intersection_of_relative_to eq)
apply (blast intro: *)
done
qed
proposition continuous_map_componentwise:
"continuous_map X (product_topology Y I) f \<longleftrightarrow>
f ` (topspace X) \<subseteq> extensional I \<and> (\<forall>k \<in> I. continuous_map X (Y k) (\<lambda>x. f x k))"
(is "?lhs \<longleftrightarrow> _ \<and> ?rhs")
proof (cases "\<forall>x \<in> topspace X. f x \<in> extensional I")
case True
then have "f ` (topspace X) \<subseteq> extensional I"
by force
moreover have ?rhs if L: ?lhs
proof -
have "openin X {x \<in> topspace X. f x k \<in> U}" if "k \<in> I" and "openin (Y k) U" for k U
proof -
have "openin (product_topology Y I) ({Y. Y k \<in> U} \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (Y i)))"
apply (simp add: openin_product_topology flip: arbitrary_union_of_relative_to)
apply (simp add: relative_to_def)
using that apply (blast intro: arbitrary_union_of_inc finite_intersection_of_inc)
done
with that have "openin X {x \<in> topspace X. f x \<in> ({Y. Y k \<in> U} \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (Y i)))}"
using L unfolding continuous_map_def by blast
moreover have "{x \<in> topspace X. f x \<in> ({Y. Y k \<in> U} \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (Y i)))} = {x \<in> topspace X. f x k \<in> U}"
using L by (auto simp: continuous_map_def)
ultimately show ?thesis
by metis
qed
with that
show ?thesis
by (auto simp: continuous_map_def)
qed
moreover have ?lhs if ?rhs
proof -
have 1: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (Y i))"
using that True by (auto simp: continuous_map_def PiE_iff)
have 2: "{x \<in> S. \<exists>T\<in>\<T>. f x \<in> T} = (\<Union>T\<in>\<T>. {x \<in> S. f x \<in> T})" for S \<T>
by blast
have 3: "{x \<in> S. \<forall>U\<in>\<U>. f x \<in> U} = (\<Inter> (insert S ((\<lambda>U. {x \<in> S. f x \<in> U}) ` \<U>)))" for S \<U>
by blast
show ?thesis
unfolding continuous_map_def openin_product_topology arbitrary_def
proof (clarsimp simp: all_union_of 1 2)
fix \<T>
assume \<T>: "\<T> \<subseteq> Collect (finite intersection_of (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (Y i) U)
relative_to (\<Pi>\<^sub>E i\<in>I. topspace (Y i)))"
show "openin X (\<Union>T\<in>\<T>. {x \<in> topspace X. f x \<in> T})"
proof (rule openin_Union; clarify)
fix S T
assume "T \<in> \<T>"
obtain \<U> where "T = (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<U>" and "finite \<U>"
"\<U> \<subseteq> {{f. f i \<in> U} |i U. i \<in> I \<and> openin (Y i) U}"
using subsetD [OF \<T> \<open>T \<in> \<T>\<close>] by (auto simp: intersection_of_def relative_to_def)
with that show "openin X {x \<in> topspace X. f x \<in> T}"
apply (simp add: continuous_map_def 1 cong: conj_cong)
unfolding 3
apply (rule openin_Inter; auto)
done
qed
qed
qed
ultimately show ?thesis
by metis
next
case False
then show ?thesis
by (auto simp: continuous_map_def PiE_def)
qed
lemma continuous_map_componentwise_UNIV:
"continuous_map X (product_topology Y UNIV) f \<longleftrightarrow> (\<forall>k. continuous_map X (Y k) (\<lambda>x. f x k))"
by (simp add: continuous_map_componentwise)
lemma continuous_map_product_projection [continuous_intros]:
"k \<in> I \<Longrightarrow> continuous_map (product_topology X I) (X k) (\<lambda>x. x k)"
using continuous_map_componentwise [of "product_topology X I" X I id] by simp
declare continuous_map_from_subtopology [OF continuous_map_product_projection, continuous_intros]
proposition open_map_product_projection:
assumes "i \<in> I"
shows "open_map (product_topology Y I) (Y i) (\<lambda>f. f i)"
unfolding openin_product_topology all_union_of arbitrary_def open_map_def image_Union
proof clarify
fix \<V>
assume \<V>: "\<V> \<subseteq> Collect
(finite intersection_of
(\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (Y i) U) relative_to
topspace (product_topology Y I))"
show "openin (Y i) (\<Union>x\<in>\<V>. (\<lambda>f. f i) ` x)"
proof (rule openin_Union, clarify)
fix S V
assume "V \<in> \<V>"
obtain \<F> where "finite \<F>"
and V: "V = (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<F>"
and \<F>: "\<F> \<subseteq> {{f. f i \<in> U} |i U. i \<in> I \<and> openin (Y i) U}"
using subsetD [OF \<V> \<open>V \<in> \<V>\<close>]
by (auto simp: intersection_of_def relative_to_def)
show "openin (Y i) ((\<lambda>f. f i) ` V)"
proof (subst openin_subopen; clarify)
fix x f
assume "f \<in> V"
let ?T = "{a \<in> topspace(Y i).
(\<lambda>j. if j = i then a
else if j \<in> I then f j else undefined) \<in> (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<F>}"
show "\<exists>T. openin (Y i) T \<and> f i \<in> T \<and> T \<subseteq> (\<lambda>f. f i) ` V"
proof (intro exI conjI)
show "openin (Y i) ?T"
proof (rule openin_continuous_map_preimage)
have "continuous_map (Y i) (Y k) (\<lambda>x. if k = i then x else f k)" if "k \<in> I" for k
proof (cases "k=i")
case True
then show ?thesis
by (metis (mono_tags) continuous_map_id eq_id_iff)
next
case False
then show ?thesis
by simp (metis IntD1 PiE_iff V \<open>f \<in> V\<close> that)
qed
then show "continuous_map (Y i) (product_topology Y I)
(\<lambda>x j. if j = i then x else if j \<in> I then f j else undefined)"
by (auto simp: continuous_map_componentwise assms extensional_def)
next
have "openin (product_topology Y I) (\<Pi>\<^sub>E i\<in>I. topspace (Y i))"
by (metis openin_topspace topspace_product_topology)
moreover have "openin (product_topology Y I) (\<Inter>B\<in>\<F>. (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> B)"
if "\<F> \<noteq> {}"
proof -
show ?thesis
proof (rule openin_Inter)
show "\<And>X. X \<in> (\<inter>) (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) ` \<F> \<Longrightarrow> openin (product_topology Y I) X"
unfolding openin_product_topology relative_to_def
apply (clarify intro!: arbitrary_union_of_inc)
apply (rename_tac F)
apply (rule_tac x=F in exI)
using subsetD [OF \<F>]
apply (force intro: finite_intersection_of_inc)
done
qed (use \<open>finite \<F>\<close> \<open>\<F> \<noteq> {}\<close> in auto)
qed
ultimately show "openin (product_topology Y I) ((\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<F>)"
by (auto simp only: Int_Inter_eq split: if_split)
qed
next
have eqf: "(\<lambda>j. if j = i then f i else if j \<in> I then f j else undefined) = f"
using PiE_arb V \<open>f \<in> V\<close> by force
show "f i \<in> ?T"
using V assms \<open>f \<in> V\<close> by (auto simp: PiE_iff eqf)
next
show "?T \<subseteq> (\<lambda>f. f i) ` V"
unfolding V by (auto simp: intro!: rev_image_eqI)
qed
qed
qed
qed
lemma retraction_map_product_projection:
assumes "i \<in> I"
shows "(retraction_map (product_topology X I) (X i) (\<lambda>x. x i) \<longleftrightarrow>
(topspace (product_topology X I) = {}) \<longrightarrow> topspace (X i) = {})"
(is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
using retraction_imp_surjective_map by force
next
assume R: ?rhs
show ?lhs
proof (cases "topspace (product_topology X I) = {}")
case True
then show ?thesis
using R by (auto simp: retraction_map_def retraction_maps_def continuous_map_on_empty)
next
case False
have *: "\<exists>g. continuous_map (X i) (product_topology X I) g \<and> (\<forall>x\<in>topspace (X i). g x i = x)"
if z: "z \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))" for z
proof -
have cm: "continuous_map (X i) (X j) (\<lambda>x. if j = i then x else z j)" if "j \<in> I" for j
using \<open>j \<in> I\<close> z by (case_tac "j = i") auto
show ?thesis
using \<open>i \<in> I\<close> that
by (rule_tac x="\<lambda>x j. if j = i then x else z j" in exI) (auto simp: continuous_map_componentwise PiE_iff extensional_def cm)
qed
show ?thesis
using \<open>i \<in> I\<close> False
by (auto simp: retraction_map_def retraction_maps_def assms continuous_map_product_projection *)
qed
qed
subsection \<open>Open Pi-sets in the product topology\<close>
proposition openin_PiE_gen:
"openin (product_topology X I) (PiE I S) \<longleftrightarrow>
PiE I S = {} \<or>
finite {i \<in> I. ~(S i = topspace(X i))} \<and> (\<forall>i \<in> I. openin (X i) (S i))"
(is "?lhs \<longleftrightarrow> _ \<or> ?rhs")
proof (cases "PiE I S = {}")
case False
moreover have "?lhs = ?rhs"
proof
assume L: ?lhs
moreover
obtain z where z: "z \<in> PiE I S"
using False by blast
ultimately obtain U where fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}"
and "Pi\<^sub>E I U \<noteq> {}"
and sub: "Pi\<^sub>E I U \<subseteq> Pi\<^sub>E I S"
by (fastforce simp add: openin_product_topology_alt)
then have *: "\<And>i. i \<in> I \<Longrightarrow> U i \<subseteq> S i"
by (simp add: subset_PiE)
show ?rhs
proof (intro conjI ballI)
show "finite {i \<in> I. S i \<noteq> topspace (X i)}"
apply (rule finite_subset [OF _ fin], clarify)
using *
by (metis False L openin_subset topspace_product_topology subset_PiE subset_antisym)
next
fix i :: "'a"
assume "i \<in> I"
then show "openin (X i) (S i)"
using open_map_product_projection [of i I X] L
apply (simp add: open_map_def)
apply (drule_tac x="PiE I S" in spec)
apply (simp add: False image_projection_PiE split: if_split_asm)
done
qed
next
assume ?rhs
then show ?lhs
apply (simp only: openin_product_topology)
apply (rule arbitrary_union_of_inc)
apply (auto simp: product_topology_base_alt)
done
qed
ultimately show ?thesis
by simp
qed simp
corollary openin_PiE:
"finite I \<Longrightarrow> openin (product_topology X I) (PiE I S) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. openin (X i) (S i))"
by (simp add: openin_PiE_gen)
proposition compact_space_product_topology:
"compact_space(product_topology X I) \<longleftrightarrow>
topspace(product_topology X I) = {} \<or> (\<forall>i \<in> I. compact_space(X i))"
(is "?lhs = ?rhs")
proof (cases "topspace(product_topology X I) = {}")
case False
then obtain z where z: "z \<in> (\<Pi>\<^sub>E i\<in>I. topspace(X i))"
by auto
show ?thesis
proof
assume L: ?lhs
show ?rhs
proof (clarsimp simp add: False compact_space_def)
fix i
assume "i \<in> I"
with L have "continuous_map (product_topology X I) (X i) (\<lambda>f. f i)"
by (simp add: continuous_map_product_projection)
moreover
have "\<And>x. x \<in> topspace (X i) \<Longrightarrow> x \<in> (\<lambda>f. f i) ` (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
using \<open>i \<in> I\<close> z
apply (rule_tac x="\<lambda>j. if j = i then x else if j \<in> I then z j else undefined" in image_eqI, auto)
done
then have "(\<lambda>f. f i) ` (\<Pi>\<^sub>E i\<in>I. topspace (X i)) = topspace (X i)"
using \<open>i \<in> I\<close> z by auto
ultimately show "compactin (X i) (topspace (X i))"
by (metis L compact_space_def image_compactin topspace_product_topology)
qed
next
assume R: ?rhs
show ?lhs
proof (cases "I = {}")
case True
with R show ?thesis
by (simp add: compact_space_def)
next
case False
then obtain i where "i \<in> I"
by blast
show ?thesis
using R
proof
assume com [rule_format]: "\<forall>i\<in>I. compact_space (X i)"
let ?\<C> = "{{f. f i \<in> U} |i U. i \<in> I \<and> openin (X i) U}"
show "compact_space (product_topology X I)"
proof (rule Alexander_subbase_alt)
show "topspace (product_topology X I) \<subseteq> \<Union>?\<C>"
unfolding topspace_product_topology using \<open>i \<in> I\<close> by blast
next
fix C
assume Csub: "C \<subseteq> ?\<C>" and UC: "topspace (product_topology X I) \<subseteq> \<Union>C"
define \<D> where "\<D> \<equiv> \<lambda>i. {U. openin (X i) U \<and> {f. f i \<in> U} \<in> C}"
show "\<exists>C'. finite C' \<and> C' \<subseteq> C \<and> topspace (product_topology X I) \<subseteq> \<Union>C'"
proof (cases "\<exists>i. i \<in> I \<and> topspace (X i) \<subseteq> \<Union>(\<D> i)")
case True
then obtain i where "i \<in> I"
and i: "topspace (X i) \<subseteq> \<Union>(\<D> i)"
unfolding \<D>_def by blast
then have *: "\<And>\<U>. \<lbrakk>Ball \<U> (openin (X i)); topspace (X i) \<subseteq> \<Union>\<U>\<rbrakk> \<Longrightarrow>
\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> topspace (X i) \<subseteq> \<Union>\<F>"
using com [OF \<open>i \<in> I\<close>] by (auto simp: compact_space_def compactin_def)
have "topspace (X i) \<subseteq> \<Union>(\<D> i)"
using i by auto
with * obtain \<F> where "finite \<F> \<and> \<F> \<subseteq> (\<D> i) \<and> topspace (X i) \<subseteq> \<Union>\<F>"
unfolding \<D>_def by fastforce
with \<open>i \<in> I\<close> show ?thesis
unfolding \<D>_def
by (rule_tac x="(\<lambda>U. {x. x i \<in> U}) ` \<F>" in exI) auto
next
case False
then have "\<forall>i \<in> I. \<exists>y. y \<in> topspace (X i) \<and> y \<notin> \<Union>(\<D> i)"
by force
then obtain g where g: "\<And>i. i \<in> I \<Longrightarrow> g i \<in> topspace (X i) \<and> g i \<notin> \<Union>(\<D> i)"
by metis
then have "(\<lambda>i. if i \<in> I then g i else undefined) \<in> topspace (product_topology X I)"
by (simp add: PiE_I)
moreover have "(\<lambda>i. if i \<in> I then g i else undefined) \<notin> \<Union>C"
using Csub g unfolding \<D>_def by force
ultimately show ?thesis
using UC by blast
qed
qed (simp add: product_topology)
qed (simp add: compact_space_topspace_empty)
qed
qed
qed (simp add: compact_space_topspace_empty)
corollary compactin_PiE:
"compactin (product_topology X I) (PiE I S) \<longleftrightarrow>
PiE I S = {} \<or> (\<forall>i \<in> I. compactin (X i) (S i))"
by (auto simp: compactin_subspace subtopology_PiE subset_PiE compact_space_product_topology
PiE_eq_empty_iff)
lemma in_product_topology_closure_of:
"z \<in> (product_topology X I) closure_of S
\<Longrightarrow> i \<in> I \<Longrightarrow> z i \<in> ((X i) closure_of ((\<lambda>x. x i) ` S))"
using continuous_map_product_projection
by (force simp: continuous_map_eq_image_closure_subset image_subset_iff)
lemma homeomorphic_space_singleton_product:
"product_topology X {k} homeomorphic_space (X k)"
unfolding homeomorphic_space
apply (rule_tac x="\<lambda>x. x k" in exI)
apply (rule bijective_open_imp_homeomorphic_map)
apply (simp_all add: continuous_map_product_projection open_map_product_projection)
unfolding PiE_over_singleton_iff
apply (auto simp: image_iff inj_on_def)
done
subsection\<open>Relationship with connected spaces, paths, etc.\<close>
proposition connected_space_product_topology:
"connected_space(product_topology X I) \<longleftrightarrow>
(\<Pi>\<^sub>E i\<in>I. topspace (X i)) = {} \<or> (\<forall>i \<in> I. connected_space(X i))"
(is "?lhs \<longleftrightarrow> ?eq \<or> ?rhs")
proof (cases ?eq)
case False
moreover have "?lhs = ?rhs"
proof
assume ?lhs
moreover
have "connectedin(X i) (topspace(X i))"
if "i \<in> I" and ci: "connectedin(product_topology X I) (topspace(product_topology X I))" for i
proof -
have cm: "continuous_map (product_topology X I) (X i) (\<lambda>f. f i)"
by (simp add: \<open>i \<in> I\<close> continuous_map_product_projection)
show ?thesis
using connectedin_continuous_map_image [OF cm ci] \<open>i \<in> I\<close>
by (simp add: False image_projection_PiE)
qed
ultimately show ?rhs
by (meson connectedin_topspace)
next
assume cs [rule_format]: ?rhs
have False
if disj: "U \<inter> V = {}" and subUV: "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<subseteq> U \<union> V"
and U: "openin (product_topology X I) U"
and V: "openin (product_topology X I) V"
and "U \<noteq> {}" "V \<noteq> {}"
for U V
proof -
obtain f where "f \<in> U"
using \<open>U \<noteq> {}\<close> by blast
then have f: "f \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
using U openin_subset by fastforce
have "U \<subseteq> topspace(product_topology X I)" "V \<subseteq> topspace(product_topology X I)"
using U V openin_subset by blast+
moreover have "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<subseteq> U"
proof -
obtain C where "(finite intersection_of (\<lambda>F. \<exists>i U. F = {x. x i \<in> U} \<and> i \<in> I \<and> openin (X i) U) relative_to
(\<Pi>\<^sub>E i\<in>I. topspace (X i))) C" "C \<subseteq> U" "f \<in> C"
using U \<open>f \<in> U\<close> unfolding openin_product_topology union_of_def by auto
then obtain \<T> where "finite \<T>"
and t: "\<And>C. C \<in> \<T> \<Longrightarrow> \<exists>i u. (i \<in> I \<and> openin (X i) u) \<and> C = {x. x i \<in> u}"
and subU: "topspace (product_topology X I) \<inter> \<Inter>\<T> \<subseteq> U"
and ftop: "f \<in> topspace (product_topology X I)"
and fint: "f \<in> \<Inter> \<T>"
by (fastforce simp: relative_to_def intersection_of_def subset_iff)
let ?L = "\<Union>C\<in>\<T>. {i. (\<lambda>x. x i) ` C \<subset> topspace (X i)}"
obtain L where "finite L"
and L: "\<And>i U. \<lbrakk>i \<in> I; openin (X i) U; U \<subset> topspace(X i); {x. x i \<in> U} \<in> \<T>\<rbrakk> \<Longrightarrow> i \<in> L"
proof
show "finite ?L"
proof (rule finite_Union)
fix M
assume "M \<in> (\<lambda>C. {i. (\<lambda>x. x i) ` C \<subset> topspace (X i)}) ` \<T>"
then obtain C where "C \<in> \<T>" and C: "M = {i. (\<lambda>x. x i) ` C \<subset> topspace (X i)}"
by blast
then obtain j V where "j \<in> I" and ope: "openin (X j) V" and Ceq: "C = {x. x j \<in> V}"
using t by meson
then have "f j \<in> V"
using \<open>C \<in> \<T>\<close> fint by force
then have "(\<lambda>x. x k) ` {x. x j \<in> V} = UNIV" if "k \<noteq> j" for k
using that
apply (clarsimp simp add: set_eq_iff)
apply (rule_tac x="\<lambda>m. if m = k then x else f m" in image_eqI, auto)
done
then have "{i. (\<lambda>x. x i) ` C \<subset> topspace (X i)} \<subseteq> {j}"
using Ceq by auto
then show "finite M"
using C finite_subset by fastforce
qed (use \<open>finite \<T>\<close> in blast)
next
fix i U
assume "i \<in> I" and ope: "openin (X i) U" and psub: "U \<subset> topspace (X i)" and int: "{x. x i \<in> U} \<in> \<T>"
then show "i \<in> ?L"
by (rule_tac a="{x. x i \<in> U}" in UN_I) (force+)
qed
show ?thesis
proof
fix h
assume h: "h \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
define g where "g \<equiv> \<lambda>i. if i \<in> L then f i else h i"
have gin: "g \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
unfolding g_def using f h by auto
moreover have "g \<in> X" if "X \<in> \<T>" for X
using fint openin_subset t [OF that] L g_def h that by fastforce
ultimately have "g \<in> U"
using subU by auto
have "h \<in> U" if "finite M" "h \<in> PiE I (topspace \<circ> X)" "{i \<in> I. h i \<noteq> g i} \<subseteq> M" for M h
using that
proof (induction arbitrary: h)
case empty
then show ?case
using PiE_ext \<open>g \<in> U\<close> gin by force
next
case (insert i M)
define f where "f \<equiv> \<lambda>j. if j = i then g i else h j"
have fin: "f \<in> PiE I (topspace \<circ> X)"
unfolding f_def using gin insert.prems(1) by auto
have subM: "{j \<in> I. f j \<noteq> g j} \<subseteq> M"
unfolding f_def using insert.prems(2) by auto
have "f \<in> U"
using insert.IH [OF fin subM] .
show ?case
proof (cases "h \<in> V")
case True
show ?thesis
proof (cases "i \<in> I")
case True
let ?U = "{x \<in> topspace(X i). (\<lambda>j. if j = i then x else h j) \<in> U}"
let ?V = "{x \<in> topspace(X i). (\<lambda>j. if j = i then x else h j) \<in> V}"
have False
proof (rule connected_spaceD [OF cs [OF \<open>i \<in> I\<close>]])
have "\<And>k. k \<in> I \<Longrightarrow> continuous_map (X i) (X k) (\<lambda>x. if k = i then x else h k)"
using continuous_map_eq_topcontinuous_at insert.prems(1) topcontinuous_at_def by fastforce
then have cm: "continuous_map (X i) (product_topology X I) (\<lambda>x j. if j = i then x else h j)"
using \<open>i \<in> I\<close> insert.prems(1)
by (auto simp: continuous_map_componentwise extensional_def)
show "openin (X i) ?U"
by (rule openin_continuous_map_preimage [OF cm U])
show "openin (X i) ?V"
by (rule openin_continuous_map_preimage [OF cm V])
show "topspace (X i) \<subseteq> ?U \<union> ?V"
proof clarsimp
fix x
assume "x \<in> topspace (X i)" and "(\<lambda>j. if j = i then x else h j) \<notin> V"
with True subUV \<open>h \<in> Pi\<^sub>E I (topspace \<circ> X)\<close>
show "(\<lambda>j. if j = i then x else h j) \<in> U"
by (drule_tac c="(\<lambda>j. if j = i then x else h j)" in subsetD) auto
qed
show "?U \<inter> ?V = {}"
using disj by blast
show "?U \<noteq> {}"
using \<open>U \<noteq> {}\<close> f_def
proof -
have "(\<lambda>j. if j = i then g i else h j) \<in> U"
using \<open>f \<in> U\<close> f_def by blast
moreover have "f i \<in> topspace (X i)"
by (metis PiE_iff True comp_apply fin)
ultimately have "\<exists>b. b \<in> topspace (X i) \<and> (\<lambda>a. if a = i then b else h a) \<in> U"
using f_def by auto
then show ?thesis
by blast
qed
have "(\<lambda>j. if j = i then h i else h j) = h"
by force
moreover have "h i \<in> topspace (X i)"
using True insert.prems(1) by auto
ultimately show "?V \<noteq> {}"
using \<open>h \<in> V\<close> by force
qed
then show ?thesis ..
next
case False
show ?thesis
proof (cases "h = f")
case True
show ?thesis
by (rule insert.IH [OF insert.prems(1)]) (simp add: True subM)
next
case False
then show ?thesis
using gin insert.prems(1) \<open>i \<notin> I\<close> unfolding f_def by fastforce
qed
qed
next
case False
then show ?thesis
using subUV insert.prems(1) by auto
qed
qed
then show "h \<in> U"
unfolding g_def using PiE_iff \<open>finite L\<close> h by fastforce
qed
qed
ultimately show ?thesis
using disj inf_absorb2 \<open>V \<noteq> {}\<close> by fastforce
qed
then show ?lhs
unfolding connected_space_def
by auto
qed
ultimately show ?thesis
by simp
qed (simp add: connected_space_topspace_empty)
lemma connectedin_PiE:
"connectedin (product_topology X I) (PiE I S) \<longleftrightarrow>
PiE I S = {} \<or> (\<forall>i \<in> I. connectedin (X i) (S i))"
by (fastforce simp add: connectedin_def subtopology_PiE connected_space_product_topology subset_PiE PiE_eq_empty_iff
topspace_subtopology_subset)
lemma path_connected_space_product_topology:
"path_connected_space(product_topology X I) \<longleftrightarrow>
topspace(product_topology X I) = {} \<or> (\<forall>i \<in> I. path_connected_space(X i))"
(is "?lhs \<longleftrightarrow> ?eq \<or> ?rhs")
proof (cases ?eq)
case False
moreover have "?lhs = ?rhs"
proof
assume L: ?lhs
show ?rhs
proof (clarsimp simp flip: path_connectedin_topspace)
fix i :: "'a"
assume "i \<in> I"
have cm: "continuous_map (product_topology X I) (X i) (\<lambda>f. f i)"
by (simp add: \<open>i \<in> I\<close> continuous_map_product_projection)
show "path_connectedin (X i) (topspace (X i))"
using path_connectedin_continuous_map_image [OF cm L [unfolded path_connectedin_topspace [symmetric]]]
by (metis \<open>i \<in> I\<close> False retraction_imp_surjective_map retraction_map_product_projection)
qed
next
assume R [rule_format]: ?rhs
show ?lhs
unfolding path_connected_space_def topspace_product_topology
proof clarify
fix x y
assume x: "x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))" and y: "y \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
have "\<forall>i. \<exists>g. i \<in> I \<longrightarrow> pathin (X i) g \<and> g 0 = x i \<and> g 1 = y i"
using PiE_mem R path_connected_space_def x y by force
then obtain g where g: "\<And>i. i \<in> I \<Longrightarrow> pathin (X i) (g i) \<and> g i 0 = x i \<and> g i 1 = y i"
by metis
with x y show "\<exists>g. pathin (product_topology X I) g \<and> g 0 = x \<and> g 1 = y"
apply (rule_tac x="\<lambda>a. \<lambda>i \<in> I. g i a" in exI)
apply (force simp: pathin_def continuous_map_componentwise)
done
qed
qed
ultimately show ?thesis
by simp
qed (simp add: path_connected_space_topspace_empty)
lemma path_connectedin_PiE:
"path_connectedin (product_topology X I) (PiE I S) \<longleftrightarrow>
PiE I S = {} \<or> (\<forall>i \<in> I. path_connectedin (X i) (S i))"
by (fastforce simp add: path_connectedin_def subtopology_PiE path_connected_space_product_topology subset_PiE PiE_eq_empty_iff topspace_subtopology_subset)
subsection \<open>Projections from a function topology to a component\<close>
lemma quotient_map_product_projection:
assumes "i \<in> I"
shows "quotient_map(product_topology X I) (X i) (\<lambda>x. x i) \<longleftrightarrow>
(topspace(product_topology X I) = {} \<longrightarrow> topspace(X i) = {})"
(is "?lhs = ?rhs")
proof
assume ?lhs with assms show ?rhs
by (auto simp: continuous_open_quotient_map open_map_product_projection)
next
assume ?rhs with assms show ?lhs
by (auto simp: Abstract_Topology.retraction_imp_quotient_map retraction_map_product_projection)
qed
lemma product_topology_homeomorphic_component:
assumes "i \<in> I" "\<And>j. \<lbrakk>j \<in> I; j \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>a. topspace(X j) = {a}"
shows "product_topology X I homeomorphic_space (X i)"
proof -
have "quotient_map (product_topology X I) (X i) (\<lambda>x. x i)"
using assms by (force simp add: quotient_map_product_projection PiE_eq_empty_iff)
moreover
have "inj_on (\<lambda>x. x i) (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
using assms by (auto simp: inj_on_def PiE_iff) (metis extensionalityI singletonD)
ultimately show ?thesis
unfolding homeomorphic_space_def
by (rule_tac x="\<lambda>x. x i" in exI) (simp add: homeomorphic_map_def flip: homeomorphic_map_maps)
qed
lemma topological_property_of_product_component:
assumes major: "P (product_topology X I)"
and minor: "\<And>z i. \<lbrakk>z \<in> (\<Pi>\<^sub>E i\<in>I. topspace(X i)); P(product_topology X I); i \<in> I\<rbrakk>
\<Longrightarrow> P(subtopology (product_topology X I) (PiE I (\<lambda>j. if j = i then topspace(X i) else {z j})))"
(is "\<And>z i. \<lbrakk>_; _; _\<rbrakk> \<Longrightarrow> P (?SX z i)")
and PQ: "\<And>X X'. X homeomorphic_space X' \<Longrightarrow> (P X \<longleftrightarrow> Q X')"
shows "(\<Pi>\<^sub>E i\<in>I. topspace(X i)) = {} \<or> (\<forall>i \<in> I. Q(X i))"
proof -
have "Q(X i)" if "(\<Pi>\<^sub>E i\<in>I. topspace(X i)) \<noteq> {}" "i \<in> I" for i
proof -
from that obtain f where f: "f \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
by force
have "?SX f i homeomorphic_space X i"
apply (simp add: subtopology_PiE )
using product_topology_homeomorphic_component [OF \<open>i \<in> I\<close>, of "\<lambda>j. subtopology (X j) (if j = i then topspace (X i) else {f j})"]
using f by fastforce
then show ?thesis
using minor [OF f major \<open>i \<in> I\<close>] PQ by auto
qed
then show ?thesis by metis
qed
end