Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Function_Topology.thy Sprache: Isabelle

Original von: Isabelle^©

(* Author: Sébastien Gouëzel [email protected] with additions from LCP
 License: BSD
*)

theory Function_Topology
 imports
 Elementary_Topology
 Abstract_Limits
 Connected
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>\Pi\<^sub>E I X\, the set of elements from \'i\ to \'a\ such that the \i\-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\<^marker>\<open>tag important\<close> 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 \ ('a \ real) topology"
 where "powertop_real \ product_topology (\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 ?\) 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 ?\) A = (finite intersection_of ?\ relative_to ?TOP) A" for A
 proof -
 have 1: "\U. (\\. finite \ \ \ \ Collect ?\ \ \\ = U) \ ?TOP \ U = \\"
 if \: "\ \<subseteq> Collect ?\<Omega>" and "finite' \" "A = \<Inter>\" "\ \<noteq> {}" for \
 proof -
 have "\U \ \. \Y. U = Pi\<^sub>E I Y \ (\i. openin (X i) (Y i)) \ finite {i. Y i \ topspace (X i)}"
 using \ by auto
 then obtain Y where Y: "\U. U \ \ \ U = Pi\<^sub>E I (Y U) \ (\i. openin (X i) (Y U i)) \ finite {i. (Y U) i \ topspace (X i)}"
 by metis
 obtain U where "U \ \"
 using \<open>\ \<noteq> {}\<close> by blast
 let ?F = "\U. (\i. {f. f i \ Y U i}) ` {i \ I. Y U i \ topspace (X i)}"
 show ?thesis
 proof (intro conjI exI)
 show "finite (\U\\. ?F U)"
 using Y \<open>finite' \\<close> by auto
 show "?TOP \ \(\U\\. ?F U) = \\"
 proof
 have *: "f \ U"
 if "U \ \" and "\V\\. \i. i \ I \ Y V i \ topspace (X i) \ f i \ Y V i"
 and "\i\I. f i \ topspace (X i)" and "f \ extensional I" for f U
 proof -
 have "Pi\<^sub>E I (Y U) = U"
 using Y \<open>U \<in> \\<close> by blast
 then show "f \ U"
 using that unfolding PiE_def Pi_def by blast
 qed
 show "?TOP \ \(\U\\. ?F U) \ \\"
 by (auto simp: PiE_iff *)
 show "\\ \ ?TOP \ \(\U\\. ?F U)"
 using Y openin_subset \<open>finite' \\<close> by fastforce
 qed
 qed (use Y openin_subset in \<open>blast+\<close>)
 qed
 have 2: "\\'. finite' \' \ \' \ Collect ?\ \ \\' = ?TOP \ \\"
 if \: "\ \<subseteq> Collect ?\<Psi>" and "finite \" for \
 proof (cases "\={}")
 case True
 then show ?thesis
 apply (rule_tac x="{?TOP}" in exI, simp)
 apply (rule_tac x="\i. topspace (X i)" in exI)
 apply force
 done
 next
 case False
 then obtain U where "U \ \"
 by blast
 have "\U \ \. \i Y. U = {f. f i \ Y} \ i \ I \ openin (X i) Y"
 using \ by auto
 then obtain J Y where
 Y: "\U. U \ \ \ U = {f. f (J U) \ Y U} \ J U \ I \ openin (X (J U)) (Y U)"
 by metis
 let ?G = "\U. \\<^sub>E i\I. if i = J U then Y U else topspace (X i)"
 show ?thesis
 proof (intro conjI exI)
 show "finite (?G ` \)" "?G ` \ \ {}"
 using \<open>finite \\<close> \<open>U \<in> \\<close> by blast+
 have *: "\U. U \ \ \ openin (X (J U)) (Y U)"
 using Y by force
 show "?G ` \ \ {Pi\<^sub>E I Y |Y. (\i. openin (X i) (Y i)) \ finite {i. Y i \ topspace (X i)}}"
 apply clarsimp
 apply (rule_tac x=" (\i. if i = J U then Y U else topspace (X i))" in exI)
 apply (auto simp: *)
 done
 next
 show "(\U\\. ?G U) = ?TOP \ \\"
 proof
 have "(\\<^sub>E i\I. if i = J U then Y U else topspace (X i)) \ (\\<^sub>E i\I. topspace (X i))"
 apply (clarsimp simp: PiE_iff Ball_def all_conj_distrib split: if_split_asm)
 using Y \<open>U \<in> \\<close> openin_subset by blast+
 then have "(\U\\. ?G U) \ ?TOP"
 using \<open>U \<in> \\<close>
 by fastforce
 moreover have "(\U\\. ?G U) \ \\"
 using PiE_mem Y by fastforce
 ultimately show "(\U\\. ?G U) \ ?TOP \ \\"
 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) = (\\<^sub>E i\I. topspace(T i))"
proof
 show "topspace (product_topology T I) \ (\\<^sub>E i\I. topspace (T i))"
 unfolding product_topology_def topology_generated_by_topspace
 unfolding topspace_def by auto
 have "(\\<^sub>E i\I. topspace (T i)) \ {(\\<^sub>E i\I. X i) |X. (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)}}"
 using openin_topspace not_finite_existsD by auto
 then show "(\\<^sub>E i\I. topspace (T i)) \ topspace (product_topology T I)"
 unfolding product_topology_def using PiE_def by (auto)
qed

lemma product_topology_basis:
 assumes "\i. openin (T i) (X i)" "finite {i. X i \ topspace (T i)}"
 shows "openin (product_topology T I) (\\<^sub>E i\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 \ U"
 shows "\X. x \ (\\<^sub>E i\I. X i) \ (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)} \ (\\<^sub>E i\I. X i) \ U"
proof -
 have "generate_topology_on {(\\<^sub>E i\I. X i) |X. (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)}} U"
 using assms unfolding product_topology_def by (intro openin_topology_generated_by) auto
 then have "\x. x\U \ \X. x \ (\\<^sub>E i\I. X i) \ (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)} \ (\\<^sub>E i\I. X i) \ U"
 proof induction
 case (Int U V x)
 then obtain XU XV where H:
 "x \ Pi\<^sub>E I XU" "(\i. openin (T i) (XU i))" "finite {i. XU i \ topspace (T i)}" "Pi\<^sub>E I XU \ U"
 "x \ Pi\<^sub>E I XV" "(\i. openin (T i) (XV i))" "finite {i. XV i \ topspace (T i)}" "Pi\<^sub>E I XV \ V"
 by auto meson
 define X where "X = (\i. XU i \ XV i)"
 have "Pi\<^sub>E I X \ Pi\<^sub>E I XU \ Pi\<^sub>E I XV"
 unfolding X_def by (auto simp add: PiE_iff)
 then have "Pi\<^sub>E I X \ U \ V" using H by auto
 moreover have "\i. openin (T i) (X i)"
 unfolding X_def using H by auto
 moreover have "finite {i. X i \ topspace (T i)}"
 apply (rule rev_finite_subset[of "{i. XU i \ topspace (T i)} \ {i. XV i \ topspace (T i)}"])
 unfolding X_def using H by auto
 moreover have "x \ 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 \ K" "x \ k" by auto
 with UN have "\X. x \ Pi\<^sub>E I X \ (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)} \ Pi\<^sub>E I X \ k"
 by simp
 then obtain X where "x \ Pi\<^sub>E I X \ (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)} \ Pi\<^sub>E I X \ k"
 by blast
 then have "x \ Pi\<^sub>E I X \ (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)} \ Pi\<^sub>E I X \ (\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 {(\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) (\\<^sub>E i\I. (S i)) = product_topology (\i. subtopology (X i) (S i)) I"
proof -
 let ?P = "\F. \i U. F = {f. f i \ U} \ i \ I \ openin (X i) U"
 let ?X = "\\<^sub>E i\I. topspace (X i)"
 have "finite intersection_of ?P relative_to ?X \ 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 "\ = 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 \ 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 flip: PiE_Int)
 done
qed

lemma product_topology_base_alt:
 "finite intersection_of (\F. (\i U. F = {f. f i \ U} \ i \ I \ 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 "(\F. ?lhs F \ ?rhs F)"
 unfolding all_relative_to all_intersection_of topspace_product_topology
 proof clarify
 fix \<F>
 assume "finite \" and "\ \ {{f. f i \ U} |i U. i \ I \ openin (X i) U}"
 then show "\U. (\\<^sub>E i\I. topspace (X i)) \ \\ = Pi\<^sub>E I U \
 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: "(\\<^sub>E i\I. topspace (X i)) \ \\ = Pi\<^sub>E I U"
 and fin: "finite {i \ I. U i \ topspace (X i)}"
 and ope: "\i. i \ I \ openin (X i) (U i)"
 by auto
 obtain i V where "F = {f. f i \ V}" "i \ I" "openin (X i) V"
 using insert by auto
 let ?U = "\j. U j \ (if j = i then V else topspace(X j))"
 show ?case
 proof (intro exI conjI)
 show "(\\<^sub>E i\I. topspace (X i)) \ \(insert 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 \ I. ?U i \ topspace (X i)}"
 by (rule rev_finite_subset [OF finite.insertI [OF fin]]) auto
 next
 show "\i\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 "(\F. ?rhs F \ ?lhs F)"
 proof clarify
 fix U :: "'a \ 'b set"
 assume fin: "finite {i \ I. U i \ topspace (X i)}" and ope: "\i\I. openin (X i) (U i)"
 let ?U = "\i\{i \ I. U i \ topspace (X i)}. {x. x i \ U i}"
 show "?lhs (Pi\<^sub>E I U)"
 unfolding relative_to_def topspace_product_topology
 proof (intro exI conjI)
 show "(finite intersection_of (\F. \i U. F = {f. f i \ U} \ i \ I \ openin (X i) U)) ?U"
 using fin ope by (intro finite_intersection_of_Inter finite_intersection_of_inc) auto
 show "(\\<^sub>E i\I. topspace (X i)) \ ?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 \
 (\<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 (\i. (X i) closure_of (S i))"
proof -
 have *: "(\T. f \ T \ openin (product_topology X I) T \ (\y\Pi\<^sub>E I S. y \ 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: "\i. i \ I \ f i \ topspace (X i)" and ext: "f \ extensional I" for f
 proof
 assume L[rule_format]: ?lhs
 show ?rhs
 proof clarify
 fix i T
 assume "i \ I" "f i \ T" "openin (X i) T" "S i \ T = {}"
 then have "openin (product_topology X I) ((\\<^sub>E i\I. topspace (X i)) \ {x. x i \ 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) \ {f. f i \ T}"] \S i \ T = {}\ \f i \ T\ \i \ I\
 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
 assume
 \: "\ \<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 \ U" "U \ \"
 then have "(finite intersection_of (\F. \i U. F = {x. x i \ U} \ i \ I \ 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> \\<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) \ \ \ \ U" "f \ topspace (product_topology X I) \ \ \"
 apply (clarsimp simp add: relative_to_def intersection_of_def)
 apply (rule that, auto dest!: subsetD)
 done
 then have "f \ PiE I (topspace \ X)" "f \ \\" and subU: "PiE I (topspace \ X) \ \\ \ U"
 by (auto simp: PiE_iff)
 have *: "f i \ topspace (X i) \ \{U. openin (X i) U \ {x. x i \ U} \ \}
 \<and> openin (X i) (topspace (X i) \<inter> \<Inter>{U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>})"
 if "i \ I" for i
 proof -
 have "finite ((\U. {x. x i \ U}) -` \)"
 proof (rule finite_vimageI [OF \<open>finite \<T>\<close>])
 show "inj (\U. {x. x i \ U})"
 by (auto simp: inj_on_def)
 qed
 then have fin: "finite {U. openin (X i) U \ {x. x i \ U} \ \}"
 by (rule rev_finite_subset) auto
 have "openin (X i) (\ (insert (topspace (X i)) {U. openin (X i) U \ {x. x i \ U} \ \}))"
 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 "\i \ I. \x. x \ S i \ \ 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 "\y\Pi\<^sub>E I S. \x\\. y \ x"
 proof
 show "\U \ \. (\i \ I. \ i) \ U"
 proof
 have "restrict \ I \ PiE I (topspace \ X) \ \\"
 using \<T> by (fastforce simp: \<Phi>_def PiE_def dest: \<theta>)
 then show "restrict \ I \ U"
 using subU by blast
 qed (rule \<open>U \<in> \\<close>)
 next
 show "(\i \ I. \ i) \ 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) \ PiE I S = {} \ (\i \ 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 \ extensional I \ closedin (product_topology X I) {f} \ (\i \ 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 (\S. S \ {{},{\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 \ S \ {{},{\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 \ I"
 shows "continuous_map (product_topology T I) (T i) (\x. x i)"
proof -
 {
 fix U assume "openin (T i) U"
 define X where "X = (\j. if j = i then U else topspace (T j))"
 then have *: "(\x. x i) -` U \ (\\<^sub>E i\I. topspace (T i)) = (\\<^sub>E j\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 **: "(\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)}"
 unfolding X_def using \<open>openin (T i) U\<close> by auto
 have "openin (product_topology T I) ((\x. x i) -` U \ (\\<^sub>E i\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 "\i. i \ I \ continuous_map T1 (T i) (\x. f x i)"
 "\i x. i \ I \ x \ topspace T1 \ 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 \ {Pi\<^sub>E I X |X. (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)}}"
 then obtain X where H: "U = Pi\<^sub>E I X" "\i. openin (T i) (X i)" "finite {i. X i \ topspace (T i)}"
 by blast
 define J where "J = {i \ I. X i \ topspace (T i)}"
 have "finite J" "J \ I" unfolding J_def using H(3) by auto
 have "(\x. f x i)-`(topspace(T i)) \ topspace T1 = topspace T1" if "i \ I" for i
 using that assms(1) by (simp add: continuous_map_preimage_topspace)
 then have *: "(\x. f x i)-`(X i) \ topspace T1 = topspace T1" if "i \ I-J" for i
 using that unfolding J_def by auto
 have "f-`U \ topspace T1 = (\i\I. (\x. f x i)-`(X i) \ topspace T1) \ (topspace T1)"
 by (subst H(1), auto simp add: PiE_iff assms)
 also have "... = (\i\J. (\x. f x i)-`(X i) \ topspace T1) \ (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 \ topspace T1)" by simp
next
 show "f `topspace T1 \ \{Pi\<^sub>E I X |X. (\i. openin (T i) (X i)) \ finite {i. X i \ 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 "\i. i \ I \ continuous_map T1 (T i) (\x. f x i)"
 "\i x. i \ I \ x \ topspace T1 \ f x i = undefined"
proof -
 fix i assume "i \ I"
 have "(\x. f x i) = (\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) (\x. f x i)"
 by simp
next
 fix i x assume "i \ I" "x \ topspace T1"
 have "f x \ topspace (product_topology T I)"
 using assms \<open>x \<in> topspace T1\<close> unfolding continuous_map_def by auto
 then have "f x \ (\\<^sub>E i\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 \ I"
 shows "continuous_map (product_topology T I) (product_topology T J) (\x. restrict x J)"
proof (rule continuous_map_coordinatewise_then_product)
 fix i assume "i \ J"
 then have "(\x. restrict x J i) = (\x. x i)" unfolding restrict_def by auto
 then show "continuous_map (product_topology T I) (T i) (\x. restrict x J i)"
 using \<open>i \<in> J\<close> \<open>J \<subseteq> I\<close> by auto
next
 fix i assume "i \ J"
 then show "restrict x J i = undefined" for x::"'a \ 'b"
 unfolding restrict_def by auto
qed

subsubsection\<^marker>\<open>tag important\<close> \<open>Powers of a single topological space as a topological space, using type classes\<close>

instantiation "fun" :: (type, topological_space) topological_space
begin

definition\<^marker>\<open>tag important\<close> open_fun_def:
 "open U = openin (product_topology (\i. euclidean) UNIV) U"

instance proof
 have "topspace (product_topology (\(i::'a). euclidean::('b topology)) UNIV) = UNIV"
 unfolding topspace_product_topology topspace_euclidean by auto
 then show "open (UNIV::('a \ '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 \ ('b::topological_space) set"
 assumes "\i. open (X i)" "finite {i. X i \ UNIV}"
 shows "open (Pi\<^sub>E UNIV X)"
 by (simp add: assms open_fun_def product_topology_basis)

lemma euclidean_product_topology:
 "product_topology (\i. euclidean::('b::topological_space) topology) UNIV = euclidean"
by (metis open_openin topology_eq open_fun_def)

proposition product_topology_basis':
 fixes x::"'i \ 'a" and U::"'i \ ('b::topological_space) set"
 assumes "finite I" "\i. i \ I \ open (U i)"
 shows "open {f. \i\I. f (x i) \ U i}"
proof -
 define J where "J = x`I"
 define V where "V = (\y. if y \ J then \{U i|i. i\I \ x i = y} else UNIV)"
 define X where "X = (\y. if y \ 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 \ 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. \i\I. f (x i) \ U i}"
 apply (auto simp add: PiE_iff) unfolding X_def V_def J_def
 proof (auto)
 fix f :: "'a \ 'b" and i :: 'i
 assume a1: "i \ I"
 assume a2: "\i. f i \ (if i \ x`I then if i \ x`I then \{U ia |ia. ia \ I \ x ia = i} else UNIV else UNIV)"
 have f3: "x i \ x`I"
 using a1 by blast
 have "U i \ {U ia |ia. ia \ I \ x ia = x i}"
 using a1 by blast
 then show "f (x i) \ 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 (\x. x i::('b::topological_space))"
 using continuous_map_product_coordinates [of _ UNIV "\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 \ 'b \ 'c::topological_space"
 assumes "\i. continuous_on S (\x. f x i)"
 shows "continuous_on S f"
 using continuous_map_coordinatewise_then_product [of UNIV, where T = "\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 (\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 (\x. f x i)"
proof -
 have "continuous_on S ((\q. q i) \ 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 \ real) \ 'b \ real"
 shows "continuous_on (A \ S) f \ (\i. continuous_on (A \ S) (\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_normed_vector set"
 assumes biB: "\i. i \ I \ b i \ B"
 shows "continuous_map euclidean (top_of_set (span B)) (\x. \i\I. x i *\<^sub>R b i)"
proof (rule continuous_map_euclidean_top_of_set)
 show "(\x. \i\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 (\x. \i\ I. x i *\<^sub>R b i)"
 by (intro continuous_intros) auto
qed

subsubsection\<^marker>\<open>tag important\<close> \<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 \ F" "countable F"
 shows "countable {x::(nat \ 'a). (\i. x i \ F) \ finite {i. x i \ a}}"
proof -
 have *: "{x::(nat \ 'a). (\i. x i \ F) \ finite {i. x i \ 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. (\i. x i \ F) \ (\i\N. x i = a)}" for N::nat
 proof (induction N)
 case 0
 have "{x. (\i. x i \ F) \ (\i\(0::nat). x i = a)} = {(\i. a)}"
 using \<open>a \<in> F\<close> by auto
 then show ?case by auto
 next
 case (Suc N)
 define f::"((nat \ 'a) \ 'a) \ (nat \ 'a)"
 where "f = (\(x, b). (\i. if i = N then b else x i))"
 have "{x. (\i. x i \ F) \ (\i\Suc N. x i = a)} \ f`({x. (\i. x i \ F) \ (\i\N. x i = a)} \ F)"
 proof (auto)
 fix x assume H: "\i::nat. x i \ F" "\i\Suc N. x i = a"
 define y where "y = (\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) \ {x. (\i. x i \ F) \ (\i\N. x i = a)} \ F"
 unfolding y_def using H \<open>a \<in> F\<close> by auto
 ultimately show "x \ f`({x. (\i. x i \ F) \ (\i\N. x i = a)} \ F)"
 by (metis (no_types, lifting) image_eqI)
 qed
 moreover have "countable ({x. (\i. x i \ F) \ (\i\N. x i = a)} \ 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) \ 'b set" and b::'b
 assumes "\i. countable (F i)"
 shows "countable {f::('a \ 'b). (\i. f i \ F i) \ (finite {i. f i \ b})}"
proof -
 define G where "G = (\i. F i) \ {b}"
 have "countable G" unfolding G_def using assms by auto
 have "b \ G" unfolding G_def by auto
 define pi where "pi = (\(x::(nat \ 'b)). (\ i::'a. x ((to_nat::('a \ nat)) i)))"
 have "{f::('a \ 'b). (\i. f i \ F i) \ (finite {i. f i \ 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: "\i. f i \ F i" "finite {i. f i \ b}"
 define I where "I = {i. f i \ b}"
 define g where "g = (\j. if j \ to_nat`I then f (from_nat j) else b)"
 have "{j. g j \ b} \ to_nat`I" unfolding g_def by auto
 then have "finite {j. g j \ b}"
 unfolding I_def using H(2) using finite_surj by blast
 moreover have "g j \ G" for j
 unfolding g_def G_def using H by auto
 ultimately have "g \ {g::(nat \ 'b). (\j. g j \ G) \ (finite {j. g j \ b})}"
 by auto
 moreover have "f = pi g"
 unfolding pi_def g_def I_def using H by fastforce
 ultimately show "f \ pi`{g. (\j. g j \ G) \ finite {j. g j \ 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 \ 'b"
 have "\A::('b \ nat \ 'b set). \x. (\i. x \ A x i \ open (A x i)) \ (\S. open S \ x \ S \ (\i. A x i \ S))"
 apply (rule choice) using first_countable_basis by auto
 then obtain A::"('b \ nat \ 'b set)" where A: "\x i. x \ A x i"
 "\x i. open (A x i)"
 "\x S. open S \ x \ S \ (\i. A x i \ 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 = (\i. (A (x i))`UNIV \ {UNIV})"
 have "countable (B i)" for i unfolding B_def by auto
 have open_B: "\X i. X \ B i \ open X"
 by (auto simp: B_def A)
 define K where "K = {Pi\<^sub>E UNIV X | X. (\i. X i \ B i) \ finite {i. X i \ UNIV}}"
 have "Pi\<^sub>E UNIV (\i. UNIV) \ K"
 unfolding K_def B_def by auto
 then have "K \ {}" by auto
 have "countable {X. (\i. X i \ B i) \ finite {i. X i \ UNIV}}"
 apply (rule countable_product_event_const) using \<open>\<And>i. countable (B i)\<close> by auto
 moreover have "K = (\X. Pi\<^sub>E UNIV X)`{X. (\i. X i \ B i) \ finite {i. X i \ UNIV}}"
 unfolding K_def by auto
 ultimately have "countable K" by auto
 have "x \ k" if "k \ K" for k
 using that unfolding K_def B_def apply auto using A(1) by auto
 have "open k" if "k \ K" for k
 using that unfolding K_def by (blast intro: open_B open_PiE elim: )
 have Inc: "\k\K. k \ U" if "open U \ x \ U" for U
 proof -
 have "openin (product_topology (\i. euclidean) UNIV) U" "x \ 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 "\X. x \ (\\<^sub>E i\UNIV. X i) \ (\i. open (X i)) \ finite {i. X i \ UNIV} \ (\\<^sub>E i\UNIV. X i) \ U"
 by simp
 then obtain X where H: "x \ (\\<^sub>E i\UNIV. X i)"
 "\i. open (X i)"
 "finite {i. X i \ UNIV}"
 "(\\<^sub>E i\UNIV. X i) \ U"
 by auto
 define I where "I = {i. X i \ UNIV}"
 define Y where "Y = (\i. if i \ I then (SOME y. y \ B i \ y \ X i) else UNIV)"
 have *: "\y. y \ B i \ y \ 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 \ B i \ Y i \ X i" for i
 apply (cases "i \ 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 \ UNIV} \ I"
 unfolding Y_def by auto
 then have ***: "finite {i. Y i \ UNIV}"
 unfolding I_def using H(3) rev_finite_subset by blast
 have "(\i. Y i \ B i) \ finite {i. Y i \ UNIV}"
 using ** *** by auto
 then have "Pi\<^sub>E UNIV Y \ K"
 unfolding K_def by auto

 have "Y i \ X i" for i
 apply (cases "i \ I") using ** apply simp unfolding Y_def I_def by auto
 then have "Pi\<^sub>E UNIV Y \ Pi\<^sub>E UNIV X" by auto
 then have "Pi\<^sub>E UNIV Y \ U" using H(4) by auto
 then show ?thesis using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> by auto
 qed

 show "\L. (\(i::nat). x \ L i \ open (L i)) \ (\U. open U \ x \ U \ (\i. L i \ 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 "\K::(('a::countable \ '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 \ topological_basis B"
 using ex_countable_basis by auto
 then have "B \ {}" by (meson UNIV_I empty_iff open_UNIV topological_basisE)
 define B2 where "B2 = B \ {UNIV}"
 have "countable B2"
 unfolding B2_def using B by auto
 have "open U" if "U \ 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. (\i::'a. X i \ B2) \ finite {i. X i \ UNIV}}"
 have i: "\k\K. \X. (k = Pi\<^sub>E UNIV X) \ (\i. open (X i)) \ finite {i. X i \ UNIV}"
 unfolding K_def using \<open>\<And>U. U \<in> B2 \<Longrightarrow> open U\<close> by auto

 have "countable {X. (\(i::'a). X i \ B2) \ finite {i. X i \ UNIV}}"
 apply (rule countable_product_event_const) using \<open>countable B2\<close> by auto
 moreover have "K = (\X. Pi\<^sub>E UNIV X)`{X. (\i. X i \ B2) \ finite {i. X i \ 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\'b" assume "open U" "x \ U"
 then have "openin (product_topology (\i. euclidean) UNIV) U"
 unfolding open_fun_def by auto
 with product_topology_open_contains_basis[OF this \<open>x \<in> U\<close>]
 have "\X. x \ (\\<^sub>E i\UNIV. X i) \ (\i. open (X i)) \ finite {i. X i \ UNIV} \ (\\<^sub>E i\UNIV. X i) \ U"
 by simp
 then obtain X where H: "x \ (\\<^sub>E i\UNIV. X i)"
 "\i. open (X i)"
 "finite {i. X i \ UNIV}"
 "(\\<^sub>E i\UNIV. X i) \ U"
 by auto
 then have "x i \ X i" for i by auto
 define I where "I = {i. X i \ UNIV}"
 define Y where "Y = (\i. if i \ I then (SOME y. y \ B2 \ y \ X i \ x i \ y) else UNIV)"
 have *: "\y. y \ B2 \ y \ X i \ x i \ 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 \ B2 \ Y i \ X i \ x i \ Y i" for i
 using someI_ex[OF *]
 apply (cases "i \ I")
 unfolding Y_def using * apply (auto)
 unfolding B2_def I_def by auto
 have "{i. Y i \ UNIV} \ I"
 unfolding Y_def by auto
 then have ***: "finite {i. Y i \ UNIV}"
 unfolding I_def using H(3) rev_finite_subset by blast
 have "(\i. Y i \ B2) \ finite {i. Y i \ UNIV}"
 using ** *** by auto
 then have "Pi\<^sub>E UNIV Y \ K"
 unfolding K_def by auto

 have "Y i \ X i" for i
 apply (cases "i \ I") using ** apply simp unfolding Y_def I_def by auto
 then have "Pi\<^sub>E UNIV Y \ Pi\<^sub>E UNIV X" by auto
 then have "Pi\<^sub>E UNIV Y \ U" using H(4) by auto

 have "x \ Pi\<^sub>E UNIV Y"
 using ** by auto

 show "\V\K. x \ V \ V \ 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 \ 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>The Alexander subbase theorem\<close>

theorem Alexander_subbase:
 assumes X: "topology (arbitrary union_of (finite intersection_of (\x. x \ \) relative_to \\)) = X"
 and fin: "\C. \C \ \; \C = topspace X\ \ \C'. finite C' \ C' \ C \ \C' = topspace X"
 shows "compact_space X"
proof -
 have U\: "\<Union>\ = topspace X"
 by (simp flip: X)
 have False if \: "\<forall>U\<in>\. openin X U" and sub: "topspace X \<subseteq> \<Union>\"
 and neg: "\\. \\ \ \; finite \\ \ \ topspace X \ \\" for \
 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: "\ \ {}"
 unfolding \<A>_def using sub \ neg by force
 have 2: "\\ \ \" if "\\{}" and \: "subset.chain \ \" for \
 unfolding \<A>_def
 proof (intro CollectI conjI ballI allI impI notI)
 show "openin X U" if U: "U \ \\" for U
 using U \<C> unfolding \<A>_def subset_chain_def by force
 have "\ \ \"
 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 \" and "\ \ \\" and "topspace X \ \\" for \
 proof -
 obtain \ where "\ \<in> \<C>" "\<F> \<subseteq> \"
 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 *: "\\. \\W. W\\ \ openin X W; topspace X \ \\; \ \ \;
 \<And>\<F>. \<lbrakk>finite \<F>; \<F> \<subseteq> \<W>; topspace X \<subseteq> \<Union>\<F>\<rbrakk> \<Longrightarrow> False\<rbrakk>
 \<Longrightarrow> \<W> = \<K>"
 and ope: "\U\\. openin X U" and top: "topspace X \ \\"
 and non: "\\. \finite \; \ \ \; topspace X \ \\\ \ False"
 unfolding \<A>_def by simp_all metis+
 then obtain x where "x \ topspace X" "x \ \(\ \ \)"
 proof -
 have "\(\ \ \) \ \\"
 by (metis \<open>\<Union>\ = topspace X\<close> fin inf.bounded_iff non order_refl)
 then have "\a. a \ \(\ \ \) \ a \ \\"
 by blast
 then show ?thesis
 using that by (metis U\)
 qed
 obtain C where C: "openin X C" "C \ \" "x \ C"
 using \<open>x \<in> topspace X\<close> ope top by auto
 then have "C \ topspace X"
 by (metis openin_subset)
 then have "(arbitrary union_of (finite intersection_of (\x. x \ \) relative_to \\)) C"
 using openin_subbase C unfolding X [symmetric] by blast
 moreover have "C \ 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> \) relative_to topspace X) W"
 and "x \ W" "W \ \" "\\ \ topspace X" "C = \\"
 using C by (auto simp: union_of_def U\)
 then have "\\ \ topspace X"
 by (metis \<open>C \<subseteq> topspace X\<close>)
 then have "topspace X \ \"
 using \<open>\<Union>\<V> \<noteq> topspace X\<close> by blast
 then obtain \' where \': "finite \'" "\' \<subseteq> \" "x \<in> \<Inter>\'" "W = topspace X \<inter> \<Inter>\'"
 using W \<open>x \<in> W\<close> unfolding relative_to_def intersection_of_def by auto
 then have "\\' \ \\"
 using \<open>W \<in> \<V>\<close> \<open>\<Union>\<V> \<noteq> topspace X\<close> \<open>\<Union>\<V> \<subseteq> topspace X\<close> by blast
 then have "\\' \ C"
 using U\ \<open>C = \<Union>\<V>\<close> \<open>W = topspace X \<inter> \<Inter>\'\<close> \<open>W \<in> \<V>\<close> by auto
 have "\b \ \'. \C'. finite C' \ C' \ \ \ topspace X \ \(insert b C')"
 proof
 fix b
 assume "b \ \'"
 have "insert b \ = \" if neg: "\ (\C'. finite C' \ C' \ \ \ topspace X \ \(insert b C'))"
 proof (rule *)
 show "openin X W" if "W \ insert b \" for W
 using that
 proof
 have "b \ \"
 using \<open>b \<in> \'\<close> \<open>\' \<subseteq> \\<close> by blast
 then have "\\. finite \ \ \ \ \ \ \\ = b"
 by (rule_tac x="{b}" in exI) auto
 moreover have "\\ \ b = b"
 using \'(2) \<open>b \<in> \'\<close> by auto
 ultimately show "openin X W" if "W = b"
 using that \<open>b \<in> \'\<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 \ \"
 by (simp add: \<open>W \<in> \<K>\<close> ope)
 qed
 next
 show "topspace X \ \ (insert b \)"
 using top by auto
 next
 show False if "finite \" and "\ \ insert b \" "topspace X \ \\" for \
 proof -
 have "insert b (\ \ \) = \"
 using non that by blast
 then show False
 by (metis Int_lower2 finite_insert neg that(1) that(3))
 qed
 qed auto
 then show "\C'. finite C' \ C' \ \ \ topspace X \ \(insert b C')"
 using \<open>b \<in> \'\<close> \<open>x \<notin> \<Union>(\ \<inter> \<K>)\<close> \'
 by (metis IntI InterE Union_iff subsetD insertI1)
 qed
 then obtain F where F: "\b \ \'. finite (F b) \ F b \ \ \ topspace X \ \(insert b (F b))"
 by metis
 let ?\<D> = "insert C (\<Union>(F ` \'))"
 show False
 proof (rule non)
 have "topspace X \ (\b \ \'. \(insert b (F b)))"
 using F by (simp add: INT_greatest)
 also have "\ \ \?\"
 using \<open>\<Inter>\' \<subseteq> C\<close> by force
 finally show "topspace X \ \?\" .
 show "?\ \ \"
 using \<open>C \<in> \<K>\<close> F by auto
 show "finite ?\"
 using \<open>finite \'\<close> F by auto
 qed
 qed
 then show ?thesis
 by (force simp: compact_space_def compactin_def)
qed

corollary Alexander_subbase_alt:
 assumes "U \ \\"
 and fin: "\C. \C \ \; U \ \C\ \ \C'. finite C' \ C' \ C \ U \ \C'"
 and X: "topology
 (arbitrary union_of
 (finite intersection_of (\<lambda>x. x \<in> \) relative_to U)) = X"
shows "compact_space X"
proof -
 have "topspace X = U"
 using X topspace_subbase by fastforce
 have eq: "\ (Collect ((\x. x \ \) relative_to U)) = U"
 unfolding relative_to_def
 using \<open>U \<subseteq> \<Union>\\<close> by blast
 have *: "\\. finite \ \ \ \ \ \ \\ = topspace X"
 if "\ \ Collect ((\x. x \ \) relative_to topspace X)" and UC: "\\ = topspace X" for \
 proof -
 have "\ \ (\U. topspace X \ U) ` \"
 using that by (auto simp: relative_to_def)
 then obtain \' where "\' \<subseteq> \" and \': "\<C> = (\<inter>) (topspace X) ` \'"
 by (auto simp: subset_image_iff)
 moreover have "U \ \\'"
 using \' \<open>topspace X = U\<close> UC by auto
 ultimately obtain \<C>' where "finite \<C>'" "\<C>' \<subseteq> \'" "U \<subseteq> \<Union>\<C>'"
 using fin [of \'] \<open>topspace X = U\<close> \<open>U \<subseteq> \<Union>\\<close> by blast
 then show ?thesis
 unfolding \' ex_finite_subset_image \<open>topspace X = U\<close> by auto
 qed
 show ?thesis
 apply (rule Alexander_subbase [where \ = "Collect ((\<lambda>x. x \<in> \) 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 \
 f ` (topspace X) \<subseteq> extensional I \<and> (\<forall>k \<in> I. continuous_map X (Y k) (\<lambda>x. f x k))"
 (is "?lhs \ _ \ ?rhs")
proof (cases "\x \ topspace X. f x \ extensional I")
 case True
 then have "f ` (topspace X) \ extensional I"
 by force
 moreover have ?rhs if L: ?lhs
 proof -
 have "openin X {x \ topspace X. f x k \ U}" if "k \ I" and "openin (Y k) U" for k U
 proof -
 have "openin (product_topology Y I) ({Y. Y k \ U} \ (\\<^sub>E i\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 \ topspace X. f x \ ({Y. Y k \ U} \ (\\<^sub>E i\I. topspace (Y i)))}"
 using L unfolding continuous_map_def by blast
 moreover have "{x \ topspace X. f x \ ({Y. Y k \ U} \ (\\<^sub>E i\I. topspace (Y i)))} = {x \ topspace X. f x k \ 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: "\x. x \ topspace X \ f x \ (\\<^sub>E i\I. topspace (Y i))"
 using that True by (auto simp: continuous_map_def PiE_iff)
 have 2: "{x \ S. \T\\. f x \ T} = (\T\\. {x \ S. f x \ T})" for S \
 by blast
 have 3: "{x \ S. \U\\. f x \ U} = (\ (insert S ((\U. {x \ S. f x \ U}) ` \)))" for S \
 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 (\T\\. {x \ topspace X. f x \ T})"
 proof (rule openin_Union; clarify)
 fix S T
 assume "T \ \"
 obtain \ where "T = (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\" and "finite \"
 "\ \ {{f. f i \ U} |i U. i \ I \ 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 \ topspace X. f x \ 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 \ (\k. continuous_map X (Y k) (\x. f x k))"
 by (simp add: continuous_map_componentwise)

lemma continuous_map_product_projection [continuous_intros]:
 "k \ I \ continuous_map (product_topology X I) (X k) (\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 \ I"
 shows "open_map (product_topology Y I) (Y i) (\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) (\x\\. (\f. f i) ` x)"
 proof (rule openin_Union, clarify)
 fix S V
 assume "V \ \"
 obtain \<F> where "finite \<F>"
 and V: "V = (\\<^sub>E i\I. topspace (Y i)) \ \\"
 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) ((\f. f i) ` V)"
 proof (subst openin_subopen; clarify)
 fix x f
 assume "f \ V"
 let ?T = "{a \ 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 "\T. openin (Y i) T \ f i \ T \ T \ (\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) (\x. if k = i then x else f k)" if "k \ 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) (\\<^sub>E i\I. topspace (Y i))"
 by (metis openin_topspace topspace_product_topology)
 moreover have "openin (product_topology Y I) (\B\\. (\\<^sub>E i\I. topspace (Y i)) \ B)"
 if "\ \ {}"
 proof -
 show ?thesis
 proof (rule openin_Inter)
 show "\X. X \ (\) (\\<^sub>E i\I. topspace (Y i)) ` \ \ 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) ((\\<^sub>E i\I. topspace (Y i)) \ \\)"
 by (auto simp only: Int_Inter_eq split: if_split)
 qed
 next
 have eqf: "(\j. if j = i then f i else if j \ I then f j else undefined) = f"
 using PiE_arb V \<open>f \<in> V\<close> by force
 show "f i \ ?T"
 using V assms \<open>f \<in> V\<close> by (auto simp: PiE_iff eqf)
 next
 show "?T \ (\f. f i) ` V"
 unfolding V by (auto simp: intro!: rev_image_eqI)
 qed
 qed
 qed
qed

lemma retraction_map_product_projection:
 assumes "i \ I"
 shows "(retraction_map (product_topology X I) (X i) (\x. x i) \
 (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
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.31 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Function_Topology.thy Sprache: Isabelle

Original von: Isabelle©

¤ Dauer der Verarbeitung: 0.31 Sekunden (vorverarbeitet) ¤

Haftungshinweis

Bemerkung:

Bot Zugriff

^© Kompilation durch diese Firma

Original von: Isabelle^©