(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr with additions from LCP License: BSD *) theory Function_Topology imports Elementary_Topology Abstract_Limits Connected begin section ‹Function Topology› text ‹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⇩_{E}I X›, the set of elements from ‹'i› to ‹'a› such that the ‹i›-th coordinate belongs to ‹X i› for all ‹i ∈ I›. 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 ‹thy›) 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] ‹continuous_map T1 T2 f = ((∀ U. openin T2 U ⟶ openin T1 (f-`U ∩ topspace(T1))) ∧ (f`(topspace T1) ⊆ (topspace T2)))›} be the natural continuity definition of a map from the topology ‹T1› to the topology ‹T2›. Then the current ‹continuous_on› (with type classes) can be redefined as @{text [display] ‹continuous_on s f = continuous_map (top_of_set s) (topology euclidean) f›} In fact, I need ‹continuous_map› to express the continuity of the projection on subfactors for the product topology, in Lemma~‹continuous_on_restrict_product_topology›, and I show the above equivalence in Lemma~‹continuous_map_iff_continuous›. 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 🗏‹~~/src/HOL/Library/Finite_Map.thy›. › subsection ‹The product topology› text ‹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 ‹undefined› along all coordinates. So, we use the first formulation, which moreover seems to give rise to more straightforward proofs. › definition✐‹tag important› product_topology::"('i ⇒ ('a topology)) ⇒ ('i set) ⇒ (('i ⇒ 'a) topology)" where "product_topology T I = topology_generated_by {(Π⇩_{E}i∈I. X i) |X. (∀i. openin (T i) (X i)) ∧ finite {i. X i ≠ topspace (T i)}}" abbreviation powertop_real :: "'a set ⇒ ('a ⇒ real) topology" where "powertop_real ≡ product_topology (λi. euclideanreal)" text ‹The total set of the product topology is the product of the total sets along each coordinate.› proposition product_topology: "product_topology X I = topology (arbitrary union_of ((finite intersection_of (λF. ∃i U. F = {f. f i ∈ U} ∧ i ∈ I ∧ openin (X i) U)) relative_to (Π⇩_{E}i∈I. topspace (X i))))" (is "_ = topology (_ union_of ((_ intersection_of ?Ψ) relative_to ?TOP))") proof - let ?Ω = "(λF. ∃Y. F = Pi⇩_{E}I Y ∧ (∀i. openin (X i) (Y i)) ∧ finite {i. Y i ≠ 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 𝒰: "𝒰 ⊆ Collect ?Ω" and "finite' 𝒰" "A = ⋂𝒰" "𝒰 ≠ {}" for 𝒰 proof - have "∀U ∈ 𝒰. ∃Y. U = Pi⇩_{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⇩_{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 ‹𝒰 ≠ {}› 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 ‹finite' 𝒰› 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 by (smt (verit) PiE_iff Y that) show "?TOP ∩ ⋂(⋃U∈𝒰. ?F U) ⊆ ⋂𝒰" by (auto simp: PiE_iff *) show "⋂𝒰 ⊆ ?TOP ∩ ⋂(⋃U∈𝒰. ?F U)" using Y openin_subset ‹finite' 𝒰› by fastforce qed qed (use Y openin_subset in ‹blast+›) qed have 2: "∃𝒰'. finite' 𝒰' ∧ 𝒰' ⊆ Collect ?Ω ∧ ⋂𝒰' = ?TOP ∩ ⋂𝒰" if 𝒰: "𝒰 ⊆ Collect ?Ψ" 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. Π⇩_{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 ‹finite 𝒰› ‹U ∈ 𝒰› by blast+ have *: "⋀U. U ∈ 𝒰 ⟹ openin (X (J U)) (Y U)" using Y by force show "?G ` 𝒰 ⊆ {Pi⇩_{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 "(Π⇩_{E}i∈I. if i = J U then Y U else topspace (X i)) ⊆ (Π⇩_{E}i∈I. topspace (X i))" by (simp add: PiE_mono Y ‹U ∈ 𝒰› openin_subset) then have "(⋂U∈𝒰. ?G U) ⊆ ?TOP" using ‹U ∈ 𝒰› 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) = (Π⇩_{E}i∈I. topspace(T i))" proof show "topspace (product_topology T I) ⊆ (Π⇩_{E}i∈I. topspace (T i))" unfolding product_topology_def topology_generated_by_topspace unfolding topspace_def by auto have "(Π⇩_{E}i∈I. topspace (T i)) ∈ {(Π⇩_{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 "(Π⇩_{E}i∈I. topspace (T i)) ⊆ topspace (product_topology T I)" unfolding product_topology_def using PiE_def by (auto) qed lemma product_topology_trivial_iff: "product_topology X I = trivial_topology ⟷ (∃i ∈ I. X i = trivial_topology)" by (auto simp: PiE_eq_empty_iff simp flip: null_topspace_iff_trivial) lemma topspace_product_topology_alt: "topspace (product_topology X I) = {x ∈ extensional I. ∀i ∈ I. x i ∈ topspace(X i)}" by (fastforce simp: PiE_iff) lemma product_topology_basis: assumes "⋀i. openin (T i) (X i)" "finite {i. X i ≠ topspace (T i)}" shows "openin (product_topology T I) (Π⇩_{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 ∈ (Π⇩_{E}i∈I. X i) ∧ (∀i. openin (T i) (X i)) ∧ finite {i. X i ≠ topspace (T i)} ∧ (Π⇩_{E}i∈I. X i) ⊆ U" proof - define IT where "IT ≡ λX. {i. X i ≠ topspace (T i)}" have "generate_topology_on {(Π⇩_{E}i∈I. X i) |X. (∀i. openin (T i) (X i)) ∧ finite (IT X)} U" using assms unfolding product_topology_def IT_def by (intro openin_topology_generated_by) auto then have "⋀x. x∈U ⟹ ∃X. x ∈ (Π⇩_{E}i∈I. X i) ∧ (∀i. openin (T i) (X i)) ∧ finite (IT X) ∧ (Π⇩_{E}i∈I. X i) ⊆ U" proof induction case (Int U V x) then obtain XU XV where H: "x ∈ Pi⇩_{E}I XU" "⋀i. openin (T i) (XU i)" "finite (IT XU)" "Pi⇩_{E}I XU ⊆ U" "x ∈ Pi⇩_{E}I XV" "⋀i. openin (T i) (XV i)" "finite (IT XV)" "Pi⇩_{E}I XV ⊆ V" by (meson Int_iff) define X where "X = (λi. XU i ∩ XV i)" have "Pi⇩_{E}I X ⊆ Pi⇩_{E}I XU ∩ Pi⇩_{E}I XV" by (auto simp add: PiE_iff X_def) then have "Pi⇩_{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 (IT X)" apply (rule rev_finite_subset[of "IT XU ∪ IT XV"]) using H by (auto simp: X_def IT_def) moreover have "x ∈ Pi⇩_{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 ‹k ∈ K› UN show ?case by (meson Sup_upper2) qed auto then show ?thesis using ‹x ∈ U› IT_def by blast 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 (λF. (∃i U. F = {f. f i ∈ U} ∧ i ∈ I ∧ openin (X i) U))) relative_to topspace (product_topology X I))" by (simp add: istopology_subbase product_topology) lemma subtopology_product_topology: "subtopology (product_topology X I) (Π⇩_{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 = "Π⇩_{E}i∈I. topspace (X i)" have "finite intersection_of ?P relative_to ?X ∩ Pi⇩_{E}I S = finite intersection_of (?P relative_to ?X ∩ Pi⇩_{E}I S) relative_to ?X ∩ Pi⇩_{E}I S" by (rule finite_intersection_of_relative_to) also have "… = finite intersection_of ((λF. ∃i U. F = {f. f i ∈ U} ∧ i ∈ I ∧ (openin (X i) relative_to S i) U) relative_to ?X ∩ Pi⇩_{E}I S) relative_to ?X ∩ Pi⇩_{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⇩_{E}I S = finite intersection_of (λF. ∃i U. F = {f. f i ∈ U} ∧ i ∈ I ∧ (openin (X i) relative_to S i) U) relative_to ?X ∩ Pi⇩_{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 (Π⇩_{E}i∈I. topspace (X i)) = (λF. (∃U. F = Pi⇩_{E}I U ∧ finite {i ∈ I. U i ≠ topspace(X i)} ∧ (∀i ∈ 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 ℱ assume "finite ℱ" and "ℱ ⊆ {{f. f i ∈ U} |i U. i ∈ I ∧ openin (X i) U}" then show "∃U. (Π⇩_{E}i∈I. topspace (X i)) ∩ ⋂ℱ = Pi⇩_{E}I U ∧ finite {i ∈ I. U i ≠ topspace (X i)} ∧ (∀i∈I. openin (X i) (U i))" proof (induction) case (insert F ℱ) then obtain U where eq: "(Π⇩_{E}i∈I. topspace (X i)) ∩ ⋂ℱ = Pi⇩_{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 "(Π⇩_{E}i∈I. topspace (X i)) ∩ ⋂(insert F ℱ) = Pi⇩_{E}I ?U" using eq PiE_mem ‹i ∈ I› by (auto simp: ‹F = {f. f i ∈ V}›) 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: ‹openin (X i) V› 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⇩_{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 "(Π⇩_{E}i∈I. topspace (X i)) ∩ ?U = Pi⇩_{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 ⟷ (∀x ∈ S. ∃U. finite {i ∈ I. U i ≠ topspace(X i)} ∧ (∀i ∈ I. openin (X i) (U i)) ∧ x ∈ Pi⇩_{E}I U ∧ Pi⇩_{E}I U ⊆ S)" unfolding openin_product_topology arbitrary_union_of_alt product_topology_base_alt topspace_product_topology by (smt (verit, best)) 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⇩_{E}I S. y ∈ T)) ⟷ (∀i ∈ I. ∀T. f i ∈ T ∧ openin (X i) T ⟶ S i ∩ T ≠ {})" (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) ((Π⇩_{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 𝒰: "𝒰 ⊆ Collect (finite intersection_of (λF. ∃i U. F = {x. x i ∈ U} ∧ i ∈ I ∧ openin (X i) U) relative_to (Π⇩_{E}i∈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 (Π⇩_{E}i∈I. topspace (X i))) U" by blast with ‹f ∈ U› ‹U ∈ 𝒰› obtain 𝒯 where "finite 𝒯" and 𝒯: "⋀C. C ∈ 𝒯 ⟹ ∃i ∈ I. ∃V. openin (X i) V ∧ C = {x. x i ∈ 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} ∈ 𝒯} ∧ openin (X i) (topspace (X i) ∩ ⋂{U. openin (X i) U ∧ {x. x i ∈ U} ∈ 𝒯})" if "i ∈ I" for i proof - have "finite ((λU. {x. x i ∈ U}) -` 𝒯)" proof (rule finite_vimageI [OF ‹finite 𝒯›]) 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 ‹f ∈ ⋂ 𝒯› by (fastforce simp: that top) qed define Φ where "Φ ≡ λi. topspace (X i) ∩ ⋂{U. openin (X i) U ∧ {f. f i ∈ U} ∈ 𝒯}" have "∀i ∈ I. ∃x. x ∈ S i ∩ Φ i" using R [OF _ *] unfolding Φ_def by blast then obtain θ where θ [rule_format]: "∀i ∈ I. θ i ∈ S i ∩ Φ i" by metis show "∃y∈Pi⇩_{E}I S. ∃x∈𝒰. y ∈ x" proof show "∃U ∈ 𝒰. (λi ∈ I. θ i) ∈ U" proof have "restrict θ I ∈ PiE I (topspace ∘ X) ∩ ⋂𝒯" using 𝒯 by (fastforce simp: Φ_def PiE_def dest: θ) then show "restrict θ I ∈ U" using subU by blast qed (rule ‹U ∈ 𝒰›) next show "(λi ∈ I. θ i) ∈ Pi⇩_{E}I S" using θ 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))" by (smt (verit, best) PiE_eq closedin_empty closure_of_eq closure_of_product_topology) 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 ‹The basic property of the product topology is the continuity of projections:› 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 ∩ (Π⇩_{E}i∈I. topspace (T i)) = (Π⇩_{E}j∈I. X j)" unfolding X_def using assms openin_subset[OF ‹openin (T i) U›] 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 ‹openin (T i) U› by auto have "openin (product_topology T I) ((λx. x i) -` U ∩ (Π⇩_{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⇩_{E}I X |X. (∀i. openin (T i) (X i)) ∧ finite {i. X i ≠ topspace (T i)}}" then obtain X where H: "U = Pi⇩_{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 * ‹J ⊆ I› by auto also have "openin T1 (...)" using H(2) ‹J ⊆ I› ‹finite J› assms(1) by blast ultimately show "openin T1 (f-`U ∩ topspace T1)" by simp next have "f ∈ topspace T1 → topspace (product_topology T I)" using assms continuous_map_funspace by (force simp: Pi_iff) then show "f `topspace T1 ⊆ ⋃{Pi⇩_{E}I X |X. (∀i. openin (T i) (X i)) ∧ finite {i. X i ≠ topspace (T i)}}" by (fastforce simp add: product_topology_def Pi_iff) 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) (...)" by (metis ‹i ∈ I› assms continuous_map_compose continuous_map_product_coordinates) 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 ‹x ∈ topspace T1› unfolding continuous_map_def by auto then have "f x ∈ (Π⇩_{E}i∈I. topspace (T i))" using topspace_product_topology by metis then show "f x i = undefined" using ‹i ∉ I› 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 ‹i ∈ J› ‹J ⊆ I› 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✐‹tag important› ‹Powers of a single topological space as a topological space, using type classes› instantiation "fun" :: (type, topological_space) topological_space begin definition✐‹tag important› 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⇩_{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 V where "V ≡ (λy. if y ∈ x`I then ⋂{U i|i. i∈I ∧ x i = y} else UNIV)" define X where "X ≡ (λy. if y ∈ x`I then V y else UNIV)" have *: "open (X i)" for i unfolding X_def V_def using assms by auto then have "open (Pi⇩_{E}UNIV X)" by (simp add: X_def assms(1) open_PiE) moreover have "Pi⇩_{E}UNIV X = {f. ∀i∈I. f (x i) ∈ U i}" by (fastforce simp add: PiE_iff X_def V_def split: if_split_asm) ultimately show ?thesis by simp qed text ‹The results proved in the general situation of products of possibly different spaces have their counterparts in this simpler setting.› 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" by (metis UNIV_I assms continuous_map_iff_continuous euclidean_product_topology continuous_map_coordinatewise_then_product) lemma continuous_on_product_then_coordinatewise: assumes "continuous_on S f" shows "continuous_on S (λx. f x i)" by (metis UNIV_I assms continuous_map_iff_continuous continuous_map_product_then_coordinatewise(1) euclidean_product_topology) 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 *⇩_{R}b i)" proof (rule continuous_map_euclidean_top_of_set) show "(λx. ∑i∈I. x i *⇩_{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 *⇩_{R}b i)" by (intro continuous_intros) auto qed subsubsection✐‹tag important› ‹Topological countability for product spaces› text ‹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.› 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}} ⊆ (⋃N. {x. (∀i. x i ∈ F) ∧ (∀i≥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 ‹a ∈ F› by auto then show ?case by auto next case (Suc N) define f::"((nat ⇒ 'a) × 'a) ⇒ (nat ⇒ 'a)" where "f = (λ(x, b). x(N:=b))" 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" have "f (x(N:=a), x N) = x" unfolding f_def by auto moreover have "(x(N:=a), x N) ∈ {x. (∀i. x i ∈ F) ∧ (∀i≥N. x i = a)} × F" using H ‹a ∈ F› 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})} ⊆ pi`{g::(nat ⇒ 'b). (∀j. g j ∈ G) ∧ (finite {j. g j ≠ 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 ‹b ∈ G› ‹countable G›] 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 ‹‹B i› is a countable basis of neighborhoods of ‹x⇩_{i}›.› define B where "B = (λi. (A (x i))`UNIV ∪ {UNIV})" have countB: "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⇩_{E}UNIV X | X. (∀i. X i ∈ B i) ∧ finite {i. X i ≠ UNIV}}" have "Pi⇩_{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}}" by (simp add: countB countable_product_event_const) moreover have "K = (λX. Pi⇩_{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 I: "x ∈ k" if "k ∈ K" for k using that unfolding K_def B_def apply auto using A(1) by auto have II: "open k" if "k ∈ K" for k using that unfolding K_def by (blast intro: open_B open_PiE) 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 U ∧ x ∈ U› unfolding open_fun_def by auto with product_topology_open_contains_basis[OF this] have "∃X. x ∈ (Π⇩_{E}i∈UNIV. X i) ∧ (∀i. open (X i)) ∧ finite {i. X i ≠ UNIV} ∧ (Π⇩_{E}i∈UNIV. X i) ⊆ U" by simp then obtain X where H: "x ∈ (Π⇩_{E}i∈UNIV. X i)" "⋀i. open (X i)" "finite {i. X i ≠ UNIV}" "(Π⇩_{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 proof (cases "i ∈ I") case True then show ?thesis by (metis (mono_tags, lifting) "*" Nitpick.Eps_psimp Y_def) next case False then show ?thesis by (simp add: B_def I_def Y_def) qed have "{i. Y i ≠ UNIV} ⊆ I" unfolding Y_def by auto with ** have "(∀i. Y i ∈ B i) ∧ finite {i. Y i ≠ UNIV}" using H(3) I_def finite_subset by blast then have "Pi⇩_{E}UNIV Y ∈ K" unfolding K_def by auto have "Y i ⊆ X i" for i using "**" by auto then have "Pi⇩_{E}UNIV Y ⊆ U" by (metis H(4) PiE_mono subset_trans) then show ?thesis using ‹Pi⇩_{E}UNIV Y ∈ K› by auto qed show "∃L. (∀(i::nat). x ∈ L i ∧ open (L i)) ∧ (∀U. open U ∧ x ∈ U ⟶ (∃i. L i ⊆ U))" using ‹countable K› I II Inc by (simp add: first_countableI) qed proposition product_topology_countable_basis: shows "∃K::(('a::countable ⇒ 'b::second_countable_topology) set set). topological_basis K ∧ countable K ∧ (∀k∈K. ∃X. (k = Pi⇩_{E}UNIV X) ∧ (∀i. open (X i)) ∧ finite {i. X i ≠ 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⇩_{E}UNIV X | X. (∀i::'a. X i ∈ B2) ∧ finite {i. X i ≠ UNIV}}" have i: "∀k∈K. ∃X. (k = Pi⇩_{E}UNIV X) ∧ (∀i. open (X i)) ∧ finite {i. X i ≠ UNIV}" unfolding K_def using ‹⋀U. U ∈ B2 ⟹ open U› by auto have "countable {X. (∀(i::'a). X i ∈ B2) ∧ finite {i. X i ≠ UNIV}}" using ‹countable B2› by (intro countable_product_event_const) auto moreover have "K = (λX. Pi⇩_{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 ‹x ∈ U›] obtain X where H: "x ∈ (Π⇩_{E}i∈UNIV. X i)" "⋀i. open (X i)" "finite {i. X i ≠ UNIV}" "(Π⇩_{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 (X i)› ‹x i ∈ X i› by (meson UnCI topological_basisE) have **: "Y i ∈ B2 ∧ Y i ⊆ X i ∧ x i ∈ Y i" for i using someI_ex[OF *] by (simp add: B2_def I_def Y_def) have "{i. Y i ≠ UNIV} ⊆ I" unfolding Y_def by auto then have "(∀i. Y i ∈ B2) ∧ finite {i. Y i ≠ UNIV}" using "**" H(3) I_def finite_subset by blast then have "Pi⇩_{E}UNIV Y ∈ K" unfolding K_def by auto then show "∃V∈K. x ∈ V ∧ V ⊆ U" by (meson "**" H(4) PiE_I PiE_mono UNIV_I order.trans) next fix U assume "U ∈ K" show "open U" using ‹U ∈ K› unfolding open_fun_def K_def by clarify (metis ‹U ∈ K› 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 proof show "∃B::('a ⇒ 'b) set set. countable B ∧ open = generate_topology B" using product_topology_countable_basis topological_basis_imp_subbasis by auto qed subsection‹The Alexander subbase theorem› 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ℬ: "⋃ℬ = topspace X" by (simp flip: X) have False if 𝒰: "∀U∈𝒰. openin X U" and sub: "topspace X ⊆ ⋃𝒰" and neg: "⋀ℱ. ⟦ℱ ⊆ 𝒰; finite ℱ⟧ ⟹ ¬ topspace X ⊆ ⋃ℱ" for 𝒰 proof - define 𝒜 where "𝒜 ≡ {𝒞. (∀U ∈ 𝒞. openin X U) ∧ topspace X ⊆ ⋃𝒞 ∧ (∀ℱ. finite ℱ ⟶ ℱ ⊆ 𝒞 ⟶ ~(topspace X ⊆ ⋃ℱ))}" have 1: "𝒜 ≠ {}" unfolding 𝒜_def using sub 𝒰 neg by force have 2: "⋃𝒞 ∈ 𝒜" if "𝒞≠{}" and 𝒞: "subset.chain 𝒜 𝒞" for 𝒞 unfolding 𝒜_def proof (intro CollectI conjI ballI allI impI notI) show "openin X U" if U: "U ∈ ⋃𝒞" for U using U 𝒞 unfolding 𝒜_def subset_chain_def by force have "𝒞 ⊆ 𝒜" using subset_chain_def 𝒞 by blast with that 𝒜_def show UUC: "topspace X ⊆ ⋃(⋃𝒞)" by blast show "False" if "finite ℱ" and "ℱ ⊆ ⋃𝒞" and "topspace X ⊆ ⋃ℱ" for ℱ proof - obtain ℬ where "ℬ ∈ 𝒞" "ℱ ⊆ ℬ" by (metis Sup_empty 𝒞 ‹ℱ ⊆ ⋃𝒞› ‹finite ℱ› UUC empty_subsetI finite.emptyI finite_subset_Union_chain neg) then show False using 𝒜_def ‹𝒞 ⊆ 𝒜› ‹finite ℱ› ‹topspace X ⊆ ⋃ℱ› by blast qed qed obtain 𝒦 where "𝒦 ∈ 𝒜" and "⋀X. ⟦X∈𝒜; 𝒦 ⊆ X⟧ ⟹ X = 𝒦" using subset_Zorn_nonempty [OF 1 2] by metis then have *: "⋀𝒲. ⟦⋀W. W∈𝒲 ⟹ openin X W; topspace X ⊆ ⋃𝒲; 𝒦 ⊆ 𝒲; ⋀ℱ. ⟦finite ℱ; ℱ ⊆ 𝒲; topspace X ⊆ ⋃ℱ⟧ ⟹ False⟧ ⟹ 𝒲 = 𝒦" and ope: "∀U∈𝒦. openin X U" and top: "topspace X ⊆ ⋃𝒦" and non: "⋀ℱ. ⟦finite ℱ; ℱ ⊆ 𝒦; topspace X ⊆ ⋃ℱ⟧ ⟹ False" unfolding 𝒜_def by simp_all metis+ then obtain x where "x ∈ topspace X" "x ∉ ⋃(ℬ ∩ 𝒦)" proof - have "⋃(ℬ ∩ 𝒦) ≠ ⋃ℬ" by (metis ‹⋃ℬ = topspace X› 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 ‹x ∈ topspace X› 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 ‹𝒦 ∈ 𝒜› ‹C ∈ 𝒦› unfolding 𝒜_def by blast ultimately obtain 𝒱 W where W: "(finite intersection_of (λx. x ∈ ℬ) 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 ‹C ⊆ topspace X›) then have "topspace X ∉ 𝒱" using ‹⋃𝒱 ≠ topspace X› by blast then obtain ℬ' where ℬ': "finite ℬ'" "ℬ' ⊆ ℬ" "x ∈ ⋂ℬ'" "W = topspace X ∩ ⋂ℬ'" using W ‹x ∈ W› unfolding relative_to_def intersection_of_def by auto then have "⋂ℬ' ⊆ ⋃ℬ" using ‹W ∈ 𝒱› ‹⋃𝒱 ≠ topspace X› ‹⋃𝒱 ⊆ topspace X› by blast then have "⋂ℬ' ⊆ C" using Uℬ ‹C = ⋃𝒱› ‹W = topspace X ∩ ⋂ℬ'› ‹W ∈ 𝒱› 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 ‹b ∈ ℬ'› ‹ℬ' ⊆ ℬ› by blast then have "∃𝒰. finite 𝒰 ∧ 𝒰 ⊆ ℬ ∧ ⋂𝒰 = b" by (rule_tac x="{b}" in exI) auto moreover have "⋃ℬ ∩ b = b" using ℬ'(2) ‹b ∈ ℬ'› by auto ultimately show "openin X W" if "W = b" using that ‹b ∈ ℬ'› 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: ‹W ∈ 𝒦› 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 ‹b ∈ ℬ'› ‹x ∉ ⋃(ℬ ∩ 𝒦)› ℬ' 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 ?𝒟 = "insert C (⋃(F ` ℬ'))" show False proof (rule non) have "topspace X ⊆ (⋂b ∈ ℬ'. ⋃(insert b (F b)))" using F by (simp add: INT_greatest) also have "… ⊆ ⋃?𝒟" using ‹⋂ℬ' ⊆ C› by force finally show "topspace X ⊆ ⋃?𝒟" . show "?𝒟 ⊆ 𝒦" using ‹C ∈ 𝒦› F by auto show "finite ?𝒟" using ‹finite ℬ'› 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 (λx. x ∈ ℬ) 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 ‹U ⊆ ⋃ℬ› 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 "ℬ' ⊆ ℬ" and ℬ': "𝒞 = (∩) (topspace X) ` ℬ'" by (auto simp: subset_image_iff) moreover have "U ⊆ ⋃ℬ'" using ℬ' ‹topspace X = U› UC by auto ultimately obtain 𝒞' where "finite 𝒞'" "𝒞' ⊆ ℬ'" "U ⊆ ⋃𝒞'" using fin [of ℬ'] ‹topspace X = U› ‹U ⊆ ⋃ℬ› by blast then show ?thesis unfolding ℬ' ex_finite_subset_image ‹topspace X = U› by auto qed show ?thesis apply (rule Alexander_subbase [where ℬ = "Collect ((λx. x ∈ ℬ) 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) ⊆ extensional I ∧ (∀k ∈ I. continuous_map X (Y k) (λ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} ∩ (Π⇩_{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} ∩ (Π⇩_{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} ∩ (Π⇩_{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 ∈ (Π⇩_{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 𝒯 assume 𝒯: "𝒯 ⊆ Collect (finite intersection_of (λF. ∃i U. F = {f. f i ∈ U} ∧ i ∈ I ∧ openin (Y i) U) relative_to (Π⇩_{E}i∈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 = (Π⇩_{E}i∈I. topspace (Y i)) ∩ ⋂𝒰" and "finite 𝒰" "𝒰 ⊆ {{f. f i ∈ U} |i U. i ∈ I ∧ openin (Y i) U}" using subsetD [OF 𝒯 ‹T ∈ 𝒯›] 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 qed (auto simp: continuous_map_def PiE_def) 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 𝒱 assume 𝒱: "𝒱 ⊆ Collect (finite intersection_of (λF. ∃i U. F = {f. f i ∈ U} ∧ i ∈ I ∧ 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 ℱ where "finite ℱ" and V: "V = (Π⇩_{E}i∈I. topspace (Y i)) ∩ ⋂ℱ" and ℱ: "ℱ ⊆ {{f. f i ∈ U} |i U. i ∈ I ∧ openin (Y i) U}" using subsetD [OF 𝒱 ‹V ∈ 𝒱›] 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). (λj∈I. f j)(i:=a) ∈ (Π⇩_{E}i∈I. topspace (Y i)) ∩ ⋂ℱ}" 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 ‹f ∈ V› that) qed then show "continuous_map (Y i) (product_topology Y I) (λx. (λj∈I. f j)(i:=x))" by (auto simp: continuous_map_componentwise assms extensional_def restrict_def) next have "openin (product_topology Y I) (Π⇩_{E}i∈I. topspace (Y i))" by (metis openin_topspace topspace_product_topology) moreover have "openin (product_topology Y I) (⋂B∈ℱ. (Π⇩_{E}i∈I. topspace (Y i)) ∩ B)" if "ℱ ≠ {}" proof - show ?thesis proof (rule openin_Inter) show "⋀X. X ∈ (∩) (Π⇩_{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) using subsetD [OF ℱ] by (metis (mono_tags, lifting) finite_intersection_of_inc mem_Collect_eq topspace_product_topology) qed (use ‹finite ℱ› ‹ℱ ≠ {}› in auto) qed ultimately show "openin (product_topology Y I) ((Π⇩_{E}i∈I. topspace (Y i)) ∩ ⋂ℱ)" by (auto simp only: Int_Inter_eq split: if_split) qed next have eqf: "(λj∈I. f j)(i:=f i) = f" using PiE_arb V ‹f ∈ V› by force show "f i ∈ ?T" using V assms ‹f ∈ V› 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) ⟷ ((product_topology X I) = trivial_topology) ⟶ (X i) = trivial_topology)" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs using retraction_imp_surjective_map by (metis image_empty subtopology_eq_discrete_topology_empty) next assume R: ?rhs show ?lhs proof (cases "(product_topology X I) = trivial_topology") case True then show ?thesis using R by (auto simp: retraction_map_def retraction_maps_def) next case False have *: "∃g. continuous_map (X i) (product_topology X I) g ∧ (∀x∈topspace (X i). g x i = x)" if z: "z ∈ (Π⇩_{E}i∈I. topspace (X i))" for z proof - have cm: "continuous_map (X i) (X j) (λx. if j = i then x else z j)" if "j ∈ I" for j using ‹j ∈ I› z by (case_tac "j = i") auto show ?thesis using ‹i ∈ I› that by (rule_tac x="λx j. if j = i then x else z j" in exI) (auto simp: continuous_map_componentwise PiE_iff extensional_def cm) qed with ‹i ∈ I› False assms show ?thesis by (auto simp: retraction_map_def retraction_maps_def simp flip: null_topspace_iff_trivial) qed qed subsection ‹Open Pi-sets in the product topology› proposition openin_PiE_gen: "openin (product_topology X I) (PiE I S) ⟷ PiE I S = {} ∨ finite {i ∈ I. S i ≠ topspace (X i)} ∧ (∀i ∈ I. openin (X i) (S i))" (is "?lhs ⟷ _ ∨ ?rhs") proof (cases "PiE I S = {}") case False moreover have "?lhs = ?rhs" proof assume L: ?lhs moreover obtain z where z: "z ∈ PiE I S" using False by blast ultimately obtain U where fin: "finite {i ∈ I. U i ≠ topspace (X i)}" and "Pi⇩_{E}I U ≠ {}" and sub: "Pi⇩_{E}I U ⊆ Pi⇩_{E}I S" by (fastforce simp add: openin_product_topology_alt) then have *: "⋀i. i ∈ I ⟹ U i ⊆ S i" by (simp add: subset_PiE) show ?rhs proof (intro conjI ballI) show "finite {i ∈ I. S i ≠ 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 ∈ 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 unfolding openin_product_topology by (intro arbitrary_union_of_inc) (auto simp: product_topology_base_alt) qed ultimately show ?thesis by simp qed simp corollary openin_PiE: "finite I ⟹ openin (product_topology X I) (PiE I S) ⟷ PiE I S = {} ∨ (∀i ∈ I. openin (X i) (S i))" by (simp add: openin_PiE_gen) proposition compact_space_product_topology: "compact_space(product_topology X I) ⟷ (product_topology X I) = trivial_topology ∨ (∀i ∈ I. compact_space(X i))" (is "?lhs = ?rhs") proof (cases "(product_topology X I) = trivial_topology") case False then obtain z where z: "z ∈ (Π⇩_{E}i∈I. topspace(X i))" by (auto simp flip: null_topspace_iff_trivial) show ?thesis proof assume L: ?lhs show ?rhs proof (clarsimp simp add: False compact_space_def) fix i assume "i ∈ I" with L have "continuous_map (product_topology X I) (X i) (λf. f i)" by (simp add: continuous_map_product_projection) moreover have "⋀x. x ∈ topspace (X i) ⟹ x ∈ (λf. f i) ` (Π⇩_{E}i∈I. topspace (X i))" using ‹i ∈ I› z by (rule_tac x="z(i:=x)" in image_eqI) auto then have "(λf. f i) ` (Π⇩_{E}i∈I. topspace (X i)) = topspace (X i)" using ‹i ∈ I› 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 ∈ I" by blast show ?thesis using R proof assume com [rule_format]: "∀i∈I. compact_space (X i)" let ?𝒞 = "{{f. f i ∈ U} |i U. i ∈ I ∧ openin (X i) U}" show "compact_space (product_topology X I)" proof (rule Alexander_subbase_alt) show "topspace (product_topology X I) ⊆ ⋃?𝒞" unfolding topspace_product_topology using ‹i ∈ I› by blast next fix C assume Csub: "C ⊆ ?𝒞" and UC: "topspace (product_topology X I) ⊆ ⋃C" define 𝒟 where "𝒟 ≡ λi. {U. openin (X i) U ∧ {f. f i ∈ U} ∈ C}" show "∃C'. finite C' ∧ C' ⊆ C ∧ topspace (product_topology X I) ⊆ ⋃C'" proof (cases "∃i. i ∈ I ∧ topspace (X i) ⊆ ⋃(𝒟 i)") case True then obtain i where "i ∈ I" and i: "topspace (X i) ⊆ ⋃(𝒟 i)" unfolding 𝒟_def by blast then have *: "⋀𝒰. ⟦Ball 𝒰 (openin (X i)); topspace (X i) ⊆ ⋃𝒰⟧ ⟹ ∃ℱ. finite ℱ ∧ ℱ ⊆ 𝒰 ∧ topspace (X i) ⊆ ⋃ℱ" using com [OF ‹i ∈ I›] by (auto simp: compact_space_def compactin_def) have "topspace (X i) ⊆ ⋃(𝒟 i)" using i by auto with * obtain ℱ where "finite ℱ ∧ ℱ ⊆ (𝒟 i) ∧ topspace (X i) ⊆ ⋃ℱ" unfolding 𝒟_def by fastforce with ‹i ∈ I› show ?thesis unfolding 𝒟_def by (rule_tac x="(λU. {x. x i ∈ U}) ` ℱ" in exI) auto next case False then have "∀i ∈ I. ∃y. y ∈ topspace (X i) ∧ y ∉ ⋃(𝒟 i)" by force then obtain g where g: "⋀i. i ∈ I ⟹ g i ∈ topspace (X i) ∧ g i ∉ ⋃(𝒟 i)" by metis then have "(λi. if i ∈ I then g i else undefined) ∈ topspace (product_topology X I)" by (simp add: PiE_I) moreover have "(λi. if i ∈ I then g i else undefined) ∉ ⋃C" using Csub g unfolding 𝒟_def by force ultimately show ?thesis using UC by blast qed qed (simp add: product_topology) qed simp qed qed qed auto corollary compactin_PiE: "compactin (product_topology X I) (PiE I S) ⟷ PiE I S = {} ∨ (∀i ∈ I. compactin (X i) (S i))" by (fastforce simp add: compactin_subspace subtopology_product_topology compact_space_product_topology subset_PiE product_topology_trivial_iff subtopology_trivial_iff) lemma in_product_topology_closure_of: "z ∈ (product_topology X I) closure_of S ⟹ i ∈ I ⟹ z i ∈ ((X i) closure_of ((λ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="λ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‹Relationship with connected spaces, paths, etc.› proposition connected_space_product_topology: "connected_space(product_topology X I) ⟷ (∃i ∈ I. X i = trivial_topology) ∨ (∀i ∈ I. connected_space(X i))" (is "?lhs ⟷ ?eq ∨ ?rhs") proof (cases ?eq) case False moreover have "?lhs = ?rhs" proof assume ?lhs moreover have "connectedin(X i) (topspace(X i))" if "i ∈ I" and ci: "connectedin(product_topology X I) (topspace(product_topology X I))" for i proof - have cm: "co