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