(* Title: Examples/SML_Relativization/Topology/SML_Product_Topology.thy Author: Mihails Milehins Copyright 2021 (C) Mihails Milehins *) section‹Relativization of the results about product topologies› theory SML_Product_Topology imports SML_Topological_Space "../Foundations/Product_Type_Ext" begin subsection‹Definitions and common properties› ud‹ open_prod_inst.open_prod:: ('a::topological_space × 'b::topological_space) set ⇒ _ › ud‹open::('a::topological_space × 'b::topological_space) set ⇒ bool› ctr relativization synthesis ctr_simps assumes [transfer_domain_rule, transfer_rule]: "Domainp B = (λx. x ∈ U⇩_{1})" "Domainp A = (λx. x ∈ U⇩_{2})" and [transfer_rule]: "bi_unique A" "right_total A" "bi_unique B" "right_total B" trp (?'a A) and (?'b B) in open_ow: open_prod.with_def (‹'(/on _ _ with _ _ : «open» _/')› [1000, 999, 1000, 999, 1000] 10) locale product_topology_ow = ts⇩_{1}: topological_space_ow U⇩_{1}τ⇩_{1}+ ts⇩_{2}: topological_space_ow U⇩_{2}τ⇩_{2}for U⇩_{1}:: "'at set" and τ⇩_{1}:: "'at set ⇒ bool" and U⇩_{2}:: "'bt set"and τ⇩_{2}:: "'bt set ⇒ bool" + fixes τ :: "('at × 'bt) set ⇒ bool" assumes open_prod[tts_implicit]: "τ = open_ow U⇩_{1}U⇩_{2}τ⇩_{2}τ⇩_{1}" begin sublocale topological_space_ow ‹U⇩_{1}× U⇩_{2}› τ proof let ?U = "U⇩_{1}× U⇩_{2}" have open_prod': "τ S = open_ow U⇩_{1}U⇩_{2}τ⇩_{2}τ⇩_{1}S" for S by (simp only: open_prod) note op = open_prod'[unfolded open_ow_def, THEN iffD2, rule_format] show "τ (U⇩_{1}× U⇩_{2})" by (rule op) auto show "⟦ S ⊆ ?U; T ⊆ ?U; τ S; τ T ⟧ ⟹ τ (S ∩ T)" for S T proof- assume "S ⊆ ?U" and "T ⊆ ?U" and "τ S" and "τ T" from ‹S ⊆ ?U› ‹T ⊆ ?U› have "S ∩ T ⊆ ?U" by auto show "τ (S ∩ T)" proof(rule op) fix x assume "x ∈ S ∩ T" then have "x ∈ S" and "x ∈ T" by auto from open_prod'[ unfolded open_ow_def, THEN iffD1, rule_format, OF ‹τ S› ‹x ∈ S› ] obtain A⇩_{S}B⇩_{S}where "A⇩_{S}⊆ U⇩_{1}" "B⇩_{S}⊆ U⇩_{2}" "τ⇩_{1}A⇩_{S}" "τ⇩_{2}B⇩_{S}" "x ∈ A⇩_{S}× B⇩_{S}" "A⇩_{S}× B⇩_{S}⊆ S" by auto from open_prod'[ unfolded open_ow_def, THEN iffD1, rule_format, OF ‹τ T› ‹x ∈ T› ] obtain A⇩_{T}B⇩_{T}where "A⇩_{T}⊆ U⇩_{1}" "B⇩_{T}⊆ U⇩_{2}" "τ⇩_{1}A⇩_{T}" "τ⇩_{2}B⇩_{T}" "x ∈ A⇩_{T}× B⇩_{T}" "A⇩_{T}× B⇩_{T}⊆ T" by auto from ‹A⇩_{S}⊆ U⇩_{1}› ‹A⇩_{T}⊆ U⇩_{1}› have "A⇩_{S}∩ A⇩_{T}⊆ U⇩_{1}" by auto moreover from ‹B⇩_{S}⊆ U⇩_{2}› ‹B⇩_{T}⊆ U⇩_{2}› have "B⇩_{S}∩ B⇩_{T}⊆ U⇩_{2}" by auto moreover from ‹A⇩_{S}⊆ U⇩_{1}› ‹A⇩_{T}⊆ U⇩_{1}› ‹τ⇩_{1}A⇩_{S}› ‹τ⇩_{1}A⇩_{T}› have "τ⇩_{1}(A⇩_{S}∩ A⇩_{T})" by auto moreover from ‹B⇩_{S}⊆ U⇩_{2}› ‹B⇩_{T}⊆ U⇩_{2}› ‹τ⇩_{2}B⇩_{S}› ‹τ⇩_{2}B⇩_{T}› have "τ⇩_{2}(B⇩_{S}∩ B⇩_{T})" by auto moreover from ‹x ∈ A⇩_{S}× B⇩_{S}› ‹x ∈ A⇩_{T}× B⇩_{T}› have "x ∈ (A⇩_{S}∩ A⇩_{T}) × (B⇩_{S}∩ B⇩_{T})" by clarsimp moreover from ‹A⇩_{S}× B⇩_{S}⊆ S› ‹A⇩_{T}× B⇩_{T}⊆ T› have "(A⇩_{S}∩ A⇩_{T}) × (B⇩_{S}∩ B⇩_{T}) ⊆ S ∩ T" by auto ultimately show "∃A∈Pow U⇩_{1}. ∃B∈Pow U⇩_{2}. τ⇩_{1}A ∧ τ⇩_{2}B ∧ A × B ⊆ S ∩ T ∧ x ∈ A × B" by auto qed qed show "⟦ K ⊆ Pow ?U; ∀S∈K. τ S ⟧ ⟹ τ (⋃K)" for K proof - assume "K ⊆ Pow ?U" and "∀S∈K. τ S" from ‹K ⊆ Pow ?U› have "⋃K ⊆ ?U" by auto show "τ (⋃K)" proof(rule op) fix x assume "x ∈ ⋃K" then obtain k where k: "x ∈ k" and "k ∈ K" by clarsimp from ‹k ∈ K› have "k ⊆ ⋃K" by auto from ‹k ∈ K› have "τ k" by (rule ‹∀S∈K. τ S›[rule_format]) from open_prod'[ unfolded open_ow_def, THEN iffD1, rule_format, OF this ‹x ∈ k› ] obtain A B where "A ⊆ U⇩_{1}" "B ⊆ U⇩_{2}" "τ⇩_{1}A" "τ⇩_{2}B" "x ∈ A × B" "A × B ⊆ k" by auto from ‹A × B ⊆ k› ‹k ⊆ ⋃K› have "A × B ⊆ ⋃K" by simp from ‹A ⊆ U⇩_{1}› ‹B ⊆ U⇩_{2}› ‹τ⇩_{1}A› ‹τ⇩_{2}B› ‹x ∈ A × B› this show " ∃A∈Pow U⇩_{1}. ∃B∈Pow U⇩_{2}. τ⇩_{1}A ∧ τ⇩_{2}B ∧ A × B ⊆ ⋃ K ∧ x ∈ A × B" by auto qed qed qed end subsection‹Transfer rules› lemma (in product_topology_ow) open_with_oo_transfer[transfer_rule]: includes lifting_syntax fixes A :: "['at, 'a] ⇒ bool" and B :: "['bt, 'b] ⇒ bool" assumes tdr_U⇩_{1}[transfer_domain_rule]: "Domainp A = (λx. x ∈ U⇩_{1})" and [transfer_rule]: "bi_unique A" "right_total A" and tdr_U⇩_{2}[transfer_domain_rule]: "Domainp B = (λx. x ∈ U⇩_{2})" and [transfer_rule]: "bi_unique B" "right_total B" and τ⇩_{1}τ⇩_{1}'[transfer_rule]: "(rel_set A ===> (=)) τ⇩_{1}τ⇩_{1}'" and τ⇩_{2}τ⇩_{2}'[transfer_rule]: "(rel_set B ===> (=)) τ⇩_{2}τ⇩_{2}'" shows "(rel_set (rel_prod A B) ===> (=)) τ (open_prod.with τ⇩_{2}' τ⇩_{1}')" unfolding open_prod.with_def apply transfer_prover_start apply transfer_step+ apply simp apply(fold subset_eq) unfolding open_prod open_ow_def tdr_U⇩_{1}tdr_U⇩_{2}by (meson Pow_iff) subsection‹Relativization› context product_topology_ow begin tts_context tts: (?'a to U⇩_{1}) and (?'b to U⇩_{2}) rewriting ctr_simps substituting ts⇩_{1}.topological_space_ow_axioms and ts⇩_{2}.topological_space_ow_axioms eliminating ‹?U ≠ {}› through (fold tts_implicit, insert closed_empty, simp) applying [folded tts_implicit] begin tts_lemma open_prod_intro: assumes "S ⊆ U⇩_{1}× U⇩_{2}" and "⋀x. ⟦x ∈ U⇩_{1}× U⇩_{2}; x ∈ S⟧ ⟹ ∃A∈Pow U⇩_{1}. ∃B∈Pow U⇩_{2}. τ⇩_{1}A ∧ τ⇩_{2}B ∧ A × B ⊆ S ∧ x ∈ A × B" shows "τ S" is open_prod_intro. tts_lemma open_Times: assumes "S ⊆ U⇩_{1}" and "T ⊆ U⇩_{2}" and "τ⇩_{1}S" and "τ⇩_{2}T" shows "τ (S × T)" is open_Times. tts_lemma open_vimage_fst: assumes "S ⊆ U⇩_{1}" and "τ⇩_{1}S" shows "τ (fst -` S ∩ U⇩_{1}× U⇩_{2})" is open_vimage_fst. tts_lemma closed_vimage_fst: assumes "S ⊆ U⇩_{1}" and "ts⇩_{1}.closed S" shows "closed (fst -` S ∩ U⇩_{1}× U⇩_{2})" is closed_vimage_fst. tts_lemma closed_Times: assumes "S ⊆ U⇩_{1}" and "T ⊆ U⇩_{2}" and "ts⇩_{1}.closed S" and "ts⇩_{2}.closed T" shows "closed (S × T)" is closed_Times. tts_lemma open_image_fst: assumes "S ⊆ U⇩_{1}× U⇩_{2}" and "τ S" shows "τ⇩_{1}(fst ` S)" is open_image_fst. tts_lemma open_image_snd: assumes "S ⊆ U⇩_{1}× U⇩_{2}" and "τ S" shows "τ⇩_{2}(snd ` S)" is open_image_snd. end tts_context tts: (?'a to U⇩_{1}) and (?'b to U⇩_{2}) rewriting ctr_simps substituting ts⇩_{1}.topological_space_ow_axioms and ts⇩_{2}.topological_space_ow_axioms eliminating ‹?U ≠ {}› through (fold tts_implicit, unfold connected_ow_def, simp) applying [folded tts_implicit] begin tts_lemma connected_Times: assumes "S ⊆ U⇩_{1}" and "T ⊆ U⇩_{2}" and "ts⇩_{1}.connected S" and "ts⇩_{2}.connected T" shows "connected (S × T)" is connected_Times. tts_lemma connected_Times_eq: assumes "S ⊆ U⇩_{1}" and "T ⊆ U⇩_{2}" shows "connected (S × T) = (S = {} ∨ T = {} ∨ ts⇩_{1}.connected S ∧ ts⇩_{2}.connected T)" is connected_Times_eq. end tts_context tts: (?'b to U⇩_{1}) and (?'a to U⇩_{2}) rewriting ctr_simps substituting ts⇩_{1}.topological_space_ow_axioms and ts⇩_{2}.topological_space_ow_axioms eliminating ‹?U ≠ {}› through (fold tts_implicit, insert closed_empty, simp) applying [folded tts_implicit] begin tts_lemma open_vimage_snd: assumes "S ⊆ U⇩_{2}" and "τ⇩_{2}S" shows "τ (snd -` S ∩ U⇩_{1}× U⇩_{2})" is open_vimage_snd. tts_lemma closed_vimage_snd: assumes "S ⊆ U⇩_{2}" and "ts⇩_{2}.closed S" shows "closed (snd -` S ∩ U⇩_{1}× U⇩_{2})" is closed_vimage_snd. end end text‹\newpage› end