:: Some Remarks about Product Spaces
:: by Sebastian Koch
::
:: Received September 29, 2018
:: Copyright (c) 2018-2021 Association of Mizar Users


:: into FUNCT_1 ?
:: compare FUNCT_1:4
theorem Th1: :: TOPS_5:1
for f being one-to-one Function
for y being object st rng f = {y} holds
dom f = {((f ") . y)}
proof end;

:: into FUNCT_1 ?
theorem Th2: :: TOPS_5:2
for f being one-to-one Function
for y1, y2 being object st rng f = {y1,y2} holds
dom f = {((f ") . y1),((f ") . y2)}
proof end;

:: into PARTFUN1 ?
registration
let X, Y be set ;
cluster empty Relation-like X -defined Y -valued Function-like one-to-one for set ;
existence
ex b1 being Function st
( b1 is empty & b1 is X -defined & b1 is Y -valued & b1 is one-to-one )
proof end;
end;

:: into FINSET_1 ?
registration
let T, S be set ;
let f be Function of T,S;
let G be finite Subset-Family of T;
cluster f .: G -> finite ;
coherence
f .: G is finite
proof end;
end;

:: into RELSET_2 ?
theorem Th3: :: TOPS_5:3
for A being set
for F being Subset-Family of A
for R being Relation holds R .: (meet F) c= meet { (R .: X) where X is Subset of A : X in F }
proof end;

:: into RELSET_2 ?
theorem Th4: :: TOPS_5:4
for A being set
for F being Subset-Family of A
for f being one-to-one Function holds f .: (meet F) = meet { (f .: X) where X is Subset of A : X in F }
proof end;

:: into EQREL_1 ?
theorem Th5: :: TOPS_5:5
for X being set
for Y being non empty set
for f being Function of X,Y holds { (f " {y}) where y is Element of Y : y in rng f } is a_partition of X
proof end;

:: into FUNCOP_1 ?
theorem :: TOPS_5:6
for X being non empty set
for x, y being object st X --> x = X --> y holds
x = y
proof end;

:: into FUNCOP_1 ?
theorem Th7: :: TOPS_5:7
for i being object
for J being ManySortedSet of {i} holds J = {i} --> (J . i)
proof end;

:: into CARD_1 ?
theorem Th8: :: TOPS_5:8
for I being 2 -element set
for i, j being Element of I st i <> j holds
I = {i,j}
proof end;

:: into FUNCT_4 ?
:: compare FUNCT_4:66
theorem Th9: :: TOPS_5:9
for I being 2 -element set
for f being ManySortedSet of I
for i, j being Element of I st i <> j holds
f = (i,j) --> ((f . i),(f . j))
proof end;

:: into FUNCT_4 ?
theorem Th10: :: TOPS_5:10
for a, b, c, d being object st a <> b holds
(a,b) --> (c,d) = (b,a) --> (d,c)
proof end;

:: into FUNCT_4 ?
theorem Th11: :: TOPS_5:11
for f being Function
for i, j being object st i in dom f & j in dom f holds
f = f +* ((i,j) --> ((f . i),(f . j)))
proof end;

:: into FUNCT_4 ?
:: compare FUNCT_7:15, FUNCT_4:114
theorem Th12: :: TOPS_5:12
for x, y, z being object holds (x .--> y) +* (x .--> z) = x .--> z
proof end;

:: into PBOOLE ?
registration
cluster Relation-like non non-empty Function-like for set ;
existence
not for b1 being Function holds b1 is non-empty
proof end;
end;

:: BEGIN into CARD_3 ?
theorem Th13: :: TOPS_5:13
for X, Y being non empty set
for y being Element of Y holds X --> y in product (X --> Y)
proof end;

theorem Th14: :: TOPS_5:14
for X being non empty set
for Y being set
for Z being Subset of Y holds product (X --> Z) c= product (X --> Y)
proof end;

theorem Th15: :: TOPS_5:15
for X being non empty set
for i being object holds product ({i} --> X) = { ({i} --> x) where x is Element of X : verum }
proof end;

theorem Th16: :: TOPS_5:16
for X being non empty set
for i, f being object holds
( f in product ({i} --> X) iff ex x being Element of X st f = {i} --> x )
proof end;

:: compare YELLOW17:8
theorem :: TOPS_5:17
for X being non empty set
for i being object
for x being Element of X holds (proj (({i} --> X),i)) . ({i} --> x) = x
proof end;

Lm1: for f being Function st rng f = {{}} holds
product f = {}
proof end;

:: compare CARD_3:26
theorem :: TOPS_5:18
for X, Y being set holds
( ( X <> {} & Y = {} ) iff product (X --> Y) = {} )
proof end;

registration
let f be empty Function;
let x be object ;
cluster proj (f,x) -> trivial ;
coherence
proj (f,x) is trivial
proof end;
end;

theorem Th19: :: TOPS_5:19
for f being trivial Function
for x being object st x in dom f holds
proj (f,x) is one-to-one
proof end;

registration
let x, y be object ;
cluster proj ((x .--> y),x) -> one-to-one ;
coherence
proj ((x .--> y),x) is one-to-one
proof end;
end;

registration
let I be 1 -element set ;
let J be ManySortedSet of I;
let i be Element of I;
cluster proj (J,i) -> one-to-one ;
coherence
proj (J,i) is one-to-one
proof end;
end;

theorem :: TOPS_5:20
for X being non empty set
for Y being Subset of X
for i being object holds (proj (({i} --> X),i)) .: (product ({i} --> Y)) = Y
proof end;

theorem Th21: :: TOPS_5:21
for f, g being non-empty Function
for i, x being object st x in (product f) /\ (product (f +* g)) holds
(proj (f,i)) . x = (proj ((f +* g),i)) . x
proof end;

theorem Th22: :: TOPS_5:22
for f, g being non-empty Function
for i being object
for A being set st A c= (product f) /\ (product (f +* g)) holds
(proj (f,i)) .: A = (proj ((f +* g),i)) .: A
proof end;

theorem Th23: :: TOPS_5:23
for f, g being non-empty Function st dom g c= dom f & ( for i being object st i in dom g holds
g . i c= f . i ) holds
product (f +* g) c= product f
proof end;

theorem Th24: :: TOPS_5:24
for f, g being non-empty Function st dom g c= dom f & ( for i being object st i in dom g holds
g . i c= f . i ) holds
for i being object st i in (dom f) \ (dom g) holds
(proj (f,i)) .: (product (f +* g)) = f . i
proof end;

theorem Th25: :: TOPS_5:25
for f, g being non-empty Function st dom g c= dom f & ( for i being object st i in dom g holds
g . i c= f . i ) holds
for i being object st i in dom g holds
(proj (f,i)) .: (product (f +* g)) = g . i
proof end;

theorem Th26: :: TOPS_5:26
for f, g being non-empty Function st dom g = dom f & ( for i being object st i in dom g holds
g . i c= f . i ) holds
for i being object st i in dom g holds
(proj (f,i)) .: (product g) = g . i
proof end;

theorem Th27: :: TOPS_5:27
for f being Function
for X, Y being set
for i being object st X c= Y holds
product (f +* (i .--> X)) c= product (f +* (i .--> Y))
proof end;

theorem Th28: :: TOPS_5:28
for i, j being object
for A, B, C, D being set st A c= C & B c= D holds
product ((i,j) --> (A,B)) c= product ((i,j) --> (C,D))
proof end;

theorem Th29: :: TOPS_5:29
for X, Y being set
for f, i, j being object st i <> j holds
( f in product ((i,j) --> (X,Y)) iff ex x, y being object st
( x in X & y in Y & f = (i,j) --> (x,y) ) )
proof end;

theorem Th30: :: TOPS_5:30
for f being non-empty Function
for X, Y being set
for i, j, x, y being object
for g being Function st x in X & y in Y & i <> j & g in product f holds
g +* ((i,j) --> (x,y)) in product (f +* ((i,j) --> (X,Y)))
proof end;

theorem Th31: :: TOPS_5:31
for f being Function
for A, B, C, D being set
for i, j being object st A c= C & B c= D holds
product (f +* ((i,j) --> (A,B))) c= product (f +* ((i,j) --> (C,D)))
proof end;

theorem :: TOPS_5:32
for f being Function
for A, B being set
for i, j being object st i in dom f & j in dom f & A c= f . i & B c= f . j holds
product (f +* ((i,j) --> (A,B))) c= product f
proof end;

:: $\prod_{i\in I} A_i \cap \prod_{i\in I} B_i = \prod_{i\in I} (A_i \cap B_i)$
:: compare MSUALG_2:1
theorem Th33: :: TOPS_5:33
for I being set
for f, g being ManySortedSet of I holds (product f) /\ (product g) = product (f (/\) g)
proof end;

Lm2: for I being 2 -element set
for f being ManySortedSet of I
for i, j being Element of I
for x being object st i <> j holds
f +* (i,x) = (i,j) --> (x,(f . j))
proof end;

theorem Th34: :: TOPS_5:34
for I being 2 -element set
for f being ManySortedSet of I
for i, j being Element of I
for x being object st i <> j holds
( f +* (i,x) = (i,j) --> (x,(f . j)) & f +* (j,x) = (i,j) --> ((f . i),x) )
proof end;

theorem Th35: :: TOPS_5:35
for f being non-empty Function
for X being set
for i being object st i in dom f holds
( f +* (i,X) is non-empty iff not X is empty )
proof end;

theorem Th36: :: TOPS_5:36
for f being non-empty Function
for X being set
for i being object st i in dom f holds
( product (f +* (i,X)) = {} iff X is empty )
proof end;

theorem Th37: :: TOPS_5:37
for f being non-empty Function
for X being set
for i, x being object
for g being Function st i in dom f & x in X & g in product f holds
g +* (i,x) in product (f +* (i,X))
proof end;

theorem Th38: :: TOPS_5:38
for f being Function
for X, Y being set
for i being object st i in dom f & X c= Y holds
product (f +* (i,X)) c= product (f +* (i,Y))
proof end;

:: compare YELLOW17:2
theorem Th39: :: TOPS_5:39
for f being Function
for X being set
for i being object st i in dom f & X c= f . i holds
product (f +* (i,X)) c= product f
proof end;

theorem :: TOPS_5:40
for f being non-empty Function
for X, Y being non empty set
for i, j being object st i in dom f & j in dom f & ( not X c= f . i or not f . j c= Y ) & product (f +* (i,X)) c= product (f +* (j,Y)) holds
( i = j & X c= Y )
proof end;

theorem :: TOPS_5:41
for f being non-empty Function
for X being set
for i being object st i in dom f & product (f +* (i,X)) c= product f holds
X c= f . i
proof end;

theorem Th42: :: TOPS_5:42
for f being non-empty Function
for X, Y being non empty set
for i, j being object st i in dom f & j in dom f & ( X <> f . i or Y <> f . j ) & product (f +* (i,X)) = product (f +* (j,Y)) holds
( i = j & X = Y )
proof end;

theorem Th43: :: TOPS_5:43
for f being non-empty Function
for X being set
for i being object st i in dom f & X c= f . i holds
(proj (f,i)) .: (product (f +* (i,X))) = X
proof end;

theorem Th44: :: TOPS_5:44
for x, y, z being object holds (x .--> y) +* (x,z) = x .--> z
proof end;

:: END into FUNCT_7 ?
:: into PRALG_1 ?
registration
let I be non empty set ;
let J be 1-sorted-yielding non-Empty ManySortedSet of I;
cluster Carrier J -> non-empty ;
coherence
Carrier J is non-empty
proof end;
end;

theorem Th45: :: TOPS_5:45
for T, S being TopSpace
for f being Function of T,S holds
( f is open iff ex B being Basis of T st
for V being Subset of T st V in B holds
f .: V is open )
proof end;

theorem :: TOPS_5:46
for T1, T2, S1, S2 being non empty TopSpace
for f being Function of T1,S1
for g being Function of T2,S2 st f is open & g is open holds
[:f,g:] is open
proof end;

theorem Th47: :: TOPS_5:47
for S, T being non empty TopSpace
for f being Function of S,T st f is bijective & ex K being Basis of S ex L being Basis of T st f .: K = L holds
f is being_homeomorphism
proof end;

theorem Th48: :: TOPS_5:48
for S, T being non empty TopSpace
for f being Function of S,T st f is bijective & ex K being prebasis of S ex L being prebasis of T st f .: K = L holds
f is being_homeomorphism
proof end;

:: compare TOPGEN_5:71 (the converse)
theorem Th49: :: TOPS_5:49
for S, T being TopSpace st ex K being Basis of S ex L being Basis of T st K = INTERSECTION (L,{([#] S)}) holds
S is SubSpace of T
proof end;

theorem Th50: :: TOPS_5:50
for S, T being TopSpace st [#] S c= [#] T & ex K being prebasis of S ex L being prebasis of T st K = INTERSECTION (L,{([#] S)}) holds
S is SubSpace of T
proof end;

theorem Th51: :: TOPS_5:51
for S, T being TopSpace st ex K being prebasis of S ex L being prebasis of T st
( [#] S in K & K = INTERSECTION (L,{([#] S)}) ) holds
S is SubSpace of T
proof end;

theorem Th52: :: TOPS_5:52
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I holds rng (proj (J,i)) = the carrier of (J . i)
proof end;

registration
let X be set ;
let T be TopStruct ;
cluster X --> T -> TopStruct-yielding ;
coherence
X --> T is TopStruct-yielding ;
end;

definition
let F be Relation;
attr F is TopSpace-yielding means :Def1: :: TOPS_5:def 1
 for x being object st x in rng F holds
x is TopSpace;
end;

:: deftheorem Def1 defines TopSpace-yielding TOPS_5:def 1 :
for F being Relation holds
( F is TopSpace-yielding iff for x being object st x in rng F holds
x is TopSpace );

registration
cluster Relation-like TopSpace-yielding -> TopStruct-yielding for set ;
coherence
for b1 being Relation st b1 is TopSpace-yielding holds
b1 is TopStruct-yielding
proof end;
end;

registration
cluster Relation-like Function-like TopSpace-yielding -> 1-sorted-yielding for set ;
coherence
for b1 being Function st b1 is TopSpace-yielding holds
b1 is 1-sorted-yielding ;
end;

registration
let X be set ;
let T be TopSpace;
cluster X --> T -> TopSpace-yielding ;
coherence
X --> T is TopSpace-yielding
proof end;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like total non-Empty TopSpace-yielding for set ;
existence
ex b1 being ManySortedSet of I st
( b1 is TopSpace-yielding & b1 is non-Empty )
proof end;
end;

definition
let I be non empty set ;
let J be non-Empty TopSpace-yielding ManySortedSet of I;
let i be Element of I;
:: original: .
redefine func J . i -> non empty TopSpace;
coherence
J . i is non empty TopSpace
proof end;
end;

definition
let f be Function;
func ProjMap f -> ManySortedFunction of dom f means :Def2: :: TOPS_5:def 2
 for x being object st x in dom f holds
it . x = proj (f,x);
existence
ex b1 being ManySortedFunction of dom f st
for x being object st x in dom f holds
b1 . x = proj (f,x)
proof end;
uniqueness
for b1, b2 being ManySortedFunction of dom f st ( for x being object st x in dom f holds
b1 . x = proj (f,x) ) & ( for x being object st x in dom f holds
b2 . x = proj (f,x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines ProjMap TOPS_5:def 2 :
for f being Function
for b2 being ManySortedFunction of dom f holds
( b2 = ProjMap f iff for x being object st x in dom f holds
b2 . x = proj (f,x) );

registration
let f be empty Function;
cluster ProjMap f -> empty ;
coherence
ProjMap f is empty ;
end;

registration
let f be non-empty Function;
cluster ProjMap f -> non-empty ;
coherence
ProjMap f is non-empty
proof end;
end;

registration
let f be non non-empty Function;
cluster ProjMap f -> empty-yielding ;
coherence
ProjMap f is empty-yielding
proof end;
end;

definition
let I be non empty set ;
let J be non-Empty TopStruct-yielding ManySortedSet of I;
func ProjMap J -> ManySortedSet of I equals :: TOPS_5:def 3
 ProjMap (Carrier J);
coherence
ProjMap (Carrier J) is ManySortedSet of I
proof end;
end;

:: deftheorem defines ProjMap TOPS_5:def 3 :
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I holds ProjMap J = ProjMap (Carrier J);

registration
let I be non empty set ;
let J be non-Empty TopStruct-yielding ManySortedSet of I;
cluster ProjMap J -> non empty non-empty Function-yielding ;
coherence
( ProjMap J is Function-yielding & not ProjMap J is empty & ProjMap J is non-empty ) ;
end;

theorem Th53: :: TOPS_5:53
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I holds (ProjMap J) . i = proj (J,i)
proof end;

:: this functor will be used to express the notion of
:: "all but finitely many factors being the full factor space"
:: when considering the canonical base of the product topology
definition
let I be non empty set ;
let J be non-Empty TopStruct-yielding ManySortedSet of I;
let f be I -valued one-to-one Function;
func product_basis_selector (J,f) -> ManySortedSet of rng f equals :: TOPS_5:def 4
((ProjMap J) .:.: (I -indexing (f "))) | (rng f);
coherence
((ProjMap J) .:.: (I -indexing (f "))) | (rng f) is ManySortedSet of rng f
proof end;
end;

:: deftheorem defines product_basis_selector TOPS_5:def 4 :
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for f being b1 -valued one-to-one Function holds product_basis_selector (J,f) = ((ProjMap J) .:.: (I -indexing (f "))) | (rng f);

registration
let I be non empty set ;
let J be non-Empty TopStruct-yielding ManySortedSet of I;
let f be empty I -valued one-to-one Function;
cluster product_basis_selector (J,f) -> empty ;
coherence
product_basis_selector (J,f) is empty ;
end;

theorem Th54: :: TOPS_5:54
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for f being b1 -valued one-to-one Function
for i being Element of I st i in rng f holds
(product_basis_selector (J,f)) . i = (proj (J,i)) .: ((f ") . i)
proof end;

theorem Th55: :: TOPS_5:55
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for f being b1 -valued one-to-one Function st f " is non-empty & dom f c= bool (product (Carrier J)) holds
product_basis_selector (J,f) is non-empty
proof end;

theorem Th56: :: TOPS_5:56
for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I holds {} in product_prebasis J
proof end;

:: compare YELLOW17:16
theorem Th57: :: TOPS_5:57
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for P being non empty Subset of (product (Carrier J)) st P in product_prebasis J holds
ex i being Element of I st
( (proj (J,i)) .: P is open & ( for j being Element of I st j <> i holds
(proj (J,j)) .: P = [#] (J . j) ) )
proof end;

theorem Th58: :: TOPS_5:58
for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for P being non empty Subset of (product (Carrier J)) st P in product_prebasis J holds
( ( for j being Element of I holds (proj (J,j)) .: P is open ) & ex i being Element of I st
for j being Element of I st j <> i holds
(proj (J,j)) .: P = [#] (J . j) )
proof end;

theorem Th59: :: TOPS_5:59
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for f being b1 -valued one-to-one Function
for X being Subset-Family of (product (Carrier J)) st X c= product_prebasis J & dom f = X & f " is non-empty & ( for A being Subset of (product (Carrier J)) st A in X holds
(proj (J,(f /. A))) .: A is open ) holds
for i being Element of I holds
( ( not i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i) ) & ( i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open ) )
proof end;

theorem Th60: :: TOPS_5:60
for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for f being b1 -valued one-to-one Function
for X being Subset-Family of (product (Carrier J)) st X c= product_prebasis J & dom f = X & f " is non-empty & ( for A being Subset of (product (Carrier J)) st A in X holds
(proj (J,(f /. A))) .: A is open ) holds
for i being Element of I holds
( (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open & ( not i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i) ) )
proof end;

Lm3: for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for P being Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds
ex X being Subset-Family of (product (Carrier J)) ex f being b1 -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )
proof end;

:: Theorem of canonical product base characterization
theorem :: TOPS_5:61
for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for P being Subset of (product (Carrier J)) holds
( P in FinMeetCl (product_prebasis J) iff ex X being Subset-Family of (product (Carrier J)) ex f being b1 -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) ) ) by Lm3, CANTOR_1:def 3;

theorem Th62: :: TOPS_5:62
for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for P being non empty Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds
ex X being Subset-Family of (product (Carrier J)) ex f being b1 -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & ( for i being Element of I holds
( (proj (J,i)) .: P is open & ( not i in rng f implies (proj (J,i)) .: P = [#] (J . i) ) ) ) )
proof end;

theorem Th63: :: TOPS_5:63
for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for P being non empty Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds
ex I0 being finite Subset of I st
for i being Element of I holds
( (proj (J,i)) .: P is open & ( not i in I0 implies (proj (J,i)) .: P = [#] (J . i) ) )
proof end;

:: characterization of the canonical prebasis of
:: the product topology over one factor
theorem Th64: :: TOPS_5:64
for I being 1 -element set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for P being Subset of (product (Carrier J)) holds
( P in product_prebasis J iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )
proof end;

Lm4: for I being 1 -element set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for P being Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds
ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) )
proof end;

Lm5: for I being 1 -element set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for P being Subset of (product (Carrier J)) holds
( P in FinMeetCl (product_prebasis J) iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )
proof end;

Lm6: for I being 1 -element set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for P being Subset of (product (Carrier J)) holds
( P in UniCl (FinMeetCl (product_prebasis J)) iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )
proof end;

Lm7: for I being 1 -element set
for J being non-Empty TopSpace-yielding ManySortedSet of I holds UniCl (FinMeetCl (product_prebasis J)) = product_prebasis J
proof end;

theorem Th65: :: TOPS_5:65
for I being 1 -element set
for J being non-Empty TopSpace-yielding ManySortedSet of I holds the topology of (product J) = product_prebasis J
proof end;

:: characterization of open sets in the product topology over one factor
theorem :: TOPS_5:66
for I being 1 -element set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for P being Subset of (product J) holds
( P is open iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )
proof end;

registration
let I be non empty set ;
let J be non-Empty TopStruct-yielding ManySortedSet of I;
let i be Element of I;
cluster proj (J,i) -> onto continuous ;
coherence
( proj (J,i) is continuous & proj (J,i) is onto )
proof end;
end;

registration
let I be non empty set ;
let J be non-Empty TopSpace-yielding ManySortedSet of I;
let i be Element of I;
cluster proj (J,i) -> open ;
coherence
proj (J,i) is open
proof end;
end;

theorem Th67: :: TOPS_5:67
for I being 1 -element set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I holds proj (J,i) is being_homeomorphism
proof end;

:: the product topology over one factor is homeomorphic to that factor
theorem :: TOPS_5:68
for I being 1 -element set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I holds product J,J . i are_homeomorphic
proof end;

Lm8: for I being 2 -element set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i, j being Element of I
for P being Subset of (product (Carrier J)) holds
( not i <> j or not P in product_prebasis J or ex V being Subset of (J . i) st
( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st
( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )
proof end;

:: characterization of the canonical prebasis of
:: the product topology over two factors
theorem Th69: :: TOPS_5:69
for I being 2 -element set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i, j being Element of I
for P being Subset of (product (Carrier J)) st i <> j holds
( P in product_prebasis J iff ( ex V being Subset of (J . i) st
( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st
( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) ) )
proof end;

Lm9: for I being 2 -element set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i, j being Element of I
for P being Subset of (product (Carrier J)) st i <> j & P in FinMeetCl (product_prebasis J) holds
ex V being Subset of (J . i) ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) )
proof end;

:: characterization of the canonical basis of
:: the product topology over two factors
theorem :: TOPS_5:70
for I being 2 -element set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i, j being Element of I
for P being Subset of (product (Carrier J)) st i <> j holds
( P in FinMeetCl (product_prebasis J) iff ex V being Subset of (J . i) ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) ) )
proof end;

theorem :: TOPS_5:71
for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i, j being Element of I holds <:(proj (J,i)),(proj (J,j)):> is Function of (product J),[:(J . i),(J . j):] by BORSUK_1:def 2;

:: can be generalized: P only needs to contain the square F.i x F.j
:: at one point p, the Proof works the same
theorem Th72: :: TOPS_5:72
for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for P being Subset of (product (Carrier J))
for i, j being Element of I st i <> j & ex F being ManySortedSet of I st
( P = product F & ( for k being Element of I holds F . k c= (Carrier J) . k ) ) holds
<:(proj (J,i)),(proj (J,j)):> .: P = [:((proj (J,i)) .: P),((proj (J,j)) .: P):]
proof end;

theorem Th73: :: TOPS_5:73
for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i, j being Element of I
for f being Function of (product J),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds
( f is onto & f is open )
proof end;

theorem Th74: :: TOPS_5:74
for I being 2 -element set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i, j being Element of I
for f being Function of (product J),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds
f is being_homeomorphism
proof end;

:: the product topology over two factors is
:: homeomorphic to the cartesian product of these two factors
:: ( [: S,T :], [: T,S :] are_homeomorphic is a corrolary,
:: but it is already in the MML)
theorem :: TOPS_5:75
for I being 2 -element set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i, j being Element of I st i <> j holds
product J,[:(J . i),(J . j):] are_homeomorphic
proof end;

registration
let I1, I2 be non empty set ;
let J be non-Empty TopSpace-yielding ManySortedSet of I2;
let f be Function of I1,I2;
cluster f * J -> non-Empty TopSpace-yielding ;
coherence
( J * f is TopSpace-yielding & J * f is non-Empty )
proof end;
end;

definition
let I1, I2 be non empty set ;
let J1 be non-Empty TopSpace-yielding ManySortedSet of I1;
let J2 be non-Empty TopSpace-yielding ManySortedSet of I2;
let p be Function of I1,I2;
assume that
A1: p is bijective and
A2: for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ;
mode ProductHomeo of J1,J2,p -> Function of (product J1),(product J2) means :Def5: :: TOPS_5:def 5
 ex F being ManySortedFunction of I1 st
( ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st
( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)
for i being Element of I1 holds (it . g) . (p . i) = (F . i) . (g . i) ) );
existence
ex b1 being Function of (product J1),(product J2) ex F being ManySortedFunction of I1 st
( ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st
( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)
for i being Element of I1 holds (b1 . g) . (p . i) = (F . i) . (g . i) ) )
proof end;
end;

:: deftheorem Def5 defines ProductHomeo TOPS_5:def 5 :
for I1, I2 being non empty set
for J1 being non-Empty TopSpace-yielding ManySortedSet of I1
for J2 being non-Empty TopSpace-yielding ManySortedSet of I2
for p being Function of I1,I2 st p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) holds
for b6 being Function of (product J1),(product J2) holds
( b6 is ProductHomeo of J1,J2,p iff ex F being ManySortedFunction of I1 st
( ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st
( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)
for i being Element of I1 holds (b6 . g) . (p . i) = (F . i) . (g . i) ) ) );

:: characterization of images of certain subsets under product homeomorphism
theorem Th76: :: TOPS_5:76
for I1, I2 being non empty set
for J1 being non-Empty TopSpace-yielding ManySortedSet of I1
for J2 being non-Empty TopSpace-yielding ManySortedSet of I2
for p being Function of I1,I2
for H being ProductHomeo of J1,J2,p
for F being ManySortedFunction of I1 st p is bijective & ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st
( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)
for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) holds
for i being Element of I1
for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))
proof end;

theorem Th77: :: TOPS_5:77
for I1, I2 being non empty set
for J1 being non-Empty TopSpace-yielding ManySortedSet of I1
for J2 being non-Empty TopSpace-yielding ManySortedSet of I2
for p being Function of I1,I2
for H being ProductHomeo of J1,J2,p st p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) holds
H is bijective
proof end;

theorem Th78: :: TOPS_5:78
for I1, I2 being non empty set
for J1 being non-Empty TopSpace-yielding ManySortedSet of I1
for J2 being non-Empty TopSpace-yielding ManySortedSet of I2
for p being Function of I1,I2
for H being ProductHomeo of J1,J2,p st p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) holds
H is being_homeomorphism
proof end;

:: pairwise homeomorphic factors lead to homeomorphic products
theorem Th79: :: TOPS_5:79
for I1, I2 being non empty set
for J1 being non-Empty TopSpace-yielding ManySortedSet of I1
for J2 being non-Empty TopSpace-yielding ManySortedSet of I2
for p being Function of I1,I2 st p is bijective & ( for i being Element of I1 holds J1 . i,(J2 * p) . i are_homeomorphic ) holds
product J1, product J2 are_homeomorphic
proof end;

theorem :: TOPS_5:80
for I being non empty set
for J1, J2 being non-Empty TopSpace-yielding ManySortedSet of I
for p being Permutation of I st ( for i being Element of I holds J1 . i,(J2 * p) . i are_homeomorphic ) holds
product J1, product J2 are_homeomorphic by Th79;

:: permutations of the underlying set family lead to a homeomorphic copy of
:: the original product
:: (the following one could also be done with TopStruct-yielding
:: but then the theorems before couldn't be used and the long argumentation
:: would have to be repeated for most parts)
theorem :: TOPS_5:81
for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for p being Permutation of I holds product J, product (J * p) are_homeomorphic
proof end;

:: if each factor of the first product is a subspace of a corresponding
:: factor of the second product, the first product is a subspae of the second
theorem :: TOPS_5:82
for I being non empty set
for J1, J2 being non-Empty TopSpace-yielding ManySortedSet of I st ( for i being Element of I holds J1 . i is SubSpace of J2 . i ) holds
product J1 is SubSpace of product J2
proof end;