:: Properties of the Product of Compact Topological Spaces
:: by Adam Grabowski
::
:: Received February 13, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies PRE_TOPC, SUBSET_1, ZFMISC_1, XBOOLE_0, FUNCOP_1, ORDINAL2,
FUNCT_1, RELAT_1, STRUCT_0, TOPS_2, T_0TOPSP, RCOMP_1, MCART_1, PARTFUN1,
TARSKI, PBOOLE, BORSUK_1, TOPS_1, CONNSP_2, SETFAM_1, FINSET_1, FUNCT_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, SETFAM_1, FUNCT_1,
PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, DOMAIN_1,
STRUCT_0, PRE_TOPC, TOPS_2, TOPS_1, COMPTS_1, BORSUK_1, T_0TOPSP,
FINSET_1, FUNCT_3, CONNSP_2;
constructors FUNCT_3, TOPS_1, TOPS_2, COMPTS_1, BORSUK_1, T_0TOPSP, FUNCOP_1,
BINOP_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, PRE_TOPC,
TOPS_1, BORSUK_1, COMPTS_1, BORSUK_2, ZFMISC_1;
requirements SUBSET, BOOLE;
begin :: Preliminaries
theorem :: BORSUK_3:1
for S, T being TopSpace holds [#][:S, T:] = [:[#]S, [#]T:];
theorem :: BORSUK_3:2
for X, Y being non empty TopSpace, x being Point of X holds Y -->
x is continuous Function of Y, X|{x};
registration
let T be TopStruct;
cluster id T -> being_homeomorphism;
end;
definition
let S, T be TopStruct;
redefine pred S, T are_homeomorphic;
reflexivity;
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
registration
let T be TopStruct, P be empty Subset of T;
cluster T | P -> empty;
end;
registration
cluster empty -> compact for TopSpace;
end;
theorem :: BORSUK_3:4
for X, Y being non empty TopSpace, x being Point of X, f being
Function of [:Y, X | {x}:], Y st f = pr1(the carrier of Y, {x}) holds f is
one-to-one;
theorem :: BORSUK_3:5
for X, Y being non empty TopSpace, x being Point of X, f being
Function of [:X | {x}, Y:], Y st f = pr2({x}, the carrier of Y) holds f is
one-to-one;
theorem :: BORSUK_3:6
for X, Y being non empty TopSpace, x being Point of X, f being
Function of [:Y, X | {x}:], Y st f = pr1(the carrier of Y, {x}) holds f" = <:id
Y, Y --> x:>;
theorem :: BORSUK_3:7
for X, Y being non empty TopSpace, x being Point of X, f being
Function of [:X | {x}, Y:], Y st f = pr2({x}, the carrier of Y) holds f" = <:Y
--> x, id Y:>;
theorem :: BORSUK_3:8
for X, Y being non empty TopSpace, x being Point of X, f being
Function of [:Y, X | {x}:], Y st f = pr1(the carrier of Y, {x}) holds f is
being_homeomorphism;
theorem :: BORSUK_3:9
for X, Y being non empty TopSpace, x being Point of X, f being
Function of [:X | {x}, Y:], Y st f = pr2({x}, the carrier of Y) holds f is
being_homeomorphism;
begin :: On the product of compact spaces
theorem :: BORSUK_3:10
for X being non empty TopSpace, Y being compact non empty TopSpace, G
being open Subset of [:X, Y:], x being set st [:{x}, the carrier of Y:] c= G ex
f being ManySortedSet of the carrier of Y st
for i being object 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:11
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 [:[#]Y, {x}
:] 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:12
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:13
for X, Y being non empty TopSpace, x being Point of X holds [: X
| {x}, Y :], Y are_homeomorphic;
theorem :: BORSUK_3:14
for S, T being non empty TopSpace st S, T are_homeomorphic & S
is compact holds T is compact;
theorem :: BORSUK_3:15
for X, Y being TopSpace, XV being SubSpace of X holds [:Y, XV:]
is SubSpace of [:Y, X:];
theorem :: BORSUK_3:16
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;
registration
let X be non empty TopSpace, Y be compact non empty TopSpace,
x be Point of X;
cluster [:Y, X|{x}:] -> compact;
end;
theorem :: BORSUK_3:17
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 Cover of [#]X;
theorem :: BORSUK_3:18
for X, Y being compact non empty TopSpace, R being Subset-Family
of X, F being Subset-Family of [:Y, X:] st F is 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 Cover
of X;
theorem :: BORSUK_3:19
for X, Y being compact non empty TopSpace, R being Subset-Family
of X, F being Subset-Family of [:Y, X:] st F is 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 Cover of X;
theorem :: BORSUK_3:20
for X, Y being compact non empty TopSpace, F being Subset-Family
of [:Y, X:] st F is Cover of [:Y, X:] & F is open ex G being Subset-Family of
[:Y, X:] st G c= F & G is Cover of [:Y, X:] & G is finite;
registration
let T1,T2 be compact TopSpace;
cluster [:T1, T2:] -> compact;
end;
theorem :: BORSUK_3:21
for X, Y being TopSpace, XV being SubSpace of X, YV being
SubSpace of Y holds [:XV, YV:] is SubSpace of [:X, Y:];
theorem :: BORSUK_3:22
for X, Y being TopSpace, Z being Subset of [:Y, X:], V being
Subset of X, W being Subset of Y st Z = [:W, V:] holds the TopStruct of [:Y | W
, X | V:] = the TopStruct of [:Y, X:] | Z;
registration
let T be TopSpace;
cluster empty for Subset of T;
end;
registration
let T be TopSpace, P be compact Subset of T;
cluster T | P -> compact;
end;
theorem :: BORSUK_3:23
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:];