Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: exact_real_arith.summary Sprache: Isabelle

Original von: 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 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

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 "(\x \ topspace Z. ?g x \ topspace X) \ (\x \ topspace Z. ?h x \ 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 (simp add: openin_prod_Times_iff mem_Times_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 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 (simp add: continuous_map_def openin_prod_topology_alt mem_Times_iff *)
 qed
 qed (auto 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 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 \ (topspace Y = {} \ topspace X = {})"
 by (auto simp: continuous_open_quotient_map open_map_fst continuous_map_fst)

lemma quotient_map_snd [simp]:
 "quotient_map(prod_topology X Y) Y snd \ (topspace X = {} \ topspace Y = {})"
 by (auto simp: continuous_open_quotient_map open_map_snd continuous_map_snd)

lemma retraction_map_fst:
 "retraction_map (prod_topology X Y) X fst \ (topspace Y = {} \ topspace X = {})"
proof (cases "topspace Y = {}")
 case True
 then show ?thesis
 using continuous_map_image_subset_topspace
 by (fastforce simp: retraction_map_def retraction_maps_def continuous_map_fst continuous_map_on_empty)
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 \ (topspace X = {} \ topspace Y = {})"
proof (cases "topspace X = {}")
 case True
 then show ?thesis
 using continuous_map_image_subset_topspace
 by (fastforce simp: retraction_map_def retraction_maps_def continuous_map_fst continuous_map_on_empty)
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) \ topspace Y = {} \ continuous_map X Z f"
proof (cases "topspace Y = {}")
 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) \ topspace X = {} \ continuous_map Y Z f"
proof (cases "topspace X = {}")
 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)) \
 topspace (prod_topology X Y) = {} \<or> continuous_map X X' f \<and> continuous_map Y Y' g"
proof (cases "topspace (prod_topology X Y) = {}")
 case True
 then show ?thesis
 by (simp add: continuous_map_on_empty)
next
 case False
 then show ?thesis
 by (simp add: continuous_map_paired case_prod_unfold continuous_map_of_fst [unfolded o_def] continuous_map_of_snd [unfolded o_def])
qed

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) \ topspace(prod_topology X Y) = {} \ compact_space X \ compact_space Y"
proof (cases "topspace(prod_topology X Y) = {}")
 case True
 then show ?thesis
 using compact_space_topspace_empty by blast
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"
 by (simp_all add: non_mt 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 add: 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 add:)
 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)

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)) \
 topspace(prod_topology X Y) = {} \<and>
 topspace(prod_topology X' Y') = {} \<or>
 homeomorphic_maps X X' f f' \<and>
 homeomorphic_maps Y Y' g g'"
 unfolding homeomorphic_maps_def continuous_map_prod_top
 by (auto simp: continuous_map_def homeomorphic_maps_def continuous_map_prod_top)

lemma homeomorphic_maps_swap:
 "homeomorphic_maps (prod_topology X Y) (prod_topology Y X)
 (\<lambda>(x,y). (y,x)) (\<lambda>(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 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:
 "topspace Y = {b} \ prod_topology X Y homeomorphic_space X"
 unfolding homeomorphic_space_def
 by (rule_tac x=fst in exI) (simp add: homeomorphic_map_def inj_on_def flip: homeomorphic_map_maps)

lemma prod_topology_homeomorphic_space_right:
 "topspace X = {a} \ prod_topology X Y homeomorphic_space Y"
 unfolding homeomorphic_space_def
 by (rule_tac x=snd in exI) (simp add: homeomorphic_map_def inj_on_def flip: homeomorphic_map_maps)

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 inf.absorb_iff2 insert_subset prod_topology_homeomorphic_space_left topspace_subtopology)

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 inf.absorb_iff2 insert_subset prod_topology_homeomorphic_space_right topspace_subtopology)

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 "topspace(prod_topology X Y) = {} \ 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 metis
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

end

¤ Dauer der Verarbeitung: 0.24 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.