:: A Borsuk Theorem on Homotopy Types
:: by Andrzej Trybulec
::
:: Received August 1, 1991
:: Copyright (c) 1991-2019 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];