:: BORSUK_1 semantic presentation
begin
theorem Th1: :: BORSUK_1:1
for X being TopStruct
for Y being SubSpace of X holds the carrier of Y c= the carrier of X
proof
let X be TopStruct ; ::_thesis: for Y being SubSpace of X holds the carrier of Y c= the carrier of X
let Y be SubSpace of X; ::_thesis: the carrier of Y c= the carrier of X
( the carrier of Y = [#] Y & the carrier of X = [#] X ) ;
hence the carrier of Y c= the carrier of X by PRE_TOPC:def_4; ::_thesis: verum
end;
definition
let X, Y be non empty TopSpace;
let F be Function of X,Y;
redefine attr F is continuous means :: BORSUK_1:def 1
for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G;
compatibility
( F is continuous iff for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G )
proof
A1: [#] Y <> {} ;
thus ( F is continuous implies for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G ) ::_thesis: ( ( for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G ) implies F is continuous )
proof
assume A2: F is continuous ; ::_thesis: for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G
let W be Point of X; ::_thesis: for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G
let G be a_neighborhood of F . W; ::_thesis: ex H being a_neighborhood of W st F .: H c= G
F . W in Int G by CONNSP_2:def_1;
then A3: W in F " (Int G) by FUNCT_2:38;
F " (Int G) is open by A1, A2, TOPS_2:43;
then W in Int (F " (Int G)) by A3, TOPS_1:23;
then reconsider H = F " (Int G) as a_neighborhood of W by CONNSP_2:def_1;
take H ; ::_thesis: F .: H c= G
H c= F " G by RELAT_1:143, TOPS_1:16;
hence F .: H c= G by EQREL_1:46; ::_thesis: verum
end;
assume A4: for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G ; ::_thesis: F is continuous
now__::_thesis:_for_P1_being_Subset_of_Y_st_P1_is_open_holds_
F_"_P1_is_open
let P1 be Subset of Y; ::_thesis: ( P1 is open implies F " P1 is open )
assume A5: P1 is open ; ::_thesis: F " P1 is open
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_F_"_P1_implies_ex_P_being_Subset_of_X_st_
(_P_is_open_&_P_c=_F_"_P1_&_x_in_P_)_)_&_(_ex_P_being_Subset_of_X_st_
(_P_is_open_&_P_c=_F_"_P1_&_x_in_P_)_implies_x_in_F_"_P1_)_)
let x be set ; ::_thesis: ( ( x in F " P1 implies ex P being Subset of X st
( P is open & P c= F " P1 & x in P ) ) & ( ex P being Subset of X st
( P is open & P c= F " P1 & x in P ) implies x in F " P1 ) )
thus ( x in F " P1 implies ex P being Subset of X st
( P is open & P c= F " P1 & x in P ) ) ::_thesis: ( ex P being Subset of X st
( P is open & P c= F " P1 & x in P ) implies x in F " P1 )
proof
assume A6: x in F " P1 ; ::_thesis: ex P being Subset of X st
( P is open & P c= F " P1 & x in P )
then reconsider W = x as Point of X ;
A7: Int P1 = P1 by A5, TOPS_1:23;
F . W in P1 by A6, FUNCT_2:38;
then P1 is a_neighborhood of F . W by A7, CONNSP_2:def_1;
then consider H being a_neighborhood of W such that
A8: F .: H c= P1 by A4;
take Int H ; ::_thesis: ( Int H is open & Int H c= F " P1 & x in Int H )
thus Int H is open ; ::_thesis: ( Int H c= F " P1 & x in Int H )
A9: Int H c= H by TOPS_1:16;
dom F = the carrier of X by FUNCT_2:def_1;
then A10: H c= F " (F .: H) by FUNCT_1:76;
F " (F .: H) c= F " P1 by A8, RELAT_1:143;
then H c= F " P1 by A10, XBOOLE_1:1;
hence Int H c= F " P1 by A9, XBOOLE_1:1; ::_thesis: x in Int H
thus x in Int H by CONNSP_2:def_1; ::_thesis: verum
end;
thus ( ex P being Subset of X st
( P is open & P c= F " P1 & x in P ) implies x in F " P1 ) ; ::_thesis: verum
end;
hence F " P1 is open by TOPS_1:25; ::_thesis: verum
end;
hence F is continuous by A1, TOPS_2:43; ::_thesis: verum
end;
end;
:: deftheorem defines continuous BORSUK_1:def_1_:_
for X, Y being non empty TopSpace
for F being Function of X,Y holds
( F is continuous iff for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G );
registration
let X, Y, Z be non empty TopSpace;
let F be continuous Function of X,Y;
let G be continuous Function of Y,Z;
clusterF * G -> continuous for Function of X,Z;
coherence
for b1 being Function of X,Z st b1 = G * F holds
b1 is continuous by TOPS_2:46;
end;
theorem Th2: :: BORSUK_1:2
for X, Y being non empty TopSpace
for A being continuous Function of X,Y
for G being Subset of Y holds A " (Int G) c= Int (A " G)
proof
let X, Y be non empty TopSpace; ::_thesis: for A being continuous Function of X,Y
for G being Subset of Y holds A " (Int G) c= Int (A " G)
let A be continuous Function of X,Y; ::_thesis: for G being Subset of Y holds A " (Int G) c= Int (A " G)
let G be Subset of Y; ::_thesis: A " (Int G) c= Int (A " G)
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A " (Int G) or e in Int (A " G) )
A1: A " (Int G) c= A " G by RELAT_1:143, TOPS_1:16;
[#] Y <> {} ;
then A2: A " (Int G) is open by TOPS_2:43;
assume e in A " (Int G) ; ::_thesis: e in Int (A " G)
hence e in Int (A " G) by A2, A1, TOPS_1:22; ::_thesis: verum
end;
theorem Th3: :: BORSUK_1:3
for Y, X being non empty TopSpace
for W being Point of Y
for A being continuous Function of X,Y
for G being a_neighborhood of W holds A " G is a_neighborhood of A " {W}
proof
let Y, X be non empty TopSpace; ::_thesis: for W being Point of Y
for A being continuous Function of X,Y
for G being a_neighborhood of W holds A " G is a_neighborhood of A " {W}
let W be Point of Y; ::_thesis: for A being continuous Function of X,Y
for G being a_neighborhood of W holds A " G is a_neighborhood of A " {W}
let A be continuous Function of X,Y; ::_thesis: for G being a_neighborhood of W holds A " G is a_neighborhood of A " {W}
let G be a_neighborhood of W; ::_thesis: A " G is a_neighborhood of A " {W}
W in Int G by CONNSP_2:def_1;
then {W} c= Int G by ZFMISC_1:31;
then A1: A " {W} c= A " (Int G) by RELAT_1:143;
A " (Int G) c= Int (A " G) by Th2;
hence A " {W} c= Int (A " G) by A1, XBOOLE_1:1; :: according to CONNSP_2:def_2 ::_thesis: verum
end;
definition
let X, Y be non empty TopSpace;
let W be Point of Y;
let A be continuous Function of X,Y;
let G be a_neighborhood of W;
:: original: "
redefine funcA " G -> a_neighborhood of A " {W};
correctness
coherence
A " G is a_neighborhood of A " {W};
by Th3;
end;
theorem Th4: :: BORSUK_1:4
for X being non empty TopSpace
for A, B being Subset of X
for U being a_neighborhood of B st A c= B holds
U is a_neighborhood of A
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X
for U being a_neighborhood of B st A c= B holds
U is a_neighborhood of A
let A, B be Subset of X; ::_thesis: for U being a_neighborhood of B st A c= B holds
U is a_neighborhood of A
let U be a_neighborhood of B; ::_thesis: ( A c= B implies U is a_neighborhood of A )
assume A1: A c= B ; ::_thesis: U is a_neighborhood of A
B c= Int U by CONNSP_2:def_2;
hence A c= Int U by A1, XBOOLE_1:1; :: according to CONNSP_2:def_2 ::_thesis: verum
end;
registration
let X be non empty TopSpace;
let x be Point of X;
cluster{x} -> compact for Subset of X;
coherence
for b1 being Subset of X st b1 = {x} holds
b1 is compact
proof
reconsider B = {x} as Subset of X ;
now__::_thesis:_for_F_being_Subset-Family_of_X_st_F_is_Cover_of_B_&_F_is_open_holds_
ex_G_being_Subset-Family_of_X_st_
(_G_c=_F_&_G_is_Cover_of_B_&_G_is_finite_)
let F be Subset-Family of X; ::_thesis: ( F is Cover of B & F is open implies ex G being Subset-Family of X st
( G c= F & G is Cover of B & G is finite ) )
assume that
A1: F is Cover of B and
F is open ; ::_thesis: ex G being Subset-Family of X st
( G c= F & G is Cover of B & G is finite )
B c= union F by A1, SETFAM_1:def_11;
then x in union F by ZFMISC_1:31;
then consider A being set such that
A2: x in A and
A3: A in F by TARSKI:def_4;
reconsider G = {A} as Subset-Family of X by A3, ZFMISC_1:31;
take G = G; ::_thesis: ( G c= F & G is Cover of B & G is finite )
thus G c= F by A3, ZFMISC_1:31; ::_thesis: ( G is Cover of B & G is finite )
A in G by TARSKI:def_1;
then x in union G by A2, TARSKI:def_4;
then B c= union G by ZFMISC_1:31;
hence G is Cover of B by SETFAM_1:def_11; ::_thesis: G is finite
thus G is finite ; ::_thesis: verum
end;
hence for b1 being Subset of X st b1 = {x} holds
b1 is compact by COMPTS_1:def_4; ::_thesis: verum
end;
end;
begin
definition
let X, Y be TopSpace;
func[:X,Y:] -> strict TopSpace means :Def2: :: BORSUK_1:def 2
( 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 ) } } )
proof
set t = { (union A) where A is Subset-Family of [: the carrier of X, the carrier of Y:] : 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 ) } } ;
{ (union A) where A is Subset-Family of [: the carrier of X, the carrier of Y:] : 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 ) } } c= bool [: the carrier of X, the carrier of Y:]
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (union A) where A is Subset-Family of [: the carrier of X, the carrier of Y:] : 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 ) } } or e in bool [: the carrier of X, the carrier of Y:] )
assume e in { (union A) where A is Subset-Family of [: the carrier of X, the carrier of Y:] : 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 ) } } ; ::_thesis: e in bool [: the carrier of X, the carrier of Y:]
then ex A being Subset-Family of [: the carrier of X, the carrier of Y:] st
( e = union A & 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 ) } ) ;
hence e in bool [: the carrier of X, the carrier of Y:] ; ::_thesis: verum
end;
then reconsider t = { (union A) where A is Subset-Family of [: the carrier of X, the carrier of Y:] : 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 ) } } as Subset-Family of [: the carrier of X, the carrier of Y:] ;
set T = TopStruct(# [: the carrier of X, the carrier of Y:],t #);
now__::_thesis:_(_the_carrier_of_TopStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],t_#)_in_the_topology_of_TopStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],t_#)_&_(_for_a_being_Subset-Family_of_TopStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],t_#)_st_a_c=_the_topology_of_TopStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],t_#)_holds_
union_a_in_the_topology_of_TopStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],t_#)_)_&_(_for_a,_b_being_Subset_of_TopStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],t_#)_st_a_in_the_topology_of_TopStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],t_#)_&_b_in_the_topology_of_TopStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],t_#)_holds_
a_/\_b_in_the_topology_of_TopStruct(#_[:_the_carrier_of_X,_the_carrier_of_Y:],t_#)_)_)
reconsider A = {[: the carrier of X, the carrier of Y:]} as Subset-Family of [: the carrier of X, the carrier of Y:] by ZFMISC_1:68;
reconsider A = A as Subset-Family of [: the carrier of X, the carrier of Y:] ;
A1: 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 ) }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A or e in { [: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 ) } )
assume e in A ; ::_thesis: e in { [: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 ) }
then A2: e = [: the carrier of X, the carrier of Y:] by TARSKI:def_1;
( the carrier of X in the topology of X & the carrier of Y in the topology of Y ) by PRE_TOPC:def_1;
hence e in { [: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 ) } by A2; ::_thesis: verum
end;
the carrier of TopStruct(# [: the carrier of X, the carrier of Y:],t #) = union A by ZFMISC_1:25;
hence the carrier of TopStruct(# [: the carrier of X, the carrier of Y:],t #) in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) by A1; ::_thesis: ( ( for a being Subset-Family of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a c= the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds
union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) ) & ( for a, b being Subset of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) & b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds
a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) ) )
thus for a being Subset-Family of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a c= the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds
union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) ::_thesis: for a, b being Subset of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) & b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds
a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #)
proof
let a be Subset-Family of TopStruct(# [: the carrier of X, the carrier of Y:],t #); ::_thesis: ( a c= the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) implies union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) )
set A = { [: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 & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) } ;
{ [: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 & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) } c= bool [: the carrier of X, the carrier of Y:]
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { [: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 & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) } or e in bool [: the carrier of X, the carrier of Y:] )
assume e in { [: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 & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) } ; ::_thesis: e in bool [: the carrier of X, the carrier of Y:]
then ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) ;
hence e in bool [: the carrier of X, the carrier of Y:] ; ::_thesis: verum
end;
then reconsider A = { [: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 & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) } as Subset-Family of [: the carrier of X, the carrier of Y:] ;
assume A3: a c= the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) ; ::_thesis: union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #)
A4: union A = union a
proof
thus union A c= union a :: according to XBOOLE_0:def_10 ::_thesis: union a c= union A
proof
let e1, e2 be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [e1,e2] in union A or [e1,e2] in union a )
assume [e1,e2] in union A ; ::_thesis: [e1,e2] in union a
then consider u being set such that
A5: [e1,e2] in u and
A6: u in A by TARSKI:def_4;
ex X1 being Subset of X ex Y1 being Subset of Y st
( u = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) by A6;
hence [e1,e2] in union a by A5, TARSKI:def_4; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in union a or e in union A )
assume e in union a ; ::_thesis: e in union A
then consider u being set such that
A7: e in u and
A8: u in a by TARSKI:def_4;
u in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) by A3, A8;
then consider B being Subset-Family of [: the carrier of X, the carrier of Y:] such that
A9: u = union B and
A10: B 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 ) } ;
consider x being set such that
A11: e in x and
A12: x in B by A7, A9, TARSKI:def_4;
x in { [: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 ) } by A10, A12;
then consider X1 being Subset of X, Y1 being Subset of Y such that
A13: x = [:X1,Y1:] and
A14: ( X1 in the topology of X & Y1 in the topology of Y ) ;
[:X1,Y1:] c= u by A9, A12, A13, ZFMISC_1:74;
then x in A by A8, A13, A14;
hence e in union A by A11, TARSKI:def_4; ::_thesis: verum
end;
A c= { [:X2,Y2:] where X2 is Subset of X, Y2 is Subset of Y : ( X2 in the topology of X & Y2 in the topology of Y ) }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A or e in { [:X2,Y2:] where X2 is Subset of X, Y2 is Subset of Y : ( X2 in the topology of X & Y2 in the topology of Y ) } )
assume e in A ; ::_thesis: e in { [:X2,Y2:] where X2 is Subset of X, Y2 is Subset of Y : ( X2 in the topology of X & Y2 in the topology of Y ) }
then ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) ;
hence e in { [:X2,Y2:] where X2 is Subset of X, Y2 is Subset of Y : ( X2 in the topology of X & Y2 in the topology of Y ) } ; ::_thesis: verum
end;
hence union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) by A4; ::_thesis: verum
end;
let a, b be Subset of TopStruct(# [: the carrier of X, the carrier of Y:],t #); ::_thesis: ( a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) & b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) implies a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) )
set 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 & [:X1,Y1:] c= a /\ b ) } ;
{ [: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 & [:X1,Y1:] c= a /\ b ) } c= bool [: the carrier of X, the carrier of Y:]
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { [: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 & [:X1,Y1:] c= a /\ b ) } or e in bool [: the carrier of X, the carrier of Y:] )
assume e in { [: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 & [:X1,Y1:] c= a /\ b ) } ; ::_thesis: e in bool [: the carrier of X, the carrier of Y:]
then ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b ) ;
hence e in bool [: the carrier of X, the carrier of Y:] ; ::_thesis: verum
end;
then reconsider 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 & [:X1,Y1:] c= a /\ b ) } as Subset-Family of [: the carrier of X, the carrier of Y:] ;
assume that
A15: a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) and
A16: b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) ; ::_thesis: a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #)
consider A being Subset-Family of [: the carrier of X, the carrier of Y:] such that
A17: a = union A and
A18: 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 ) } by A15;
consider B being Subset-Family of [: the carrier of X, the carrier of Y:] such that
A19: b = union B and
A20: B 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 ) } by A16;
A21: a /\ b = union C
proof
thus a /\ b c= union C :: according to XBOOLE_0:def_10 ::_thesis: union C c= a /\ b
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in a /\ b or e in union C )
assume A22: e in a /\ b ; ::_thesis: e in union C
then e in a by XBOOLE_0:def_4;
then consider u1 being set such that
A23: e in u1 and
A24: u1 in A by A17, TARSKI:def_4;
A25: u1 in { [: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 ) } by A18, A24;
e in b by A22, XBOOLE_0:def_4;
then consider u2 being set such that
A26: e in u2 and
A27: u2 in B by A19, TARSKI:def_4;
A28: u2 in { [:X2,Y2:] where X2 is Subset of X, Y2 is Subset of Y : ( X2 in the topology of X & Y2 in the topology of Y ) } by A20, A27;
A29: u2 c= b by A19, A27, ZFMISC_1:74;
consider X1 being Subset of X, Y1 being Subset of Y such that
A30: u1 = [:X1,Y1:] and
A31: ( X1 in the topology of X & Y1 in the topology of Y ) by A25;
consider X2 being Subset of X, Y2 being Subset of Y such that
A32: u2 = [:X2,Y2:] and
A33: ( X2 in the topology of X & Y2 in the topology of Y ) by A28;
u1 c= a by A17, A24, ZFMISC_1:74;
then [:X1,Y1:] /\ [:X2,Y2:] c= a /\ b by A30, A32, A29, XBOOLE_1:27;
then A34: [:(X1 /\ X2),(Y1 /\ Y2):] c= a /\ b by ZFMISC_1:100;
( X1 /\ X2 in the topology of X & Y1 /\ Y2 in the topology of Y ) by A31, A33, PRE_TOPC:def_1;
then A35: [:(X1 /\ X2),(Y1 /\ Y2):] in C by A34;
e in [:(X1 /\ X2),(Y1 /\ Y2):] by A23, A26, A30, A32, ZFMISC_1:113;
hence e in union C by A35, TARSKI:def_4; ::_thesis: verum
end;
let e1, e2 be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [e1,e2] in union C or [e1,e2] in a /\ b )
assume [e1,e2] in union C ; ::_thesis: [e1,e2] in a /\ b
then consider u being set such that
A36: [e1,e2] in u and
A37: u in C by TARSKI:def_4;
ex X1 being Subset of X ex Y1 being Subset of Y st
( u = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b ) by A37;
hence [e1,e2] in a /\ b by A36; ::_thesis: verum
end;
C 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 ) }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in C or e in { [: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 ) } )
assume e in C ; ::_thesis: e in { [: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 ) }
then ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b ) ;
hence e in { [: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 ) } ; ::_thesis: verum
end;
hence a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) by A21; ::_thesis: verum
end;
then reconsider T = TopStruct(# [: the carrier of X, the carrier of Y:],t #) as strict TopSpace by PRE_TOPC:def_1;
take T ; ::_thesis: ( the carrier of T = [: the carrier of X, the carrier of Y:] & the topology of T = { (union A) where A is Subset-Family of T : 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 ) } } )
thus ( the carrier of T = [: the carrier of X, the carrier of Y:] & the topology of T = { (union A) where A is Subset-Family of T : 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 ) } } ) ; ::_thesis: verum
end;
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 Def2 defines [: BORSUK_1:def_2_:_
for X, Y being TopSpace
for b3 being strict TopSpace holds
( b3 = [:X,Y:] iff ( the carrier of b3 = [: the carrier of X, the carrier of Y:] & the topology of b3 = { (union A) where A is Subset-Family of b3 : 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 ) } } ) );
registration
let T1 be TopSpace;
let T2 be empty TopSpace;
cluster[:T1,T2:] -> empty strict ;
coherence
[:T1,T2:] is empty
proof
the carrier of [:T1,T2:] = [: the carrier of T1, the carrier of T2:] by Def2;
hence [:T1,T2:] is empty ; ::_thesis: verum
end;
cluster[:T2,T1:] -> empty strict ;
coherence
[:T2,T1:] is empty
proof
the carrier of [:T2,T1:] = [: the carrier of T2, the carrier of T1:] by Def2;
hence [:T2,T1:] is empty ; ::_thesis: verum
end;
end;
registration
let X, Y be non empty TopSpace;
cluster[:X,Y:] -> non empty strict ;
coherence
not [:X,Y:] is empty
proof
the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
hence not the carrier of [:X,Y:] is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
theorem Th5: :: BORSUK_1:5
for X, Y being TopSpace
for B being Subset of [:X,Y:] holds
( B is open iff ex A being Subset-Family of [:X,Y:] st
( B = union A & ( for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) )
proof
let X, Y be TopSpace; ::_thesis: for B being Subset of [:X,Y:] holds
( B is open iff ex A being Subset-Family of [:X,Y:] st
( B = union A & ( for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) )
let B be Subset of [:X,Y:]; ::_thesis: ( B is open iff ex A being Subset-Family of [:X,Y:] st
( B = union A & ( for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) )
A1: the topology of [:X,Y:] = { (union A) where A is Subset-Family of [:X,Y:] : 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 ) } } by Def2;
thus ( B is open implies ex A being Subset-Family of [:X,Y:] st
( B = union A & ( for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) ) ::_thesis: ( ex A being Subset-Family of [:X,Y:] st
( B = union A & ( for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) implies B is open )
proof
assume B in the topology of [:X,Y:] ; :: according to PRE_TOPC:def_2 ::_thesis: ex A being Subset-Family of [:X,Y:] st
( B = union A & ( for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) )
then consider A being Subset-Family of [:X,Y:] such that
A2: B = union A and
A3: 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 ) } by A1;
take A ; ::_thesis: ( B = union A & ( for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) )
thus B = union A by A2; ::_thesis: for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
let e be set ; ::_thesis: ( e in A implies ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) )
assume e in A ; ::_thesis: ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
then e in { [: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 ) } by A3;
then consider X1 being Subset of X, Y1 being Subset of Y such that
A4: ( e = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y ) ;
reconsider Y1 = Y1 as Subset of Y ;
reconsider X1 = X1 as Subset of X ;
take X1 ; ::_thesis: ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
take Y1 ; ::_thesis: ( e = [:X1,Y1:] & X1 is open & Y1 is open )
thus ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A4, PRE_TOPC:def_2; ::_thesis: verum
end;
given A being Subset-Family of [:X,Y:] such that A5: B = union A and
A6: for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ; ::_thesis: B is open
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 ) }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A or e in { [: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 ) } )
assume e in A ; ::_thesis: e in { [: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 ) }
then consider X1 being Subset of X, Y1 being Subset of Y such that
A7: e = [:X1,Y1:] and
A8: ( X1 is open & Y1 is open ) by A6;
( X1 in the topology of X & Y1 in the topology of Y ) by A8, PRE_TOPC:def_2;
hence e in { [: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 ) } by A7; ::_thesis: verum
end;
hence B in the topology of [:X,Y:] by A1, A5; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;
definition
let X, Y be TopSpace;
let A be Subset of X;
let B be Subset of Y;
:: original: [:
redefine func[:A,B:] -> Subset of [:X,Y:];
correctness
coherence
[:A,B:] is Subset of [:X,Y:];
proof
thus [:A,B:] is Subset of [:X,Y:] by Def2; ::_thesis: verum
end;
end;
definition
let X, Y be non empty TopSpace;
let x be Point of X;
let y be Point of Y;
:: original: [
redefine func[x,y] -> Point of [:X,Y:];
correctness
coherence
[x,y] is Point of [:X,Y:];
proof
thus [x,y] is Point of [:X,Y:] by Def2; ::_thesis: verum
end;
end;
theorem Th6: :: BORSUK_1:6
for X, Y being TopSpace
for V being Subset of X
for W being Subset of Y st V is open & W is open holds
[:V,W:] is open
proof
let X, Y be TopSpace; ::_thesis: for V being Subset of X
for W being Subset of Y st V is open & W is open holds
[:V,W:] is open
let V be Subset of X; ::_thesis: for W being Subset of Y st V is open & W is open holds
[:V,W:] is open
let W be Subset of Y; ::_thesis: ( V is open & W is open implies [:V,W:] is open )
assume A1: ( V is open & W is open ) ; ::_thesis: [:V,W:] is open
reconsider PP = {[:V,W:]} as Subset-Family of [:X,Y:] ;
reconsider PP = PP as Subset-Family of [:X,Y:] ;
A2: now__::_thesis:_for_e_being_set_st_e_in_PP_holds_
ex_V_being_Subset_of_X_ex_W_being_Subset_of_Y_st_
(_e_=_[:V,W:]_&_V_is_open_&_W_is_open_)
let e be set ; ::_thesis: ( e in PP implies ex V being Subset of X ex W being Subset of Y st
( e = [:V,W:] & V is open & W is open ) )
assume A3: e in PP ; ::_thesis: ex V being Subset of X ex W being Subset of Y st
( e = [:V,W:] & V is open & W is open )
take V = V; ::_thesis: ex W being Subset of Y st
( e = [:V,W:] & V is open & W is open )
take W = W; ::_thesis: ( e = [:V,W:] & V is open & W is open )
thus ( e = [:V,W:] & V is open & W is open ) by A1, A3, TARSKI:def_1; ::_thesis: verum
end;
[:V,W:] = union {[:V,W:]} by ZFMISC_1:25;
hence [:V,W:] is open by A2, Th5; ::_thesis: verum
end;
theorem Th7: :: BORSUK_1:7
for X, Y being TopSpace
for V being Subset of X
for W being Subset of Y holds Int [:V,W:] = [:(Int V),(Int W):]
proof
let X, Y be TopSpace; ::_thesis: for V being Subset of X
for W being Subset of Y holds Int [:V,W:] = [:(Int V),(Int W):]
let V be Subset of X; ::_thesis: for W being Subset of Y holds Int [:V,W:] = [:(Int V),(Int W):]
let W be Subset of Y; ::_thesis: Int [:V,W:] = [:(Int V),(Int W):]
thus Int [:V,W:] c= [:(Int V),(Int W):] :: according to XBOOLE_0:def_10 ::_thesis: [:(Int V),(Int W):] c= Int [:V,W:]
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in Int [:V,W:] or e in [:(Int V),(Int W):] )
assume e in Int [:V,W:] ; ::_thesis: e in [:(Int V),(Int W):]
then consider Q being Subset of [:X,Y:] such that
A1: Q is open and
A2: Q c= [:V,W:] and
A3: e in Q by TOPS_1:22;
consider A being Subset-Family of [:X,Y:] such that
A4: Q = union A and
A5: for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A1, Th5;
consider a being set such that
A6: e in a and
A7: a in A by A3, A4, TARSKI:def_4;
consider X1 being Subset of X, Y1 being Subset of Y such that
A8: a = [:X1,Y1:] and
A9: X1 is open and
A10: Y1 is open by A5, A7;
[:X1,Y1:] c= Q by A4, A7, A8, ZFMISC_1:74;
then A11: [:X1,Y1:] c= [:V,W:] by A2, XBOOLE_1:1;
then Y1 c= W by A6, A8, ZFMISC_1:114;
then A12: Y1 c= Int W by A10, TOPS_1:24;
X1 c= V by A6, A8, A11, ZFMISC_1:114;
then X1 c= Int V by A9, TOPS_1:24;
then [:X1,Y1:] c= [:(Int V),(Int W):] by A12, ZFMISC_1:96;
hence e in [:(Int V),(Int W):] by A6, A8; ::_thesis: verum
end;
( Int V c= V & Int W c= W ) by TOPS_1:16;
then [:(Int V),(Int W):] c= [:V,W:] by ZFMISC_1:96;
hence [:(Int V),(Int W):] c= Int [:V,W:] by Th6, TOPS_1:24; ::_thesis: verum
end;
theorem Th8: :: BORSUK_1:8
for X, Y being non empty TopSpace
for x being Point of X
for y being Point of Y
for V being a_neighborhood of x
for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]
proof
let X, Y be non empty TopSpace; ::_thesis: for x being Point of X
for y being Point of Y
for V being a_neighborhood of x
for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]
let x be Point of X; ::_thesis: for y being Point of Y
for V being a_neighborhood of x
for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]
let y be Point of Y; ::_thesis: for V being a_neighborhood of x
for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]
let V be a_neighborhood of x; ::_thesis: for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]
let W be a_neighborhood of y; ::_thesis: [:V,W:] is a_neighborhood of [x,y]
( x in Int V & y in Int W ) by CONNSP_2:def_1;
then [x,y] in [:(Int V),(Int W):] by ZFMISC_1:87;
hence [x,y] in Int [:V,W:] by Th7; :: according to CONNSP_2:def_1 ::_thesis: verum
end;
theorem Th9: :: BORSUK_1:9
for X, Y being non empty TopSpace
for A being Subset of X
for B being Subset of Y
for V being a_neighborhood of A
for W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]
proof
let X, Y be non empty TopSpace; ::_thesis: for A being Subset of X
for B being Subset of Y
for V being a_neighborhood of A
for W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]
let A be Subset of X; ::_thesis: for B being Subset of Y
for V being a_neighborhood of A
for W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]
let B be Subset of Y; ::_thesis: for V being a_neighborhood of A
for W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]
let V be a_neighborhood of A; ::_thesis: for W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]
let W be a_neighborhood of B; ::_thesis: [:V,W:] is a_neighborhood of [:A,B:]
( A c= Int V & B c= Int W ) by CONNSP_2:def_2;
then [:A,B:] c= [:(Int V),(Int W):] by ZFMISC_1:96;
hence [:A,B:] c= Int [:V,W:] by Th7; :: according to CONNSP_2:def_2 ::_thesis: verum
end;
definition
let X, Y be non empty TopSpace;
let x be Point of X;
let y be Point of Y;
let V be a_neighborhood of x;
let W be a_neighborhood of y;
:: original: [:
redefine func[:V,W:] -> a_neighborhood of [x,y];
correctness
coherence
[:V,W:] is a_neighborhood of [x,y];
by Th8;
end;
theorem Th10: :: BORSUK_1:10
for X, Y being non empty TopSpace
for XT being Point of [:X,Y:] ex W being Point of X ex T being Point of Y st XT = [W,T]
proof
let X, Y be non empty TopSpace; ::_thesis: for XT being Point of [:X,Y:] ex W being Point of X ex T being Point of Y st XT = [W,T]
let XT be Point of [:X,Y:]; ::_thesis: ex W being Point of X ex T being Point of Y st XT = [W,T]
the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
hence ex W being Point of X ex T being Point of Y st XT = [W,T] by DOMAIN_1:1; ::_thesis: verum
end;
definition
let X, Y be non empty TopSpace;
let A be Subset of X;
let t be Point of Y;
let V be a_neighborhood of A;
let W be a_neighborhood of t;
:: original: [:
redefine func[:V,W:] -> a_neighborhood of [:A,{t}:];
correctness
coherence
[:V,W:] is a_neighborhood of [:A,{t}:];
proof
W is a_neighborhood of {t} by CONNSP_2:8;
hence [:V,W:] is a_neighborhood of [:A,{t}:] by Th9; ::_thesis: verum
end;
end;
definition
let X, Y be TopSpace;
let A be Subset of [:X,Y:];
func Base-Appr A -> Subset-Family of [:X,Y:] equals :: BORSUK_1:def 3
{ [: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:]
proof
set B = { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } ;
{ [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } c= bool the carrier of [:X,Y:]
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } or e in bool the carrier of [:X,Y:] )
assume e in { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } ; ::_thesis: e in bool the carrier of [:X,Y:]
then ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & [:X1,Y1:] c= A & X1 is open & Y1 is open ) ;
hence e in bool the carrier of [:X,Y:] ; ::_thesis: verum
end;
hence { [: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:] ; ::_thesis: verum
end;
end;
:: deftheorem defines Base-Appr BORSUK_1:def_3_:_
for X, Y being TopSpace
for A being Subset of [:X,Y:] holds Base-Appr A = { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } ;
registration
let X, Y be TopSpace;
let A be Subset of [:X,Y:];
cluster Base-Appr A -> open ;
coherence
Base-Appr A is open
proof
let B be Subset of [:X,Y:]; :: according to TOPS_2:def_1 ::_thesis: ( not B in Base-Appr A or B is open )
assume B in Base-Appr A ; ::_thesis: B is open
then ex X1 being Subset of X ex Y1 being Subset of Y st
( B = [:X1,Y1:] & [:X1,Y1:] c= A & X1 is open & Y1 is open ) ;
hence B is open by Th6; ::_thesis: verum
end;
end;
theorem Th11: :: BORSUK_1:11
for X, Y being TopSpace
for A, B being Subset of [:X,Y:] st A c= B holds
Base-Appr A c= Base-Appr B
proof
let X, Y be TopSpace; ::_thesis: for A, B being Subset of [:X,Y:] st A c= B holds
Base-Appr A c= Base-Appr B
let A, B be Subset of [:X,Y:]; ::_thesis: ( A c= B implies Base-Appr A c= Base-Appr B )
assume A1: A c= B ; ::_thesis: Base-Appr A c= Base-Appr B
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in Base-Appr A or e in Base-Appr B )
assume e in Base-Appr A ; ::_thesis: e in Base-Appr B
then consider X1 being Subset of X, Y1 being Subset of Y such that
A2: e = [:X1,Y1:] and
A3: [:X1,Y1:] c= A and
A4: ( X1 is open & Y1 is open ) ;
[:X1,Y1:] c= B by A1, A3, XBOOLE_1:1;
hence e in Base-Appr B by A2, A4; ::_thesis: verum
end;
theorem Th12: :: BORSUK_1:12
for X, Y being TopSpace
for A being Subset of [:X,Y:] holds union (Base-Appr A) c= A
proof
let X, Y be TopSpace; ::_thesis: for A being Subset of [:X,Y:] holds union (Base-Appr A) c= A
let A be Subset of [:X,Y:]; ::_thesis: union (Base-Appr A) c= A
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in union (Base-Appr A) or e in A )
assume e in union (Base-Appr A) ; ::_thesis: e in A
then consider B being set such that
A1: e in B and
A2: B in Base-Appr A by TARSKI:def_4;
ex X1 being Subset of X ex Y1 being Subset of Y st
( B = [:X1,Y1:] & [:X1,Y1:] c= A & X1 is open & Y1 is open ) by A2;
hence e in A by A1; ::_thesis: verum
end;
theorem Th13: :: BORSUK_1:13
for X, Y being TopSpace
for A being Subset of [:X,Y:] st A is open holds
A = union (Base-Appr A)
proof
let X, Y be TopSpace; ::_thesis: for A being Subset of [:X,Y:] st A is open holds
A = union (Base-Appr A)
let A be Subset of [:X,Y:]; ::_thesis: ( A is open implies A = union (Base-Appr A) )
assume A is open ; ::_thesis: A = union (Base-Appr A)
then consider B being Subset-Family of [:X,Y:] such that
A1: A = union B and
A2: for e being set st e in B holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by Th5;
thus A c= union (Base-Appr A) :: according to XBOOLE_0:def_10 ::_thesis: union (Base-Appr A) c= A
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A or e in union (Base-Appr A) )
assume e in A ; ::_thesis: e in union (Base-Appr A)
then consider u being set such that
A3: e in u and
A4: u in B by A1, TARSKI:def_4;
( ex X1 being Subset of X ex Y1 being Subset of Y st
( u = [:X1,Y1:] & X1 is open & Y1 is open ) & u c= A ) by A1, A2, A4, ZFMISC_1:74;
then u in Base-Appr A ;
hence e in union (Base-Appr A) by A3, TARSKI:def_4; ::_thesis: verum
end;
thus union (Base-Appr A) c= A by Th12; ::_thesis: verum
end;
theorem Th14: :: BORSUK_1:14
for X, Y being TopSpace
for A being Subset of [:X,Y:] holds Int A = union (Base-Appr A)
proof
let X, Y be TopSpace; ::_thesis: for A being Subset of [:X,Y:] holds Int A = union (Base-Appr A)
let A be Subset of [:X,Y:]; ::_thesis: Int A = union (Base-Appr A)
( Int A = union (Base-Appr (Int A)) & Base-Appr (Int A) c= Base-Appr A ) by Th11, Th13, TOPS_1:16;
hence Int A c= union (Base-Appr A) by ZFMISC_1:77; :: according to XBOOLE_0:def_10 ::_thesis: union (Base-Appr A) c= Int A
union (Base-Appr A) is open by TOPS_2:19;
hence union (Base-Appr A) c= Int A by Th12, TOPS_1:24; ::_thesis: verum
end;
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 :: BORSUK_1:def 4
.: (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)
proof
the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
hence .: (pr1 ( the carrier of X, the carrier of Y)) is Function of (bool the carrier of [:X,Y:]),(bool the carrier of X) ; ::_thesis: verum
end;
correctness
;
func Pr2 (X,Y) -> Function of (bool the carrier of [:X,Y:]),(bool the carrier of Y) equals :: BORSUK_1:def 5
.: (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)
proof
the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
hence .: (pr2 ( the carrier of X, the carrier of Y)) is Function of (bool the carrier of [:X,Y:]),(bool the carrier of Y) ; ::_thesis: verum
end;
correctness
;
end;
:: deftheorem defines Pr1 BORSUK_1:def_4_:_
for X, Y being non empty TopSpace holds Pr1 (X,Y) = .: (pr1 ( the carrier of X, the carrier of Y));
:: deftheorem defines Pr2 BORSUK_1:def_5_:_
for X, Y being non empty TopSpace holds Pr2 (X,Y) = .: (pr2 ( the carrier of X, the carrier of Y));
theorem Th15: :: BORSUK_1:15
for X, Y being non empty TopSpace
for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(union ((Pr1 (X,Y)) .: H)),(meet ((Pr2 (X,Y)) .: H)):] c= A
proof
let X, Y be non empty TopSpace; ::_thesis: for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(union ((Pr1 (X,Y)) .: H)),(meet ((Pr2 (X,Y)) .: H)):] c= A
let A be Subset of [:X,Y:]; ::_thesis: for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(union ((Pr1 (X,Y)) .: H)),(meet ((Pr2 (X,Y)) .: H)):] c= A
let H be Subset-Family of [:X,Y:]; ::_thesis: ( ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) implies [:(union ((Pr1 (X,Y)) .: H)),(meet ((Pr2 (X,Y)) .: H)):] c= A )
assume A1: for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ; ::_thesis: [:(union ((Pr1 (X,Y)) .: H)),(meet ((Pr2 (X,Y)) .: H)):] c= A
the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
hence [:(union ((Pr1 (X,Y)) .: H)),(meet ((Pr2 (X,Y)) .: H)):] c= A by A1, EQREL_1:51; ::_thesis: verum
end;
theorem Th16: :: BORSUK_1:16
for X, Y being non empty TopSpace
for H being Subset-Family of [:X,Y:]
for C being set st C in (Pr1 (X,Y)) .: H holds
ex D being Subset of [:X,Y:] st
( D in H & C = (pr1 ( the carrier of X, the carrier of Y)) .: D )
proof
let X, Y be non empty TopSpace; ::_thesis: for H being Subset-Family of [:X,Y:]
for C being set st C in (Pr1 (X,Y)) .: H holds
ex D being Subset of [:X,Y:] st
( D in H & C = (pr1 ( the carrier of X, the carrier of Y)) .: D )
let H be Subset-Family of [:X,Y:]; ::_thesis: for C being set st C in (Pr1 (X,Y)) .: H holds
ex D being Subset of [:X,Y:] st
( D in H & C = (pr1 ( the carrier of X, the carrier of Y)) .: D )
let C be set ; ::_thesis: ( C in (Pr1 (X,Y)) .: H implies ex D being Subset of [:X,Y:] st
( D in H & C = (pr1 ( the carrier of X, the carrier of Y)) .: D ) )
assume C in (Pr1 (X,Y)) .: H ; ::_thesis: ex D being Subset of [:X,Y:] st
( D in H & C = (pr1 ( the carrier of X, the carrier of Y)) .: D )
then consider u being set such that
A1: u in dom (Pr1 (X,Y)) and
A2: u in H and
A3: C = (Pr1 (X,Y)) . u by FUNCT_1:def_6;
reconsider u = u as Subset of [:X,Y:] by A1;
take u ; ::_thesis: ( u in H & C = (pr1 ( the carrier of X, the carrier of Y)) .: u )
thus u in H by A2; ::_thesis: C = (pr1 ( the carrier of X, the carrier of Y)) .: u
the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
hence C = (pr1 ( the carrier of X, the carrier of Y)) .: u by A3, EQREL_1:47; ::_thesis: verum
end;
theorem Th17: :: BORSUK_1:17
for X, Y being non empty TopSpace
for H being Subset-Family of [:X,Y:]
for C being set st C in (Pr2 (X,Y)) .: H holds
ex D being Subset of [:X,Y:] st
( D in H & C = (pr2 ( the carrier of X, the carrier of Y)) .: D )
proof
let X, Y be non empty TopSpace; ::_thesis: for H being Subset-Family of [:X,Y:]
for C being set st C in (Pr2 (X,Y)) .: H holds
ex D being Subset of [:X,Y:] st
( D in H & C = (pr2 ( the carrier of X, the carrier of Y)) .: D )
let H be Subset-Family of [:X,Y:]; ::_thesis: for C being set st C in (Pr2 (X,Y)) .: H holds
ex D being Subset of [:X,Y:] st
( D in H & C = (pr2 ( the carrier of X, the carrier of Y)) .: D )
let C be set ; ::_thesis: ( C in (Pr2 (X,Y)) .: H implies ex D being Subset of [:X,Y:] st
( D in H & C = (pr2 ( the carrier of X, the carrier of Y)) .: D ) )
assume C in (Pr2 (X,Y)) .: H ; ::_thesis: ex D being Subset of [:X,Y:] st
( D in H & C = (pr2 ( the carrier of X, the carrier of Y)) .: D )
then consider u being set such that
A1: u in dom (Pr2 (X,Y)) and
A2: u in H and
A3: C = (Pr2 (X,Y)) . u by FUNCT_1:def_6;
reconsider u = u as Subset of [:X,Y:] by A1;
take u ; ::_thesis: ( u in H & C = (pr2 ( the carrier of X, the carrier of Y)) .: u )
thus u in H by A2; ::_thesis: C = (pr2 ( the carrier of X, the carrier of Y)) .: u
the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
hence C = (pr2 ( the carrier of X, the carrier of Y)) .: u by A3, EQREL_1:48; ::_thesis: verum
end;
theorem Th18: :: BORSUK_1:18
for X, Y being non empty TopSpace
for D being Subset of [:X,Y:] st D is open holds
for X1 being Subset of X
for Y1 being Subset of Y holds
( ( X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D implies X1 is open ) & ( Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D implies Y1 is open ) )
proof
let X, Y be non empty TopSpace; ::_thesis: for D being Subset of [:X,Y:] st D is open holds
for X1 being Subset of X
for Y1 being Subset of Y holds
( ( X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D implies X1 is open ) & ( Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D implies Y1 is open ) )
let D be Subset of [:X,Y:]; ::_thesis: ( D is open implies for X1 being Subset of X
for Y1 being Subset of Y holds
( ( X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D implies X1 is open ) & ( Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D implies Y1 is open ) ) )
set p = pr2 ( the carrier of X, the carrier of Y);
set P = .: (pr2 ( the carrier of X, the carrier of Y));
assume D is open ; ::_thesis: for X1 being Subset of X
for Y1 being Subset of Y holds
( ( X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D implies X1 is open ) & ( Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D implies Y1 is open ) )
then consider H being Subset-Family of [:X,Y:] such that
A1: D = union H and
A2: for e being set st e in H holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by Th5;
reconsider K = H as Subset-Family of [: the carrier of X, the carrier of Y:] by Def2;
let X1 be Subset of X; ::_thesis: for Y1 being Subset of Y holds
( ( X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D implies X1 is open ) & ( Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D implies Y1 is open ) )
let Y1 be Subset of Y; ::_thesis: ( ( X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D implies X1 is open ) & ( Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D implies Y1 is open ) )
thus ( X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D implies X1 is open ) ::_thesis: ( Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D implies Y1 is open )
proof
set p = pr1 ( the carrier of X, the carrier of Y);
set P = .: (pr1 ( the carrier of X, the carrier of Y));
reconsider PK = (.: (pr1 ( the carrier of X, the carrier of Y))) .: K as Subset-Family of X ;
reconsider PK = PK as Subset-Family of X ;
A3: PK is open
proof
let X1 be Subset of X; :: according to TOPS_2:def_1 ::_thesis: ( not X1 in PK or X1 is open )
reconsider x1 = X1 as Subset of X ;
assume X1 in PK ; ::_thesis: X1 is open
then consider c being Subset of [: the carrier of X, the carrier of Y:] such that
A4: c in K and
A5: x1 = (.: (pr1 ( the carrier of X, the carrier of Y))) . c by FUNCT_2:65;
dom (.: (pr1 ( the carrier of X, the carrier of Y))) = bool [: the carrier of X, the carrier of Y:] by FUNCT_2:def_1;
then A6: X1 = (pr1 ( the carrier of X, the carrier of Y)) .: c by A5, FUNCT_3:7;
A7: ( c = {} or c <> {} ) ;
ex X2 being Subset of X ex Y2 being Subset of Y st
( c = [:X2,Y2:] & X2 is open & Y2 is open ) by A2, A4;
hence X1 is open by A6, A7, EQREL_1:49; ::_thesis: verum
end;
assume X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D ; ::_thesis: X1 is open
then X1 = union ((.: (pr1 ( the carrier of X, the carrier of Y))) .: K) by A1, EQREL_1:53;
hence X1 is open by A3, TOPS_2:19; ::_thesis: verum
end;
reconsider PK = (.: (pr2 ( the carrier of X, the carrier of Y))) .: K as Subset-Family of Y ;
reconsider PK = PK as Subset-Family of Y ;
A8: PK is open
proof
let Y1 be Subset of Y; :: according to TOPS_2:def_1 ::_thesis: ( not Y1 in PK or Y1 is open )
reconsider y1 = Y1 as Subset of Y ;
assume Y1 in PK ; ::_thesis: Y1 is open
then consider c being Subset of [: the carrier of X, the carrier of Y:] such that
A9: c in K and
A10: y1 = (.: (pr2 ( the carrier of X, the carrier of Y))) . c by FUNCT_2:65;
dom (.: (pr2 ( the carrier of X, the carrier of Y))) = bool [: the carrier of X, the carrier of Y:] by FUNCT_2:def_1;
then A11: Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: c by A10, FUNCT_3:7;
A12: ( c = {} or c <> {} ) ;
ex X2 being Subset of X ex Y2 being Subset of Y st
( c = [:X2,Y2:] & X2 is open & Y2 is open ) by A2, A9;
hence Y1 is open by A11, A12, EQREL_1:49; ::_thesis: verum
end;
assume Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D ; ::_thesis: Y1 is open
then Y1 = union ((.: (pr2 ( the carrier of X, the carrier of Y))) .: K) by A1, EQREL_1:53;
hence Y1 is open by A8, TOPS_2:19; ::_thesis: verum
end;
theorem Th19: :: BORSUK_1:19
for X, Y being non empty TopSpace
for H being Subset-Family of [:X,Y:] st H is open holds
( (Pr1 (X,Y)) .: H is open & (Pr2 (X,Y)) .: H is open )
proof
let X, Y be non empty TopSpace; ::_thesis: for H being Subset-Family of [:X,Y:] st H is open holds
( (Pr1 (X,Y)) .: H is open & (Pr2 (X,Y)) .: H is open )
let H be Subset-Family of [:X,Y:]; ::_thesis: ( H is open implies ( (Pr1 (X,Y)) .: H is open & (Pr2 (X,Y)) .: H is open ) )
reconsider P1 = (Pr1 (X,Y)) .: H as Subset-Family of X ;
reconsider P2 = (Pr2 (X,Y)) .: H as Subset-Family of Y ;
assume A1: H is open ; ::_thesis: ( (Pr1 (X,Y)) .: H is open & (Pr2 (X,Y)) .: H is open )
A2: P2 is open
proof
let Y1 be Subset of Y; :: according to TOPS_2:def_1 ::_thesis: ( not Y1 in P2 or Y1 is open )
assume Y1 in P2 ; ::_thesis: Y1 is open
then consider D being Subset of [:X,Y:] such that
A3: D in H and
A4: Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D by Th17;
D is open by A1, A3, TOPS_2:def_1;
hence Y1 is open by A4, Th18; ::_thesis: verum
end;
P1 is open
proof
let X1 be Subset of X; :: according to TOPS_2:def_1 ::_thesis: ( not X1 in P1 or X1 is open )
assume X1 in P1 ; ::_thesis: X1 is open
then consider D being Subset of [:X,Y:] such that
A5: D in H and
A6: X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D by Th16;
D is open by A1, A5, TOPS_2:def_1;
hence X1 is open by A6, Th18; ::_thesis: verum
end;
hence ( (Pr1 (X,Y)) .: H is open & (Pr2 (X,Y)) .: H is open ) by A2; ::_thesis: verum
end;
theorem Th20: :: BORSUK_1:20
for X, Y being non empty TopSpace
for H being Subset-Family of [:X,Y:] st ( (Pr1 (X,Y)) .: H = {} or (Pr2 (X,Y)) .: H = {} ) holds
H = {}
proof
let X, Y be non empty TopSpace; ::_thesis: for H being Subset-Family of [:X,Y:] st ( (Pr1 (X,Y)) .: H = {} or (Pr2 (X,Y)) .: H = {} ) holds
H = {}
let H be Subset-Family of [:X,Y:]; ::_thesis: ( ( (Pr1 (X,Y)) .: H = {} or (Pr2 (X,Y)) .: H = {} ) implies H = {} )
( dom (Pr1 (X,Y)) = bool the carrier of [:X,Y:] & dom (Pr2 (X,Y)) = bool the carrier of [:X,Y:] ) by FUNCT_2:def_1;
hence ( ( (Pr1 (X,Y)) .: H = {} or (Pr2 (X,Y)) .: H = {} ) implies H = {} ) ; ::_thesis: verum
end;
theorem Th21: :: BORSUK_1:21
for X, Y being non empty TopSpace
for H being Subset-Family of [:X,Y:]
for X1 being Subset of X
for Y1 being Subset of Y st H is Cover of [:X1,Y1:] holds
( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )
proof
let X, Y be non empty TopSpace; ::_thesis: for H being Subset-Family of [:X,Y:]
for X1 being Subset of X
for Y1 being Subset of Y st H is Cover of [:X1,Y1:] holds
( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )
let H be Subset-Family of [:X,Y:]; ::_thesis: for X1 being Subset of X
for Y1 being Subset of Y st H is Cover of [:X1,Y1:] holds
( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )
let X1 be Subset of X; ::_thesis: for Y1 being Subset of Y st H is Cover of [:X1,Y1:] holds
( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )
let Y1 be Subset of Y; ::_thesis: ( H is Cover of [:X1,Y1:] implies ( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) ) )
A1: dom (.: (pr2 ( the carrier of X, the carrier of Y))) = bool (dom (pr2 ( the carrier of X, the carrier of Y))) by FUNCT_3:def_1
.= bool [: the carrier of X, the carrier of Y:] by FUNCT_3:def_5 ;
A2: the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
assume A3: [:X1,Y1:] c= union H ; :: according to SETFAM_1:def_11 ::_thesis: ( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )
thus ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) ::_thesis: ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 )
proof
assume Y1 <> {} ; ::_thesis: (Pr1 (X,Y)) .: H is Cover of X1
then consider y being Point of Y such that
A4: y in Y1 by SUBSET_1:4;
let e be set ; :: according to TARSKI:def_3,SETFAM_1:def_11 ::_thesis: ( not e in X1 or e in union ((Pr1 (X,Y)) .: H) )
assume A5: e in X1 ; ::_thesis: e in union ((Pr1 (X,Y)) .: H)
then reconsider x = e as Point of X ;
[x,y] in [:X1,Y1:] by A4, A5, ZFMISC_1:87;
then consider A being set such that
A6: [x,y] in A and
A7: A in H by A3, TARSKI:def_4;
[x,y] in [: the carrier of X, the carrier of Y:] by ZFMISC_1:87;
then A8: [x,y] in dom (pr1 ( the carrier of X, the carrier of Y)) by FUNCT_3:def_4;
A9: dom (.: (pr1 ( the carrier of X, the carrier of Y))) = bool (dom (pr1 ( the carrier of X, the carrier of Y))) by FUNCT_3:def_1
.= bool [: the carrier of X, the carrier of Y:] by FUNCT_3:def_4 ;
e = (pr1 ( the carrier of X, the carrier of Y)) . (x,y) by FUNCT_3:def_4;
then A10: e in (pr1 ( the carrier of X, the carrier of Y)) .: A by A6, A8, FUNCT_1:def_6;
(.: (pr1 ( the carrier of X, the carrier of Y))) . A = (pr1 ( the carrier of X, the carrier of Y)) .: A by A2, A7, EQREL_1:47;
then (pr1 ( the carrier of X, the carrier of Y)) .: A in (Pr1 (X,Y)) .: H by A2, A7, A9, FUNCT_1:def_6;
hence e in union ((Pr1 (X,Y)) .: H) by A10, TARSKI:def_4; ::_thesis: verum
end;
assume X1 <> {} ; ::_thesis: (Pr2 (X,Y)) .: H is Cover of Y1
then consider x being Point of X such that
A11: x in X1 by SUBSET_1:4;
let e be set ; :: according to TARSKI:def_3,SETFAM_1:def_11 ::_thesis: ( not e in Y1 or e in union ((Pr2 (X,Y)) .: H) )
assume A12: e in Y1 ; ::_thesis: e in union ((Pr2 (X,Y)) .: H)
then reconsider y = e as Point of Y ;
[x,y] in [:X1,Y1:] by A11, A12, ZFMISC_1:87;
then consider A being set such that
A13: [x,y] in A and
A14: A in H by A3, TARSKI:def_4;
[x,y] in [: the carrier of X, the carrier of Y:] by ZFMISC_1:87;
then A15: [x,y] in dom (pr2 ( the carrier of X, the carrier of Y)) by FUNCT_3:def_5;
e = (pr2 ( the carrier of X, the carrier of Y)) . (x,y) by FUNCT_3:def_5;
then A16: e in (pr2 ( the carrier of X, the carrier of Y)) .: A by A13, A15, FUNCT_1:def_6;
(.: (pr2 ( the carrier of X, the carrier of Y))) . A = (pr2 ( the carrier of X, the carrier of Y)) .: A by A2, A14, EQREL_1:48;
then (pr2 ( the carrier of X, the carrier of Y)) .: A in (Pr2 (X,Y)) .: H by A2, A14, A1, FUNCT_1:def_6;
hence e in union ((Pr2 (X,Y)) .: H) by A16, TARSKI:def_4; ::_thesis: verum
end;
theorem Th22: :: BORSUK_1:22
for X, Y being TopSpace
for H being Subset-Family of X
for Y being Subset of X st H is Cover of Y holds
ex F being Subset-Family of X st
( F c= H & F is Cover of Y & ( for C being set st C in F holds
C meets Y ) )
proof
let X, Y be TopSpace; ::_thesis: for H being Subset-Family of X
for Y being Subset of X st H is Cover of Y holds
ex F being Subset-Family of X st
( F c= H & F is Cover of Y & ( for C being set st C in F holds
C meets Y ) )
let H be Subset-Family of X; ::_thesis: for Y being Subset of X st H is Cover of Y holds
ex F being Subset-Family of X st
( F c= H & F is Cover of Y & ( for C being set st C in F holds
C meets Y ) )
let Y be Subset of X; ::_thesis: ( H is Cover of Y implies ex F being Subset-Family of X st
( F c= H & F is Cover of Y & ( for C being set st C in F holds
C meets Y ) ) )
assume A1: H is Cover of Y ; ::_thesis: ex F being Subset-Family of X st
( F c= H & F is Cover of Y & ( for C being set st C in F holds
C meets Y ) )
defpred S1[ set ] means ( $1 in H & $1 /\ Y <> {} );
{ Z where Z is Subset of X : S1[Z] } is Subset-Family of X from DOMAIN_1:sch_7();
then reconsider F = { Z where Z is Subset of X : ( Z in H & Z /\ Y <> {} ) } as Subset-Family of X ;
reconsider F = F as Subset-Family of X ;
take F ; ::_thesis: ( F c= H & F is Cover of Y & ( for C being set st C in F holds
C meets Y ) )
thus F c= H ::_thesis: ( F is Cover of Y & ( for C being set st C in F holds
C meets Y ) )
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in F or e in H )
assume e in F ; ::_thesis: e in H
then ex Z being Subset of X st
( e = Z & Z in H & Z /\ Y <> {} ) ;
hence e in H ; ::_thesis: verum
end;
A2: Y c= union H by A1, SETFAM_1:def_11;
thus F is Cover of Y ::_thesis: for C being set st C in F holds
C meets Y
proof
let e be set ; :: according to TARSKI:def_3,SETFAM_1:def_11 ::_thesis: ( not e in Y or e in union F )
assume A3: e in Y ; ::_thesis: e in union F
then consider u being set such that
A4: e in u and
A5: u in H by A2, TARSKI:def_4;
reconsider u = u as Subset of X by A5;
u /\ Y <> {} by A3, A4, XBOOLE_0:def_4;
then u in F by A5;
hence e in union F by A4, TARSKI:def_4; ::_thesis: verum
end;
let C be set ; ::_thesis: ( C in F implies C meets Y )
assume C in F ; ::_thesis: C meets Y
then ex Z being Subset of X st
( C = Z & Z in H & Z /\ Y <> {} ) ;
hence C /\ Y <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
theorem Th23: :: BORSUK_1:23
for X, Y being non empty TopSpace
for F being Subset-Family of X
for H being Subset-Family of [:X,Y:] st F is finite & F c= (Pr1 (X,Y)) .: H holds
ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 (X,Y)) .: G )
proof
let X, Y be non empty TopSpace; ::_thesis: for F being Subset-Family of X
for H being Subset-Family of [:X,Y:] st F is finite & F c= (Pr1 (X,Y)) .: H holds
ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 (X,Y)) .: G )
let F be Subset-Family of X; ::_thesis: for H being Subset-Family of [:X,Y:] st F is finite & F c= (Pr1 (X,Y)) .: H holds
ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 (X,Y)) .: G )
let H be Subset-Family of [:X,Y:]; ::_thesis: ( F is finite & F c= (Pr1 (X,Y)) .: H implies ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 (X,Y)) .: G ) )
assume that
A1: F is finite and
A2: F c= (Pr1 (X,Y)) .: H ; ::_thesis: ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 (X,Y)) .: G )
defpred S1[ set , set ] means ( $2 in dom (Pr1 (X,Y)) & $2 in H & $1 = (Pr1 (X,Y)) . $2 );
A3: for e being set st e in F holds
ex u being set st S1[e,u] by A2, FUNCT_1:def_6;
consider f being Function such that
A4: dom f = F and
A5: for e being set st e in F holds
S1[e,f . e] from CLASSES1:sch_1(A3);
A6: f .: F c= H
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in f .: F or e in H )
assume e in f .: F ; ::_thesis: e in H
then ex u being set st
( u in dom f & u in F & e = f . u ) by FUNCT_1:def_6;
hence e in H by A5; ::_thesis: verum
end;
then reconsider G = f .: F as Subset-Family of [:X,Y:] by XBOOLE_1:1;
take G ; ::_thesis: ( G c= H & G is finite & F = (Pr1 (X,Y)) .: G )
thus G c= H by A6; ::_thesis: ( G is finite & F = (Pr1 (X,Y)) .: G )
thus G is finite by A1; ::_thesis: F = (Pr1 (X,Y)) .: G
now__::_thesis:_for_e_being_set_holds_
(_e_in_F_iff_ex_u_being_set_st_
(_u_in_dom_(Pr1_(X,Y))_&_u_in_G_&_e_=_(Pr1_(X,Y))_._u_)_)
let e be set ; ::_thesis: ( e in F iff ex u being set st
( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) )
thus ( e in F iff ex u being set st
( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) ) ::_thesis: verum
proof
thus ( e in F implies ex u being set st
( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) ) ::_thesis: ( ex u being set st
( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) implies e in F )
proof
assume A7: e in F ; ::_thesis: ex u being set st
( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u )
take f . e ; ::_thesis: ( f . e in dom (Pr1 (X,Y)) & f . e in G & e = (Pr1 (X,Y)) . (f . e) )
thus f . e in dom (Pr1 (X,Y)) by A5, A7; ::_thesis: ( f . e in G & e = (Pr1 (X,Y)) . (f . e) )
thus f . e in G by A4, A7, FUNCT_1:def_6; ::_thesis: e = (Pr1 (X,Y)) . (f . e)
thus e = (Pr1 (X,Y)) . (f . e) by A5, A7; ::_thesis: verum
end;
given u being set such that u in dom (Pr1 (X,Y)) and
A8: u in G and
A9: e = (Pr1 (X,Y)) . u ; ::_thesis: e in F
ex v being set st
( v in dom f & v in F & u = f . v ) by A8, FUNCT_1:def_6;
hence e in F by A5, A9; ::_thesis: verum
end;
end;
hence F = (Pr1 (X,Y)) .: G by FUNCT_1:def_6; ::_thesis: verum
end;
theorem :: BORSUK_1:24
for X, Y being non empty TopSpace
for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (Pr1 (X,Y)) . [:X1,Y1:] = X1 & (Pr2 (X,Y)) . [:X1,Y1:] = Y1 ) by EQREL_1:50;
theorem Th25: :: BORSUK_1:25
for Y, X being non empty TopSpace
for t being Point of Y
for A being Subset of X st A is compact holds
for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
proof
let Y, X be non empty TopSpace; ::_thesis: for t being Point of Y
for A being Subset of X st A is compact holds
for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
let t be Point of Y; ::_thesis: for A being Subset of X st A is compact holds
for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
let A be Subset of X; ::_thesis: ( A is compact implies for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G )
assume A1: A is compact ; ::_thesis: for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
let G be a_neighborhood of [:A,{t}:]; ::_thesis: ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
A2: the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
now__::_thesis:_ex_V_being_a_neighborhood_of_A_ex_W_being_a_neighborhood_of_t_st_[:V,W:]_c=_G
percases ( A <> {} X or A = {} X ) ;
supposeA3: A <> {} X ; ::_thesis: ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
[:A,{t}:] c= Int G by CONNSP_2:def_2;
then [:A,{t}:] c= union (Base-Appr G) by Th14;
then Base-Appr G is Cover of [:A,{t}:] by SETFAM_1:def_11;
then consider K being Subset-Family of [:X,Y:] such that
A4: K c= Base-Appr G and
A5: K is Cover of [:A,{t}:] and
A6: for c being set st c in K holds
c meets [:A,{t}:] by Th22;
reconsider PK = (Pr1 (X,Y)) .: K as Subset-Family of X ;
K is open by A4, TOPS_2:11;
then A7: (Pr1 (X,Y)) .: K is open by Th19;
PK is Cover of A by A5, Th21;
then consider M being Subset-Family of X such that
A8: M c= (Pr1 (X,Y)) .: K and
A9: M is Cover of A and
A10: M is finite by A1, A7, COMPTS_1:def_4;
consider N being Subset-Family of [:X,Y:] such that
A11: N c= K and
A12: N is finite and
A13: (Pr1 (X,Y)) .: N = M by A8, A10, Th23;
reconsider F = (Pr1 (X,Y)) .: N as Subset-Family of X ;
A14: N is Cover of [:A,{t}:]
proof
let e1, e2 be set ; :: according to RELAT_1:def_3,SETFAM_1:def_11 ::_thesis: ( not [e1,e2] in [:A,{t}:] or [e1,e2] in union N )
A15: A c= union M by A9, SETFAM_1:def_11;
assume A16: [e1,e2] in [:A,{t}:] ; ::_thesis: [e1,e2] in union N
then [e1,e2] `2 in {t} by MCART_1:10;
then [e1,e2] `2 = t by TARSKI:def_1;
then A17: [e1,e2] = [([e1,e2] `1),t] ;
[e1,e2] `1 in A by A16, MCART_1:10;
then consider X1 being set such that
A18: [e1,e2] `1 in X1 and
A19: X1 in M by A15, TARSKI:def_4;
consider XY being Subset of [:X,Y:] such that
A20: XY in N and
A21: (Pr1 (X,Y)) . XY = X1 by A13, A19, FUNCT_2:65;
XY in K by A11, A20;
then XY in Base-Appr G by A4;
then consider X2 being Subset of X, Y2 being Subset of Y such that
A22: XY = [:X2,Y2:] and
[:X2,Y2:] c= G and
X2 is open and
Y2 is open ;
XY meets [:A,{t}:] by A6, A11, A20;
then consider xy being set such that
A23: xy in XY and
A24: xy in [:A,{t}:] by XBOOLE_0:3;
xy `2 in {t} by A24, MCART_1:10;
then xy `2 = t by TARSKI:def_1;
then A25: t in Y2 by A22, A23, MCART_1:10;
XY <> {} by A18, A21, FUNCT_3:8;
then [e1,e2] `1 in X2 by A18, A21, A22, EQREL_1:50;
then [e1,e2] in [:X2,Y2:] by A25, A17, ZFMISC_1:87;
hence [e1,e2] in union N by A20, A22, TARSKI:def_4; ::_thesis: verum
end;
then F is Cover of A by Th21;
then A26: A c= union F by SETFAM_1:def_11;
reconsider H = (Pr2 (X,Y)) .: N as Subset-Family of Y ;
A27: now__::_thesis:_for_C_being_set_st_C_in_H_holds_
t_in_C
let C be set ; ::_thesis: ( C in H implies t in C )
assume C in H ; ::_thesis: t in C
then consider D being Subset of [:X,Y:] such that
A28: D in N and
A29: C = (pr2 ( the carrier of X, the carrier of Y)) .: D by Th17;
D meets [:A,{t}:] by A6, A11, A28;
then D /\ [:A,{t}:] <> {} by XBOOLE_0:def_7;
then consider x being Point of [:X,Y:] such that
A30: x in D /\ [:A,{t}:] by SUBSET_1:4;
A31: x in [:A,{t}:] by A30, XBOOLE_0:def_4;
then x `1 in A by MCART_1:10;
then A32: (pr2 ( the carrier of X, the carrier of Y)) . ((x `1),t) = t by FUNCT_3:def_5;
x `2 in {t} by A31, MCART_1:10;
then x `2 = t by TARSKI:def_1;
then A33: x = [(x `1),t] by A2, MCART_1:21;
x in D by A30, XBOOLE_0:def_4;
hence t in C by A2, A29, A33, A32, FUNCT_2:35; ::_thesis: verum
end;
[:A,{t}:] c= union N by A14, SETFAM_1:def_11;
then N <> {} by A3, ZFMISC_1:2;
then H <> {} by Th20;
then A34: t in meet H by A27, SETFAM_1:def_1;
A35: N c= Base-Appr G by A4, A11, XBOOLE_1:1;
then A36: N is open by TOPS_2:11;
then meet H is open by A12, Th19, TOPS_2:20;
then t in Int (meet H) by A34, TOPS_1:23;
then reconsider W = meet H as a_neighborhood of t by CONNSP_2:def_1;
union F is open by A36, Th19, TOPS_2:19;
then A c= Int (union F) by A26, TOPS_1:23;
then reconsider V = union F as a_neighborhood of A by CONNSP_2:def_2;
take V = V; ::_thesis: ex W being a_neighborhood of t st [:V,W:] c= G
take W = W; ::_thesis: [:V,W:] c= G
now__::_thesis:_for_e_being_set_st_e_in_N_holds_
(_e_c=_G_&_ex_X1_being_Subset_of_X_ex_Y1_being_Subset_of_Y_st_e_=_[:X1,Y1:]_)
let e be set ; ::_thesis: ( e in N implies ( e c= G & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) )
assume e in N ; ::_thesis: ( e c= G & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] )
then e in Base-Appr G by A35;
then ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & [:X1,Y1:] c= G & X1 is open & Y1 is open ) ;
hence ( e c= G & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ; ::_thesis: verum
end;
hence [:V,W:] c= G by Th15; ::_thesis: verum
end;
suppose A = {} X ; ::_thesis: ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G
then A c= Int ({} X) ;
then reconsider V = {} X as a_neighborhood of A by CONNSP_2:def_2;
set W = the a_neighborhood of t;
take V = V; ::_thesis: ex W being a_neighborhood of t st [:V,W:] c= G
take W = the a_neighborhood of t; ::_thesis: [:V,W:] c= G
[:V,W:] = {} ;
hence [:V,W:] c= G by XBOOLE_1:2; ::_thesis: verum
end;
end;
end;
hence ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G ; ::_thesis: verum
end;
begin
definition
let X be 1-sorted ;
func TrivDecomp X -> a_partition of the carrier of X equals :: BORSUK_1:def 6
Class (id the carrier of X);
coherence
Class (id the carrier of X) is a_partition of the carrier of X ;
end;
:: deftheorem defines TrivDecomp BORSUK_1:def_6_:_
for X being 1-sorted holds TrivDecomp X = Class (id the carrier of X);
registration
let X be non empty 1-sorted ;
cluster TrivDecomp X -> non empty ;
coherence
not TrivDecomp X is empty ;
end;
theorem Th26: :: BORSUK_1:26
for X being non empty TopSpace
for A being Subset of X st A in TrivDecomp X holds
ex x being Point of X st A = {x}
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A in TrivDecomp X holds
ex x being Point of X st A = {x}
let A be Subset of X; ::_thesis: ( A in TrivDecomp X implies ex x being Point of X st A = {x} )
assume A in TrivDecomp X ; ::_thesis: ex x being Point of X st A = {x}
then consider x being set such that
A1: x in the carrier of X and
A2: A = Class ((id the carrier of X),x) by EQREL_1:def_3;
reconsider x = x as Point of X by A1;
take x ; ::_thesis: A = {x}
thus A = {x} by A2, EQREL_1:25; ::_thesis: verum
end;
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 ) )
proof
let X be non empty TopSpace; ::_thesis: 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 ) )
let A be Subset of X; ::_thesis: 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 ) )
let V be a_neighborhood of A; ::_thesis: 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 ) )
take Int V ; ::_thesis: ( Int V is open & A c= Int V & Int V c= V & ( for B being Subset of X st B in TrivDecomp X & B meets Int V holds
B c= Int V ) )
thus Int V is open ; ::_thesis: ( A c= Int V & Int V c= V & ( for B being Subset of X st B in TrivDecomp X & B meets Int V holds
B c= Int V ) )
thus A c= Int V by CONNSP_2:def_2; ::_thesis: ( Int V c= V & ( for B being Subset of X st B in TrivDecomp X & B meets Int V holds
B c= Int V ) )
thus Int V c= V by TOPS_1:16; ::_thesis: for B being Subset of X st B in TrivDecomp X & B meets Int V holds
B c= Int V
let B be Subset of X; ::_thesis: ( B in TrivDecomp X & B meets Int V implies B c= Int V )
assume that
A1: B in TrivDecomp X and
A2: B meets Int V ; ::_thesis: B c= Int V
consider x being Point of X such that
A3: B = {x} by A1, Th26;
x in Int V by A2, A3, ZFMISC_1:50;
hence B c= Int V by A3, ZFMISC_1:31; ::_thesis: verum
end;
definition
let X be TopSpace;
let D be a_partition of the carrier of X;
func space D -> strict TopSpace means :Def7: :: BORSUK_1:def 7
( the carrier of it = D & the topology of it = { A where A is Subset of D : union A in the topology of X } );
existence
ex b1 being strict TopSpace st
( the carrier of b1 = D & the topology of b1 = { A where A is Subset of D : union A in the topology of X } )
proof
set t = { A where A is Subset of D : union A in the topology of X } ;
{ A where A is Subset of D : union A in the topology of X } c= bool D
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { A where A is Subset of D : union A in the topology of X } or e in bool D )
assume e in { A where A is Subset of D : union A in the topology of X } ; ::_thesis: e in bool D
then ex A being Subset of D st
( e = A & union A in the topology of X ) ;
hence e in bool D ; ::_thesis: verum
end;
then reconsider t = { A where A is Subset of D : union A in the topology of X } as Subset-Family of D ;
set T = TopStruct(# D,t #);
TopStruct(# D,t #) is TopSpace-like
proof
union D = the carrier of X by EQREL_1:def_4;
then ( D c= D & union D in the topology of X ) by PRE_TOPC:def_1;
hence the carrier of TopStruct(# D,t #) in the topology of TopStruct(# D,t #) ; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of TopStruct(# D,t #)) holds
( not b1 c= the topology of TopStruct(# D,t #) or union b1 in the topology of TopStruct(# D,t #) ) ) & ( for b1, b2 being Element of bool the carrier of TopStruct(# D,t #) holds
( not b1 in the topology of TopStruct(# D,t #) or not b2 in the topology of TopStruct(# D,t #) or b1 /\ b2 in the topology of TopStruct(# D,t #) ) ) )
thus for a being Subset-Family of TopStruct(# D,t #) st a c= the topology of TopStruct(# D,t #) holds
union a in the topology of TopStruct(# D,t #) ::_thesis: for b1, b2 being Element of bool the carrier of TopStruct(# D,t #) holds
( not b1 in the topology of TopStruct(# D,t #) or not b2 in the topology of TopStruct(# D,t #) or b1 /\ b2 in the topology of TopStruct(# D,t #) )
proof
let a be Subset-Family of TopStruct(# D,t #); ::_thesis: ( a c= the topology of TopStruct(# D,t #) implies union a in the topology of TopStruct(# D,t #) )
A1: { (union A) where A is Subset of TopStruct(# D,t #) : A in a } c= bool the carrier of X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (union A) where A is Subset of TopStruct(# D,t #) : A in a } or e in bool the carrier of X )
assume e in { (union A) where A is Subset of TopStruct(# D,t #) : A in a } ; ::_thesis: e in bool the carrier of X
then consider A being Subset of TopStruct(# D,t #) such that
A2: e = union A and
A in a ;
e c= the carrier of X
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in e or u in the carrier of X )
assume u in e ; ::_thesis: u in the carrier of X
then consider x being set such that
A3: u in x and
A4: x in A by A2, TARSKI:def_4;
x in the carrier of TopStruct(# D,t #) by A4;
hence u in the carrier of X by A3; ::_thesis: verum
end;
hence e in bool the carrier of X ; ::_thesis: verum
end;
assume A5: a c= the topology of TopStruct(# D,t #) ; ::_thesis: union a in the topology of TopStruct(# D,t #)
{ (union A) where A is Subset of TopStruct(# D,t #) : A in a } c= the topology of X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (union A) where A is Subset of TopStruct(# D,t #) : A in a } or e in the topology of X )
assume e in { (union A) where A is Subset of TopStruct(# D,t #) : A in a } ; ::_thesis: e in the topology of X
then consider A being Subset of TopStruct(# D,t #) such that
A6: e = union A and
A7: A in a ;
A in the topology of TopStruct(# D,t #) by A5, A7;
then ex B being Subset of D st
( A = B & union B in the topology of X ) ;
hence e in the topology of X by A6; ::_thesis: verum
end;
then union { (union A) where A is Subset of TopStruct(# D,t #) : A in a } in the topology of X by A1, PRE_TOPC:def_1;
then union (union a) in the topology of X by EQREL_1:54;
hence union a in the topology of TopStruct(# D,t #) ; ::_thesis: verum
end;
let a, b be Subset of TopStruct(# D,t #); ::_thesis: ( not a in the topology of TopStruct(# D,t #) or not b in the topology of TopStruct(# D,t #) or a /\ b in the topology of TopStruct(# D,t #) )
assume that
A8: a in the topology of TopStruct(# D,t #) and
A9: b in the topology of TopStruct(# D,t #) ; ::_thesis: a /\ b in the topology of TopStruct(# D,t #)
consider B being Subset of D such that
A10: b = B and
A11: union B in the topology of X by A9;
consider A being Subset of D such that
A12: a = A and
A13: union A in the topology of X by A8;
union (A /\ B) = (union A) /\ (union B) by EQREL_1:62;
then union (A /\ B) in the topology of X by A13, A11, PRE_TOPC:def_1;
hence a /\ b in the topology of TopStruct(# D,t #) by A12, A10; ::_thesis: verum
end;
then reconsider T = TopStruct(# D,t #) as strict TopSpace ;
take T ; ::_thesis: ( the carrier of T = D & the topology of T = { A where A is Subset of D : union A in the topology of X } )
thus ( the carrier of T = D & the topology of T = { A where A is Subset of D : union A in the topology of X } ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = D & the topology of b1 = { A where A is Subset of D : union A in the topology of X } & the carrier of b2 = D & the topology of b2 = { A where A is Subset of D : union A in the topology of X } holds
b1 = b2 ;
end;
:: deftheorem Def7 defines space BORSUK_1:def_7_:_
for X being TopSpace
for D being a_partition of the carrier of X
for b3 being strict TopSpace holds
( b3 = space D iff ( the carrier of b3 = D & the topology of b3 = { A where A is Subset of D : union A in the topology of X } ) );
registration
let X be non empty TopSpace;
let D be a_partition of the carrier of X;
cluster space D -> non empty strict ;
coherence
not space D is empty by Def7;
end;
theorem Th27: :: BORSUK_1:27
for X being non empty TopSpace
for D being non empty a_partition of the carrier of X
for A being Subset of D holds
( union A in the topology of X iff A in the topology of (space D) )
proof
let X be non empty TopSpace; ::_thesis: for D being non empty a_partition of the carrier of X
for A being Subset of D holds
( union A in the topology of X iff A in the topology of (space D) )
let D be non empty a_partition of the carrier of X; ::_thesis: for A being Subset of D holds
( union A in the topology of X iff A in the topology of (space D) )
let B be Subset of D; ::_thesis: ( union B in the topology of X iff B in the topology of (space D) )
A1: the topology of (space D) = { A where A is Subset of D : union A in the topology of X } by Def7;
hence ( union B in the topology of X implies B in the topology of (space D) ) ; ::_thesis: ( B in the topology of (space D) implies union B in the topology of X )
assume B in the topology of (space D) ; ::_thesis: union B in the topology of X
then ex A being Subset of D st
( B = A & union A in the topology of X ) by A1;
hence union B in the topology of X ; ::_thesis: verum
end;
definition
let X be non empty TopSpace;
let D be non empty a_partition of the carrier of X;
func Proj D -> continuous Function of X,(space D) equals :: BORSUK_1:def 8
proj D;
coherence
proj D is continuous Function of X,(space D)
proof
reconsider F = proj D as Function of X,(space D) by Def7;
A1: the carrier of (space D) = D by Def7;
F is continuous
proof
let W be Point of X; :: according to BORSUK_1:def_1 ::_thesis: for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G
let G be a_neighborhood of F . W; ::_thesis: ex H being a_neighborhood of W st F .: H c= G
reconsider H = union (Int G) as Subset of X by A1, EQREL_1:61;
F . W in Int G by CONNSP_2:def_1;
then W in F " (Int G) by FUNCT_2:38;
then A2: W in union (Int G) by A1, EQREL_1:67;
Int G in the topology of (space D) by PRE_TOPC:def_2;
then union (Int G) in the topology of X by A1, Th27;
then H is open by PRE_TOPC:def_2;
then W in Int H by A2, TOPS_1:23;
then W in Int (F " (Int G)) by A1, EQREL_1:67;
then reconsider N = F " (Int G) as a_neighborhood of W by CONNSP_2:def_1;
take N ; ::_thesis: F .: N c= G
( F .: N c= Int G & Int G c= G ) by FUNCT_1:75, TOPS_1:16;
hence F .: N c= G by XBOOLE_1:1; ::_thesis: verum
end;
hence proj D is continuous Function of X,(space D) ; ::_thesis: verum
end;
correctness
;
end;
:: deftheorem defines Proj BORSUK_1:def_8_:_
for X being non empty TopSpace
for D being non empty a_partition of the carrier of X holds Proj D = proj D;
theorem :: BORSUK_1:28
for X being non empty TopSpace
for D being non empty a_partition of the carrier of X
for W being Point of X holds W in (Proj D) . W by EQREL_1:def_9;
theorem Th29: :: BORSUK_1:29
for X being non empty TopSpace
for D being non empty a_partition of the carrier of X
for W being Point of (space D) ex W9 being Point of X st (Proj D) . W9 = W
proof
let X be non empty TopSpace; ::_thesis: for D being non empty a_partition of the carrier of X
for W being Point of (space D) ex W9 being Point of X st (Proj D) . W9 = W
let D be non empty a_partition of the carrier of X; ::_thesis: for W being Point of (space D) ex W9 being Point of X st (Proj D) . W9 = W
let W be Point of (space D); ::_thesis: ex W9 being Point of X st (Proj D) . W9 = W
reconsider p = W as Element of D by Def7;
consider W9 being Point of X such that
A1: (proj D) . W9 = p by EQREL_1:68;
take W9 ; ::_thesis: (Proj D) . W9 = W
thus (Proj D) . W9 = W by A1; ::_thesis: verum
end;
theorem Th30: :: BORSUK_1:30
for X being non empty TopSpace
for D being non empty a_partition of the carrier of X holds rng (Proj D) = the carrier of (space D)
proof
let X be non empty TopSpace; ::_thesis: for D being non empty a_partition of the carrier of X holds rng (Proj D) = the carrier of (space D)
let D be non empty a_partition of the carrier of X; ::_thesis: rng (Proj D) = the carrier of (space D)
thus rng (Proj D) c= the carrier of (space D) ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (space D) c= rng (Proj D)
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the carrier of (space D) or e in rng (Proj D) )
assume e in the carrier of (space D) ; ::_thesis: e in rng (Proj D)
then ex p being Point of X st (Proj D) . p = e by Th29;
hence e in rng (Proj D) by FUNCT_2:4; ::_thesis: verum
end;
definition
let XX be non empty TopSpace;
let X be non empty SubSpace of XX;
let D be non empty a_partition of the carrier of X;
func TrivExt D -> non empty a_partition of the carrier of XX equals :: BORSUK_1:def 9
D \/ { {p} where p is Point of XX : not p in the carrier of X } ;
coherence
D \/ { {p} where p is Point of XX : not p in the carrier of X } is non empty a_partition of the carrier of XX
proof
set E = D \/ { {p} where p is Point of XX : not p in the carrier of X } ;
D \/ { {p} where p is Point of XX : not p in the carrier of X } c= bool the carrier of XX
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in D \/ { {p} where p is Point of XX : not p in the carrier of X } or e in bool the carrier of XX )
assume A1: e in D \/ { {p} where p is Point of XX : not p in the carrier of X } ; ::_thesis: e in bool the carrier of XX
now__::_thesis:_e_in_bool_the_carrier_of_XX
percases ( e in D or e in { {p} where p is Point of XX : not p in the carrier of X } ) by A1, XBOOLE_0:def_3;
supposeA2: e in D ; ::_thesis: e in bool the carrier of XX
bool the carrier of X c= bool the carrier of XX by Th1, ZFMISC_1:67;
hence e in bool the carrier of XX by A2, TARSKI:def_3; ::_thesis: verum
end;
suppose e in { {p} where p is Point of XX : not p in the carrier of X } ; ::_thesis: e in bool the carrier of XX
then ex p being Point of XX st
( e = {p} & not p in the carrier of X ) ;
hence e in bool the carrier of XX ; ::_thesis: verum
end;
end;
end;
hence e in bool the carrier of XX ; ::_thesis: verum
end;
then reconsider E = D \/ { {p} where p is Point of XX : not p in the carrier of X } as Subset-Family of XX ;
E is a_partition of the carrier of XX
proof
now__::_thesis:_for_e_being_set_holds_
(_(_e_in_the_carrier_of_XX_\_the_carrier_of_X_implies_ex_Z_being_set_st_
(_e_in_Z_&_Z_in__{__{p}_where_p_is_Point_of_XX_:_not_p_in_the_carrier_of_X__}__)_)_&_(_ex_Z_being_set_st_
(_e_in_Z_&_Z_in__{__{p}_where_p_is_Point_of_XX_:_not_p_in_the_carrier_of_X__}__)_implies_e_in_the_carrier_of_XX_\_the_carrier_of_X_)_)
let e be set ; ::_thesis: ( ( e in the carrier of XX \ the carrier of X implies ex Z being set st
( e in Z & Z in { {p} where p is Point of XX : not p in the carrier of X } ) ) & ( ex Z being set st
( e in Z & Z in { {p} where p is Point of XX : not p in the carrier of X } ) implies e in the carrier of XX \ the carrier of X ) )
thus ( e in the carrier of XX \ the carrier of X implies ex Z being set st
( e in Z & Z in { {p} where p is Point of XX : not p in the carrier of X } ) ) ::_thesis: ( ex Z being set st
( e in Z & Z in { {p} where p is Point of XX : not p in the carrier of X } ) implies e in the carrier of XX \ the carrier of X )
proof
assume A3: e in the carrier of XX \ the carrier of X ; ::_thesis: ex Z being set st
( e in Z & Z in { {p} where p is Point of XX : not p in the carrier of X } )
take {e} ; ::_thesis: ( e in {e} & {e} in { {p} where p is Point of XX : not p in the carrier of X } )
thus e in {e} by TARSKI:def_1; ::_thesis: {e} in { {p} where p is Point of XX : not p in the carrier of X }
not e in the carrier of X by A3, XBOOLE_0:def_5;
hence {e} in { {p} where p is Point of XX : not p in the carrier of X } by A3; ::_thesis: verum
end;
given Z being set such that A4: e in Z and
A5: Z in { {p} where p is Point of XX : not p in the carrier of X } ; ::_thesis: e in the carrier of XX \ the carrier of X
consider p being Point of XX such that
A6: Z = {p} and
A7: not p in the carrier of X by A5;
e = p by A4, A6, TARSKI:def_1;
hence e in the carrier of XX \ the carrier of X by A7, XBOOLE_0:def_5; ::_thesis: verum
end;
then A8: union { {p} where p is Point of XX : not p in the carrier of X } = the carrier of XX \ the carrier of X by TARSKI:def_4;
thus union E = (union D) \/ (union { {p} where p is Point of XX : not p in the carrier of X } ) by ZFMISC_1:78
.= the carrier of X \/ ( the carrier of XX \ the carrier of X) by A8, EQREL_1:def_4
.= the carrier of XX by Th1, XBOOLE_1:45 ; :: according to EQREL_1:def_4 ::_thesis: for b1 being Element of bool the carrier of XX holds
( not b1 in E or ( not b1 = {} & ( for b2 being Element of bool the carrier of XX holds
( not b2 in E or b1 = b2 or b1 misses b2 ) ) ) )
let A be Subset of XX; ::_thesis: ( not A in E or ( not A = {} & ( for b1 being Element of bool the carrier of XX holds
( not b1 in E or A = b1 or A misses b1 ) ) ) )
assume A9: A in E ; ::_thesis: ( not A = {} & ( for b1 being Element of bool the carrier of XX holds
( not b1 in E or A = b1 or A misses b1 ) ) )
now__::_thesis:_A_<>_{}
percases ( A in D or A in { {p} where p is Point of XX : not p in the carrier of X } ) by A9, XBOOLE_0:def_3;
suppose A in D ; ::_thesis: A <> {}
hence A <> {} by EQREL_1:def_4; ::_thesis: verum
end;
suppose A in { {p} where p is Point of XX : not p in the carrier of X } ; ::_thesis: A <> {}
then ex p being Point of XX st
( A = {p} & not p in the carrier of X ) ;
hence A <> {} ; ::_thesis: verum
end;
end;
end;
hence A <> {} ; ::_thesis: for b1 being Element of bool the carrier of XX holds
( not b1 in E or A = b1 or A misses b1 )
let B be Subset of XX; ::_thesis: ( not B in E or A = B or A misses B )
assume A10: B in E ; ::_thesis: ( A = B or A misses B )
now__::_thesis:_(_A_=_B_or_A_misses_B_)
percases ( A in D or A in { {p} where p is Point of XX : not p in the carrier of X } ) by A9, XBOOLE_0:def_3;
supposeA11: A in D ; ::_thesis: ( A = B or A misses B )
now__::_thesis:_(_A_=_B_or_A_misses_B_)
percases ( B in D or B in { {p} where p is Point of XX : not p in the carrier of X } ) by A10, XBOOLE_0:def_3;
suppose B in D ; ::_thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by A11, EQREL_1:def_4; ::_thesis: verum
end;
suppose B in { {p} where p is Point of XX : not p in the carrier of X } ; ::_thesis: ( A = B or A misses B )
then ex p being Point of XX st
( B = {p} & not p in the carrier of X ) ;
then B misses the carrier of X by ZFMISC_1:50;
hence ( A = B or A misses B ) by A11, XBOOLE_1:63; ::_thesis: verum
end;
end;
end;
hence ( A = B or A misses B ) ; ::_thesis: verum
end;
suppose A in { {p} where p is Point of XX : not p in the carrier of X } ; ::_thesis: ( A = B or A misses B )
then A12: ex p being Point of XX st
( A = {p} & not p in the carrier of X ) ;
then A13: A misses the carrier of X by ZFMISC_1:50;
now__::_thesis:_(_A_=_B_or_A_misses_B_)
percases ( B in D or B in { {p} where p is Point of XX : not p in the carrier of X } ) by A10, XBOOLE_0:def_3;
suppose B in D ; ::_thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by A13, XBOOLE_1:63; ::_thesis: verum
end;
suppose B in { {p} where p is Point of XX : not p in the carrier of X } ; ::_thesis: ( A = B or A misses B )
then ex p being Point of XX st
( B = {p} & not p in the carrier of X ) ;
hence ( A = B or A misses B ) by A12, ZFMISC_1:11; ::_thesis: verum
end;
end;
end;
hence ( A = B or A misses B ) ; ::_thesis: verum
end;
end;
end;
hence ( A = B or A misses B ) ; ::_thesis: verum
end;
hence D \/ { {p} where p is Point of XX : not p in the carrier of X } is non empty a_partition of the carrier of XX ; ::_thesis: verum
end;
correctness
;
end;
:: deftheorem defines TrivExt BORSUK_1:def_9_:_
for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X holds TrivExt D = D \/ { {p} where p is Point of XX : not p in the carrier of X } ;
theorem Th31: :: BORSUK_1:31
for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for A being Subset of XX holds
( not A in TrivExt D or A in D or ex x being Point of XX st
( not x in [#] X & A = {x} ) )
proof
let XX be non empty TopSpace; ::_thesis: for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for A being Subset of XX holds
( not A in TrivExt D or A in D or ex x being Point of XX st
( not x in [#] X & A = {x} ) )
let X be non empty SubSpace of XX; ::_thesis: for D being non empty a_partition of the carrier of X
for A being Subset of XX holds
( not A in TrivExt D or A in D or ex x being Point of XX st
( not x in [#] X & A = {x} ) )
let D be non empty a_partition of the carrier of X; ::_thesis: for A being Subset of XX holds
( not A in TrivExt D or A in D or ex x being Point of XX st
( not x in [#] X & A = {x} ) )
let A be Subset of XX; ::_thesis: ( not A in TrivExt D or A in D or ex x being Point of XX st
( not x in [#] X & A = {x} ) )
assume A1: A in TrivExt D ; ::_thesis: ( A in D or ex x being Point of XX st
( not x in [#] X & A = {x} ) )
now__::_thesis:_(_(_A_in_D_&_A_in_D_)_or_(_A_in__{__{p}_where_p_is_Point_of_XX_:_not_p_in_the_carrier_of_X__}__&_ex_x_being_Point_of_XX_st_
(_not_x_in_[#]_X_&_A_=_{x}_)_)_)
percases ( A in D or A in { {p} where p is Point of XX : not p in the carrier of X } ) by A1, XBOOLE_0:def_3;
case A in D ; ::_thesis: A in D
hence A in D ; ::_thesis: verum
end;
case A in { {p} where p is Point of XX : not p in the carrier of X } ; ::_thesis: ex x being Point of XX st
( not x in [#] X & A = {x} )
then consider x being Point of XX such that
A2: A = {x} and
A3: not x in the carrier of X ;
take x = x; ::_thesis: ( not x in [#] X & A = {x} )
thus not x in [#] X by A3; ::_thesis: A = {x}
thus A = {x} by A2; ::_thesis: verum
end;
end;
end;
hence ( A in D or ex x being Point of XX st
( not x in [#] X & A = {x} ) ) ; ::_thesis: verum
end;
theorem Th32: :: BORSUK_1:32
for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for x being Point of XX st not x in the carrier of X holds
{x} in TrivExt D
proof
let XX be non empty TopSpace; ::_thesis: for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for x being Point of XX st not x in the carrier of X holds
{x} in TrivExt D
let X be non empty SubSpace of XX; ::_thesis: for D being non empty a_partition of the carrier of X
for x being Point of XX st not x in the carrier of X holds
{x} in TrivExt D
let D be non empty a_partition of the carrier of X; ::_thesis: for x being Point of XX st not x in the carrier of X holds
{x} in TrivExt D
let x be Point of XX; ::_thesis: ( not x in the carrier of X implies {x} in TrivExt D )
union (TrivExt D) = the carrier of XX by EQREL_1:def_4;
then consider A being set such that
A1: x in A and
A2: A in TrivExt D by TARSKI:def_4;
assume not x in the carrier of X ; ::_thesis: {x} in TrivExt D
then not A in D by A1;
then A in { {p} where p is Point of XX : not p in the carrier of X } by A2, XBOOLE_0:def_3;
then ex p being Point of XX st
( A = {p} & not p in the carrier of X ) ;
hence {x} in TrivExt D by A1, A2, TARSKI:def_1; ::_thesis: verum
end;
theorem Th33: :: BORSUK_1:33
for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for W being Point of XX st W in the carrier of X holds
(Proj (TrivExt D)) . W = (Proj D) . W
proof
let XX be non empty TopSpace; ::_thesis: for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for W being Point of XX st W in the carrier of X holds
(Proj (TrivExt D)) . W = (Proj D) . W
let X be non empty SubSpace of XX; ::_thesis: for D being non empty a_partition of the carrier of X
for W being Point of XX st W in the carrier of X holds
(Proj (TrivExt D)) . W = (Proj D) . W
let D be non empty a_partition of the carrier of X; ::_thesis: for W being Point of XX st W in the carrier of X holds
(Proj (TrivExt D)) . W = (Proj D) . W
let W be Point of XX; ::_thesis: ( W in the carrier of X implies (Proj (TrivExt D)) . W = (Proj D) . W )
assume A1: W in the carrier of X ; ::_thesis: (Proj (TrivExt D)) . W = (Proj D) . W
then reconsider p = W as Point of X ;
( D c= TrivExt D & (proj D) . p in D ) by XBOOLE_1:7;
then reconsider A = (Proj D) . W as Element of TrivExt D ;
W in A by A1, EQREL_1:def_9;
hence (Proj (TrivExt D)) . W = (Proj D) . W by EQREL_1:65; ::_thesis: verum
end;
theorem Th34: :: BORSUK_1:34
for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for W being Point of XX st not W in the carrier of X holds
(Proj (TrivExt D)) . W = {W}
proof
let XX be non empty TopSpace; ::_thesis: for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for W being Point of XX st not W in the carrier of X holds
(Proj (TrivExt D)) . W = {W}
let X be non empty SubSpace of XX; ::_thesis: for D being non empty a_partition of the carrier of X
for W being Point of XX st not W in the carrier of X holds
(Proj (TrivExt D)) . W = {W}
let D be non empty a_partition of the carrier of X; ::_thesis: for W being Point of XX st not W in the carrier of X holds
(Proj (TrivExt D)) . W = {W}
let W be Point of XX; ::_thesis: ( not W in the carrier of X implies (Proj (TrivExt D)) . W = {W} )
assume not W in the carrier of X ; ::_thesis: (Proj (TrivExt D)) . W = {W}
then ( W in {W} & {W} in TrivExt D ) by Th32, TARSKI:def_1;
hence (Proj (TrivExt D)) . W = {W} by EQREL_1:65; ::_thesis: verum
end;
theorem Th35: :: BORSUK_1:35
for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for W, W9 being Point of XX st not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 holds
W = W9
proof
let XX be non empty TopSpace; ::_thesis: for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for W, W9 being Point of XX st not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 holds
W = W9
let X be non empty SubSpace of XX; ::_thesis: for D being non empty a_partition of the carrier of X
for W, W9 being Point of XX st not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 holds
W = W9
let D be non empty a_partition of the carrier of X; ::_thesis: for W, W9 being Point of XX st not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 holds
W = W9
let W, W9 be Point of XX; ::_thesis: ( not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 implies W = W9 )
assume not W in the carrier of X ; ::_thesis: ( not (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 or W = W9 )
then A1: (Proj (TrivExt D)) . W = {W} by Th34;
W9 in (Proj (TrivExt D)) . W9 by EQREL_1:def_9;
hence ( not (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 or W = W9 ) by A1, TARSKI:def_1; ::_thesis: verum
end;
theorem Th36: :: BORSUK_1:36
for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for e being Point of XX st (Proj (TrivExt D)) . e in the carrier of (space D) holds
e in the carrier of X
proof
let XX be non empty TopSpace; ::_thesis: for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for e being Point of XX st (Proj (TrivExt D)) . e in the carrier of (space D) holds
e in the carrier of X
let X be non empty SubSpace of XX; ::_thesis: for D being non empty a_partition of the carrier of X
for e being Point of XX st (Proj (TrivExt D)) . e in the carrier of (space D) holds
e in the carrier of X
let D be non empty a_partition of the carrier of X; ::_thesis: for e being Point of XX st (Proj (TrivExt D)) . e in the carrier of (space D) holds
e in the carrier of X
let e be Point of XX; ::_thesis: ( (Proj (TrivExt D)) . e in the carrier of (space D) implies e in the carrier of X )
assume (Proj (TrivExt D)) . e in the carrier of (space D) ; ::_thesis: e in the carrier of X
then A1: (Proj (TrivExt D)) . e in D by Def7;
e in (Proj (TrivExt D)) . e by EQREL_1:def_9;
hence e in the carrier of X by A1; ::_thesis: verum
end;
theorem Th37: :: BORSUK_1:37
for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for e being set st e in the carrier of X holds
(Proj (TrivExt D)) . e in the carrier of (space D)
proof
let XX be non empty TopSpace; ::_thesis: for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for e being set st e in the carrier of X holds
(Proj (TrivExt D)) . e in the carrier of (space D)
let X be non empty SubSpace of XX; ::_thesis: for D being non empty a_partition of the carrier of X
for e being set st e in the carrier of X holds
(Proj (TrivExt D)) . e in the carrier of (space D)
let D be non empty a_partition of the carrier of X; ::_thesis: for e being set st e in the carrier of X holds
(Proj (TrivExt D)) . e in the carrier of (space D)
let e be set ; ::_thesis: ( e in the carrier of X implies (Proj (TrivExt D)) . e in the carrier of (space D) )
assume A1: e in the carrier of X ; ::_thesis: (Proj (TrivExt D)) . e in the carrier of (space D)
then reconsider x = e as Point of X ;
the carrier of X c= the carrier of XX by Th1;
then (Proj D) . x = (Proj (TrivExt D)) . x by A1, Th33;
hence (Proj (TrivExt D)) . e in the carrier of (space D) ; ::_thesis: verum
end;
begin
definition
let X be non empty TopSpace;
mode u.s.c._decomposition of X -> non empty a_partition of the carrier of X means :Def10: :: BORSUK_1:def 10
for A being Subset of X st A in it holds
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 it & B meets W holds
B c= W ) );
correctness
existence
ex b1 being non empty a_partition of the carrier of X st
for A being Subset of X st A in b1 holds
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 b1 & B meets W holds
B c= W ) );
proof
take TrivDecomp X ; ::_thesis: for A being Subset of X st A in TrivDecomp X holds
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 ) )
thus for A being Subset of X st A in TrivDecomp X holds
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 ) ) by Lm1; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines u.s.c._decomposition BORSUK_1:def_10_:_
for X being non empty TopSpace
for b2 being non empty a_partition of the carrier of X holds
( b2 is u.s.c._decomposition of X iff for A being Subset of X st A in b2 holds
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 b2 & B meets W holds
B c= W ) ) );
theorem Th38: :: BORSUK_1:38
for X being non empty TopSpace
for D being u.s.c._decomposition of X
for t being Point of (space D)
for G being a_neighborhood of (Proj D) " {t} holds (Proj D) .: G is a_neighborhood of t
proof
let X be non empty TopSpace; ::_thesis: for D being u.s.c._decomposition of X
for t being Point of (space D)
for G being a_neighborhood of (Proj D) " {t} holds (Proj D) .: G is a_neighborhood of t
let D be u.s.c._decomposition of X; ::_thesis: for t being Point of (space D)
for G being a_neighborhood of (Proj D) " {t} holds (Proj D) .: G is a_neighborhood of t
let t be Point of (space D); ::_thesis: for G being a_neighborhood of (Proj D) " {t} holds (Proj D) .: G is a_neighborhood of t
let G be a_neighborhood of (Proj D) " {t}; ::_thesis: (Proj D) .: G is a_neighborhood of t
A1: the carrier of (space D) = D by Def7;
then (Proj D) " {t} = t by EQREL_1:66;
then consider W being Subset of X such that
A2: W is open and
A3: (Proj D) " {t} c= W and
A4: W c= G and
A5: for B being Subset of X st B in D & B meets W holds
B c= W by A1, Def10;
set Q = (Proj D) .: W;
A6: (Proj D) .: ((Proj D) " {t}) c= (Proj D) .: W by A3, RELAT_1:123;
union ((Proj D) .: W) = (proj D) " ((Proj D) .: W) by A1, EQREL_1:67
.= W by A5, EQREL_1:69 ;
then union ((Proj D) .: W) in the topology of X by A2, PRE_TOPC:def_2;
then (Proj D) .: W in the topology of (space D) by A1, Th27;
then A7: (Proj D) .: W is open by PRE_TOPC:def_2;
rng (Proj D) = the carrier of (space D) by Th30;
then {t} c= (Proj D) .: W by A6, FUNCT_1:77;
then A8: t in (Proj D) .: W by ZFMISC_1:31;
(Proj D) .: W c= (Proj D) .: G by A4, RELAT_1:123;
then t in Int ((Proj D) .: G) by A7, A8, TOPS_1:22;
hence (Proj D) .: G is a_neighborhood of t by CONNSP_2:def_1; ::_thesis: verum
end;
theorem Th39: :: BORSUK_1:39
for X being non empty TopSpace holds TrivDecomp X is u.s.c._decomposition of X
proof
let X be non empty TopSpace; ::_thesis: TrivDecomp X is u.s.c._decomposition of X
thus for A being Subset of X st A in TrivDecomp X holds
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 ) ) by Lm1; :: according to BORSUK_1:def_10 ::_thesis: verum
end;
definition
let X be TopSpace;
let IT be SubSpace of X;
attrIT is closed means :Def11: :: BORSUK_1:def 11
for A being Subset of X st A = the carrier of IT holds
A is closed ;
end;
:: deftheorem Def11 defines closed BORSUK_1:def_11_:_
for X being TopSpace
for IT being SubSpace of X holds
( IT is closed iff for A being Subset of X st A = the carrier of IT holds
A is closed );
Lm2: for T being TopStruct holds TopStruct(# the carrier of T, the topology of T #) is SubSpace of T
proof
let T be TopStruct ; ::_thesis: TopStruct(# the carrier of T, the topology of T #) is SubSpace of T
set S = TopStruct(# the carrier of T, the topology of T #);
thus [#] TopStruct(# the carrier of T, the topology of T #) c= [#] T ; :: according to PRE_TOPC:def_4 ::_thesis: for b1 being Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #) holds
( ( not b1 in the topology of TopStruct(# the carrier of T, the topology of T #) or ex b2 being Element of bool the carrier of T st
( b2 in the topology of T & b1 = b2 /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) ) & ( for b2 being Element of bool the carrier of T holds
( not b2 in the topology of T or not b1 = b2 /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) or b1 in the topology of TopStruct(# the carrier of T, the topology of T #) ) )
let P be Subset of TopStruct(# the carrier of T, the topology of T #); ::_thesis: ( ( not P in the topology of TopStruct(# the carrier of T, the topology of T #) or ex b1 being Element of bool the carrier of T st
( b1 in the topology of T & P = b1 /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) ) & ( for b1 being Element of bool the carrier of T holds
( not b1 in the topology of T or not P = b1 /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) or P in the topology of TopStruct(# the carrier of T, the topology of T #) ) )
hereby ::_thesis: ( for b1 being Element of bool the carrier of T holds
( not b1 in the topology of T or not P = b1 /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) or P in the topology of TopStruct(# the carrier of T, the topology of T #) )
reconsider Q = P as Subset of T ;
assume A1: P in the topology of TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) )
take Q = Q; ::_thesis: ( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) )
thus Q in the topology of T by A1; ::_thesis: P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #))
thus P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) by XBOOLE_1:28; ::_thesis: verum
end;
given Q being Subset of T such that A2: ( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) ; ::_thesis: P in the topology of TopStruct(# the carrier of T, the topology of T #)
thus P in the topology of TopStruct(# the carrier of T, the topology of T #) by A2, XBOOLE_1:28; ::_thesis: verum
end;
registration
let X be TopSpace;
cluster strict TopSpace-like closed for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is strict & b1 is closed )
proof
reconsider Y = TopStruct(# the carrier of X, the topology of X #) as strict SubSpace of X by Lm2;
take Y ; ::_thesis: ( Y is strict & Y is closed )
Y is closed
proof
let A be Subset of X; :: according to BORSUK_1:def_11 ::_thesis: ( A = the carrier of Y implies A is closed )
assume A = the carrier of Y ; ::_thesis: A is closed
then A = [#] X ;
hence A is closed ; ::_thesis: verum
end;
hence ( Y is strict & Y is closed ) ; ::_thesis: verum
end;
end;
registration
let X be non empty TopSpace;
cluster non empty strict TopSpace-like closed for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is strict & b1 is closed & not b1 is empty )
proof
X | ([#] X) is closed
proof
let A be Subset of X; :: according to BORSUK_1:def_11 ::_thesis: ( A = the carrier of (X | ([#] X)) implies A is closed )
assume A = the carrier of (X | ([#] X)) ; ::_thesis: A is closed
then A = [#] (X | ([#] X))
.= [#] X by PRE_TOPC:def_5 ;
hence A is closed ; ::_thesis: verum
end;
hence ex b1 being SubSpace of X st
( b1 is strict & b1 is closed & not b1 is empty ) ; ::_thesis: verum
end;
end;
definition
let XX be non empty TopSpace;
let X be non empty closed SubSpace of XX;
let D be u.s.c._decomposition of X;
:: original: TrivExt
redefine func TrivExt D -> u.s.c._decomposition of XX;
correctness
coherence
TrivExt D is u.s.c._decomposition of XX;
proof
let A be Subset of XX; :: according to BORSUK_1:def_10 ::_thesis: ( A in TrivExt D implies for V being a_neighborhood of A ex W being Subset of XX st
( W is open & A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) ) )
assume A1: A in TrivExt D ; ::_thesis: for V being a_neighborhood of A ex W being Subset of XX st
( W is open & A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) )
let V be a_neighborhood of A; ::_thesis: ex W being Subset of XX st
( W is open & A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) )
A2: A c= Int V by CONNSP_2:def_2;
A3: Int V c= V by TOPS_1:16;
now__::_thesis:_ex_H_being_Element_of_bool_the_carrier_of_XX_st_
(_H_is_open_&_A_c=_H_&_H_c=_V_&_(_for_B_being_Subset_of_XX_st_B_in_TrivExt_D_&_B_meets_H_holds_
B_c=_H_)_)
percases ( A in D or ex x being Point of XX st
( not x in [#] X & A = {x} ) ) by A1, Th31;
supposeA4: A in D ; ::_thesis: ex H being Element of bool the carrier of XX st
( H is open & A c= H & H c= V & ( for B being Subset of XX st B in TrivExt D & B meets H holds
B c= H ) )
then reconsider C = A as Subset of X ;
reconsider E = (Int V) /\ ([#] X) as Subset of X ;
( E is open & C c= E ) by A2, TOPS_2:24, XBOOLE_1:19;
then C c= Int E by TOPS_1:23;
then E is a_neighborhood of C by CONNSP_2:def_2;
then consider W being Subset of X such that
A5: W is open and
A6: C c= W and
A7: W c= E and
A8: for B being Subset of X st B in D & B meets W holds
B c= W by A4, Def10;
consider G being Subset of XX such that
A9: G is open and
A10: W = G /\ ([#] X) by A5, TOPS_2:24;
take H = G /\ (Int V); ::_thesis: ( H is open & A c= H & H c= V & ( for B being Subset of XX st B in TrivExt D & B meets H holds
B c= H ) )
thus H is open by A9; ::_thesis: ( A c= H & H c= V & ( for B being Subset of XX st B in TrivExt D & B meets H holds
B c= H ) )
A11: W c= G by A10, XBOOLE_1:17;
then C c= G by A6, XBOOLE_1:1;
hence A c= H by A2, XBOOLE_1:19; ::_thesis: ( H c= V & ( for B being Subset of XX st B in TrivExt D & B meets H holds
B c= H ) )
H c= Int V by XBOOLE_1:17;
hence H c= V by A3, XBOOLE_1:1; ::_thesis: for B being Subset of XX st B in TrivExt D & B meets H holds
B c= H
let B be Subset of XX; ::_thesis: ( B in TrivExt D & B meets H implies B c= H )
assume that
A12: B in TrivExt D and
A13: B meets H ; ::_thesis: B c= H
E c= Int V by XBOOLE_1:17;
then W c= Int V by A7, XBOOLE_1:1;
then A14: W c= H by A11, XBOOLE_1:19;
now__::_thesis:_B_c=_H
percases ( B in D or ex y being Point of XX st
( not y in [#] X & B = {y} ) ) by A12, Th31;
supposeA15: B in D ; ::_thesis: B c= H
B meets G by A13, XBOOLE_1:74;
then B meets W by A10, A15, XBOOLE_1:77;
then B c= W by A8, A15;
hence B c= H by A14, XBOOLE_1:1; ::_thesis: verum
end;
suppose ex y being Point of XX st
( not y in [#] X & B = {y} ) ; ::_thesis: B c= H
then consider y being Point of XX such that
not y in [#] X and
A16: B = {y} ;
y in H by A13, A16, ZFMISC_1:50;
hence B c= H by A16, ZFMISC_1:31; ::_thesis: verum
end;
end;
end;
hence B c= H ; ::_thesis: verum
end;
supposeA17: ex x being Point of XX st
( not x in [#] X & A = {x} ) ; ::_thesis: ex W being Element of bool the carrier of XX st
( W is open & A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) )
[#] X c= [#] XX by PRE_TOPC:def_4;
then reconsider C = [#] X as Subset of XX ;
take W = (Int V) \ C; ::_thesis: ( W is open & A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) )
C is closed by Def11;
then (Int V) /\ (C `) is open ;
hence W is open by SUBSET_1:13; ::_thesis: ( A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) )
consider x being Point of XX such that
A18: not x in [#] X and
A19: A = {x} by A17;
x in A by A19, TARSKI:def_1;
then x in W by A2, A18, XBOOLE_0:def_5;
hence A c= W by A19, ZFMISC_1:31; ::_thesis: ( W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) )
W c= Int V by XBOOLE_1:36;
hence W c= V by A3, XBOOLE_1:1; ::_thesis: for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W
let B be Subset of XX; ::_thesis: ( B in TrivExt D & B meets W implies B c= W )
assume that
A20: B in TrivExt D and
A21: B meets W ; ::_thesis: B c= W
now__::_thesis:_not_B_in_D
A22: W misses C by XBOOLE_1:79;
assume B in D ; ::_thesis: contradiction
hence contradiction by A21, A22, XBOOLE_1:63; ::_thesis: verum
end;
then consider y being Point of XX such that
not y in [#] X and
A23: B = {y} by A20, Th31;
y in W by A21, A23, ZFMISC_1:50;
hence B c= W by A23, ZFMISC_1:31; ::_thesis: verum
end;
end;
end;
hence ex W being Subset of XX st
( W is open & A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) ) ; ::_thesis: verum
end;
end;
definition
let X be non empty TopSpace;
let IT be u.s.c._decomposition of X;
attrIT is DECOMPOSITION-like means :Def12: :: BORSUK_1:def 12
for A being Subset of X st A in IT holds
A is compact ;
end;
:: deftheorem Def12 defines DECOMPOSITION-like BORSUK_1:def_12_:_
for X being non empty TopSpace
for IT being u.s.c._decomposition of X holds
( IT is DECOMPOSITION-like iff for A being Subset of X st A in IT holds
A is compact );
registration
let X be non empty TopSpace;
cluster non empty with_non-empty_elements DECOMPOSITION-like for u.s.c._decomposition of X;
existence
ex b1 being u.s.c._decomposition of X st b1 is DECOMPOSITION-like
proof
reconsider D = TrivDecomp X as u.s.c._decomposition of X by Th39;
take D ; ::_thesis: D is DECOMPOSITION-like
let A be Subset of X; :: according to BORSUK_1:def_12 ::_thesis: ( A in D implies A is compact )
assume A in D ; ::_thesis: A is compact
then ex x being Point of X st A = {x} by Th26;
hence A is compact ; ::_thesis: verum
end;
end;
definition
let X be non empty TopSpace;
mode DECOMPOSITION of X is DECOMPOSITION-like u.s.c._decomposition of X;
end;
definition
let XX be non empty TopSpace;
let X be non empty closed SubSpace of XX;
let D be DECOMPOSITION of X;
:: original: TrivExt
redefine func TrivExt D -> DECOMPOSITION of XX;
correctness
coherence
TrivExt D is DECOMPOSITION of XX;
proof
TrivExt D is DECOMPOSITION-like
proof
let A be Subset of XX; :: according to BORSUK_1:def_12 ::_thesis: ( A in TrivExt D implies A is compact )
assume A in TrivExt D ; ::_thesis: A is compact
then consider W being Point of XX such that
A1: A = (proj (TrivExt D)) . W by EQREL_1:68;
A2: A = (Proj (TrivExt D)) . W by A1;
A3: the carrier of (space D) = D by Def7;
now__::_thesis:_A_is_compact
percases ( W in the carrier of X or not W in the carrier of X ) ;
suppose W in the carrier of X ; ::_thesis: A is compact
then reconsider W9 = W as Point of X ;
A4: A = (Proj D) . W9 by A2, Th33;
then reconsider B = A as Subset of X by A3, TARSKI:def_3;
B is compact by A3, A4, Def12;
hence A is compact by COMPTS_1:19; ::_thesis: verum
end;
suppose not W in the carrier of X ; ::_thesis: A is compact
then A = {W} by A2, Th34;
hence A is compact ; ::_thesis: verum
end;
end;
end;
hence A is compact ; ::_thesis: verum
end;
hence TrivExt D is DECOMPOSITION of XX ; ::_thesis: verum
end;
end;
definition
let X be non empty TopSpace;
let Y be non empty closed SubSpace of X;
let D be DECOMPOSITION of Y;
:: original: space
redefine func space D -> strict closed SubSpace of space (TrivExt D);
correctness
coherence
space D is strict closed SubSpace of space (TrivExt D);
proof
A1: the topology of (space (TrivExt D)) = { A where A is Subset of (TrivExt D) : union A in the topology of X } by Def7;
A2: the carrier of (space (TrivExt D)) = TrivExt D by Def7;
A3: the topology of (space D) = { A where A is Subset of D : union A in the topology of Y } by Def7;
A4: the carrier of (space D) = D by Def7;
A5: ( [#] (space D) = D & [#] (space (TrivExt D)) = TrivExt D ) by Def7;
now__::_thesis:_(_[#]_(space_D)_c=_[#]_(space_(TrivExt_D))_&_(_for_P_being_Subset_of_(space_D)_holds_
(_(_P_in_the_topology_of_(space_D)_implies_ex_Q_being_Subset_of_(space_(TrivExt_D))_st_
(_Q_in_the_topology_of_(space_(TrivExt_D))_&_P_=_Q_/\_([#]_(space_D))_)_)_&_(_ex_Q_being_Subset_of_(space_(TrivExt_D))_st_
(_Q_in_the_topology_of_(space_(TrivExt_D))_&_P_=_Q_/\_([#]_(space_D))_)_implies_P_in_the_topology_of_(space_D)_)_)_)_)
thus [#] (space D) c= [#] (space (TrivExt D)) by A5, XBOOLE_1:7; ::_thesis: for P being Subset of (space D) holds
( ( P in the topology of (space D) implies ex Q being Subset of (space (TrivExt D)) st
( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) ) & ( ex Q being Subset of (space (TrivExt D)) st
( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) implies P in the topology of (space D) ) )
let P be Subset of (space D); ::_thesis: ( ( P in the topology of (space D) implies ex Q being Subset of (space (TrivExt D)) st
( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) ) & ( ex Q being Subset of (space (TrivExt D)) st
( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) implies P in the topology of (space D) ) )
thus ( P in the topology of (space D) implies ex Q being Subset of (space (TrivExt D)) st
( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) ) ::_thesis: ( ex Q being Subset of (space (TrivExt D)) st
( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) implies P in the topology of (space D) )
proof
D c= TrivExt D by XBOOLE_1:7;
then A6: P c= TrivExt D by A4, XBOOLE_1:1;
assume P in the topology of (space D) ; ::_thesis: ex Q being Subset of (space (TrivExt D)) st
( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) )
then consider A being Subset of D such that
A7: P = A and
A8: union A in the topology of Y by A3;
reconsider B = union A as Subset of Y by A8;
consider C being Subset of X such that
A9: C in the topology of X and
A10: B = C /\ ([#] Y) by A8, PRE_TOPC:def_4;
{ {x} where x is Point of X : x in C \ ([#] Y) } c= TrivExt D
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { {x} where x is Point of X : x in C \ ([#] Y) } or e in TrivExt D )
assume e in { {x} where x is Point of X : x in C \ ([#] Y) } ; ::_thesis: e in TrivExt D
then consider x being Point of X such that
A11: e = {x} and
A12: x in C \ ([#] Y) ;
not x in the carrier of Y by A12, XBOOLE_0:def_5;
hence e in TrivExt D by A11, Th32; ::_thesis: verum
end;
then reconsider Q = P \/ { {x} where x is Point of X : x in C \ ([#] Y) } as Subset of (space (TrivExt D)) by A2, A6, XBOOLE_1:8;
take Q ; ::_thesis: ( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) )
now__::_thesis:_for_e_being_set_holds_
(_(_e_in_C_implies_ex_u_being_set_st_
(_e_in_u_&_u_in_Q_)_)_&_(_ex_u_being_set_st_
(_e_in_u_&_u_in_Q_)_implies_e_in_C_)_)
let e be set ; ::_thesis: ( ( e in C implies ex u being set st
( e in u & u in Q ) ) & ( ex u being set st
( e in u & u in Q ) implies e in C ) )
thus ( e in C implies ex u being set st
( e in u & u in Q ) ) ::_thesis: ( ex u being set st
( e in u & u in Q ) implies e in C )
proof
assume A13: e in C ; ::_thesis: ex u being set st
( e in u & u in Q )
then reconsider x = e as Point of X ;
now__::_thesis:_(_(_e_in_[#]_Y_&_ex_u_being_set_st_
(_e_in_u_&_u_in_Q_)_)_or_(_not_e_in_[#]_Y_&_ex_u_being_set_st_
(_e_in_u_&_u_in_Q_)_)_)
percases ( e in [#] Y or not e in [#] Y ) ;
case e in [#] Y ; ::_thesis: ex u being set st
( e in u & u in Q )
then e in B by A10, A13, XBOOLE_0:def_4;
then consider u being set such that
A14: ( e in u & u in P ) by A7, TARSKI:def_4;
take u = u; ::_thesis: ( e in u & u in Q )
thus ( e in u & u in Q ) by A14, XBOOLE_0:def_3; ::_thesis: verum
end;
caseA15: not e in [#] Y ; ::_thesis: ex u being set st
( e in u & u in Q )
take u = {e}; ::_thesis: ( e in u & u in Q )
thus e in u by TARSKI:def_1; ::_thesis: u in Q
x in C \ ([#] Y) by A13, A15, XBOOLE_0:def_5;
then u in { {y} where y is Point of X : y in C \ ([#] Y) } ;
hence u in Q by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence ex u being set st
( e in u & u in Q ) ; ::_thesis: verum
end;
given u being set such that A16: e in u and
A17: u in Q ; ::_thesis: e in C
now__::_thesis:_e_in_C
percases ( u in P or u in { {x} where x is Point of X : x in C \ ([#] Y) } ) by A17, XBOOLE_0:def_3;
suppose u in P ; ::_thesis: e in C
then e in B by A7, A16, TARSKI:def_4;
hence e in C by A10, XBOOLE_0:def_4; ::_thesis: verum
end;
suppose u in { {x} where x is Point of X : x in C \ ([#] Y) } ; ::_thesis: e in C
then consider x being Point of X such that
A18: u = {x} and
A19: x in C \ ([#] Y) ;
e = x by A16, A18, TARSKI:def_1;
hence e in C by A19, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
hence e in C ; ::_thesis: verum
end;
then C = union Q by TARSKI:def_4;
hence Q in the topology of (space (TrivExt D)) by A2, A1, A9; ::_thesis: P = Q /\ ([#] (space D))
P c= Q by XBOOLE_1:7;
hence P c= Q /\ ([#] (space D)) by XBOOLE_1:19; :: according to XBOOLE_0:def_10 ::_thesis: Q /\ ([#] (space D)) c= P
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in Q /\ ([#] (space D)) or e in P )
assume A20: e in Q /\ ([#] (space D)) ; ::_thesis: e in P
then A21: e in [#] (space D) ;
A22: now__::_thesis:_not_e_in__{__{x}_where_x_is_Point_of_X_:_x_in_C_\_([#]_Y)__}_
assume e in { {x} where x is Point of X : x in C \ ([#] Y) } ; ::_thesis: contradiction
then consider x being Point of X such that
A23: e = {x} and
A24: x in C \ ([#] Y) ;
A25: not x in the carrier of Y by A24, XBOOLE_0:def_5;
then not (Proj (TrivExt D)) . x in the carrier of (space D) by Th36;
hence contradiction by A21, A23, A25, Th34; ::_thesis: verum
end;
e in Q by A20, XBOOLE_0:def_4;
hence e in P by A22, XBOOLE_0:def_3; ::_thesis: verum
end;
given Q being Subset of (space (TrivExt D)) such that A26: Q in the topology of (space (TrivExt D)) and
A27: P = Q /\ ([#] (space D)) ; ::_thesis: P in the topology of (space D)
A28: union P is Subset of Y by A4, EQREL_1:61;
now__::_thesis:_for_e_being_set_holds_
(_(_e_in_(union_Q)_/\_([#]_Y)_implies_ex_u_being_set_st_
(_e_in_u_&_u_in_P_)_)_&_(_ex_u_being_set_st_
(_e_in_u_&_u_in_P_)_implies_e_in_(union_Q)_/\_([#]_Y)_)_)
let e be set ; ::_thesis: ( ( e in (union Q) /\ ([#] Y) implies ex u being set st
( e in u & u in P ) ) & ( ex u being set st
( e in u & u in P ) implies e in (union Q) /\ ([#] Y) ) )
thus ( e in (union Q) /\ ([#] Y) implies ex u being set st
( e in u & u in P ) ) ::_thesis: ( ex u being set st
( e in u & u in P ) implies e in (union Q) /\ ([#] Y) )
proof
assume A29: e in (union Q) /\ ([#] Y) ; ::_thesis: ex u being set st
( e in u & u in P )
then A30: (Proj (TrivExt D)) . e in the carrier of (space D) by Th37;
e in union Q by A29, XBOOLE_0:def_4;
then consider u being set such that
A31: e in u and
A32: u in Q by TARSKI:def_4;
take u ; ::_thesis: ( e in u & u in P )
thus e in u by A31; ::_thesis: u in P
u is Element of TrivExt D by A32, Def7;
then u = (Proj (TrivExt D)) . e by A31, EQREL_1:65;
hence u in P by A27, A32, A30, XBOOLE_0:def_4; ::_thesis: verum
end;
given u being set such that A33: e in u and
A34: u in P ; ::_thesis: e in (union Q) /\ ([#] Y)
u in Q by A27, A34, XBOOLE_0:def_4;
then A35: e in union Q by A33, TARSKI:def_4;
e in union P by A33, A34, TARSKI:def_4;
hence e in (union Q) /\ ([#] Y) by A28, A35, XBOOLE_0:def_4; ::_thesis: verum
end;
then A36: union P = (union Q) /\ ([#] Y) by TARSKI:def_4;
ex A being Subset of (TrivExt D) st
( Q = A & union A in the topology of X ) by A1, A26;
then union P in the topology of Y by A36, PRE_TOPC:def_4;
hence P in the topology of (space D) by A4, A3; ::_thesis: verum
end;
then reconsider T = space D as SubSpace of space (TrivExt D) by PRE_TOPC:def_4;
T is closed
proof
let A be Subset of (space (TrivExt D)); :: according to BORSUK_1:def_11 ::_thesis: ( A = the carrier of T implies A is closed )
assume A37: A = the carrier of T ; ::_thesis: A is closed
reconsider C = A ` as Subset of (TrivExt D) by Def7;
reconsider B = union A as Subset of X by A2, EQREL_1:61;
B = the carrier of Y by A4, A37, EQREL_1:def_4;
then B is closed by Def11;
then A38: B ` in the topology of X by PRE_TOPC:def_2;
union C = B ` by A2, EQREL_1:63;
then A ` in the topology of (space (TrivExt D)) by A38, Th27;
then A ` is open by PRE_TOPC:def_2;
hence A is closed by TOPS_1:3; ::_thesis: verum
end;
hence space D is strict closed SubSpace of space (TrivExt D) ; ::_thesis: verum
end;
end;
begin
Lm3: TopSpaceMetr RealSpace = TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #)
by PCOMPS_1:def_5;
definition
func I[01] -> TopStruct means :Def13: :: BORSUK_1:def 13
for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
it = (TopSpaceMetr RealSpace) | P;
existence
ex b1 being TopStruct st
for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
b1 = (TopSpaceMetr RealSpace) | P
proof
reconsider P = [.0,1.] as non empty Subset of (TopSpaceMetr RealSpace) by Lm3, METRIC_1:def_13, XXREAL_1:1;
take (TopSpaceMetr RealSpace) | P ; ::_thesis: for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
(TopSpaceMetr RealSpace) | P = (TopSpaceMetr RealSpace) | P
thus for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
(TopSpaceMetr RealSpace) | P = (TopSpaceMetr RealSpace) | P ; ::_thesis: verum
end;
uniqueness
for b1, b2 being TopStruct st ( for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
b1 = (TopSpaceMetr RealSpace) | P ) & ( for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
b2 = (TopSpaceMetr RealSpace) | P ) holds
b1 = b2
proof
reconsider P = [.0,1.] as Subset of (TopSpaceMetr RealSpace) by Lm3, METRIC_1:def_13;
let I1, I2 be TopStruct ; ::_thesis: ( ( for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
I1 = (TopSpaceMetr RealSpace) | P ) & ( for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
I2 = (TopSpaceMetr RealSpace) | P ) implies I1 = I2 )
assume that
A1: for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
I1 = (TopSpaceMetr RealSpace) | P and
A2: for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
I2 = (TopSpaceMetr RealSpace) | P ; ::_thesis: I1 = I2
I1 = (TopSpaceMetr RealSpace) | P by A1;
hence I1 = I2 by A2; ::_thesis: verum
end;
end;
:: deftheorem Def13 defines I[01] BORSUK_1:def_13_:_
for b1 being TopStruct holds
( b1 = I[01] iff for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
b1 = (TopSpaceMetr RealSpace) | P );
registration
cluster I[01] -> non empty strict TopSpace-like ;
coherence
( I[01] is strict & not I[01] is empty & I[01] is TopSpace-like )
proof
reconsider P = [.0,1.] as non empty Subset of (TopSpaceMetr RealSpace) by Lm3, METRIC_1:def_13, XXREAL_1:1;
I[01] = (TopSpaceMetr RealSpace) | P by Def13;
hence ( I[01] is strict & not I[01] is empty & I[01] is TopSpace-like ) ; ::_thesis: verum
end;
end;
theorem Th40: :: BORSUK_1:40
the carrier of I[01] = [.0,1.]
proof
reconsider P = [.0,1.] as Subset of (TopSpaceMetr RealSpace) by Lm3, METRIC_1:def_13;
A1: I[01] = (TopSpaceMetr RealSpace) | P by Def13;
thus the carrier of I[01] = [#] I[01]
.= [.0,1.] by A1, PRE_TOPC:def_5 ; ::_thesis: verum
end;
definition
func 0[01] -> Point of I[01] equals :: BORSUK_1:def 14
0 ;
coherence
0 is Point of I[01] by Th40, XXREAL_1:1;
func 1[01] -> Point of I[01] equals :: BORSUK_1:def 15
1;
coherence
1 is Point of I[01] by Th40, XXREAL_1:1;
end;
:: deftheorem defines 0[01] BORSUK_1:def_14_:_
0[01] = 0 ;
:: deftheorem defines 1[01] BORSUK_1:def_15_:_
1[01] = 1;
definition
let A be non empty TopSpace;
let B be non empty SubSpace of A;
let F be Function of A,B;
attrF is being_a_retraction means :Def16: :: BORSUK_1:def 16
for W being Point of A st W in the carrier of B holds
F . W = W;
end;
:: deftheorem Def16 defines being_a_retraction BORSUK_1:def_16_:_
for A being non empty TopSpace
for B being non empty SubSpace of A
for F being Function of A,B holds
( F is being_a_retraction iff for W being Point of A st W in the carrier of B holds
F . W = W );
definition
let X be non empty TopSpace;
let Y be non empty SubSpace of X;
predY is_a_retract_of X means :: BORSUK_1:def 17
ex F being continuous Function of X,Y st F is being_a_retraction ;
predY is_an_SDR_of X means :: BORSUK_1:def 18
ex H being continuous Function of [:X,I[01]:],X st
for A being Point of X holds
( H . [A,0[01]] = A & H . [A,1[01]] in the carrier of Y & ( A in the carrier of Y implies for T being Point of I[01] holds H . [A,T] = A ) );
end;
:: deftheorem defines is_a_retract_of BORSUK_1:def_17_:_
for X being non empty TopSpace
for Y being non empty SubSpace of X holds
( Y is_a_retract_of X iff ex F being continuous Function of X,Y st F is being_a_retraction );
:: deftheorem defines is_an_SDR_of BORSUK_1:def_18_:_
for X being non empty TopSpace
for Y being non empty SubSpace of X holds
( Y is_an_SDR_of X iff ex H being continuous Function of [:X,I[01]:],X st
for A being Point of X holds
( H . [A,0[01]] = A & H . [A,1[01]] in the carrier of Y & ( A in the carrier of Y implies for T being Point of I[01] holds H . [A,T] = A ) ) );
theorem :: BORSUK_1:41
for XX being non empty TopSpace
for X being non empty closed SubSpace of XX
for D being DECOMPOSITION of X st X is_a_retract_of XX holds
space D is_a_retract_of space (TrivExt D)
proof
let XX be non empty TopSpace; ::_thesis: for X being non empty closed SubSpace of XX
for D being DECOMPOSITION of X st X is_a_retract_of XX holds
space D is_a_retract_of space (TrivExt D)
let X be non empty closed SubSpace of XX; ::_thesis: for D being DECOMPOSITION of X st X is_a_retract_of XX holds
space D is_a_retract_of space (TrivExt D)
let D be DECOMPOSITION of X; ::_thesis: ( X is_a_retract_of XX implies space D is_a_retract_of space (TrivExt D) )
thus ( X is_a_retract_of XX implies space D is_a_retract_of space (TrivExt D) ) ::_thesis: verum
proof
given R being continuous Function of XX,X such that A1: R is being_a_retraction ; :: according to BORSUK_1:def_17 ::_thesis: space D is_a_retract_of space (TrivExt D)
now__::_thesis:_for_xx,_xx9_being_Point_of_XX_holds_
(_not_(Proj_(TrivExt_D))_._xx_=_(Proj_(TrivExt_D))_._xx9_or_not_((Proj_D)_*_R)_._xx_<>_((Proj_D)_*_R)_._xx9_)
given xx, xx9 being Point of XX such that A2: ( (Proj (TrivExt D)) . xx = (Proj (TrivExt D)) . xx9 & ((Proj D) * R) . xx <> ((Proj D) * R) . xx9 ) ; ::_thesis: contradiction
xx in the carrier of X by A2, Th35;
then R . xx = xx by A1, Def16;
then A3: (Proj D) . xx = ((Proj D) * R) . xx by FUNCT_2:15;
xx9 in the carrier of X by A2, Th35;
then A4: R . xx9 = xx9 by A1, Def16;
( (Proj (TrivExt D)) . xx = (Proj D) . xx & (Proj (TrivExt D)) . xx9 = (Proj D) . xx9 ) by A2, Th33, Th35;
hence contradiction by A2, A4, A3, FUNCT_2:15; ::_thesis: verum
end;
then consider F being Function of the carrier of (space (TrivExt D)), the carrier of (space D) such that
A5: F * (Proj (TrivExt D)) = (Proj D) * R by EQREL_1:56;
reconsider F = F as Function of (space (TrivExt D)),(space D) ;
F is continuous
proof
let W be Point of (space (TrivExt D)); :: according to BORSUK_1:def_1 ::_thesis: for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G
let G be a_neighborhood of F . W; ::_thesis: ex H being a_neighborhood of W st F .: H c= G
reconsider GG = ((Proj D) * R) " G as a_neighborhood of (Proj (TrivExt D)) " {W} by A5, Th4, EQREL_1:57;
reconsider V9 = (Proj (TrivExt D)) .: GG as a_neighborhood of W by Th38;
take V = V9; ::_thesis: F .: V c= G
F .: V = ((Proj D) * R) .: GG by A5, RELAT_1:126;
hence F .: V c= G by FUNCT_1:75; ::_thesis: verum
end;
then reconsider F9 = F as continuous Function of (space (TrivExt D)),(space D) ;
take F9 ; :: according to BORSUK_1:def_17 ::_thesis: F9 is being_a_retraction
let W be Point of (space (TrivExt D)); :: according to BORSUK_1:def_16 ::_thesis: ( W in the carrier of (space D) implies F9 . W = W )
consider W9 being Point of XX such that
A6: (Proj (TrivExt D)) . W9 = W by Th29;
assume A7: W in the carrier of (space D) ; ::_thesis: F9 . W = W
then W9 in the carrier of X by A6, Th36;
then A8: W9 = R . W9 by A1, Def16;
A9: F9 . W = (F * (Proj (TrivExt D))) . W9 by A6, FUNCT_2:15;
(Proj D) . W9 = (Proj (TrivExt D)) . W9 by A6, A7, Th33, Th36;
hence F9 . W = W by A5, A6, A8, A9, FUNCT_2:15; ::_thesis: verum
end;
end;
theorem :: BORSUK_1:42
for XX being non empty TopSpace
for X being non empty closed SubSpace of XX
for D being DECOMPOSITION of X st X is_an_SDR_of XX holds
space D is_an_SDR_of space (TrivExt D)
proof
let XX be non empty TopSpace; ::_thesis: for X being non empty closed SubSpace of XX
for D being DECOMPOSITION of X st X is_an_SDR_of XX holds
space D is_an_SDR_of space (TrivExt D)
let X be non empty closed SubSpace of XX; ::_thesis: for D being DECOMPOSITION of X st X is_an_SDR_of XX holds
space D is_an_SDR_of space (TrivExt D)
let D be DECOMPOSITION of X; ::_thesis: ( X is_an_SDR_of XX implies space D is_an_SDR_of space (TrivExt D) )
given CH1 being continuous Function of [:XX,I[01]:],XX such that A1: for A being Point of XX holds
( CH1 . [A,0[01]] = A & CH1 . [A,1[01]] in the carrier of X & ( A in the carrier of X implies for T being Point of I[01] holds CH1 . [A,T] = A ) ) ; :: according to BORSUK_1:def_18 ::_thesis: space D is_an_SDR_of space (TrivExt D)
the carrier of [:XX,I[01]:] = [: the carrier of XX, the carrier of I[01]:] by Def2;
then reconsider II = [:(Proj (TrivExt D)),(id the carrier of I[01]):] as Function of the carrier of [:XX,I[01]:], the carrier of [:(space (TrivExt D)),I[01]:] by Def2;
now__::_thesis:_for_xx,_xx9_being_Point_of_[:XX,I[01]:]_holds_
(_not_II_._xx_=_II_._xx9_or_not_((Proj_(TrivExt_D))_*_CH1)_._xx_<>_((Proj_(TrivExt_D))_*_CH1)_._xx9_)
given xx, xx9 being Point of [:XX,I[01]:] such that A2: II . xx = II . xx9 and
A3: ((Proj (TrivExt D)) * CH1) . xx <> ((Proj (TrivExt D)) * CH1) . xx9 ; ::_thesis: contradiction
A4: ( ((Proj (TrivExt D)) * CH1) . xx = (Proj (TrivExt D)) . (CH1 . xx) & ((Proj (TrivExt D)) * CH1) . xx9 = (Proj (TrivExt D)) . (CH1 . xx9) ) by FUNCT_2:15;
consider x being Point of XX, t being Point of I[01] such that
A5: xx = [x,t] by Th10;
consider x9 being Point of XX, t9 being Point of I[01] such that
A6: xx9 = [x9,t9] by Th10;
A7: ( II . (x,t) = [((Proj (TrivExt D)) . x),t] & II . (x9,t9) = [((Proj (TrivExt D)) . x9),t9] ) by EQREL_1:58;
then ( t = t9 & (Proj (TrivExt D)) . x = (Proj (TrivExt D)) . x9 ) by A2, A5, A6, XTUPLE_0:1;
then ( CH1 . xx = x & CH1 . xx9 = x9 ) by A1, A3, A5, A6, Th35;
hence contradiction by A2, A3, A5, A6, A7, A4, XTUPLE_0:1; ::_thesis: verum
end;
then consider THETA being Function of the carrier of [:(space (TrivExt D)),I[01]:], the carrier of (space (TrivExt D)) such that
A8: (Proj (TrivExt D)) * CH1 = THETA * II by EQREL_1:56;
reconsider THETA = THETA as Function of [:(space (TrivExt D)),I[01]:],(space (TrivExt D)) ;
THETA is continuous
proof
let WT be Point of [:(space (TrivExt D)),I[01]:]; :: according to BORSUK_1:def_1 ::_thesis: for G being a_neighborhood of THETA . WT ex H being a_neighborhood of WT st THETA .: H c= G
reconsider xt9 = WT as Element of [: the carrier of (space (TrivExt D)), the carrier of I[01]:] by Def2;
let G be a_neighborhood of THETA . WT; ::_thesis: ex H being a_neighborhood of WT st THETA .: H c= G
reconsider FF = (Proj (TrivExt D)) * CH1 as continuous Function of [:XX,I[01]:],(space (TrivExt D)) ;
consider W being Point of (space (TrivExt D)), T being Point of I[01] such that
A9: WT = [W,T] by Th10;
II " {xt9} = [:((Proj (TrivExt D)) " {W}),{T}:] by A9, EQREL_1:60;
then reconsider GG = FF " G as a_neighborhood of [:((Proj (TrivExt D)) " {W}),{T}:] by A8, Th4, EQREL_1:57;
W in the carrier of (space (TrivExt D)) ;
then A10: W in TrivExt D by Def7;
then (Proj (TrivExt D)) " {W} = W by EQREL_1:66;
then (Proj (TrivExt D)) " {W} is compact by A10, Def12;
then consider U being a_neighborhood of (Proj (TrivExt D)) " {W}, V being a_neighborhood of T such that
A11: [:U,V:] c= GG by Th25;
reconsider H9 = (Proj (TrivExt D)) .: U as a_neighborhood of W by Th38;
reconsider H99 = [:H9,V:] as a_neighborhood of WT by A9;
take H = H99; ::_thesis: THETA .: H c= G
II .: [:U,V:] = [:((Proj (TrivExt D)) .: U),V:] by EQREL_1:59;
then A12: ( ((Proj (TrivExt D)) * CH1) .: GG c= G & THETA .: H = ((Proj (TrivExt D)) * CH1) .: [:U,V:] ) by A8, FUNCT_1:75, RELAT_1:126;
((Proj (TrivExt D)) * CH1) .: [:U,V:] c= ((Proj (TrivExt D)) * CH1) .: GG by A11, RELAT_1:123;
hence THETA .: H c= G by A12, XBOOLE_1:1; ::_thesis: verum
end;
then reconsider THETA9 = THETA as continuous Function of [:(space (TrivExt D)),I[01]:],(space (TrivExt D)) ;
take THETA99 = THETA9; :: according to BORSUK_1:def_18 ::_thesis: for A being Point of (space (TrivExt D)) holds
( THETA99 . [A,0[01]] = A & THETA99 . [A,1[01]] in the carrier of (space D) & ( A in the carrier of (space D) implies for T being Point of I[01] holds THETA99 . [A,T] = A ) )
let W be Point of (space (TrivExt D)); ::_thesis: ( THETA99 . [W,0[01]] = W & THETA99 . [W,1[01]] in the carrier of (space D) & ( W in the carrier of (space D) implies for T being Point of I[01] holds THETA99 . [W,T] = W ) )
consider W9 being Point of XX such that
A13: (Proj (TrivExt D)) . W9 = W by Th29;
II . (W9,0[01]) = [W,0[01]] by A13, EQREL_1:58;
then A14: (THETA9 * II) . [W9,0[01]] = THETA9 . [W,0[01]] by FUNCT_2:15;
CH1 . (W9,0[01]) = W9 by A1;
hence THETA99 . [W,0[01]] = W by A8, A13, A14, FUNCT_2:15; ::_thesis: ( THETA99 . [W,1[01]] in the carrier of (space D) & ( W in the carrier of (space D) implies for T being Point of I[01] holds THETA99 . [W,T] = W ) )
A15: CH1 . [W9,1[01]] in the carrier of X by A1;
II . (W9,1[01]) = [W,1[01]] by A13, EQREL_1:58;
then A16: (THETA9 * II) . [W9,1[01]] = THETA9 . [W,1[01]] by FUNCT_2:15;
(THETA9 * II) . [W9,1[01]] = (Proj (TrivExt D)) . (CH1 . [W9,1[01]]) by A8, FUNCT_2:15;
hence THETA99 . [W,1[01]] in the carrier of (space D) by A16, A15, Th37; ::_thesis: ( W in the carrier of (space D) implies for T being Point of I[01] holds THETA99 . [W,T] = W )
assume A17: W in the carrier of (space D) ; ::_thesis: for T being Point of I[01] holds THETA99 . [W,T] = W
let T be Point of I[01]; ::_thesis: THETA99 . [W,T] = W
II . (W9,T) = [W,T] by A13, EQREL_1:58;
then A18: (THETA9 * II) . [W9,T] = THETA9 . [W,T] by FUNCT_2:15;
CH1 . (W9,T) = W9 by A1, A13, A17, Th36;
hence THETA99 . [W,T] = W by A8, A13, A18, FUNCT_2:15; ::_thesis: verum
end;
theorem :: BORSUK_1:43
for r being real number holds
( ( 0 <= r & r <= 1 ) iff r in the carrier of I[01] )
proof
let r be real number ; ::_thesis: ( ( 0 <= r & r <= 1 ) iff r in the carrier of I[01] )
A1: [.0,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by RCOMP_1:def_1;
r is Real by XREAL_0:def_1;
hence ( 0 <= r & r <= 1 implies r in the carrier of I[01] ) by A1, Th40; ::_thesis: ( r in the carrier of I[01] implies ( 0 <= r & r <= 1 ) )
assume r in the carrier of I[01] ; ::_thesis: ( 0 <= r & r <= 1 )
then ex r2 being Real st
( r2 = r & 0 <= r2 & r2 <= 1 ) by A1, Th40;
hence ( 0 <= r & r <= 1 ) ; ::_thesis: verum
end;