Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users

### Properties of the Product of Compact Topological Spaces

by

MML identifier: BORSUK_3
[ Mizar article, MML identifier index ]

```environ

vocabulary PRE_TOPC, SUBSET_1, FUNCOP_1, ORDINAL2, RELAT_1, FUNCT_1, TOPS_2,
T_0TOPSP, BOOLE, COMPTS_1, FUNCT_3, PARTFUN1, PBOOLE, TARSKI, BORSUK_1,
TOPS_1, CONNSP_2, SETFAM_1, FINSET_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, SETFAM_1, FUNCT_1,
STRUCT_0, PRE_TOPC, TOPS_2, TOPS_1, COMPTS_1, BORSUK_1, T_0TOPSP, PBOOLE,
FUNCT_2, FINSET_1, FUNCT_3, CAT_1, CONNSP_2, GRCAT_1;
constructors TOPS_2, T_0TOPSP, TOPS_1, COMPTS_1, WAYBEL_3, GRCAT_1, BORSUK_1,
MEMBERED;
clusters STRUCT_0, PRE_TOPC, BORSUK_1, BORSUK_2, TOPS_1, WAYBEL_3, WAYBEL12,
PSCOMP_1, RELSET_1, SUBSET_1, XBOOLE_0;
requirements SUBSET, BOOLE;

begin :: Preliminaries

theorem :: BORSUK_3:1
for S, T being TopSpace holds [#][:S, T:] = [:[#]S, [#]T:];

definition let X be set, Y be empty set;
cluster [:X, Y:] -> empty;
end;

definition let X be empty set, Y be set;
cluster [:X, Y:] -> empty;
end;

theorem :: BORSUK_3:2
for X, Y being non empty TopSpace,
x being Point of X holds
Y --> x is continuous map of Y, X|{x};

definition let T be non empty TopStruct;
cluster id T -> being_homeomorphism;
end;

definition let S, T be non empty TopStruct;
redefine pred S, T are_homeomorphic;
reflexivity;
symmetry;
end;

theorem :: BORSUK_3:3
for S, T, V being non empty TopSpace st
S, T are_homeomorphic & T, V are_homeomorphic holds
S, V are_homeomorphic;

begin :: On the projections and empty topological spaces

definition let T be TopStruct,
P be empty Subset of T;
cluster T | P -> empty;
end;

definition
cluster strict empty TopSpace;
end;

theorem :: BORSUK_3:4
for T1 being TopSpace,
T2 being empty TopSpace holds [:T1, T2:] is empty & [:T2, T1:] is empty;

theorem :: BORSUK_3:5
for T being empty TopSpace holds T is compact;

definition
cluster empty -> compact TopSpace;
end;

definition let T1 be TopSpace, T2 be empty TopSpace;
cluster [:T1, T2:] -> empty;
end;

theorem :: BORSUK_3:6
for X, Y being non empty TopSpace,
x being Point of X,
f being map of [:Y, X | {x}:], Y st
f = pr1(the carrier of Y, {x}) holds f is one-to-one;

theorem :: BORSUK_3:7
for X, Y being non empty TopSpace,
x being Point of X,
f being map of [:X | {x}, Y:], Y st
f = pr2({x}, the carrier of Y) holds f is one-to-one;

theorem :: BORSUK_3:8
for X, Y being non empty TopSpace,
x being Point of X,
f being map of [:Y, X | {x}:], Y st
f = pr1(the carrier of Y, {x}) holds f" = <:id Y, Y --> x:>;

theorem :: BORSUK_3:9
for X, Y being non empty TopSpace,
x being Point of X,
f being map of [:X | {x}, Y:], Y st
f = pr2({x}, the carrier of Y) holds f" = <:Y --> x, id Y:>;

theorem :: BORSUK_3:10
for X, Y being non empty TopSpace,
x being Point of X,
f being map of [:Y, X | {x}:], Y st
f = pr1(the carrier of Y, {x}) holds
f is_homeomorphism;

theorem :: BORSUK_3:11
for X, Y being non empty TopSpace,
x being Point of X,
f being map of [:X | {x}, Y:], Y st
f = pr2({x}, the carrier of Y) holds
f is_homeomorphism;

begin :: On the product of compact spaces

theorem :: BORSUK_3:12
for X being non empty TopSpace, Y being compact non empty TopSpace,
G being open Subset of [:X, Y:],
x being set st
x in { x' where x' is Point of X : [:{x'}, the carrier of Y:] c= G }
ex f being ManySortedSet of the carrier of Y st
for i being set st i in the carrier of Y
ex G1 being Subset of X, H1 being Subset of Y st f.i = [G1,H1] &
[x, i] in [:G1, H1:] & G1 is open & H1 is open & [:G1, H1:] c= G;

theorem :: BORSUK_3:13
for X being non empty TopSpace, Y being compact non empty TopSpace,
G being open Subset of [:Y, X:] holds
for x being set st x in { y where y is Point of X : [:[#]Y, {y}:] c= G }
holds
ex R be open Subset of X st x in R &
R c= { y where y is Point of X : [:[#]Y, {y}:] c= G };

theorem :: BORSUK_3:14
for X being non empty TopSpace, Y being compact non empty TopSpace,
G being open Subset of [:Y, X:] holds
{ x where x is Point of X : [:[#]Y, {x}:] c= G } in the topology of X;

theorem :: BORSUK_3:15
for X, Y being non empty TopSpace,
x being Point of X holds
[: X | {x}, Y :], Y are_homeomorphic;

theorem :: BORSUK_3:16
for S, T being non empty TopSpace st
S, T are_homeomorphic & S is compact holds T is compact;

theorem :: BORSUK_3:17
for X, Y being TopSpace,
XV being SubSpace of X holds
[:Y, XV:] is SubSpace of [:Y, X:];

theorem :: BORSUK_3:18
for X being non empty TopSpace,
Y being compact non empty TopSpace,
x being Point of X,
Z being Subset of [:Y, X:] st Z = [:[#]Y, {x}:] holds
Z is compact;

theorem :: BORSUK_3:19
for X being non empty TopSpace,
Y being compact non empty TopSpace,
x being Point of X holds
[:Y, X|{x}:] is compact;

theorem :: BORSUK_3:20
for X, Y being compact non empty TopSpace,
R being Subset-Family of X st
R = { Q where Q is open Subset of X : [:[#]Y, Q:] c=
union Base-Appr [#][:Y, X:] } holds R is open & R is_a_cover_of [#]X;

theorem :: BORSUK_3:21
for X, Y being compact non empty TopSpace,
R being Subset-Family of X,
F being Subset-Family of [:Y, X:] st
F is_a_cover_of [:Y, X:] & F is open &
R = { Q where Q is open Subset of X :
ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite &
[:[#]Y, Q:] c= union FQ } holds
R is open & R is_a_cover_of X;

theorem :: BORSUK_3:22
for X, Y being compact non empty TopSpace,
R being Subset-Family of X,
F being Subset-Family of [:Y, X:] st
F is_a_cover_of [:Y, X:] & F is open &
R = { Q where Q is open Subset of X :
ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite &
[:[#]Y, Q:] c= union FQ } holds
ex C being Subset-Family of X st C c= R & C is finite & C is_a_cover_of X;

theorem :: BORSUK_3:23
for X, Y being compact non empty TopSpace,
F being Subset-Family of [:Y, X:] st
F is_a_cover_of [:Y, X:] & F is open
ex G being Subset-Family of [:Y, X:]
st G c= F & G is_a_cover_of [:Y, X:] & G is finite;

theorem :: BORSUK_3:24
for T1, T2 be TopSpace st T1 is compact & T2 is compact holds
[:T1, T2:] is compact;

definition let T1, T2 be compact TopSpace;
cluster [:T1, T2:] -> compact;
end;

theorem :: BORSUK_3:25
for X, Y being non empty TopSpace,
XV being non empty SubSpace of X,
YV being non empty SubSpace of Y holds
[:XV, YV:] is SubSpace of [:X, Y:];

theorem :: BORSUK_3:26
for X, Y being non empty TopSpace,
Z being non empty Subset of [:Y, X:],
V being non empty Subset of X,
W being non empty Subset of Y st Z = [:W, V:] holds
the TopStruct of [:Y | W, X | V:] = the TopStruct of [:Y, X:] | Z;

definition let T be TopSpace;
cluster compact Subset of T;
end;

definition let T be TopSpace, P be compact Subset of T;
cluster T | P -> compact;
end;

theorem :: BORSUK_3:27
for T1, T2 being TopSpace,
S1 being Subset of T1,
S2 being Subset of T2 st S1 is compact & S2 is compact holds
[:S1, S2:] is compact Subset of [:T1, T2:];
```