begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th5:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th9:
theorem Th10:
theorem
canceled;
theorem Th12:
theorem Th13:
theorem Th14:
theorem
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem
canceled;
theorem Th23:
theorem Th24:
begin
theorem Th25:
theorem Th26:
theorem Th27:
theorem
:: deftheorem Def1 defines proj BORSUK_1:def 1 :
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
begin
theorem
canceled;
theorem Th35:
:: deftheorem BORSUK_1:def 2 :
canceled;
:: deftheorem defines continuous BORSUK_1:def 3 :
theorem
canceled;
theorem Th37:
theorem Th38:
theorem Th39:
theorem
canceled;
theorem
begin
definition
let X,
Y be
TopSpace;
canceled;func [:X,Y:] -> strict TopSpace means :
Def5:
( the
carrier of
it = [:the carrier of X,the carrier of Y:] & the
topology of
it = { (union A) where A is Subset-Family of it : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } );
existence
ex b1 being strict TopSpace st
( the carrier of b1 = [:the carrier of X,the carrier of Y:] & the topology of b1 = { (union A) where A is Subset-Family of b1 : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } )
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = [:the carrier of X,the carrier of Y:] & the topology of b1 = { (union A) where A is Subset-Family of b1 : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } & the carrier of b2 = [:the carrier of X,the carrier of Y:] & the topology of b2 = { (union A) where A is Subset-Family of b2 : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } holds
b1 = b2
;
end;
:: deftheorem BORSUK_1:def 4 :
canceled;
:: deftheorem Def5 defines [: BORSUK_1:def 5 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
definition
let X,
Y be
TopSpace;
let A be
Subset of
[:X,Y:];
func Base-Appr A -> Subset-Family of
[:X,Y:] equals
{ [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } ;
coherence
{ [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } is Subset-Family of [:X,Y:]
end;
:: deftheorem defines Base-Appr BORSUK_1:def 6 :
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
definition
let X,
Y be non
empty TopSpace;
func Pr1 X,
Y -> Function of
(bool the carrier of [:X,Y:]),
(bool the carrier of X) equals
.: (pr1 the carrier of X,the carrier of Y);
coherence
.: (pr1 the carrier of X,the carrier of Y) is Function of (bool the carrier of [:X,Y:]),(bool the carrier of X)
correctness
;
func Pr2 X,
Y -> Function of
(bool the carrier of [:X,Y:]),
(bool the carrier of Y) equals
.: (pr2 the carrier of X,the carrier of Y);
coherence
.: (pr2 the carrier of X,the carrier of Y) is Function of (bool the carrier of [:X,Y:]),(bool the carrier of Y)
correctness
;
end;
:: deftheorem defines Pr1 BORSUK_1:def 7 :
:: deftheorem defines Pr2 BORSUK_1:def 8 :
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem
theorem
canceled;
theorem Th67:
begin
:: deftheorem defines TrivDecomp BORSUK_1:def 9 :
theorem Th68:
Lm1:
for X being non empty TopSpace
for A being Subset of X
for V being a_neighborhood of A ex W being Subset of X st
( W is open & A c= W & W c= V & ( for B being Subset of X st B in TrivDecomp X & B meets W holds
B c= W ) )
:: deftheorem Def10 defines space BORSUK_1:def 10 :
theorem Th69:
:: deftheorem defines Proj BORSUK_1:def 11 :
theorem
theorem Th71:
theorem Th72:
:: deftheorem defines TrivExt BORSUK_1:def 12 :
theorem
canceled;
theorem Th74:
theorem Th75:
theorem Th76:
theorem Th77:
theorem Th78:
theorem Th79:
theorem Th80:
begin
:: deftheorem Def13 defines u.s.c._decomposition BORSUK_1:def 13 :
theorem Th81:
theorem Th82:
:: deftheorem Def14 defines closed BORSUK_1:def 14 :
Lm2:
for T being TopStruct holds TopStruct(# the carrier of T,the topology of T #) is SubSpace of T
:: deftheorem Def15 defines DECOMPOSITION-like BORSUK_1:def 15 :
begin
Lm3:
TopSpaceMetr RealSpace = TopStruct(# the carrier of RealSpace ,(Family_open_set RealSpace ) #)
by PCOMPS_1:def 6;
:: deftheorem Def16 defines I[01] BORSUK_1:def 16 :
theorem Th83:
:: deftheorem defines 0[01] BORSUK_1:def 17 :
:: deftheorem defines 1[01] BORSUK_1:def 18 :
:: deftheorem Def19 defines being_a_retraction BORSUK_1:def 19 :
:: deftheorem defines is_a_retract_of BORSUK_1:def 20 :
:: deftheorem defines is_an_SDR_of BORSUK_1:def 21 :
theorem
theorem
theorem