:: A Borsuk Theorem on Homotopy Types
:: by Andrzej Trybulec
::
:: Received August 1, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

:: Topological preliminaries
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
proofend;

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 )
proofend;
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)
proofend;

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}
proofend;

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

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
proofend;
end;

begin

::
:: Cartesian products of topological spaces
::
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 )  }   }  )
proofend;
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
proofend;
cluster[:T2,T1:] ->  empty strict ;
coherence
 [:T2,T1:] is empty
proofend;
end;

registration
let X, Y be non empty TopSpace;
cluster[:X,Y:] ->  non empty strict ;
coherence
 not [:X,Y:] is empty
proofend;
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 ) ) ) )
proofend;

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

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):]
proofend;

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]
proofend;

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

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]
proofend;

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}:];
proofend;
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:]
proofend;
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
proofend;
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
proofend;

theorem Th12: :: BORSUK_1:12
for X, Y being TopSpace
for A being Subset of [:X,Y:] holds union (Base-Appr A) c= A
proofend;

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)
proofend;

theorem Th14: :: BORSUK_1:14
for X, Y being TopSpace
for A being Subset of [:X,Y:] holds Int A = union (Base-Appr A)
proofend;

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)
proofend;
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)
proofend;
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
proofend;

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 )
proofend;

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 )
proofend;

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 ) )
proofend;

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 )
proofend;

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 = {}
proofend;

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 ) &amp; ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )
proofend;

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 &amp; F is Cover of Y &amp; ( for C being set st C in F holds
C meets Y ) )
proofend;

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 &amp; F c= (Pr1 (X,Y)) .: H holds
ex G being Subset-Family of [:X,Y:] st
( G c= H &amp; G is finite &amp; F = (Pr1 (X,Y)) .: G )
proofend;

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 &amp; (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
proofend;

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);
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}
proofend;

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 &amp; A c= W &amp; W c= V &amp; ( for B being Subset of X st B in TrivDecomp X &amp; B meets W holds
B c= W ) )
proofend;

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 &amp; 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 &amp; the topology of b1 =  {  A where A is Subset of D : union A in the topology of X  }  )
proofend;
uniqueness
 for b1, b2 being strict TopSpace st the carrier of b1 = D &amp; the topology of b1 =  {  A where A is Subset of D : union A in the topology of X  }  &amp; the carrier of b2 = D &amp; 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 &amp; 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) )
proofend;

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)
proofend;
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
proofend;

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)
proofend;

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
proofend;
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 &amp; A = {x} ) )
proofend;

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

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

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}
proofend;

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 &amp; (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 holds
W = W9
proofend;

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

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)
proofend;

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 :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 &amp; A c= W &amp; W c= V &amp; ( for B being Subset of X st B in it &amp; 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 &amp; A c= W &amp; W c= V &amp; ( for B being Subset of X st B in b1 &amp; B meets W holds
B c= W ) );
proofend;
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 &amp; A c= W &amp; W c= V &amp; ( for B being Subset of X st B in b2 &amp; 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
proofend;

theorem Th39: :: BORSUK_1:39
for X being non empty TopSpace holds TrivDecomp X is u.s.c._decomposition of X
proofend;

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

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 &amp; b1 is closed )
proofend;
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 &amp; b1 is closed &amp; not b1 is empty )
proofend;
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;
proofend;
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 );

:: upper semicontinuous decomposition into compacta
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
proofend;
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;
proofend;
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);
proofend;
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
proofend;
uniqueness
 for b1, b2 being TopStruct st ( for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
b1 = (TopSpaceMetr RealSpace) | P ) &amp; ( for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
b2 = (TopSpaceMetr RealSpace) | P ) holds
b1 = b2
proofend;
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 &amp; not I[01] is empty &amp; I[01] is TopSpace-like )
proofend;
end;

theorem Th40: :: BORSUK_1:40
the carrier of I[01] = [.0,1.]
proofend;

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 &amp; H . [A,1[01]] in the carrier of Y &amp; ( 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 &amp; H . [A,1[01]] in the carrier of Y &amp; ( 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)
proofend;

:: [WP: ] Borsuk_Theorem_on_Decomposition_of_Strong_Deformation_Retracts
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)
proofend;

theorem :: BORSUK_1:43
for r being real number holds
( ( 0 <= r &amp; r <= 1 ) iff r in the carrier of I[01] )
proofend;