Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Analysis/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 33 kB

Quelle Product_Topology.thy Sprache: Isabelle

section\<open>The binary product topology\<close>

theory Product_Topology
 imports Function_Topology
begin

section \<open>Product Topology\<close>

subsection\<open>Definition\<close>

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 ?\ = "(\<lambda>u. f u \<times> 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) =
 (\<lambda>U. \<exists>S' T'. U = S' \<times> T' \<and> (openin X relative_to S) S' \<and> (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"
 by (simp add: prod_topology_def open_product_open_eq)

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 \
 (\<forall>x y. (x,y) \<in> S \<longrightarrow> (\<exists>U V. openin X U \<and> openin Y V \<and> x \<in> U \<and> y \<in> V \<and> U \<times> V \<subseteq> 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"
 by (simp add: Sigma_mono interior_of_subset)
 show "openin (prod_topology X Y) ((X interior_of S) \ Y interior_of T)"
 by (simp add: openin_prod_Times_iff)
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 \<open>Missing the opposite direction. Does it hold? A converse is proved for proper maps, a stronger condition\<close>
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: \<open>closedin X C\<close> 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: \<open>closedin Y C\<close> 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 \<open>Continuity\<close>

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 \<open>f x \<in> W\<close>]
 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: \<open>x \<in> topspace Z\<close> 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"
 by (simp add: continuous_map_pairwise o_def)

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))"
 by (simp add: continuous_map_pairwise o_def)

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]
 by (simp add: continuous_map_pairwise)

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]
 by (simp add: continuous_map_pairwise)

lemma continuous_map_fst_of [continuous_intros]:
 "continuous_map Z (prod_topology X Y) f \ continuous_map Z X (fst \ f)"
 by (simp add: continuous_map_pairwise)

lemma continuous_map_snd_of [continuous_intros]:
 "continuous_map Z (prod_topology X Y) f \ continuous_map Z Y (snd \ f)"
 by (simp add: continuous_map_pairwise)

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\
 \<Longrightarrow> continuous_map X Y (\<lambda>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
 by (simp add: continuous_map_on_empty)
next
 case False
 then show ?thesis
 by (simp add: continuous_compose_quotient_map_eq)
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
 by (simp add: continuous_map_on_empty)
next
 case False
 then show ?thesis
 by (simp add: continuous_compose_quotient_map_eq)
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 \<or> continuous_map X X' f \<and> 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 \<X> where "\<X> \<equiv> (\<lambda>V. topspace X \<times> V) ` Collect (openin Y)"
 define \<Y> where "\<Y> \<equiv> (\<lambda>U. U \<times> 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 \<X>_def \<Y>_def by auto
 fix \<C> :: "('a \<times> 'b) set set"
 assume \<C>: "\<C> \<subseteq> \<X> \<union> \<Y>" "topspace X \<times> topspace Y \<subseteq> \<Union>\<C>"
 then obtain \<X>' \<Y>' where XY: "\<X>' \<subseteq> \<X>" "\<Y>' \<subseteq> \<Y>" and \<C>eq: "\<C> = \<X>' \<union> \<Y>'"
 using subset_UnE by metis
 then have sub: "topspace X \ topspace Y \ \(\' \ \')"
 using \<C> by simp
 obtain \ \<V> where \: "\<And>U. U \<in> \ \<Longrightarrow> openin X U" "\<Y>' = (\<lambda>U. U \<times> topspace Y) ` \"
 and \<V>: "\<And>V. V \<in> \<V> \<Longrightarrow> openin Y V" "\<X>' = (\<lambda>V. topspace X \<times> V) ` \<V>"
 using XY by (clarsimp simp add: \<X>_def \<Y>_def subset_image_iff) (force simp: subset_iff)
 have "\\. finite \ \ \ \ \' \ \' \ topspace X \ topspace Y \ \ \"
 proof -
 have "topspace X \ \\ \ topspace Y \ \\"
 using \ \<V> \<C> \<C>eq by auto
 then have *: "\\. finite \ \
 (\<forall>x \<in> \<D>. x \<in> (\<lambda>V. topspace X \<times> V) ` \<V> \<or> x \<in> (\<lambda>U. U \<times> topspace Y) ` \) \<and>
 (topspace X \<times> topspace Y \<subseteq> \<Union>\<D>)"
 proof
 assume "topspace X \ \\"
 with \<open>compact_space X\<close> \ obtain \<F> where "finite \<F>" "\<F> \<subseteq> \" "topspace X \<subseteq> \<Union>\<F>"
 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 \<open>compact_space Y\<close> \<V> obtain \<F> where "finite \<F>" "\<F> \<subseteq> \<V>" "topspace Y \<subseteq> \<Union>\<F>"
 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 \ \<V> by blast
 qed
 then show "\\. finite \ \ \ \ \ \ topspace X \ topspace Y \ \ \"
 using \<C> \<C>eq by blast
 next
 have "(finite intersection_of (\x. x \ \ \ x \ \) relative_to topspace X \ topspace Y)
 = (\<lambda>U. \<exists>S T. U = S \<times> T \<and> openin X S \<and> 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 \<X>_def \<Y>_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 \<X>_def \<Y>_def)
 apply (rule_tac x="{(U \ topspace Y),(topspace X \ V)}" in exI)
 using \<open>openin X U\<close> \<open>openin Y V\<close> openin_subset UV apply (fastforce simp:)
 done
 qed
 ultimately show ?thesis
 using \<open>Z = U \<times> V\<close> by auto
 qed
 ultimately show ?thesis
 by meson
 qed
 then show "topology (arbitrary union_of (finite intersection_of (\x. x \ \ \ \)
 relative_to (topspace X \<times> topspace Y))) =
 prod_topology X Y"
 by (simp add: prod_topology_def)
 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\<open>Homeomorphic maps\<close>

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 \<and> (prod_topology X' Y') = trivial_topology
 \<or> homeomorphic_maps X X' f f' \<and> 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'\
 \<Longrightarrow> 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\ \ \\<^sub>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 "\\<^sub>F x in F. fst (f x) \ U" if "openin X U" "a \ U" for U
 proof -
 have "\\<^sub>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 "\\<^sub>F x in F. snd (f x) \ U" if "openin Y U" "b \ U" for U
 proof -
 have "\\<^sub>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
 by (simp add: limitin_def)
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 \ (\\<^sub>F x in F. fst (f x) \ U)"
 and b: "b \ topspace Y" "\U. openin Y U \ b \ U \ (\\<^sub>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 "\\<^sub>F x in F. fst (f x) \ U" "\\<^sub>F x in F. snd (f x) \ V"
 by (simp_all add: a b)
 then show "\\<^sub>F x in F. f x \ Z"
 by (rule eventually_elim2) (use \<open>U \<times> V \<subseteq> Z\<close> 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 \<or> connected_space X \<and> 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 \<open>U \<noteq> {}\<close> Usub by auto
 have "\ topspace X \ topspace Y \ U"
 using Usub Vsub \<open>U \<inter> V = {}\<close> \<open>V \<noteq> {}\<close> 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 \<open>(x,y) \<notin> U\<close> 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 = {} \<or> T = {} \<or> connectedin X S \<and> connectedin Y T"
 by (auto simp: connectedin_def subtopology_Times connected_space_prod_topology subtopology_trivial_iff)

end

quality100%

¤ Dauer der Verarbeitung: 0.4 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.