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