:: BORSUK_3 semantic presentation

theorem Th1: :: BORSUK_3:1

for S, T being TopSpace holds [#] [:S,T:] = [:([#] S),([#] T):]

proof end;

registration

let X be set ;
let Y be empty set ;
cluster [:X,Y:] -> empty ;
coherence by ZFMISC_1:113;

end;

registration

let X be empty set ;
let Y be set ;
cluster [:X,Y:] -> empty ;
coherence by ZFMISC_1:113;

end;

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})

proof end;

registration

let T be non empty TopStruct ;
cluster id T -> being_homeomorphism ;
coherence by TOPGRP_1:20;

end;

Lm1: for S being non empty TopStruct holds S,S are_homeomorphic

proof end;

Lm2: for S, T being non empty TopStruct st S,T are_homeomorphic holds
T,S are_homeomorphic

proof end;

definition

let S, T be non empty TopStruct ;
:: original: are_homeomorphic
redefine pred S,T are_homeomorphic ;
reflexivity by Lm1;
symmetry 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

proof end;

registration

let T be TopStruct ;
let P be empty Subset of T;
cluster T | P -> empty ;
coherence

proof end;

end;

registration

cluster empty strict TopStruct ;
existence

proof end;

end;

theorem Th4: :: BORSUK_3:4

for T1 being TopSpace
for T2 being empty TopSpace holds
( [:T1,T2:] is empty & [:T2,T1:] is empty )

proof end;

theorem Th5: :: BORSUK_3:5

for T being empty TopSpace holds T is compact

proof end;

registration

cluster empty -> compact TopStruct ;
coherence by Th5;

end;

registration

let T1 be TopSpace;
let T2 be empty TopSpace;
cluster [:T1,T2:] -> empty compact ;
coherence by Th4;

end;

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 is one-to-one

proof end;

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 is one-to-one

proof end;

theorem Th8: :: 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 " = <:(id Y),(Y --> x):>

proof end;

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 " = <:(Y --> x),(id Y):>

proof end;

theorem :: BORSUK_3:10

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_homeomorphism

proof end;

theorem Th11: :: BORSUK_3:11

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_homeomorphism

proof end;

theorem :: BORSUK_3:12

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 in { x' where x' is Point of X : [:{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 )

proof end;

theorem Th13: :: BORSUK_3:13

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 x in { y where y is Point of X : [:([#] Y),{y}:] 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 } )

proof end;

theorem Th14: :: BORSUK_3:14

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

proof end;

theorem Th15: :: BORSUK_3:15

for X, Y being non empty TopSpace
for x being Point of X holds [:(X | {x}),Y:],Y are_homeomorphic

proof end;

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

proof end;

theorem Th16: :: BORSUK_3:16

for S, T being non empty TopSpace st S,T are_homeomorphic & S is compact holds
T is compact

proof end;

theorem Th17: :: BORSUK_3:17

for X, Y being TopSpace
for XV being SubSpace of X holds [:Y,XV:] is SubSpace of [:Y,X:]

proof end;

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) #)

proof end;

theorem Th18: :: BORSUK_3:18

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

proof end;

theorem :: BORSUK_3:19

for X being non empty TopSpace
for Y being non empty compact TopSpace
for x being Point of X holds [:Y,(X | {x}):] is compact

proof end;

theorem :: BORSUK_3:20

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_a_cover_of [#] X )

proof end;

theorem Th21: :: BORSUK_3:21

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_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 )

proof end;

theorem Th22: :: BORSUK_3:22

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_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 )

proof end;

theorem Th23: :: BORSUK_3:23

for X, Y being non empty compact TopSpace
for F being Subset-Family of [:Y,X:] st F is_a_cover_of [:Y,X:] & F is open holds
ex G being Subset-Family of [:Y,X:] st
( G c= F & G is_a_cover_of [:Y,X:] & G is finite )

proof end;

Lm5: for T1, T2 being non empty compact TopSpace holds [:T1,T2:] is compact

proof end;

theorem Th24: :: BORSUK_3:24

for T1, T2 being TopSpace st T1 is compact & T2 is compact holds
[:T1,T2:] is compact

proof end;

registration

let T1, T2 be compact TopSpace;
cluster [:T1,T2:] -> compact ;
coherence by Th24;

end;

Lm6: for X, Y being TopSpace
for XV being SubSpace of X holds [:XV,Y:] is SubSpace of [:X,Y:]

proof end;

theorem Th25: :: BORSUK_3:25

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:]

proof end;

theorem Th26: :: BORSUK_3:26

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) #)

proof end;

registration

let T be TopStruct ;
cluster compact Element of bool the carrier of T;
existence

proof end;

end;

registration

let T be TopSpace;
let P be compact Subset of T;
cluster T | P -> compact ;
coherence

proof end;

end;

theorem :: BORSUK_3:27

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:]

proof end;