Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

### The abstract of the Mizar article:

### A Borsuk Theorem on Homotopy Types

**by****Andrzej Trybulec**- Received August 1, 1991
- MML identifier: BORSUK_1

- [ Mizar article, MML identifier index ]

environ vocabulary BOOLE, FUNCT_1, RELAT_1, FUNCOP_1, FUNCT_3, MCART_1, SETFAM_1, TARSKI, SUBSET_1, EQREL_1, PRE_TOPC, ORDINAL2, CONNSP_2, TOPS_1, COMPTS_1, FINSET_1, PCOMPS_1, METRIC_1, RCOMP_1, BORSUK_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, FUNCT_1, MCART_1, DOMAIN_1, RCOMP_1, SETFAM_1, STRUCT_0, METRIC_1, PCOMPS_1, PARTFUN1, EQREL_1, FUNCT_2, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, CONNSP_2, FUNCT_3, FUNCOP_1; constructors FINSET_1, DOMAIN_1, RCOMP_1, PCOMPS_1, EQREL_1, CAT_1, TOPS_1, TOPS_2, COMPTS_1, CONNSP_2, PARTFUN1, FUNCT_3, XCMPLX_0, MEMBERED; clusters SUBSET_1, PCOMPS_1, EQREL_1, FINSET_1, PRE_TOPC, STRUCT_0, METRIC_1, FUNCOP_1, RELSET_1, XBOOLE_0, MEMBERED, ZFMISC_1, PARTFUN1, FUNCT_2; requirements NUMERALS, REAL, BOOLE, SUBSET; begin :: :: Preliminaries :: reserve e,u,X,Y,X1,X2,Y1,Y2 for set, A for Subset of X; canceled; theorem :: BORSUK_1:2 e in [:X1,Y1:] & e in [:X2,Y2:] implies e in [:X1 /\ X2, Y1 /\ Y2:]; theorem :: BORSUK_1:3 (id X).:A = A; theorem :: BORSUK_1:4 (id X)"A = A; theorem :: BORSUK_1:5 for F being Function st X c= F"X1 holds F.:X c= X1; theorem :: BORSUK_1:6 (X --> u).:X1 c= {u}; theorem :: BORSUK_1:7 [:X1,X2:] c= [:Y1,Y2:] & [:X1,X2:] <> {} implies X1 c= Y1 & X2 c= Y2; canceled; theorem :: BORSUK_1:9 e c= [:X,Y:] implies (.:pr1(X,Y)).e = pr1(X,Y).:e; theorem :: BORSUK_1:10 e c= [:X,Y:] implies (.:pr2(X,Y)).e = pr2(X,Y).:e; canceled; theorem :: BORSUK_1:12 for X1 being Subset of X, Y1 being Subset of Y st [:X1,Y1:] <> {} holds pr1(X,Y).:[:X1,Y1:] = X1 & pr2(X,Y).:[:X1,Y1:] = Y1; theorem :: BORSUK_1:13 for X1 being Subset of X, Y1 being Subset of Y st [:X1,Y1:] <> {} holds .:pr1(X,Y). [:X1,Y1:] = X1 & .:pr2(X,Y). [:X1,Y1:] = Y1; theorem :: BORSUK_1:14 for A being Subset of [:X,Y:], H being Subset-Family of [:X,Y:] st for e st e in H holds e c= A & ex X1 being Subset of X, Y1 being Subset of Y st e =[:X1,Y1:] holds [:union(.:pr1(X,Y).:H), meet(.:pr2(X,Y).:H):] c= A; theorem :: BORSUK_1:15 for A being Subset of [:X,Y:], H being Subset-Family of [:X,Y:] st for e st e in H holds e c= A & ex X1 being Subset of X, Y1 being Subset of Y st e =[:X1,Y1:] holds [:meet(.:pr1(X,Y).:H), union(.:pr2(X,Y).:H):] c= A; theorem :: BORSUK_1:16 for X being set, Y being non empty set, f being Function of X,Y for H being Subset-Family of X holds union(.:f.:H) = f.: union H; reserve X,Y,Z for non empty set; theorem :: BORSUK_1:17 for X being set, a being Subset-Family of X holds union union a = union { union A where A is Subset of X: A in a }; theorem :: BORSUK_1:18 for X being set for D being Subset-Family of X st union D = X for A being Subset of D, B being Subset of X st B = union A holds B` c= union A`; theorem :: BORSUK_1:19 for F being Function of X,Y, G being Function of X,Z st for x,x' being Element of X st F.x=F.x' holds G.x=G.x' ex H being Function of Y,Z st H*F=G; theorem :: BORSUK_1:20 for X,Y,Z for y being Element of Y, F being (Function of X,Y), G being Function of Y,Z holds F"{y} c= (G*F)"{G.y}; theorem :: BORSUK_1:21 for F being Function of X,Y, x being Element of X, z being Element of Z holds [:F,id Z:]. [x,z] = [F.x,z]; canceled; theorem :: BORSUK_1:23 for F being Function of X,Y, A being Subset of X, B being Subset of Z holds [:F,id Z:].:[:A,B:] = [:F.:A,B:]; theorem :: BORSUK_1:24 for F being Function of X,Y, y being Element of Y, z being Element of Z holds [:F,id Z:]"{[y,z]} = [:F"{y},{z}:]; definition let B be non empty set, A be set; let x be Element of B; redefine func A --> x -> Function of A,B; end; begin :: :: Partitions :: theorem :: BORSUK_1:25 for D being Subset-Family of X, A being Subset of D holds union A is Subset of X; theorem :: BORSUK_1:26 for X being set, D being a_partition of X, A,B being Subset of D holds union(A /\ B) = union A /\ union B; theorem :: BORSUK_1:27 for D being a_partition of X, A being Subset of D, B being Subset of X st B = union A holds B` = union A`; theorem :: BORSUK_1:28 ::Class(id X) is non-empty for E being Equivalence_Relation of X holds Class(E) is non empty; definition let X be non empty set; cluster non empty a_partition of X; end; definition let X; let D be non empty a_partition of X; func proj D -> Function of X, D means :: BORSUK_1:def 1 for p being Element of X holds p in it.p; end; theorem :: BORSUK_1:29 for D being non empty a_partition of X, p being Element of X, A being Element of D st p in A holds A = (proj D).p; theorem :: BORSUK_1:30 for D being non empty a_partition of X, p being Element of D holds p = proj D " {p}; theorem :: BORSUK_1:31 for D being non empty a_partition of X, A being Subset of D holds (proj D)"A = union A; theorem :: BORSUK_1:32 for D being non empty a_partition of X, W being Element of D ex W' being Element of X st proj(D).W'=W; theorem :: BORSUK_1:33 for D being non empty a_partition of X, W being Subset of X st for B being Subset of X st B in D & B meets W holds B c= W holds W = proj D " (proj D .: W); begin :: :: Topological preliminaries :: canceled; theorem :: BORSUK_1:35 for X being TopStruct, Y being SubSpace of X holds the carrier of Y c= the carrier of X; definition let X, Y be non empty TopSpace, F be map of X, Y; redefine attr F is continuous means :: BORSUK_1:def 2 for W being Point of X, G being a_neighborhood of F.W ex H being a_neighborhood of W st F.:H c= G; end; definition let X be 1-sorted,Y be non empty 1-sorted, y be Element of Y; func X --> y -> map of X,Y equals :: BORSUK_1:def 3 (the carrier of X) --> y; end; reserve X, Y for non empty TopSpace; theorem :: BORSUK_1:36 for y being Point of Y holds X --> y is continuous; definition let S, T be non empty TopSpace; cluster continuous map of S, T; end; definition let X,Y,Z be non empty TopSpace, F be continuous map of X,Y, G be continuous map of Y,Z; redefine func G*F -> continuous map of X,Z; end; theorem :: BORSUK_1:37 for A being continuous map of X,Y, G being Subset of Y holds A"Int G c= Int(A"G); theorem :: BORSUK_1:38 for W being Point of Y, A being continuous map of X,Y, G being a_neighborhood of W holds A"G is a_neighborhood of A"{W}; definition let X,Y be non empty TopSpace, W be Point of Y, A be continuous map of X,Y, G be a_neighborhood of W; redefine func A"G -> a_neighborhood of A"{W}; end; theorem :: BORSUK_1:39 for X being non empty TopSpace, A,B being Subset of X, U_ being a_neighborhood of B st A c= B holds U_ is a_neighborhood of A; canceled; theorem :: BORSUK_1:41 for X being non empty TopSpace, x being Point of X holds {x} is compact; theorem :: BORSUK_1:42 for X being TopStruct for Y being SubSpace of X, A being Subset of X, B being Subset of Y st A = B holds A is compact iff B is compact; begin :: :: Cartesian products of topological spaces :: definition let X,Y be TopSpace; canceled; func [:X,Y:] -> strict TopSpace means :: BORSUK_1:def 5 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}}; end; definition let X,Y be non empty TopSpace; cluster [:X,Y:] -> non empty; end; canceled 2; theorem :: BORSUK_1:45 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 st e in A ex X1 being Subset of X, Y1 being Subset of Y st e = [:X1,Y1:] & X1 is open & Y1 is open; definition let X,Y be TopSpace, A be Subset of X, B be Subset of Y; redefine func [:A,B:] -> Subset of [:X,Y:]; end; definition let X,Y be non empty TopSpace, x be Point of X, y be Point of Y; redefine func [x,y] -> Point of [:X,Y:]; end; theorem :: BORSUK_1:46 for X, Y being TopSpace for V being Subset of X, W being Subset of Y st V is open & W is open holds [:V,W:] is open; theorem :: BORSUK_1:47 for X, Y being TopSpace for V being Subset of X, W being Subset of Y holds Int [:V,W:] = [:Int V, Int W:]; theorem :: BORSUK_1:48 for x being Point of X, y being Point of Y, V being a_neighborhood of x, W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]; theorem :: BORSUK_1:49 for A being Subset of X, B being Subset of Y, V being a_neighborhood of A, W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]; definition let X,Y be non empty TopSpace, x be Point of X, y be Point of Y, V be a_neighborhood of x, W be a_neighborhood of y; redefine func [:V,W:] -> a_neighborhood of [x,y]; end; theorem :: BORSUK_1:50 for XT being Point of [:X,Y:] ex W being Point of X, T being Point of Y st XT=[W,T]; definition let X,Y be non empty TopSpace, A be Subset of X, t be Point of Y, V be a_neighborhood of A, W be a_neighborhood of t; redefine func [:V,W:] -> a_neighborhood of [:A,{t}:]; 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 6 { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y: [:X1,Y1:] c= A & X1 is open & Y1 is open}; end; theorem :: BORSUK_1:51 for X, Y being TopSpace for A being Subset of [:X,Y:] holds Base-Appr A is open; theorem :: BORSUK_1:52 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; theorem :: BORSUK_1:53 for X, Y being TopSpace, A being Subset of [:X,Y:] holds union Base-Appr A c= A; theorem :: BORSUK_1:54 for X, Y being TopSpace, A being Subset of [:X,Y:] st A is open holds A = union Base-Appr A; theorem :: BORSUK_1:55 for X, Y being TopSpace, A being Subset of [:X,Y:] holds Int A = union Base-Appr A; 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 7 .:pr1(the carrier of X,the carrier of Y); func Pr2(X,Y) -> Function of bool the carrier of [:X,Y:], bool the carrier of Y equals :: BORSUK_1:def 8 .:pr2(the carrier of X,the carrier of Y); end; theorem :: BORSUK_1:56 for A being Subset of [:X,Y:], H being Subset-Family of [:X,Y:] st for e st e in H holds e c= A & ex X1 being Subset of X, Y1 being Subset of Y st e =[:X1,Y1:] holds [:union(Pr1(X,Y).:H), meet(Pr2(X,Y).:H):] c= A; theorem :: BORSUK_1:57 for H being Subset-Family of [:X,Y:], C being set st C in Pr1(X,Y).:H ex D being Subset of [:X,Y:] st D in H & C = pr1(the carrier of X, the carrier of Y).:D; theorem :: BORSUK_1:58 for H being Subset-Family of [:X,Y:], C being set st C in Pr2(X,Y).:H ex D being Subset of [:X,Y:] st D in H & C = pr2(the carrier of X, the carrier of Y).:D; theorem :: BORSUK_1:59 for D being Subset of [:X,Y:] st D is open holds for X1 being Subset of X, 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); definition let X, Y be set, f be Function of bool X, bool Y; let R be Subset-Family of X; redefine func f.:R -> Subset-Family of Y; end; theorem :: BORSUK_1:60 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; theorem :: BORSUK_1:61 for H being Subset-Family of [:X,Y:] st Pr1(X,Y).:H = {} or Pr2(X,Y).:H = {} holds H = {}; theorem :: BORSUK_1:62 for H being Subset-Family of [:X,Y:], X1 being Subset of X, Y1 being Subset of Y st H is_a_cover_of [:X1,Y1:] holds (Y1 <> {} implies Pr1(X,Y).:H is_a_cover_of X1) & (X1 <> {} implies Pr2(X,Y).:H is_a_cover_of Y1); theorem :: BORSUK_1:63 for X, Y being TopSpace, H being Subset-Family of X, Y being Subset of X st H is_a_cover_of Y ex F being Subset-Family of X st F c= H & F is_a_cover_of Y & for C being set st C in F holds C meets Y; theorem :: BORSUK_1:64 for F being Subset-Family of X, H being Subset-Family of [:X,Y:] st F is finite & F c= Pr1(X,Y).:H ex G being Subset-Family of [:X,Y:] st G c= H & G is finite & F = Pr1(X,Y).:G; theorem :: BORSUK_1:65 for X1 being Subset of X, Y1 being Subset of Y st [:X1,Y1:] <> {} holds Pr1(X,Y). [:X1,Y1:] = X1 & Pr2(X,Y). [:X1,Y1:] = Y1; theorem :: BORSUK_1:66 Pr1(X,Y).{} = {} & Pr2(X,Y).{} = {}; theorem :: BORSUK_1:67 for t being Point of Y, A being Subset of X st A is compact for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A, W being a_neighborhood of t st [:V,W:] c= G; begin :: :: Partitions of topological spaces :: definition let X be 1-sorted; func TrivDecomp X -> a_partition of the carrier of X equals :: BORSUK_1:def 9 Class(id the carrier of X); end; definition let X be non empty 1-sorted; cluster TrivDecomp X -> non empty; end; theorem :: BORSUK_1:68 for A being Subset of X st A in TrivDecomp X ex x being Point of X st A = {x}; definition let X be TopSpace, D be a_partition of the carrier of X; func space D -> strict TopSpace means :: BORSUK_1:def 10 the carrier of it = D & the topology of it = { A where A is Subset of D : union A in the topology of X}; end; definition let X be non empty TopSpace, D be non empty a_partition of the carrier of X; cluster space D -> non empty; end; theorem :: BORSUK_1:69 for D being non empty a_partition of the carrier of X, A being Subset of D holds union A in the topology of X iff A in the topology of space D; definition let X be non empty TopSpace, D be non empty a_partition of the carrier of X; func Proj D -> continuous map of X, space D equals :: BORSUK_1:def 11 proj D; end; theorem :: BORSUK_1:70 for D being non empty a_partition of the carrier of X, W being Point of X holds W in Proj D.W; theorem :: BORSUK_1:71 for D being non empty a_partition of the carrier of X, W being Point of space D ex W' being Point of X st Proj(D).W'=W; theorem :: BORSUK_1:72 for D being non empty a_partition of the carrier of X holds rng Proj D = the carrier of space D; definition let XX be non empty TopSpace, X be non empty SubSpace of XX, 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 12 D \/ {{p} where p is Point of XX : not p in the carrier of X}; end; theorem :: BORSUK_1:73 for XX being non empty TopSpace, X being non empty SubSpace of XX, D being non empty a_partition of the carrier of X holds D c= TrivExt D; theorem :: BORSUK_1:74 for XX being non empty TopSpace, X being non empty SubSpace of XX, D being non empty a_partition of the carrier of X, A being Subset of XX st A in TrivExt D holds A in D or ex x being Point of XX st not x in [#]X & A = {x}; theorem :: BORSUK_1:75 for XX being non empty TopSpace, X being non empty SubSpace of XX, D being non empty a_partition of the carrier of X, x being Point of XX st not x in the carrier of X holds {x} in TrivExt D; theorem :: BORSUK_1:76 for XX being non empty TopSpace, X being non empty SubSpace of XX, D being non empty a_partition of the carrier of X, W being Point of XX st W in the carrier of X holds Proj(TrivExt D).W=Proj(D).W; theorem :: BORSUK_1:77 for XX being non empty TopSpace, X being non empty SubSpace of XX, D being non empty a_partition of the carrier of X, W being Point of XX st not W in the carrier of X holds Proj TrivExt D.W = {W}; theorem :: BORSUK_1:78 for XX being non empty TopSpace, X being non empty SubSpace of XX, D being non empty a_partition of the carrier of X, W,W' being Point of XX st not W in the carrier of X & Proj(TrivExt D).W=Proj(TrivExt D).W' holds W=W'; theorem :: BORSUK_1:79 for XX being non empty TopSpace , 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; theorem :: BORSUK_1:80 for XX being non empty TopSpace , X being non empty SubSpace of XX for D being non empty a_partition of the carrier of X for e st e in the carrier of X holds Proj TrivExt D.e in the carrier of space D; begin :: :: Upper Semicontinuous Decompositions :: definition let X be non empty TopSpace; mode u.s.c._decomposition of X -> non empty a_partition of the carrier of X means :: BORSUK_1:def 13 for A being Subset of X st A in it 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; end; theorem :: BORSUK_1:81 for D being u.s.c._decomposition of X, t being Point of space D, G being a_neighborhood of Proj D " {t} holds Proj(D).:G is a_neighborhood of t; theorem :: BORSUK_1:82 TrivDecomp X is u.s.c._decomposition of X; definition let X be TopSpace; let IT be SubSpace of X; attr IT is closed means :: BORSUK_1:def 14 for A being Subset of X st A = the carrier of IT holds A is closed; end; definition let X be TopSpace; cluster strict closed SubSpace of X; end; definition let X; cluster strict closed non empty SubSpace of X; end; definition let XX be non empty TopSpace, X be closed non empty SubSpace of XX,D be u.s.c._decomposition of X; redefine func TrivExt D -> u.s.c._decomposition of XX; end; definition let X be non empty TopSpace; let IT be u.s.c._decomposition of X; attr IT is DECOMPOSITION-like means :: BORSUK_1:def 15 for A being Subset of X st A in IT holds A is compact; :: upper semicontinuous decomposition into compacta end; definition let X be non empty TopSpace; cluster DECOMPOSITION-like u.s.c._decomposition of X; 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, X be closed non empty SubSpace of XX, D be DECOMPOSITION of X; redefine func TrivExt D -> DECOMPOSITION of XX; end; definition let X be non empty TopSpace, Y be closed non empty SubSpace of X, D be DECOMPOSITION of Y; redefine func space D -> strict closed SubSpace of space TrivExt D; end; begin definition func I[01] -> TopStruct means :: BORSUK_1:def 16 for P being Subset of TopSpaceMetr(RealSpace) st P = [.0,1.] holds it = (TopSpaceMetr RealSpace)|P; end; definition cluster I[01] -> strict non empty TopSpace-like; end; theorem :: BORSUK_1:83 the carrier of I[01] = [.0,1.]; definition func 0[01] -> Point of I[01] equals :: BORSUK_1:def 17 0; func 1[01] -> Point of I[01] equals :: BORSUK_1:def 18 1; end; definition let A be non empty TopSpace, B be non empty SubSpace of A, F be map of A,B; attr F is being_a_retraction means :: BORSUK_1:def 19 for W being Point of A st W in the carrier of B holds F.W=W; synonym F is_a_retraction; end; definition let X be non empty TopSpace,Y be non empty SubSpace of X; pred Y is_a_retract_of X means :: BORSUK_1:def 20 ex F being continuous map of X,Y st F is_a_retraction; pred Y is_an_SDR_of X means :: BORSUK_1:def 21 ex H being continuous map 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; theorem :: BORSUK_1:84 for XX being non empty TopSpace, X being closed non empty SubSpace of XX, D being DECOMPOSITION of X st X is_a_retract_of XX holds space(D) is_a_retract_of space(TrivExt D); theorem :: BORSUK_1:85 for XX being non empty TopSpace, X being closed non empty SubSpace of XX, D being DECOMPOSITION of X st X is_an_SDR_of XX holds space(D) is_an_SDR_of space(TrivExt D);

Back to top