:: Properties of the Product of Compact Topological Spaces
:: by Adam Grabowski
::
:: Received February 13, 1999
:: Copyright (c) 1999 Association of Mizar Users
theorem :: BORSUK_3:1
theorem Th2: :: BORSUK_3:2
Lm1:
for S being TopStruct holds S,S are_homeomorphic
Lm2:
for S, T being non empty TopStruct st S,T are_homeomorphic holds
T,S are_homeomorphic
theorem :: BORSUK_3:3
theorem :: BORSUK_3:4
canceled;
theorem :: BORSUK_3:5
canceled;
theorem Th6: :: BORSUK_3:6
theorem Th7: :: BORSUK_3:7
theorem Th8: :: BORSUK_3:8
theorem Th9: :: BORSUK_3:9
theorem :: BORSUK_3:10
theorem Th11: :: BORSUK_3:11
theorem :: BORSUK_3:12
theorem Th13: :: BORSUK_3:13
theorem Th14: :: BORSUK_3:14
theorem Th15: :: BORSUK_3:15
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
theorem Th16: :: BORSUK_3:16
theorem Th17: :: BORSUK_3:17
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) #)
theorem Th18: :: BORSUK_3:18
theorem :: BORSUK_3:19
theorem :: BORSUK_3:20
theorem Th21: :: BORSUK_3:21
theorem Th22: :: BORSUK_3:22
theorem Th23: :: BORSUK_3:23
Lm5:
for T1, T2 being non empty compact TopSpace holds [:T1,T2:] is compact
Lm6:
for X, Y being TopSpace
for XV being SubSpace of X holds [:XV,Y:] is SubSpace of [:X,Y:]
theorem :: BORSUK_3:24
canceled;
theorem Th25: :: BORSUK_3:25
theorem Th26: :: BORSUK_3:26
theorem :: BORSUK_3:27