# Theory SML_Product_Topology

```(* Title: Examples/SML_Relativization/Topology/SML_Product_Topology.thy
Author: 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```