:: A Borsuk Theorem on Homotopy Types :: by Andrzej Trybulec :: :: Received August 1, 1991 :: Copyright (c) 1991-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, FUNCT_1, TARSKI, RELAT_1, ZFMISC_1, MCART_1, XBOOLE_0, SETFAM_1, EQREL_1, CARD_3, PRE_TOPC, STRUCT_0, ORDINAL2, CONNSP_2, TOPS_1, RCOMP_1, FINSET_1, PCOMPS_1, METRIC_1, XXREAL_1, CARD_1, XXREAL_0, REAL_1, BORSUK_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, FINSET_1, RELAT_1, FUNCT_1, XTUPLE_0, MCART_1, DOMAIN_1, RCOMP_1, SETFAM_1, EQREL_1, FUNCT_3, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, METRIC_1, PCOMPS_1, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, CONNSP_2; constructors SETFAM_1, DOMAIN_1, FUNCT_3, FINSET_1, MEMBERED, EQREL_1, RCOMP_1, TOPS_1, TOPS_2, COMPTS_1, CONNSP_2, PCOMPS_1, RELSET_1, XTUPLE_0, BINOP_1; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, XREAL_0, MEMBERED, EQREL_1, STRUCT_0, PRE_TOPC, TOPS_1, METRIC_1, PCOMPS_1, RELSET_1, ZFMISC_1, XTUPLE_0; requirements NUMERALS, REAL, BOOLE, SUBSET; begin reserve e,u for set; :: Topological preliminaries theorem :: BORSUK_1:1 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 Function of X, Y; redefine attr F is continuous means :: BORSUK_1:def 1 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; reserve X, Y for non empty TopSpace; registration let X,Y,Z be non empty TopSpace, F be continuous Function of X,Y, G be continuous Function of Y,Z; cluster G*F -> continuous for Function of X,Z; end; theorem :: BORSUK_1:2 for A being continuous Function of X,Y, G being Subset of Y holds A"Int G c= Int(A"G); theorem :: BORSUK_1:3 for W being Point of Y, A being continuous Function 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 Function of X,Y, G be a_neighborhood of W; redefine func A"G -> a_neighborhood of A"{W}; end; theorem :: BORSUK_1:4 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; registration let X be non empty TopSpace, x be Point of X; cluster {x} -> compact for Subset of X; end; begin :: :: Cartesian products of topological spaces :: definition let X,Y be TopSpace; func [:X,Y:] -> strict TopSpace means :: 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}}; end; registration let T1 be TopSpace, T2 be empty TopSpace; cluster [:T1, T2:] -> empty; cluster [:T2, T1:] -> empty; end; registration let X,Y be non empty TopSpace; cluster [:X,Y:] -> non empty; end; theorem :: 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 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:6 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:7 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:8 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:9 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:10 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 3 { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y: [:X1,Y1:] c= A & X1 is open & Y1 is open}; end; registration let X, Y be TopSpace, A be Subset of [:X,Y:]; cluster Base-Appr A -> open; end; theorem :: 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; theorem :: BORSUK_1:12 for X, Y being TopSpace, A being Subset of [:X,Y:] holds union Base-Appr A c= A; theorem :: BORSUK_1:13 for X, Y being TopSpace, A being Subset of [:X,Y:] st A is open holds A = union Base-Appr A; theorem :: BORSUK_1:14 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 4 .: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 5 .:pr2(the carrier of X,the carrier of Y); end; 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 [:union(Pr1(X,Y).:H), meet(Pr2(X,Y).:H):] c= A; theorem :: BORSUK_1:16 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:17 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:18 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); theorem :: BORSUK_1:19 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:20 for H being Subset-Family of [:X,Y:] st Pr1(X,Y).:H = {} or Pr2( X,Y).:H = {} holds H = {}; theorem :: BORSUK_1:21 for H being Subset-Family of [:X,Y:], X1 being Subset of X, 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); theorem :: BORSUK_1:22 for X, Y being TopSpace, H being Subset-Family of X, Y being Subset of X st H is Cover of Y 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; theorem :: BORSUK_1:23 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:24 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:25 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 6 Class(id the carrier of X); end; registration let X be non empty 1-sorted; cluster TrivDecomp X -> non empty; end; theorem :: BORSUK_1:26 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 7 the carrier of it = D & the topology of it = { A where A is Subset of D : union A in the topology of X}; end; registration let X be non empty TopSpace, D be a_partition of the carrier of X; cluster space D -> non empty; end; theorem :: BORSUK_1:27 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 Function of X, space D equals :: BORSUK_1:def 8 proj D; end; theorem :: BORSUK_1:28 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:29 for D being non empty a_partition of the carrier of X, W being Point of space D ex W9 being Point of X st Proj(D).W9=W; theorem :: BORSUK_1:30 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 9 D \/ {{p } where p is Point of XX : not p in the carrier of X}; end; theorem :: BORSUK_1:31 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:32 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:33 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:34 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:35 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,W9 being Point of XX st not W in the carrier of X & Proj(TrivExt D).W=Proj(TrivExt D).W9 holds W=W9; theorem :: BORSUK_1:36 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:37 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 10 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:38 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:39 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 11 for A being Subset of X st A = the carrier of IT holds A is closed; end; registration let X be TopSpace; cluster strict closed for SubSpace of X; end; registration let X; cluster strict closed non empty for 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 12 for A being Subset of X st A in IT holds A is compact; end; :: upper semicontinuous decomposition into compacta registration let X be non empty TopSpace; cluster DECOMPOSITION-like for 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 13 for P being Subset of TopSpaceMetr( RealSpace) st P = [.0,1.] holds it = (TopSpaceMetr RealSpace)|P; end; registration cluster I[01] -> strict non empty TopSpace-like; end; theorem :: BORSUK_1:40 the carrier of I[01] = [.0,1.]; definition func 0[01] -> Point of I[01] equals :: BORSUK_1:def 14 0; func 1[01] -> Point of I[01] equals :: BORSUK_1:def 15 1; end; definition let A be non empty TopSpace, B be non empty SubSpace of A, F be Function of A,B; attr F is being_a_retraction means :: BORSUK_1:def 16 for W being Point of A st W in the carrier of B holds F.W=W; 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 17 ex F being continuous Function of X,Y st F is being_a_retraction; pred Y 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; theorem :: BORSUK_1:41 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; ::\$N Borsuk Theorem on Decomposition of Strong Deformation Retracts theorem :: BORSUK_1:42 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); theorem :: BORSUK_1:43 for r being Real holds 0 <= r & r <= 1 iff r in the carrier of I[01];