# Theory Product_Topology

```section‹The binary product topology›

theory Product_Topology
imports Function_Topology
begin

section ‹Product Topology›

subsection‹Definition›

definition prod_topology :: "'a topology ⇒ 'b topology ⇒ ('a × 'b) topology" where
"prod_topology X Y ≡ topology (arbitrary union_of (λU. U ∈ {S × T |S T. openin X S ∧ openin Y T}))"

lemma open_product_open:
assumes "open A"
shows "∃𝒰. 𝒰 ⊆ {S × T |S T. open S ∧ open T} ∧ ⋃ 𝒰 = A"
proof -
obtain f g where *: "⋀u. u ∈ A ⟹ open (f u) ∧ open (g u) ∧ u ∈ (f u) × (g u) ∧ (f u) × (g u) ⊆ A"
using open_prod_def [of A] assms by metis
let ?𝒰 = "(λu. f u × g u) ` A"
show ?thesis
by (rule_tac x="?𝒰" in exI) (auto simp: dest: *)
qed

lemma open_product_open_eq: "(arbitrary union_of (λU. ∃S T. U = S × T ∧ open S ∧ open T)) = open"
by (force simp: union_of_def arbitrary_def intro: open_product_open open_Times)

lemma openin_prod_topology:
"openin (prod_topology X Y) = arbitrary union_of (λU. U ∈ {S × T |S T. openin X S ∧ openin Y T})"
unfolding prod_topology_def
proof (rule topology_inverse')
show "istopology (arbitrary union_of (λU. U ∈ {S × T |S T. openin X S ∧ openin Y T}))"
apply (rule istopology_base, simp)
by (metis openin_Int Times_Int_Times)
qed

lemma topspace_prod_topology [simp]:
"topspace (prod_topology X Y) = topspace X × topspace Y"
proof -
have "topspace(prod_topology X Y) = ⋃ (Collect (openin (prod_topology X Y)))" (is "_ = ?Z")
unfolding topspace_def ..
also have "… = topspace X × topspace Y"
proof
show "?Z ⊆ topspace X × topspace Y"
apply (auto simp: openin_prod_topology union_of_def arbitrary_def)
using openin_subset by force+
next
have *: "∃A B. topspace X × topspace Y = A × B ∧ openin X A ∧ openin Y B"
by blast
show "topspace X × topspace Y ⊆ ?Z"
apply (rule Union_upper)
using * by (simp add: openin_prod_topology arbitrary_union_of_inc)
qed
finally show ?thesis .
qed

lemma prod_topology_trivial_iff [simp]:
"prod_topology X Y = trivial_topology ⟷ X = trivial_topology ∨ Y = trivial_topology"
by (metis (full_types) Sigma_empty1 null_topspace_iff_trivial subset_empty times_subset_iff topspace_prod_topology)

lemma subtopology_Times:
shows "subtopology (prod_topology X Y) (S × T) = prod_topology (subtopology X S) (subtopology Y T)"
proof -
have "((λU. ∃S T. U = S × T ∧ openin X S ∧ openin Y T) relative_to S × T) =
(λU. ∃S' T'. U = S' × T' ∧ (openin X relative_to S) S' ∧ (openin Y relative_to T) T')"
by (auto simp: relative_to_def Times_Int_Times fun_eq_iff) metis
then show ?thesis
by (simp add: topology_eq openin_prod_topology arbitrary_union_of_relative_to flip: openin_relative_to)
qed

lemma prod_topology_subtopology:
"prod_topology (subtopology X S) Y = subtopology (prod_topology X Y) (S × topspace Y)"
"prod_topology X (subtopology Y T) = subtopology (prod_topology X Y) (topspace X × T)"
by (auto simp: subtopology_Times)

lemma prod_topology_discrete_topology:
"discrete_topology (S × T) = prod_topology (discrete_topology S) (discrete_topology T)"
by (auto simp: discrete_topology_unique openin_prod_topology intro: arbitrary_union_of_inc)

lemma prod_topology_euclidean [simp]: "prod_topology euclidean euclidean = euclidean"

lemma prod_topology_subtopology_eu [simp]:
"prod_topology (subtopology euclidean S) (subtopology euclidean T) = subtopology euclidean (S × T)"
by (simp add: prod_topology_subtopology subtopology_subtopology Times_Int_Times)

lemma openin_prod_topology_alt:
"openin (prod_topology X Y) S ⟷
(∀x y. (x,y) ∈ S ⟶ (∃U V. openin X U ∧ openin Y V ∧ x ∈ U ∧ y ∈ V ∧ U × V ⊆ S))"
apply (auto simp: openin_prod_topology arbitrary_union_of_alt, fastforce)
by (metis mem_Sigma_iff)

lemma open_map_fst: "open_map (prod_topology X Y) X fst"
unfolding open_map_def openin_prod_topology_alt
by (force simp: openin_subopen [of X "fst ` _"] intro: subset_fst_imageI)

lemma open_map_snd: "open_map (prod_topology X Y) Y snd"
unfolding open_map_def openin_prod_topology_alt
by (force simp: openin_subopen [of Y "snd ` _"] intro: subset_snd_imageI)

lemma openin_prod_Times_iff:
"openin (prod_topology X Y) (S × T) ⟷ S = {} ∨ T = {} ∨ openin X S ∧ openin Y T"
proof (cases "S = {} ∨ T = {}")
case False
then show ?thesis
apply (simp add: openin_prod_topology_alt openin_subopen [of X S] openin_subopen [of Y T] times_subset_iff, safe)
apply (meson|force)+
done
qed force

lemma closure_of_Times:
"(prod_topology X Y) closure_of (S × T) = (X closure_of S) × (Y closure_of T)"  (is "?lhs = ?rhs")
proof
show "?lhs ⊆ ?rhs"
by (clarsimp simp: closure_of_def openin_prod_topology_alt) blast
show "?rhs ⊆ ?lhs"
by (clarsimp simp: closure_of_def openin_prod_topology_alt) (meson SigmaI subsetD)
qed

lemma closedin_prod_Times_iff:
"closedin (prod_topology X Y) (S × T) ⟷ S = {} ∨ T = {} ∨ closedin X S ∧ closedin Y T"
by (auto simp: closure_of_Times times_eq_iff simp flip: closure_of_eq)

lemma interior_of_Times: "(prod_topology X Y) interior_of (S × T) = (X interior_of S) × (Y interior_of T)"
proof (rule interior_of_unique)
show "(X interior_of S) × Y interior_of T ⊆ S × T"
show "openin (prod_topology X Y) ((X interior_of S) × Y interior_of T)"
next
show "T' ⊆ (X interior_of S) × Y interior_of T" if "T' ⊆ S × T" "openin (prod_topology X Y) T'" for T'
proof (clarsimp; intro conjI)
fix a :: "'a" and b :: "'b"
assume "(a, b) ∈ T'"
with that obtain U V where UV: "openin X U" "openin Y V" "a ∈ U" "b ∈ V" "U × V ⊆ T'"
by (metis openin_prod_topology_alt)
then show "a ∈ X interior_of S"
using interior_of_maximal_eq that(1) by fastforce
show "b ∈ Y interior_of T"
using UV interior_of_maximal_eq that(1)
by (metis SigmaI mem_Sigma_iff subset_eq)
qed
qed

text ‹Missing the opposite direction. Does it hold? A converse is proved for proper maps, a stronger condition›
lemma closed_map_prod:
assumes "closed_map (prod_topology X Y) (prod_topology X' Y') (λ(x,y). (f x, g y))"
shows "(prod_topology X Y) = trivial_topology ∨ closed_map X X' f ∧ closed_map Y Y' g"
proof (cases "(prod_topology X Y) = trivial_topology")
case False
then have ne: "topspace X ≠ {}" "topspace Y ≠ {}"
by (auto simp flip: null_topspace_iff_trivial)
have "closed_map X X' f"
unfolding closed_map_def
proof (intro strip)
fix C
assume "closedin X C"
show "closedin X' (f ` C)"
proof (cases "C={}")
case False
with assms have "closedin (prod_topology X' Y') ((λ(x,y). (f x, g y)) ` (C × topspace Y))"
by (simp add: ‹closedin X C› closed_map_def closedin_prod_Times_iff)
with False ne show ?thesis
by (simp add: image_paired_Times closedin_Times closedin_prod_Times_iff)
qed auto
qed
moreover
have "closed_map Y Y' g"
unfolding closed_map_def
proof (intro strip)
fix C
assume "closedin Y C"
show "closedin Y' (g ` C)"
proof (cases "C={}")
case False
with assms have "closedin (prod_topology X' Y') ((λ(x,y). (f x, g y)) ` (topspace X × C))"
by (simp add: ‹closedin Y C› closed_map_def closedin_prod_Times_iff)
with False ne show ?thesis
by (simp add: image_paired_Times closedin_Times closedin_prod_Times_iff)
qed auto
qed
ultimately show ?thesis
by (auto simp: False)
qed auto

subsection ‹Continuity›

lemma continuous_map_pairwise:
"continuous_map Z (prod_topology X Y) f ⟷ continuous_map Z X (fst ∘ f) ∧ continuous_map Z Y (snd ∘ f)"
(is "?lhs = ?rhs")
proof -
let ?g = "fst ∘ f" and ?h = "snd ∘ f"
have f: "f x = (?g x, ?h x)" for x
by auto
show ?thesis
proof (cases "?g ∈ topspace Z → topspace X ∧ ?h ∈ topspace Z → topspace Y")
case True
show ?thesis
proof safe
assume "continuous_map Z (prod_topology X Y) f"
then have "openin Z {x ∈ topspace Z. fst (f x) ∈ U}" if "openin X U" for U
unfolding continuous_map_def using True that
apply clarify
apply (drule_tac x="U × topspace Y" in spec)
by (auto simp: openin_prod_Times_iff mem_Times_iff Pi_iff cong: conj_cong)
with True show "continuous_map Z X (fst ∘ f)"
by (auto simp: continuous_map_def)
next
assume "continuous_map Z (prod_topology X Y) f"
then have "openin Z {x ∈ topspace Z. snd (f x) ∈ V}" if "openin Y V" for V
unfolding continuous_map_def using True that
apply clarify
apply (drule_tac x="topspace X × V" in spec)
by (simp add: openin_prod_Times_iff mem_Times_iff Pi_iff cong: conj_cong)
with True show "continuous_map Z Y (snd ∘ f)"
by (auto simp: continuous_map_def)
next
assume Z: "continuous_map Z X (fst ∘ f)" "continuous_map Z Y (snd ∘ f)"
have *: "openin Z {x ∈ topspace Z. f x ∈ W}"
if "⋀w. w ∈ W ⟹ ∃U V. openin X U ∧ openin Y V ∧ w ∈ U × V ∧ U × V ⊆ W" for W
proof (subst openin_subopen, clarify)
fix x :: "'a"
assume "x ∈ topspace Z" and "f x ∈ W"
with that [OF ‹f x ∈ W›]
obtain U V where UV: "openin X U" "openin Y V" "f x ∈ U × V" "U × V ⊆ W"
by auto
with Z  UV show "∃T. openin Z T ∧ x ∈ T ∧ T ⊆ {x ∈ topspace Z. f x ∈ W}"
apply (rule_tac x="{x ∈ topspace Z. ?g x ∈ U} ∩ {x ∈ topspace Z. ?h x ∈ V}" in exI)
apply (auto simp: ‹x ∈ topspace Z› continuous_map_def)
done
qed
show "continuous_map Z (prod_topology X Y) f"
using True by (force simp: continuous_map_def openin_prod_topology_alt mem_Times_iff *)
qed
qed (force simp: continuous_map_def)
qed

lemma continuous_map_paired:
"continuous_map Z (prod_topology X Y) (λx. (f x,g x)) ⟷ continuous_map Z X f ∧ continuous_map Z Y g"

lemma continuous_map_pairedI [continuous_intros]:
"⟦continuous_map Z X f; continuous_map Z Y g⟧ ⟹ continuous_map Z (prod_topology X Y) (λx. (f x,g x))"

lemma continuous_map_fst [continuous_intros]: "continuous_map (prod_topology X Y) X fst"
using continuous_map_pairwise [of "prod_topology X Y" X Y id]

lemma continuous_map_snd [continuous_intros]: "continuous_map (prod_topology X Y) Y snd"
using continuous_map_pairwise [of "prod_topology X Y" X Y id]

lemma continuous_map_fst_of [continuous_intros]:
"continuous_map Z (prod_topology X Y) f ⟹ continuous_map Z X (fst ∘ f)"

lemma continuous_map_snd_of [continuous_intros]:
"continuous_map Z (prod_topology X Y) f ⟹ continuous_map Z Y (snd ∘ f)"

lemma continuous_map_prod_fst:
"i ∈ I ⟹ continuous_map (prod_topology (product_topology (λi. Y) I) X) Y (λx. fst x i)"
using continuous_map_componentwise_UNIV continuous_map_fst by fastforce

lemma continuous_map_prod_snd:
"i ∈ I ⟹ continuous_map (prod_topology X (product_topology (λi. Y) I)) Y (λx. snd x i)"
using continuous_map_componentwise_UNIV continuous_map_snd by fastforce

lemma continuous_map_if_iff [simp]: "continuous_map X Y (λx. if P then f x else g x) ⟷ continuous_map X Y (if P then f else g)"
by simp

lemma continuous_map_if [continuous_intros]: "⟦P ⟹ continuous_map X Y f; ~P ⟹ continuous_map X Y g⟧
⟹ continuous_map X Y (λx. if P then f x else g x)"
by simp

lemma prod_topology_trivial1 [simp]: "prod_topology trivial_topology Y = trivial_topology"
using continuous_map_fst continuous_map_on_empty2 by blast

lemma prod_topology_trivial2 [simp]: "prod_topology X trivial_topology = trivial_topology"
using continuous_map_snd continuous_map_on_empty2 by blast

lemma continuous_map_subtopology_fst [continuous_intros]: "continuous_map (subtopology (prod_topology X Y) Z) X fst"
using continuous_map_from_subtopology continuous_map_fst by force

lemma continuous_map_subtopology_snd [continuous_intros]: "continuous_map (subtopology (prod_topology X Y) Z) Y snd"
using continuous_map_from_subtopology continuous_map_snd by force

lemma quotient_map_fst [simp]:
"quotient_map(prod_topology X Y) X fst ⟷ (Y = trivial_topology ⟶ X = trivial_topology)"
apply (simp add: continuous_open_quotient_map open_map_fst continuous_map_fst)
by (metis null_topspace_iff_trivial)

lemma quotient_map_snd [simp]:
"quotient_map(prod_topology X Y) Y snd ⟷ (X = trivial_topology ⟶ Y = trivial_topology)"
apply (simp add: continuous_open_quotient_map open_map_snd continuous_map_snd)
by (metis null_topspace_iff_trivial)

lemma retraction_map_fst:
"retraction_map (prod_topology X Y) X fst ⟷ (Y = trivial_topology ⟶ X = trivial_topology)"
proof (cases "Y = trivial_topology")
case True
then show ?thesis
using continuous_map_image_subset_topspace
by (auto simp: retraction_map_def retraction_maps_def continuous_map_pairwise)
next
case False
have "∃g. continuous_map X (prod_topology X Y) g ∧ (∀x∈topspace X. fst (g x) = x)"
if y: "y ∈ topspace Y" for y
by (rule_tac x="λx. (x,y)" in exI) (auto simp: y continuous_map_paired)
with False have "retraction_map (prod_topology X Y) X fst"
by (fastforce simp: retraction_map_def retraction_maps_def continuous_map_fst)
with False show ?thesis
by simp
qed

lemma retraction_map_snd:
"retraction_map (prod_topology X Y) Y snd ⟷ (X = trivial_topology ⟶ Y = trivial_topology)"
proof (cases "X = trivial_topology")
case True
then show ?thesis
using continuous_map_image_subset_topspace
by (fastforce simp: retraction_map_def retraction_maps_def continuous_map_fst)
next
case False
have "∃g. continuous_map Y (prod_topology X Y) g ∧ (∀y∈topspace Y. snd (g y) = y)"
if x: "x ∈ topspace X" for x
by (rule_tac x="λy. (x,y)" in exI) (auto simp: x continuous_map_paired)
with False have "retraction_map (prod_topology X Y) Y snd"
by (fastforce simp: retraction_map_def retraction_maps_def continuous_map_snd)
with False show ?thesis
by simp
qed

lemma continuous_map_of_fst:
"continuous_map (prod_topology X Y) Z (f ∘ fst) ⟷ Y = trivial_topology ∨ continuous_map X Z f"
proof (cases "Y = trivial_topology")
case True
then show ?thesis
next
case False
then show ?thesis
qed

lemma continuous_map_of_snd:
"continuous_map (prod_topology X Y) Z (f ∘ snd) ⟷ X = trivial_topology ∨ continuous_map Y Z f"
proof (cases "X = trivial_topology")
case True
then show ?thesis
next
case False
then show ?thesis
qed

lemma continuous_map_prod_top:
"continuous_map (prod_topology X Y) (prod_topology X' Y') (λ(x,y). (f x, g y)) ⟷
(prod_topology X Y) = trivial_topology ∨ continuous_map X X' f ∧ continuous_map Y Y' g"
proof (cases "(prod_topology X Y) = trivial_topology")
case False
then show ?thesis
by (auto simp: continuous_map_paired case_prod_unfold
continuous_map_of_fst [unfolded o_def] continuous_map_of_snd [unfolded o_def])
qed auto

lemma in_prod_topology_closure_of:
assumes  "z ∈ (prod_topology X Y) closure_of S"
shows "fst z ∈ X closure_of (fst ` S)" "snd z ∈ Y closure_of (snd ` S)"
using assms continuous_map_eq_image_closure_subset continuous_map_fst apply fastforce
using assms continuous_map_eq_image_closure_subset continuous_map_snd apply fastforce
done

proposition compact_space_prod_topology:
"compact_space(prod_topology X Y) ⟷ (prod_topology X Y) = trivial_topology ∨ compact_space X ∧ compact_space Y"
proof (cases "(prod_topology X Y) = trivial_topology")
case True
then show ?thesis
by fastforce
next
case False
then have non_mt: "topspace X ≠ {}" "topspace Y ≠ {}"
by auto
have "compact_space X" "compact_space Y" if "compact_space(prod_topology X Y)"
proof -
have "compactin X (fst ` (topspace X × topspace Y))"
by (metis compact_space_def continuous_map_fst image_compactin that topspace_prod_topology)
moreover
have "compactin Y (snd ` (topspace X × topspace Y))"
by (metis compact_space_def continuous_map_snd image_compactin that topspace_prod_topology)
ultimately show "compact_space X" "compact_space Y"
using non_mt by (auto simp: compact_space_def)
qed
moreover
define 𝒳 where "𝒳 ≡ (λV. topspace X × V) ` Collect (openin Y)"
define 𝒴 where "𝒴 ≡ (λU. U × topspace Y) ` Collect (openin X)"
have "compact_space(prod_topology X Y)" if "compact_space X" "compact_space Y"
proof (rule Alexander_subbase_alt)
show toptop: "topspace X × topspace Y ⊆ ⋃(𝒳 ∪ 𝒴)"
unfolding 𝒳_def 𝒴_def by auto
fix 𝒞 :: "('a × 'b) set set"
assume 𝒞: "𝒞 ⊆ 𝒳 ∪ 𝒴" "topspace X × topspace Y ⊆ ⋃𝒞"
then obtain 𝒳' 𝒴' where XY: "𝒳' ⊆ 𝒳" "𝒴' ⊆ 𝒴" and 𝒞eq: "𝒞 = 𝒳' ∪ 𝒴'"
using subset_UnE by metis
then have sub: "topspace X × topspace Y ⊆ ⋃(𝒳' ∪ 𝒴')"
using 𝒞 by simp
obtain 𝒰 𝒱 where 𝒰: "⋀U. U ∈ 𝒰 ⟹ openin X U" "𝒴' = (λU. U × topspace Y) ` 𝒰"
and 𝒱: "⋀V. V ∈ 𝒱 ⟹ openin Y V" "𝒳' = (λV. topspace X × V) ` 𝒱"
using XY by (clarsimp simp add: 𝒳_def 𝒴_def subset_image_iff) (force simp: subset_iff)
have "∃𝒟. finite 𝒟 ∧ 𝒟 ⊆ 𝒳' ∪ 𝒴' ∧ topspace X × topspace Y ⊆ ⋃ 𝒟"
proof -
have "topspace X ⊆ ⋃𝒰 ∨ topspace Y ⊆ ⋃𝒱"
using 𝒰 𝒱 𝒞 𝒞eq by auto
then have *: "∃𝒟. finite 𝒟 ∧
(∀x ∈ 𝒟. x ∈ (λV. topspace X × V) ` 𝒱 ∨ x ∈ (λU. U × topspace Y) ` 𝒰) ∧
(topspace X × topspace Y ⊆ ⋃𝒟)"
proof
assume "topspace X ⊆ ⋃𝒰"
with ‹compact_space X› 𝒰 obtain ℱ where "finite ℱ" "ℱ ⊆ 𝒰" "topspace X ⊆ ⋃ℱ"
by (meson compact_space_alt)
with that show ?thesis
by (rule_tac x="(λD. D × topspace Y) ` ℱ" in exI) auto
next
assume "topspace Y ⊆ ⋃𝒱"
with ‹compact_space Y› 𝒱 obtain ℱ where "finite ℱ" "ℱ ⊆ 𝒱" "topspace Y ⊆ ⋃ℱ"
by (meson compact_space_alt)
with that show ?thesis
by (rule_tac x="(λC. topspace X × C) ` ℱ" in exI) auto
qed
then show ?thesis
using that 𝒰 𝒱 by blast
qed
then show "∃𝒟. finite 𝒟 ∧ 𝒟 ⊆ 𝒞 ∧ topspace X × topspace Y ⊆ ⋃ 𝒟"
using 𝒞 𝒞eq by blast
next
have "(finite intersection_of (λx. x ∈ 𝒳 ∨ x ∈ 𝒴) relative_to topspace X × topspace Y)
= (λU. ∃S T. U = S × T ∧ openin X S ∧ openin Y T)"
(is "?lhs = ?rhs")
proof -
have "?rhs U" if "?lhs U" for U
proof -
have "topspace X × topspace Y ∩ ⋂ T ∈ {A × B |A B. A ∈ Collect (openin X) ∧ B ∈ Collect (openin Y)}"
if "finite T" "T ⊆ 𝒳 ∪ 𝒴" for T
using that
proof induction
case (insert B ℬ)
then show ?case
unfolding 𝒳_def 𝒴_def
apply (simp add: Int_ac subset_eq image_def)
apply (metis (no_types) openin_Int openin_topspace Times_Int_Times)
done
qed auto
then show ?thesis
using that
by (auto simp: subset_eq  elim!: relative_toE intersection_ofE)
qed
moreover
have "?lhs Z" if Z: "?rhs Z" for Z
proof -
obtain U V where "Z = U × V" "openin X U" "openin Y V"
using Z by blast
then have UV: "U × V = (topspace X × topspace Y) ∩ (U × V)"
by (simp add: Sigma_mono inf_absorb2 openin_subset)
moreover
have "?lhs ((topspace X × topspace Y) ∩ (U × V))"
proof (rule relative_to_inc)
show "(finite intersection_of (λx. x ∈ 𝒳 ∨ x ∈ 𝒴)) (U × V)"
apply (simp add: intersection_of_def 𝒳_def 𝒴_def)
apply (rule_tac x="{(U × topspace Y),(topspace X × V)}" in exI)
using ‹openin X U› ‹openin Y V› openin_subset UV apply (fastforce simp:)
done
qed
ultimately show ?thesis
using ‹Z = U × V› by auto
qed
ultimately show ?thesis
by meson
qed
then show "topology (arbitrary union_of (finite intersection_of (λx. x ∈ 𝒳 ∪ 𝒴)
relative_to (topspace X × topspace Y))) =
prod_topology X Y"
qed
ultimately show ?thesis
using False by blast
qed

lemma compactin_Times:
"compactin (prod_topology X Y) (S × T) ⟷ S = {} ∨ T = {} ∨ compactin X S ∧ compactin Y T"
by (auto simp: compactin_subspace subtopology_Times compact_space_prod_topology subtopology_trivial_iff)

subsection‹Homeomorphic maps›

lemma homeomorphic_maps_prod:
"homeomorphic_maps (prod_topology X Y) (prod_topology X' Y') (λ(x,y). (f x, g y)) (λ(x,y). (f' x, g' y)) ⟷
(prod_topology X Y) = trivial_topology ∧ (prod_topology X' Y') = trivial_topology
∨ homeomorphic_maps X X' f f' ∧ homeomorphic_maps Y Y' g g'"  (is "?lhs = ?rhs")
proof
show "?lhs ⟹ ?rhs"
by (fastforce simp: homeomorphic_maps_def continuous_map_prod_top ball_conj_distrib)
next
show "?rhs ⟹ ?lhs"
by (auto simp: homeomorphic_maps_def continuous_map_prod_top)
qed

lemma homeomorphic_maps_swap:
"homeomorphic_maps (prod_topology X Y) (prod_topology Y X) (λ(x,y). (y,x)) (λ(y,x). (x,y))"
by (auto simp: homeomorphic_maps_def case_prod_unfold continuous_map_fst continuous_map_pairedI continuous_map_snd)

lemma homeomorphic_map_swap:
"homeomorphic_map (prod_topology X Y) (prod_topology Y X) (λ(x,y). (y,x))"
using homeomorphic_map_maps homeomorphic_maps_swap by metis

lemma homeomorphic_space_prod_topology_swap:
"(prod_topology X Y) homeomorphic_space (prod_topology Y X)"
using homeomorphic_map_swap homeomorphic_space by blast

lemma embedding_map_graph:
"embedding_map X (prod_topology X Y) (λx. (x, f x)) ⟷ continuous_map X Y f"
(is "?lhs = ?rhs")
proof
assume L: ?lhs
have "snd ∘ (λx. (x, f x)) = f"
by force
moreover have "continuous_map X Y (snd ∘ (λx. (x, f x)))"
using L unfolding embedding_map_def
by (meson continuous_map_in_subtopology continuous_map_snd_of homeomorphic_imp_continuous_map)
ultimately show ?rhs
by simp
next
assume R: ?rhs
then show ?lhs
unfolding homeomorphic_map_maps embedding_map_def homeomorphic_maps_def
by (rule_tac x=fst in exI)
(auto simp: continuous_map_in_subtopology continuous_map_paired continuous_map_from_subtopology
continuous_map_fst)
qed

lemma homeomorphic_space_prod_topology:
"⟦X homeomorphic_space X''; Y homeomorphic_space Y'⟧
⟹ prod_topology X Y homeomorphic_space prod_topology X'' Y'"
using homeomorphic_maps_prod unfolding homeomorphic_space_def by blast

lemma prod_topology_homeomorphic_space_left:
"Y = discrete_topology {b} ⟹ prod_topology X Y homeomorphic_space X"
unfolding homeomorphic_space_def
apply (rule_tac x=fst in exI)
apply (simp add: homeomorphic_map_def inj_on_def discrete_topology_unique flip: homeomorphic_map_maps)
done

lemma prod_topology_homeomorphic_space_right:
"X = discrete_topology {a} ⟹ prod_topology X Y homeomorphic_space Y"
unfolding homeomorphic_space_def
by (meson homeomorphic_space_def homeomorphic_space_prod_topology_swap homeomorphic_space_trans prod_topology_homeomorphic_space_left)

lemma homeomorphic_space_prod_topology_sing1:
"b ∈ topspace Y ⟹ X homeomorphic_space (prod_topology X (subtopology Y {b}))"
by (metis empty_subsetI homeomorphic_space_sym insert_subset prod_topology_homeomorphic_space_left subtopology_eq_discrete_topology_sing topspace_subtopology_subset)

lemma homeomorphic_space_prod_topology_sing2:
"a ∈ topspace X ⟹ Y homeomorphic_space (prod_topology (subtopology X {a}) Y)"
by (metis empty_subsetI homeomorphic_space_sym insert_subset prod_topology_homeomorphic_space_right subtopology_eq_discrete_topology_sing topspace_subtopology_subset)

lemma topological_property_of_prod_component:
assumes major: "P(prod_topology X Y)"
and X: "⋀x. ⟦x ∈ topspace X; P(prod_topology X Y)⟧ ⟹ P(subtopology (prod_topology X Y) ({x} × topspace Y))"
and Y: "⋀y. ⟦y ∈ topspace Y; P(prod_topology X Y)⟧ ⟹ P(subtopology (prod_topology X Y) (topspace X × {y}))"
and PQ:  "⋀X X'. X homeomorphic_space X' ⟹ (P X ⟷ Q X')"
and PR: "⋀X X'. X homeomorphic_space X' ⟹ (P X ⟷ R X')"
shows "(prod_topology X Y) = trivial_topology ∨ Q X ∧ R Y"
proof -
have "Q X ∧ R Y" if "topspace(prod_topology X Y) ≠ {}"
proof -
from that obtain a b where a: "a ∈ topspace X" and b: "b ∈ topspace Y"
by force
show ?thesis
using X [OF a major] and Y [OF b major] homeomorphic_space_prod_topology_sing1 [OF b, of X] homeomorphic_space_prod_topology_sing2 [OF a, of Y]
by (simp add: subtopology_Times) (meson PQ PR homeomorphic_space_prod_topology_sing2 homeomorphic_space_sym)
qed
then show ?thesis by force
qed

lemma limitin_pairwise:
"limitin (prod_topology X Y) f l F ⟷ limitin X (fst ∘ f) (fst l) F ∧ limitin Y (snd ∘ f) (snd l) F"
(is "?lhs = ?rhs")
proof
assume ?lhs
then obtain a b where ev: "⋀U. ⟦(a,b) ∈ U; openin (prod_topology X Y) U⟧ ⟹ ∀⇩F x in F. f x ∈ U"
and a: "a ∈ topspace X" and b: "b ∈ topspace Y" and l: "l = (a,b)"
by (auto simp: limitin_def)
moreover have "∀⇩F x in F. fst (f x) ∈ U" if "openin X U" "a ∈ U" for U
proof -
have "∀⇩F c in F. f c ∈ U × topspace Y"
using b that ev [of "U × topspace Y"] by (auto simp: openin_prod_topology_alt)
then show ?thesis
by (rule eventually_mono) (metis (mono_tags, lifting) SigmaE2 prod.collapse)
qed
moreover have "∀⇩F x in F. snd (f x) ∈ U" if "openin Y U" "b ∈ U" for U
proof -
have "∀⇩F c in F. f c ∈ topspace X × U"
using a that ev [of "topspace X × U"] by (auto simp: openin_prod_topology_alt)
then show ?thesis
by (rule eventually_mono) (metis (mono_tags, lifting) SigmaE2 prod.collapse)
qed
ultimately show ?rhs
next
have "limitin (prod_topology X Y) f (a,b) F"
if "limitin X (fst ∘ f) a F" "limitin Y (snd ∘ f) b F" for a b
using that
proof (clarsimp simp: limitin_def)
fix Z :: "('a × 'b) set"
assume a: "a ∈ topspace X" "∀U. openin X U ∧ a ∈ U ⟶ (∀⇩F x in F. fst (f x) ∈ U)"
and b: "b ∈ topspace Y" "∀U. openin Y U ∧ b ∈ U ⟶ (∀⇩F x in F. snd (f x) ∈ U)"
and Z: "openin (prod_topology X Y) Z" "(a, b) ∈ Z"
then obtain U V where "openin X U" "openin Y V" "a ∈ U" "b ∈ V" "U × V ⊆ Z"
using Z by (force simp: openin_prod_topology_alt)
then have "∀⇩F x in F. fst (f x) ∈ U" "∀⇩F x in F. snd (f x) ∈ V"
then show "∀⇩F x in F. f x ∈ Z"
by (rule eventually_elim2) (use ‹U × V ⊆ Z› subsetD in auto)
qed
then show "?rhs ⟹ ?lhs"
by (metis prod.collapse)
qed

proposition connected_space_prod_topology:
"connected_space(prod_topology X Y) ⟷
(prod_topology X Y) = trivial_topology ∨ connected_space X ∧ connected_space Y" (is "?lhs=?rhs")
proof (cases "(prod_topology X Y) = trivial_topology")
case True
then show ?thesis
by auto
next
case False
then have nonempty: "topspace X ≠ {}" "topspace Y ≠ {}"
by force+
show ?thesis
proof
assume ?lhs
then show ?rhs
by (metis connected_space_quotient_map_image nonempty quotient_map_fst quotient_map_snd
subtopology_eq_discrete_topology_empty)
next
assume ?rhs
then have conX: "connected_space X" and conY: "connected_space Y"
using False by blast+
have False
if "openin (prod_topology X Y) U" and "openin (prod_topology X Y) V"
and UV: "topspace X × topspace Y ⊆ U ∪ V" "U ∩ V = {}"
and "U ≠ {}" and "V ≠ {}"
for U V
proof -
have Usub: "U ⊆ topspace X × topspace Y" and Vsub: "V ⊆ topspace X × topspace Y"
using that by (metis openin_subset topspace_prod_topology)+
obtain a b where ab: "(a,b) ∈ U" and a: "a ∈ topspace X" and b: "b ∈ topspace Y"
using ‹U ≠ {}› Usub by auto
have "¬ topspace X × topspace Y ⊆ U"
using Usub Vsub ‹U ∩ V = {}› ‹V ≠ {}› by auto
then obtain x y where x: "x ∈ topspace X" and y: "y ∈ topspace Y" and "(x,y) ∉ U"
by blast
have oX: "openin X {x ∈ topspace X. (x,y) ∈ U}" "openin X {x ∈ topspace X. (x,y) ∈ V}"
and oY: "openin Y {y ∈ topspace Y. (a,y) ∈ U}" "openin Y {y ∈ topspace Y. (a,y) ∈ V}"
by (force intro: openin_continuous_map_preimage [where Y = "prod_topology X Y"]
simp: that continuous_map_pairwise o_def x y a)+
have 1: "topspace Y ⊆ {y ∈ topspace Y. (a,y) ∈ U} ∪ {y ∈ topspace Y. (a,y) ∈ V}"
using a that(3) by auto
have 2: "{y ∈ topspace Y. (a,y) ∈ U} ∩ {y ∈ topspace Y. (a,y) ∈ V} = {}"
using that(4) by auto
have 3: "{y ∈ topspace Y. (a,y) ∈ U} ≠ {}"
using ab b by auto
have 4: "{y ∈ topspace Y. (a,y) ∈ V} ≠ {}"
proof -
show ?thesis
using connected_spaceD [OF conX oX] UV ‹(x,y) ∉ U› a x y
disjoint_iff_not_equal by blast
qed
show ?thesis
using connected_spaceD [OF conY oY 1 2 3 4] by auto
qed
then show ?lhs
unfolding connected_space_def topspace_prod_topology by blast
qed
qed

lemma connectedin_Times:
"connectedin (prod_topology X Y) (S × T) ⟷
S = {} ∨ T = {} ∨ connectedin X S ∧ connectedin Y T"
by (auto simp: connectedin_def subtopology_Times connected_space_prod_topology subtopology_trivial_iff)

end

```