:: Properties of the Product of Compact Topological Spaces :: by Adam Grabowski :: :: Received February 13, 1999 :: Copyright (c) 1999-2012 Association of Mizar Users begin theorem :: BORSUK_3:1 for S, T being TopSpace holds [#] [:S,T:] = [:([#] S),([#] T):] by BORSUK_1:def_2; theorem Th2: :: BORSUK_3:2 for X, Y being non empty TopSpace for x being Point of X holds Y --> x is continuous Function of Y,(X | {x}) proofend; registration let T be TopStruct ; cluster id T -> being_homeomorphism ; coherence id T is being_homeomorphism by TOPGRP_1:20; end; Lm1: for S being TopStruct holds S,S are_homeomorphic proofend; Lm2: for S, T being non empty TopStruct st S,T are_homeomorphic holds T,S are_homeomorphic proofend; definition let S, T be TopStruct ; :: original:are_homeomorphic redefine predS,T are_homeomorphic ; reflexivity for S being TopStruct holds R36(b1,b1) by Lm1; end; definition let S, T be non empty TopStruct ; :: original:are_homeomorphic redefine predS,T are_homeomorphic ; reflexivity for S being non empty TopStruct holds R36(b1,b1) by Lm1; symmetry for S, T being non empty TopStruct st R36(b1,b2) holds R36(b2,b1) by Lm2; 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 proofend; begin registration let T be TopStruct ; let P be empty Subset of T; clusterT | P -> empty ; coherence T | P is empty ; end; registration cluster empty TopSpace-like -> compact for TopStruct ; coherence for b1 being TopSpace st b1 is empty holds b1 is compact ; end; theorem Th4: :: BORSUK_3:4 for X, Y being non empty TopSpace for x being Point of X for f being Function of [:Y,(X | {x}):],Y st f = pr1 ( the carrier of Y,{x}) holds f is one-to-one proofend; theorem Th5: :: BORSUK_3:5 for X, Y being non empty TopSpace for x being Point of X for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds f is one-to-one proofend; theorem Th6: :: BORSUK_3:6 for X, Y being non empty TopSpace for x being Point of X for f being Function of [:Y,(X | {x}):],Y st f = pr1 ( the carrier of Y,{x}) holds f " = <:(id Y),(Y --> x):> proofend; theorem Th7: :: BORSUK_3:7 for X, Y being non empty TopSpace for x being Point of X for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds f " = <:(Y --> x),(id Y):> proofend; theorem :: BORSUK_3:8 for X, Y being non empty TopSpace for x being Point of X for f being Function of [:Y,(X | {x}):],Y st f = pr1 ( the carrier of Y,{x}) holds f is being_homeomorphism proofend; theorem Th9: :: BORSUK_3:9 for X, Y being non empty TopSpace for x being Point of X for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds f is being_homeomorphism proofend; begin theorem :: BORSUK_3:10 for X being non empty TopSpace for Y being non empty compact TopSpace for G being open Subset of [:X,Y:] for x being set st [:{x}, the carrier of Y:] c= G holds ex f being ManySortedSet of the carrier of Y st for i being set st i in the carrier of Y holds ex G1 being Subset of X ex 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 ) proofend; theorem Th11: :: BORSUK_3:11 for X being non empty TopSpace for Y being non empty compact TopSpace for G being open Subset of [:Y,X:] for x being set st [:([#] Y),{x}:] c= G holds ex R being open Subset of X st ( x in R & R c= { y where y is Point of X : [:([#] Y),{y}:] c= G } ) proofend; theorem Th12: :: BORSUK_3:12 for X being non empty TopSpace for Y being non empty compact TopSpace for G being open Subset of [:Y,X:] holds { x where x is Point of X : [:([#] Y),{x}:] c= G } in the topology of X proofend; theorem Th13: :: BORSUK_3:13 for X, Y being non empty TopSpace for x being Point of X holds [:(X | {x}),Y:],Y are_homeomorphic proofend; Lm3: for X, Y being non empty TopSpace for x being Point of X for Z being non empty Subset of X st Z = {x} holds [:Y,(X | Z):],Y are_homeomorphic proofend; theorem Th14: :: BORSUK_3:14 for S, T being non empty TopSpace st S,T are_homeomorphic & S is compact holds T is compact proofend; theorem Th15: :: BORSUK_3:15 for X, Y being TopSpace for XV being SubSpace of X holds [:Y,XV:] is SubSpace of [:Y,X:] proofend; Lm4: for X, Y being TopSpace for Z being Subset of [:Y,X:] for V being Subset of X st Z = [:([#] Y),V:] holds TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) proofend; theorem Th16: :: BORSUK_3:16 for X being non empty TopSpace for Y being non empty compact TopSpace for x being Point of X for Z being Subset of [:Y,X:] st Z = [:([#] Y),{x}:] holds Z is compact proofend; registration let X be non empty TopSpace; let Y be non empty compact TopSpace; let x be Point of X; cluster[:Y,(X | {x}):] -> compact ; coherence [:Y,(X | {x}):] is compact proofend; end; theorem :: BORSUK_3:17 for X, Y being non empty compact TopSpace for 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 ) proofend; theorem Th18: :: BORSUK_3:18 for X, Y being non empty compact TopSpace for R being Subset-Family of X for 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 ) proofend; theorem Th19: :: BORSUK_3:19 for X, Y being non empty compact TopSpace for R being Subset-Family of X for 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 ) proofend; theorem Th20: :: BORSUK_3:20 for X, Y being non empty compact TopSpace for F being Subset-Family of [:Y,X:] st F is Cover of [:Y,X:] & F is open holds ex G being Subset-Family of [:Y,X:] st ( G c= F & G is Cover of [:Y,X:] & G is finite ) proofend; Lm5: for T1, T2 being non empty compact TopSpace holds [:T1,T2:] is compact proofend; registration let T1, T2 be compact TopSpace; cluster[:T1,T2:] -> compact ; coherence [:T1,T2:] is compact proofend; end; Lm6: for X, Y being TopSpace for XV being SubSpace of X holds [:XV,Y:] is SubSpace of [:X,Y:] proofend; theorem Th21: :: BORSUK_3:21 for X, Y being TopSpace for XV being SubSpace of X for YV being SubSpace of Y holds [:XV,YV:] is SubSpace of [:X,Y:] proofend; theorem Th22: :: BORSUK_3:22 for X, Y being TopSpace for Z being Subset of [:Y,X:] for V being Subset of X for W being Subset of Y st Z = [:W,V:] holds TopStruct(# the carrier of [:(Y | W),(X | V):], the topology of [:(Y | W),(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) proofend; registration let T be TopSpace; cluster empty for Element of bool the carrier of T; existence ex b1 being Subset of T st b1 is empty proofend; end; registration let T be TopSpace; let P be compact Subset of T; clusterT | P -> compact ; coherence T | P is compact proofend; end; theorem :: BORSUK_3:23 for T1, T2 being TopSpace for S1 being Subset of T1 for S2 being Subset of T2 st S1 is compact & S2 is compact holds [:S1,S2:] is compact Subset of [:T1,T2:] proofend;