:: A Borsuk Theorem on Homotopy Types
:: by Andrzej Trybulec
::
:: Received August 1, 1991
:: Copyright (c) 1991-2026 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;
definitions TARSKI, PRE_TOPC, TOPS_2, CONNSP_2, EQREL_1, STRUCT_0, XBOOLE_0,
RELAT_1, SETFAM_1;
equalities STRUCT_0, BINOP_1;
expansions TARSKI, PRE_TOPC, TOPS_2, XBOOLE_0, RELAT_1;
theorems TARSKI, ZFMISC_1, DOMAIN_1, PRE_TOPC, FUNCT_1, FUNCT_2, TOPS_1,
EQREL_1, FUNCT_3, SUBSET_1, TOPS_2, CONNSP_2, COMPTS_1, SETFAM_1,
PCOMPS_1, METRIC_1, RCOMP_1, MCART_1, RELAT_1, XBOOLE_0, XBOOLE_1,
XXREAL_1, XTUPLE_0;
schemes CLASSES1, DOMAIN_1;
begin
reserve e,u for set;
:: Topological preliminaries
theorem Th1:
for X being TopStruct, Y being SubSpace of X holds the carrier
of Y c= the carrier of X
proof
let X be TopStruct, Y be SubSpace of X;
the carrier of Y = [#]Y & the carrier of X = [#]X;
hence thesis by PRE_TOPC:def 4;
end;
definition
let X, Y be non empty TopSpace, F be Function of X, Y;
redefine attr F is continuous means :: redefines continuous (PRE_TOPC, definition)
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;
compatibility
proof
A1: [#]Y <> {};
thus F is continuous implies 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
proof
assume
A2: F is continuous;
let W be Point of X, G be a_neighborhood of F.W;
F.W in Int G by CONNSP_2:def 1;
then
A3: W in F"Int G by FUNCT_2:38;
F"Int G is open by A1,A2,TOPS_2:43;
then W in Int(F"Int G) by A3,TOPS_1:23;
then reconsider H = F"Int G as a_neighborhood of W by CONNSP_2:def 1;
take H;
H c= F"G by RELAT_1:143,TOPS_1:16;
hence thesis by EQREL_1:46;
end;
assume
A4: 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;
now
let P1 be Subset of Y such that
A5: P1 is open;
now
let x be set;
thus x in F"P1 implies ex P being Subset of X st P is open & P c= F"P1
& x in P
proof
assume
A6: x in F"P1;
then reconsider W = x as Point of X;
A7: Int P1 = P1 by A5,TOPS_1:23;
F.W in P1 by A6,FUNCT_2:38;
then P1 is a_neighborhood of F.W by A7,CONNSP_2:def 1;
then consider H being a_neighborhood of W such that
A8: F.:H c= P1 by A4;
take Int H;
thus Int H is open;
A9: Int H c= H by TOPS_1:16;
dom F = the carrier of X by FUNCT_2:def 1;
then
A10: H c= F"(F.:H) by FUNCT_1:76;
F"(F.:H) c= F"P1 by A8,RELAT_1:143;
then H c= F"P1 by A10;
hence Int H c= F"P1 by A9;
thus thesis by CONNSP_2:def 1;
end;
thus (ex P being Subset of X st P is open & P c= F"P1 & x in P)
implies x in F"P1;
end;
hence F"P1 is open by TOPS_1:25;
end;
hence thesis by A1,TOPS_2:43;
end;
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;
coherence by TOPS_2:46;
end;
theorem Th2:
for A being continuous Function of X,Y, G being Subset of Y
holds A"Int G c= Int(A"G)
proof
let A be continuous Function of X,Y, G be Subset of Y;
let e be object;
A1: A"Int G c= A"G by RELAT_1:143,TOPS_1:16;
[#]Y <> {};
then
A2: A"Int G is open by TOPS_2:43;
assume e in A"Int G;
hence thesis by A2,A1,TOPS_1:22;
end;
theorem Th3:
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}
proof
let W be Point of Y, A be continuous Function of X,Y, G be a_neighborhood of
W;
W in Int G by CONNSP_2:def 1;
then {W} c= Int G by ZFMISC_1:31;
then
A1: A"{W} c= A"Int G by RELAT_1:143;
A"Int G c= Int(A"G) by Th2;
hence A"{W} c= Int(A"G) by A1;
end;
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}; :: redefines " (FUNCT_1, redefinition) → " (RELAT_1, definition)
correctness by Th3;
end;
theorem Th4:
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
proof
let X be non empty TopSpace;
let A,B be Subset of X, U be a_neighborhood of B such that
A1: A c= B;
B c= Int U by CONNSP_2:def 2;
hence A c= Int U by A1;
end;
registration
let X be non empty TopSpace, x be Point of X;
cluster {x} -> compact for Subset of X;
coherence
proof
reconsider B = {x} as Subset of X;
now
let F be Subset-Family of X such that
A1: F is Cover of B and
F is open;
B c= union F by A1,SETFAM_1:def 11;
then x in union F by ZFMISC_1:31;
then consider A being set such that
A2: x in A and
A3: A in F by TARSKI:def 4;
reconsider G = {A} as Subset-Family of X by A3,ZFMISC_1:31;
take G;
thus G c= F by A3,ZFMISC_1:31;
x in union G by A2;
then B c= union G by ZFMISC_1:31;
hence G is Cover of B by SETFAM_1:def 11;
thus G is finite;
end;
hence thesis by COMPTS_1:def 4;
end;
end;
begin
::
:: Cartesian products of topological spaces
::
definition
let X,Y be TopSpace;
func [:X,Y:] -> strict TopSpace means
:Def2:
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
proof
set t = { union A where A is Subset-Family of [: the carrier of X, the
carrier of Y:]: 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}};
t c= bool [: the carrier of X, the carrier of Y:]
proof
let e be object;
assume e in t;
then
ex A being Subset-Family of [: the carrier of X, the carrier of Y :]
st e = union A& 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};
hence thesis;
end;
then reconsider
t as Subset-Family of [: the carrier of X, the carrier of Y:];
set T = TopStruct(#[: the carrier of X, the carrier of Y:],t#);
now
reconsider A = {[: the carrier of X, the carrier of Y:]} as
Subset-Family of [: the carrier of X, the carrier of Y:] by ZFMISC_1:68;
reconsider A as Subset-Family of [: the carrier of X, the carrier of Y:];
A1: 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}
proof
let e be object;
assume e in A;
then
A2: e = [: the carrier of X, the carrier of Y:] by TARSKI:def 1;
the carrier of X in the topology of X & the carrier of Y in the
topology of Y by PRE_TOPC:def 1;
hence thesis by A2;
end;
the carrier of T = union A;
hence the carrier of T in the topology of T by A1;
thus for a being Subset-Family of T st a c= the topology of T holds
union a in the topology of T
proof
let a be Subset-Family of T;
set A = { [: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 & ex x being set st x in a & [:X1,
Y1:] c= x};
A c= bool[: the carrier of X, the carrier of Y:]
proof
let e be object;
assume e in A;
then ex X1 being Subset of X, Y1 being Subset of Y st e = [:X1,Y1:]
& X1 in the topology of X & Y1 in the topology of Y & ex x being set st x in a
& [:X1,Y1:] c= x;
hence thesis;
end;
then reconsider
A as Subset-Family of [: the carrier of X, the carrier of Y
:];
assume
A3: a c= the topology of T;
A4: union A = union a
proof
thus union A c= union a
proof
let e1,e2 be object;
assume [e1,e2] in union A;
then consider u such that
A5: [e1,e2] in u and
A6: u in A by TARSKI:def 4;
ex X1 being Subset of X, Y1 being Subset of Y st u = [:X1, Y1
:] & X1 in the topology of X & Y1 in the topology of Y & ex x being set st x in
a & [:X1,Y1:] c= x by A6;
hence thesis by A5,TARSKI:def 4;
end;
let e be object;
assume e in union a;
then consider u such that
A7: e in u and
A8: u in a by TARSKI:def 4;
u in the topology of T by A3,A8;
then consider
B being Subset-Family of [: the carrier of X, the carrier
of Y:] such that
A9: u = union B and
A10: B 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};
consider x being set such that
A11: e in x and
A12: x in B by A7,A9,TARSKI:def 4;
x in { [: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} by A10,A12;
then consider X1 being Subset of X, Y1 being Subset of Y such that
A13: x = [:X1,Y1:] and
A14: X1 in the topology of X & Y1 in the topology of Y;
[:X1,Y1:] c= u by A9,A12,A13,ZFMISC_1:74;
then x in A by A8,A13,A14;
hence thesis by A11,TARSKI:def 4;
end;
A c= { [:X2,Y2:] where X2 is Subset of X, Y2 is Subset of Y : X2
in the topology of X & Y2 in the topology of Y}
proof
let e be object;
assume e in A;
then ex X1 being Subset of X, Y1 being Subset of Y st e = [:X1,Y1:]
& X1 in the topology of X & Y1 in the topology of Y & ex x being set st x in a
& [:X1,Y1:] c= x;
hence thesis;
end;
hence thesis by A4;
end;
let a,b be Subset of T;
set 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 & [:X1,Y1:] c= a /\ b};
C c= bool[: the carrier of X, the carrier of Y:]
proof
let e be object;
assume e in C;
then ex X1 being Subset of X, Y1 being Subset of Y st e = [:X1,Y1:] &
X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b;
hence thesis;
end;
then reconsider
C as Subset-Family of [:the carrier of X, the carrier of Y:];
assume that
A15: a in the topology of T and
A16: b in the topology of T;
consider A being Subset-Family of [: the carrier of X, the carrier of Y
:] such that
A17: a = union A and
A18: 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} by A15;
consider B being Subset-Family of [: the carrier of X, the carrier of Y
:] such that
A19: b = union B and
A20: B 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} by A16;
A21: a /\ b = union C
proof
thus a /\ b c= union C
proof
let e be object;
assume
A22: e in a /\ b;
then e in a by XBOOLE_0:def 4;
then consider u1 being set such that
A23: e in u1 and
A24: u1 in A by A17,TARSKI:def 4;
A25: u1 in { [: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} by A18,A24;
e in b by A22,XBOOLE_0:def 4;
then consider u2 being set such that
A26: e in u2 and
A27: u2 in B by A19,TARSKI:def 4;
A28: u2 in { [:X2,Y2:] where X2 is Subset of X, Y2 is Subset of Y :
X2 in the topology of X & Y2 in the topology of Y} by A20,A27;
A29: u2 c= b by A19,A27,ZFMISC_1:74;
consider X1 being Subset of X, Y1 being Subset of Y such that
A30: u1 = [:X1,Y1:] and
A31: X1 in the topology of X & Y1 in the topology of Y by A25;
consider X2 being Subset of X, Y2 being Subset of Y such that
A32: u2 = [:X2,Y2:] and
A33: X2 in the topology of X & Y2 in the topology of Y by A28;
u1 c= a by A17,A24,ZFMISC_1:74;
then [:X1,Y1:] /\ [:X2,Y2:] c= a /\ b by A30,A32,A29,XBOOLE_1:27;
then
A34: [:X1 /\ X2, Y1 /\ Y2:] c= a /\ b by ZFMISC_1:100;
X1 /\ X2 in the topology of X & Y1 /\ Y2 in the topology of Y
by A31,A33,PRE_TOPC:def 1;
then
A35: [:X1 /\ X2, Y1 /\ Y2:] in C by A34;
e in [:X1 /\ X2, Y1 /\ Y2:] by A23,A26,A30,A32,ZFMISC_1:113;
hence thesis by A35,TARSKI:def 4;
end;
let e1,e2 be object;
assume [e1,e2] in union C;
then consider u such that
A36: [e1,e2] in u and
A37: u in C by TARSKI:def 4;
ex X1 being Subset of X, Y1 being Subset of Y st u = [:X1,Y1:] &
X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b by A37;
hence thesis by A36;
end;
C 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}
proof
let e be object;
assume e in C;
then ex X1 being Subset of X, Y1 being Subset of Y st e = [:X1,Y1:] &
X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b;
hence thesis;
end;
hence a /\ b in the topology of T by A21;
end;
then reconsider T as strict TopSpace by PRE_TOPC:def 1;
take T;
thus thesis;
end;
uniqueness;
end;
registration
let T1 be TopSpace, T2 be empty TopSpace;
cluster [:T1, T2:] -> empty;
coherence
proof
the carrier of [:T1, T2:] = [:the carrier of T1, the carrier of T2:]
by Def2;
hence thesis;
end;
cluster [:T2, T1:] -> empty;
coherence
proof
the carrier of [:T2, T1:] = [:the carrier of T2, the carrier of T1:]
by Def2;
hence thesis;
end;
end;
registration
let X,Y be non empty TopSpace;
cluster [:X,Y:] -> non empty;
coherence
proof
the carrier of [:X,Y:] = [:the carrier of X, the carrier of Y:] by Def2;
hence the carrier of [:X,Y:] is non empty;
end;
end;
theorem Th5:
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
proof
let X, Y be TopSpace;
let B be Subset of [:X,Y:];
A1: the topology of [:X,Y:] = { union A where A is Subset-Family of [:X,Y:]:
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}} by Def2;
thus B is open implies 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
proof
assume B in the topology of [:X,Y:];
then consider A being Subset-Family of [:X,Y:] such that
A2: B = union A and
A3: 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} by A1;
take A;
thus B = union A by A2;
let e;
assume e in A;
then e in { [: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} by A3;
then consider X1 being Subset of X, Y1 being Subset of Y such that
A4: e = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y;
reconsider Y1 as Subset of Y;
reconsider X1 as Subset of X;
take X1,Y1;
thus thesis by A4;
end;
given A being Subset-Family of [:X,Y:] such that
A5: B = union A and
A6: 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;
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}
proof
let e be object;
assume e in A;
then consider X1 being Subset of X, Y1 being Subset of Y such that
A7: e = [:X1,Y1:] and
A8: X1 is open & Y1 is open by A6;
X1 in the topology of X & Y1 in the topology of Y by A8;
hence thesis by A7;
end;
hence B in the topology of [:X,Y:] by A1,A5;
end;
definition
let X,Y be TopSpace, A be Subset of X, B be Subset of Y;
redefine func [:A,B:] -> Subset of [:X,Y:]; :: redefines [: (ZFMISC_1, definition)
correctness
proof
thus [:A,B:] is Subset of [:X,Y:] by Def2;
end;
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:]; :: redefines [ (TARSKI, definition)
correctness
proof
thus [x,y] is Point of [:X,Y:] by Def2;
end;
end;
theorem Th6:
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
proof
let X, Y be TopSpace, V be Subset of X, W be Subset of Y such that
A1: V is open & W is open;
reconsider PP = {[:V,W:]} as Subset-Family of [:X,Y:];
reconsider PP as Subset-Family of [:X,Y:];
A2: now
let e;
assume
A3: e in PP;
take V,W;
thus e = [:V,W:] & V is open & W is open by A1,A3,TARSKI:def 1;
end;
[:V,W:] = union {[:V,W:]};
hence thesis by A2,Th5;
end;
theorem Th7:
for X, Y being TopSpace for V being Subset of X, W being Subset
of Y holds Int [:V,W:] = [:Int V, Int W:]
proof
let X, Y be TopSpace, V be Subset of X, W be Subset of Y;
thus Int [:V,W:] c= [:Int V, Int W:]
proof
let e be object;
assume e in Int [:V,W:];
then consider Q being Subset of [:X,Y:]such that
A1: Q is open and
A2: Q c= [:V,W:] and
A3: e in Q by TOPS_1:22;
consider A being Subset-Family of [:X,Y:] such that
A4: Q = union A and
A5: 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 by A1,Th5;
consider a being set such that
A6: e in a and
A7: a in A by A3,A4,TARSKI:def 4;
consider X1 being Subset of X, Y1 being Subset of Y such that
A8: a = [:X1,Y1:] and
A9: X1 is open and
A10: Y1 is open by A5,A7;
[:X1,Y1:] c= Q by A4,A7,A8,ZFMISC_1:74;
then
A11: [:X1,Y1:] c= [:V,W:] by A2;
then Y1 c= W by A6,A8,ZFMISC_1:114;
then
A12: Y1 c= Int W by A10,TOPS_1:24;
X1 c= V by A6,A8,A11,ZFMISC_1:114;
then X1 c= Int V by A9,TOPS_1:24;
then [:X1,Y1:] c= [:Int V, Int W:] by A12,ZFMISC_1:96;
hence thesis by A6,A8;
end;
Int V c= V & Int W c= W by TOPS_1:16;
then [:Int V, Int W:] c= [:V,W:] by ZFMISC_1:96;
hence thesis by Th6,TOPS_1:24;
end;
theorem Th8:
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]
proof
let x be Point of X, y be Point of Y, V be a_neighborhood of x, W be
a_neighborhood of y;
x in Int V & y in Int W by CONNSP_2:def 1;
then [x,y] in [:Int V, Int W:] by ZFMISC_1:87;
hence [x,y] in Int [:V,W:] by Th7;
end;
theorem Th9:
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:]
proof
let A be Subset of X, B be Subset of Y, V be a_neighborhood of A, W be
a_neighborhood of B;
A c= Int V & B c= Int W by CONNSP_2:def 2;
then [:A,B:] c= [:Int V, Int W:] by ZFMISC_1:96;
hence [:A,B:] c= Int [:V,W:] by Th7;
end;
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]; :: redefines [: (ZFMISC_1, definition)
correctness by Th8;
end;
theorem Th10:
for XT being Point of [:X,Y:] ex W being Point of X, T being
Point of Y st XT=[W,T]
proof
let XT be Point of [:X,Y:];
the carrier of [:X,Y:] = [:the carrier of X, the carrier of Y:] by Def2;
hence thesis by DOMAIN_1:1;
end;
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}:]; :: redefines [: (ZFMISC_1, definition)
correctness
proof
W is a_neighborhood of {t} by CONNSP_2:8;
hence [:V,W:] is a_neighborhood of [:A,{t}:] by Th9;
end;
end;
definition
let X,Y be TopSpace;
let A be Subset of [:X,Y:];
func Base-Appr A -> Subset-Family of [:X,Y:] equals
{ [:X1,Y1:] where X1 is
Subset of X, Y1 is Subset of Y: [:X1,Y1:] c= A & X1 is open & Y1 is open};
coherence
proof
set B = { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y: [:X1,Y1:]
c= A & X1 is open & Y1 is open};
B c= bool the carrier of [:X,Y:]
proof
let e be object;
assume e in B;
then
ex X1 being Subset of X, Y1 being Subset of Y st e = [:X1,Y1:] & [:
X1,Y1:] c= A & X1 is open & Y1 is open;
hence thesis;
end;
hence thesis;
end;
end;
registration
let X, Y be TopSpace, A be Subset of [:X,Y:];
cluster Base-Appr A -> open;
coherence
proof
let B be Subset of [:X,Y:];
assume B in Base-Appr A;
then
ex X1 being Subset of X, Y1 being Subset of Y st B = [:X1,Y1:] & [:X1,Y1
:] c= A & X1 is open & Y1 is open;
hence thesis by Th6;
end;
end;
theorem Th11:
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
proof
let X, Y be TopSpace, A,B be Subset of [:X,Y:] such that
A1: A c= B;
let e be object;
assume e in Base-Appr A;
then consider X1 being Subset of X, Y1 being Subset of Y such that
A2: e = [:X1,Y1:] and
A3: [:X1,Y1:] c= A and
A4: X1 is open & Y1 is open;
[:X1,Y1:] c= B by A1,A3;
hence thesis by A2,A4;
end;
theorem Th12:
for X, Y being TopSpace, A being Subset of [:X,Y:] holds union
Base-Appr A c= A
proof
let X, Y be TopSpace, A be Subset of [:X,Y:];
let e be object;
assume e in union Base-Appr A;
then consider B being set such that
A1: e in B and
A2: B in Base-Appr A by TARSKI:def 4;
ex X1 being Subset of X, Y1 being Subset of Y st B = [:X1,Y1:] & [:X1,Y1
:] c= A & X1 is open & Y1 is open by A2;
hence thesis by A1;
end;
theorem Th13:
for X, Y being TopSpace, A being Subset of [:X,Y:] st A is open
holds A = union Base-Appr A
proof
let X, Y be TopSpace, A be Subset of [:X,Y:];
assume A is open;
then consider B being Subset-Family of [:X,Y:] such that
A1: A = union B and
A2: for e st e in B ex X1 being Subset of X, Y1 being Subset of Y st e =
[:X1,Y1:] & X1 is open & Y1 is open by Th5;
thus A c= union Base-Appr A
proof
let e be object;
assume e in A;
then consider u such that
A3: e in u and
A4: u in B by A1,TARSKI:def 4;
( ex X1 being Subset of X, Y1 being Subset of Y st u = [:X1,Y1:] & X1
is open & Y1 is open)& u c= A by A1,A2,A4,ZFMISC_1:74;
then u in Base-Appr A;
hence thesis by A3,TARSKI:def 4;
end;
thus thesis by Th12;
end;
theorem Th14:
for X, Y being TopSpace, A being Subset of [:X,Y:] holds Int A =
union Base-Appr A
proof
let X, Y be TopSpace, A be Subset of [:X,Y:];
Int A = union Base-Appr Int A & Base-Appr Int A c= Base-Appr A by Th11,Th13,
TOPS_1:16;
hence Int A c= union Base-Appr A by ZFMISC_1:77;
union Base-Appr A is open by TOPS_2:19;
hence thesis by Th12,TOPS_1:24;
end;
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
.:pr1(the carrier of X,the carrier of Y);
coherence
proof
the carrier of [:X,Y:] = [:the carrier of X, the carrier of Y:] by Def2;
hence thesis;
end;
correctness;
func Pr2(X,Y) -> Function of bool the carrier of [:X,Y:], bool the carrier
of Y equals
.:pr2(the carrier of X,the carrier of Y);
coherence
proof
the carrier of [:X,Y:] = [:the carrier of X, the carrier of Y:] by Def2;
hence thesis;
end;
correctness;
end;
theorem Th15:
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
proof
let A be Subset of [:X,Y:], H be Subset-Family of [:X,Y:];
assume
A1: 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:];
the carrier of [:X,Y:] = [:the carrier of X, the carrier of Y:] by Def2;
hence thesis by A1,EQREL_1:51;
end;
theorem Th16:
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
proof
let H be Subset-Family of [:X,Y:], C be set;
assume C in Pr1(X,Y).:H;
then consider u being object such that
A1: u in dom Pr1(X,Y) and
A2: u in H and
A3: C = Pr1(X,Y).u by FUNCT_1:def 6;
reconsider u as Subset of [:X,Y:] by A1;
take u;
thus u in H by A2;
the carrier of [:X,Y:] = [:the carrier of X, the carrier of Y:] by Def2;
hence thesis by A3,EQREL_1:47;
end;
theorem Th17:
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
proof
let H be Subset-Family of [:X,Y:], C be set;
assume C in Pr2(X,Y).:H;
then consider u being object such that
A1: u in dom Pr2(X,Y) and
A2: u in H and
A3: C = Pr2(X,Y).u by FUNCT_1:def 6;
reconsider u as Subset of [:X,Y:] by A1;
take u;
thus u in H by A2;
the carrier of [:X,Y:] = [:the carrier of X, the carrier of Y:] by Def2;
hence thesis by A3,EQREL_1:48;
end;
theorem Th18:
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)
proof
let D be Subset of [:X,Y:];
set p = pr2(the carrier of X, the carrier of Y);
set P = .:p;
assume D is open;
then consider H being Subset-Family of [:X,Y:] such that
A1: D = union H and
A2: for e st e in H ex X1 being Subset of X, Y1 being Subset of Y st e =
[:X1,Y1:] & X1 is open & Y1 is open by Th5;
reconsider K = H as Subset-Family of [:the carrier of X, the carrier of Y:]
by Def2;
let X1 be Subset of X, Y1 be Subset of Y;
thus X1 = pr1(the carrier of X, the carrier of Y).:D implies X1 is open
proof
set p = pr1(the carrier of X, the carrier of Y);
set P = .:p;
reconsider PK = P.:K as Subset-Family of X;
reconsider PK as Subset-Family of X;
A3: PK is open
proof
let X1 be Subset of X;
reconsider x1 = X1 as Subset of X;
assume X1 in PK;
then consider
c being Subset of[:the carrier of X, the carrier of Y:] such
that
A4: c in K and
A5: x1 = P.c by FUNCT_2:65;
dom P = bool[:the carrier of X, the carrier of Y:] by FUNCT_2:def 1;
then
A6: X1 = p.:c by A5,FUNCT_3:7;
A7: c = {} or c <> {};
ex X2 being Subset of X, Y2 being Subset of Y st c = [:X2,Y2:] & X2
is open & Y2 is open by A2,A4;
hence thesis by A6,A7,EQREL_1:49;
end;
assume X1 = p.:D;
then X1 = union(P.:K) by A1,EQREL_1:53;
hence thesis by A3,TOPS_2:19;
end;
reconsider PK = P.:K as Subset-Family of Y;
reconsider PK as Subset-Family of Y;
A8: PK is open
proof
let Y1 be Subset of Y;
reconsider y1 = Y1 as Subset of Y;
assume Y1 in PK;
then consider
c being Subset of[:the carrier of X, the carrier of Y:] such that
A9: c in K and
A10: y1 = P.c by FUNCT_2:65;
dom P = bool[:the carrier of X, the carrier of Y:] by FUNCT_2:def 1;
then
A11: Y1 = p.:c by A10,FUNCT_3:7;
A12: c = {} or c <> {};
ex X2 being Subset of X, Y2 being Subset of Y st c = [:X2,Y2:] & X2
is open & Y2 is open by A2,A9;
hence thesis by A11,A12,EQREL_1:49;
end;
assume Y1 = p.:D;
then Y1 = union(P.:K) by A1,EQREL_1:53;
hence thesis by A8,TOPS_2:19;
end;
theorem Th19:
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
proof
let H be Subset-Family of [:X,Y:];
reconsider P1 = Pr1(X,Y).:H as Subset-Family of X;
reconsider P2 = Pr2(X,Y).:H as Subset-Family of Y;
assume
A1: H is open;
A2: P2 is open
proof
let Y1 be Subset of Y;
assume Y1 in P2;
then consider D being Subset of [:X,Y:] such that
A3: D in H and
A4: Y1 = pr2(the carrier of X, the carrier of Y).:D by Th17;
D is open by A1,A3;
hence thesis by A4,Th18;
end;
P1 is open
proof
let X1 be Subset of X;
assume X1 in P1;
then consider D being Subset of [:X,Y:] such that
A5: D in H and
A6: X1 = pr1(the carrier of X, the carrier of Y).:D by Th16;
D is open by A1,A5;
hence thesis by A6,Th18;
end;
hence thesis by A2;
end;
theorem Th20:
for H being Subset-Family of [:X,Y:] st Pr1(X,Y).:H = {} or Pr2(
X,Y).:H = {} holds H = {}
proof
let H be Subset-Family of [:X,Y:];
dom Pr1(X,Y) = bool the carrier of [:X,Y:] & dom Pr2(X,Y) = bool the
carrier of [:X,Y:] by FUNCT_2:def 1;
hence thesis;
end;
theorem Th21:
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)
proof
let H be Subset-Family of [:X,Y:], X1 be Subset of X, Y1 be Subset of Y;
A1: dom .:pr2(the carrier of X, the carrier of Y) = bool dom pr2(the
carrier of X, the carrier of Y) by FUNCT_3:def 1
.= bool[:the carrier of X,the carrier of Y:] by FUNCT_3:def 5;
A2: the carrier of [:X,Y:] = [:the carrier of X, the carrier of Y:] by Def2;
assume
A3: [:X1,Y1:] c= union H;
thus Y1 <> {} implies Pr1(X,Y).:H is Cover of X1
proof
assume Y1 <> {};
then consider y being Point of Y such that
A4: y in Y1 by SUBSET_1:4;
let e be object;
assume
A5: e in X1;
then reconsider x = e as Point of X;
[x,y] in [:X1,Y1:] by A4,A5,ZFMISC_1:87;
then consider A being set such that
A6: [x,y] in A and
A7: A in H by A3,TARSKI:def 4;
[x,y] in [:the carrier of X, the carrier of Y:] by ZFMISC_1:87;
then
A8: [x,y] in dom pr1(the carrier of X, the carrier of Y) by FUNCT_3:def 4;
A9: dom .:pr1(the carrier of X, the carrier of Y) = bool dom pr1(the
carrier of X, the carrier of Y) by FUNCT_3:def 1
.= bool[:the carrier of X,the carrier of Y:] by FUNCT_3:def 4;
e = pr1(the carrier of X, the carrier of Y).(x,y) by FUNCT_3:def 4;
then
A10: e in pr1(the carrier of X, the carrier of Y).:A by A6,A8,FUNCT_1:def 6;
.:pr1(the carrier of X, the carrier of Y).A = pr1(the carrier of X,
the carrier of Y).:A by A2,A7,EQREL_1:47;
then
pr1(the carrier of X, the carrier of Y).:A in Pr1(X,Y).:H by A2,A7,A9,
FUNCT_1:def 6;
hence e in union (Pr1(X,Y).:H) by A10,TARSKI:def 4;
end;
assume X1 <> {};
then consider x being Point of X such that
A11: x in X1 by SUBSET_1:4;
let e be object;
assume
A12: e in Y1;
then reconsider y = e as Point of Y;
[x,y] in [:X1,Y1:] by A11,A12,ZFMISC_1:87;
then consider A being set such that
A13: [x,y] in A and
A14: A in H by A3,TARSKI:def 4;
[x,y] in [:the carrier of X, the carrier of Y:] by ZFMISC_1:87;
then
A15: [x,y] in dom pr2(the carrier of X, the carrier of Y) by FUNCT_3:def 5;
e = pr2(the carrier of X, the carrier of Y).(x,y) by FUNCT_3:def 5;
then
A16: e in pr2(the carrier of X, the carrier of Y).:A by A13,A15,FUNCT_1:def 6;
.:pr2(the carrier of X, the carrier of Y).A = pr2(the carrier of X, the
carrier of Y).:A by A2,A14,EQREL_1:48;
then
pr2(the carrier of X, the carrier of Y).:A in Pr2(X,Y).:H by A2,A14,A1,
FUNCT_1:def 6;
hence e in union (Pr2(X,Y).:H) by A16,TARSKI:def 4;
end;
theorem Th22:
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
proof
let X, Y be TopSpace, H be Subset-Family of X;
let Y be Subset of X;
assume
A1: H is Cover of Y;
defpred P[set] means $1 in H & $1 /\ Y <> {};
{ Z where Z is Subset of X: P[Z]} is Subset-Family of X from DOMAIN_1:
sch 7;
then reconsider F = { Z where Z is Subset of X: Z in H & Z /\ Y <> {}} as
Subset-Family of X;
reconsider F as Subset-Family of X;
take F;
thus F c= H
proof
let e be object;
assume e in F;
then ex Z being Subset of X st e = Z & Z in H & Z /\ Y <> {};
hence thesis;
end;
A2: Y c= union H by A1,SETFAM_1:def 11;
thus F is Cover of Y
proof
let e be object;
assume
A3: e in Y;
then consider u such that
A4: e in u and
A5: u in H by A2,TARSKI:def 4;
reconsider u as Subset of X by A5;
u /\ Y <> {} by A3,A4,XBOOLE_0:def 4;
then u in F by A5;
hence e in union F by A4,TARSKI:def 4;
end;
let C be set;
assume C in F;
then ex Z being Subset of X st C = Z & Z in H & Z /\ Y <> {};
hence C /\ Y <> {};
end;
theorem Th23:
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
proof
let F be Subset-Family of X, H be Subset-Family of [:X,Y:] such that
A1: F is finite and
A2: F c= Pr1(X,Y).:H;
defpred P[object,object] means
$2 in dom Pr1(X,Y) & $2 in H & $1 = Pr1(X,Y).($2);
A3: for e being object st e in F holds
ex u being object st P[e,u] by A2,FUNCT_1:def 6;
consider f being Function such that
A4: dom f = F and
A5: for e being object st e in F holds P[e,f.e] from CLASSES1:sch 1(A3);
A6: f.:F c= H
proof
let e be object;
assume e in f.:F;
then ex u being object st u in dom f & u in F & e = f.u by FUNCT_1:def 6;
hence thesis by A5;
end;
then reconsider G = f.:F as Subset-Family of [:X,Y:] by XBOOLE_1:1;
take G;
thus G c= H by A6;
thus G is finite by A1;
now
let e be object;
thus e in F iff
ex u being object st u in dom Pr1(X,Y) & u in G & e = Pr1(X,Y).u
proof
thus e in F implies
ex u being object st u in dom Pr1(X,Y) & u in G & e = Pr1(X,Y).u
proof
assume
A7: e in F;
take f.e;
thus f.e in dom Pr1(X,Y) by A5,A7;
thus f.e in G by A4,A7,FUNCT_1:def 6;
thus thesis by A5,A7;
end;
given u being object such that
u in dom Pr1(X,Y) and
A8: u in G and
A9: e = Pr1(X,Y).u;
ex v being object st v in dom f & v in F & u = f.v by A8,FUNCT_1:def 6;
hence thesis by A5,A9;
end;
end;
hence thesis by FUNCT_1:def 6;
end;
theorem
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 by EQREL_1:50;
theorem Th25:
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
proof
let t be Point of Y, A be Subset of X such that
A1: A is compact;
let G be a_neighborhood of [:A,{t}:];
A2: the carrier of [:X,Y:] = [:the carrier of X, the carrier of Y:] by Def2;
now
per cases;
suppose
A3: A <> {} X;
[:A,{t}:] c= Int G by CONNSP_2:def 2;
then [:A,{t}:] c= union Base-Appr G by Th14;
then Base-Appr G is Cover of [:A,{t}:] by SETFAM_1:def 11;
then consider K being Subset-Family of [:X,Y:] such that
A4: K c= Base-Appr G and
A5: K is Cover of [:A,{t}:] and
A6: for c being set st c in K holds c meets [:A,{t}:] by Th22;
reconsider PK = Pr1(X,Y).:K as Subset-Family of X;
K is open by A4,TOPS_2:11;
then
A7: Pr1(X,Y).:K is open by Th19;
PK is Cover of A by A5,Th21;
then consider M being Subset-Family of X such that
A8: M c= Pr1(X,Y).:K and
A9: M is Cover of A and
A10: M is finite by A1,A7,COMPTS_1:def 4;
consider N being Subset-Family of [:X,Y:] such that
A11: N c= K and
A12: N is finite and
A13: Pr1(X,Y).:N = M by A8,A10,Th23;
reconsider F = Pr1(X,Y).:N as Subset-Family of X;
A14: N is Cover of [:A,{t}:]
proof
let e1,e2 be object;
A15: A c= union M by A9,SETFAM_1:def 11;
assume
A16: [e1,e2] in [:A,{t}:];
then [e1,e2]`2 in {t} by MCART_1:10;
then [e1,e2]`2 = t by TARSKI:def 1;
then
A17: [e1,e2] = [[e1,e2]`1,t];
[e1,e2]`1 in A by A16,MCART_1:10;
then consider X1 being set such that
A18: [e1,e2]`1 in X1 and
A19: X1 in M by A15,TARSKI:def 4;
consider XY being Subset of [:X,Y:] such that
A20: XY in N and
A21: Pr1(X,Y).XY = X1 by A13,A19,FUNCT_2:65;
XY in K by A11,A20;
then XY in Base-Appr G by A4;
then consider X2 being Subset of X, Y2 being Subset of Y such that
A22: XY = [:X2,Y2:] and
[:X2,Y2:] c= G and
X2 is open and
Y2 is open;
XY meets [:A,{t}:] by A6,A11,A20;
then consider xy being object such that
A23: xy in XY and
A24: xy in [:A,{t}:] by XBOOLE_0:3;
xy`2 in {t} by A24,MCART_1:10;
then xy`2 = t by TARSKI:def 1;
then
A25: t in Y2 by A22,A23,MCART_1:10;
XY <> {} by A18,A21,FUNCT_3:8;
then [e1,e2]`1 in X2 by A18,A21,A22,EQREL_1:50;
then [e1,e2] in [:X2,Y2:] by A25,A17,ZFMISC_1:87;
hence [e1,e2] in union N by A20,A22,TARSKI:def 4;
end;
then F is Cover of A by Th21;
then
A26: A c= union F by SETFAM_1:def 11;
reconsider H = Pr2(X,Y).:N as Subset-Family of Y;
A27: now
let C be set;
assume C in H;
then consider D being Subset of [:X,Y:] such that
A28: D in N and
A29: C = pr2(the carrier of X, the carrier of Y).:D by Th17;
D meets [:A,{t}:] by A6,A11,A28;
then D /\ [:A,{t}:] <> {};
then consider x being Point of [:X,Y:] such that
A30: x in D /\ [:A,{t}:];
A31: x in [:A,{t}:] by A30,XBOOLE_0:def 4;
then x`1 in A by MCART_1:10;
then
A32: (pr2(the carrier of X, the carrier of Y)).(x`1,t) = t by FUNCT_3:def 5;
x`2 in {t} by A31,MCART_1:10;
then x`2 = t by TARSKI:def 1;
then
A33: x = [x`1,t] by A2,MCART_1:21;
x in D by A30,XBOOLE_0:def 4;
hence t in C by A2,A29,A33,A32,FUNCT_2:35;
end;
[:A,{t}:] c= union N by A14,SETFAM_1:def 11;
then N <> {} by A3,ZFMISC_1:2;
then H <> {} by Th20;
then
A34: t in meet H by A27,SETFAM_1:def 1;
A35: N c= Base-Appr G by A4,A11;
then
A36: N is open by TOPS_2:11;
then meet H is open by A12,Th19,TOPS_2:20;
then t in Int meet H by A34,TOPS_1:23;
then reconsider W = meet H as a_neighborhood of t by CONNSP_2:def 1;
union F is open by A36,Th19,TOPS_2:19;
then A c= Int union F by A26,TOPS_1:23;
then reconsider V = union F as a_neighborhood of A by CONNSP_2:def 2;
take V,W;
now
let e;
assume e in N;
then e in Base-Appr G by A35;
then ex X1 being Subset of X, Y1 being Subset of Y st e = [:X1,Y1:] &
[:X1,Y1:] c= G & X1 is open & Y1 is open;
hence
e c= G & ex X1 being Subset of X, Y1 being Subset of Y st e =[:X1
,Y1:];
end;
hence [:V,W:] c= G by Th15;
end;
suppose
A = {} X;
then A c= Int {} X;
then reconsider V = {} X as a_neighborhood of A by CONNSP_2:def 2;
set W = the a_neighborhood of t;
take V,W;
thus [:V,W:] c= G;
end;
end;
hence thesis;
end;
begin
::
:: Partitions of topological spaces
::
definition
let X be 1-sorted;
func TrivDecomp X -> a_partition of the carrier of X equals
Class(id the
carrier of X);
coherence;
end;
registration
let X be non empty 1-sorted;
cluster TrivDecomp X -> non empty;
coherence;
end;
theorem Th26:
for A being Subset of X st A in TrivDecomp X ex x being Point of X st A = {x}
proof
let A be Subset of X;
assume A in TrivDecomp X;
then consider x being object such that
A1: x in the carrier of X and
A2: A = Class(id the carrier of X,x) by EQREL_1:def 3;
reconsider x as Point of X by A1;
take x;
thus thesis by A2,EQREL_1:25;
end;
Lm1: for A being Subset of X 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
TrivDecomp X & B meets W holds B c= W
proof
let A be Subset of X;
let V be a_neighborhood of A;
take Int V;
thus Int V is open;
thus A c= Int V by CONNSP_2:def 2;
thus Int V c= V by TOPS_1:16;
let B be Subset of X such that
A1: B in TrivDecomp X and
A2: B meets Int V;
consider x being Point of X such that
A3: B = {x} by A1,Th26;
x in Int V by A2,A3,ZFMISC_1:50;
hence thesis by A3,ZFMISC_1:31;
end;
definition
let X be TopSpace, D be a_partition of the carrier of X;
func space D -> strict TopSpace means
:Def7:
the carrier of it = D & the
topology of it = { A where A is Subset of D : union A in the topology of X};
existence
proof
set t = { A where A is Subset of D : union A in the topology of X};
t c= bool D
proof
let e be object;
assume e in t;
then ex A being Subset of D st e = A & union A in the topology of X;
hence thesis;
end;
then reconsider t as Subset-Family of D;
set T = TopStruct(#D,t#);
T is TopSpace-like
proof
union D = the carrier of X by EQREL_1:def 4;
then D c= D & union D in the topology of X by PRE_TOPC:def 1;
hence the carrier of T in the topology of T;
thus for a being Subset-Family of T st a c= the topology of T holds
union a in the topology of T
proof
let a be Subset-Family of T;
A1: { union A where A is Subset of T: A in a } c= bool the carrier of X
proof
let e be object;
reconsider ee=e as set by TARSKI:1;
assume e in { union A where A is Subset of T: A in a };
then consider A being Subset of T such that
A2: e = union A and
A in a;
ee c= the carrier of X
proof
let u be object;
assume u in ee;
then consider x being set such that
A3: u in x and
A4: x in A by A2,TARSKI:def 4;
x in the carrier of T by A4;
hence thesis by A3;
end;
hence thesis;
end;
assume
A5: a c= the topology of T;
{ union A where A is Subset of T: A in a } c= the topology of X
proof
let e be object;
assume e in { union A where A is Subset of T: A in a };
then consider A being Subset of T such that
A6: e = union A and
A7: A in a;
A in the topology of T by A5,A7;
then ex B being Subset of D st A = B & union B in the topology of X;
hence thesis by A6;
end;
then union{union A where A is Subset of T: A in a} in the topology of
X by A1,PRE_TOPC:def 1;
then union union a in the topology of X by EQREL_1:54;
hence thesis;
end;
let a,b be Subset of T;
assume that
A8: a in the topology of T and
A9: b in the topology of T;
consider B being Subset of D such that
A10: b = B and
A11: union B in the topology of X by A9;
consider A being Subset of D such that
A12: a = A and
A13: union A in the topology of X by A8;
union(A /\ B) = (union A) /\ union B by EQREL_1:62;
then union(A /\ B) in the topology of X by A13,A11,PRE_TOPC:def 1;
hence thesis by A12,A10;
end;
then reconsider T as strict TopSpace;
take T;
thus thesis;
end;
uniqueness;
end;
registration
let X be non empty TopSpace, D be a_partition of the carrier of X;
cluster space D -> non empty;
coherence by Def7;
end;
theorem Th27:
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
proof
let D be non empty a_partition of the carrier of X, B be Subset of D;
A1: the topology of space D = { A where A is Subset of D : union A in the
topology of X } by Def7;
hence union B in the topology of X implies B in the topology of space D;
assume B in the topology of space D;
then ex A being Subset of D st B = A & union A in the topology of X by A1;
hence thesis;
end;
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
proj D;
coherence
proof
reconsider F = proj D as Function of X, space D by Def7;
A1: the carrier of space D = D by Def7;
F is continuous
proof
let W be Point of X, G be a_neighborhood of F.W;
reconsider H = union Int G as Subset of X by A1,EQREL_1:61;
F.W in Int G by CONNSP_2:def 1;
then W in F"Int G by FUNCT_2:38;
then
A2: W in union Int G by A1,EQREL_1:67;
Int G in the topology of space D by PRE_TOPC:def 2;
then union Int G in the topology of X by A1,Th27;
then H is open;
then W in Int H by A2,TOPS_1:23;
then W in Int(F"Int G) by A1,EQREL_1:67;
then reconsider N = F"Int G as a_neighborhood of W by CONNSP_2:def 1;
take N;
F.:N c= Int G & Int G c= G by FUNCT_1:75,TOPS_1:16;
hence thesis;
end;
hence thesis;
end;
correctness;
end;
theorem
for D being non empty a_partition of the carrier of X, W being Point
of X holds W in Proj D.W by EQREL_1:def 9;
theorem Th29:
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
proof
let D be non empty a_partition of the carrier of X, W be Point of space D;
reconsider p = W as Element of D by Def7;
consider W9 being Point of X such that
A1: (proj D).W9 = p by EQREL_1:68;
take W9;
thus thesis by A1;
end;
theorem Th30:
for D being non empty a_partition of the carrier of X holds rng
Proj D = the carrier of space D
proof
let D be non empty a_partition of the carrier of X;
thus rng Proj D c= the carrier of space D;
let e be object;
assume e in the carrier of space D;
then ex p being Point of X st (Proj D).p = e by Th29;
hence thesis by FUNCT_2:4;
end;
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
D \/ {{p
} where p is Point of XX : not p in the carrier of X};
coherence
proof
set E = D \/ {{p} where p is Point of XX : not p in the carrier of X};
E c= bool the carrier of XX
proof
let e be object;
assume
A1: e in E;
now
per cases by A1,XBOOLE_0:def 3;
suppose
A2: e in D;
bool the carrier of X c= bool the carrier of XX by Th1,ZFMISC_1:67;
hence thesis by A2;
end;
suppose
e in {{p} where p is Point of XX : not p in the carrier of X };
then
ex p being Point of XX st e = {p} & not p in the carrier of X;
hence thesis;
end;
end;
hence thesis;
end;
then reconsider E as Subset-Family of XX;
E is a_partition of the carrier of XX
proof
now
let e be object;
thus e in (the carrier of XX) \ the carrier of X implies ex Z being
set st e in Z & Z in {{p} where p is Point of XX : not p in the carrier of X}
proof
assume
A3: e in (the carrier of XX) \ the carrier of X;
take {e};
thus e in {e} by TARSKI:def 1;
not e in the carrier of X by A3,XBOOLE_0:def 5;
hence thesis by A3;
end;
given Z being set such that
A4: e in Z and
A5: Z in {{p} where p is Point of XX : not p in the carrier of X};
consider p being Point of XX such that
A6: Z = {p} and
A7: not p in the carrier of X by A5;
e = p by A4,A6,TARSKI:def 1;
hence e in (the carrier of XX) \ the carrier of X by A7,XBOOLE_0:def 5;
end;
then
A8: union {{p} where p is Point of XX : not p in the carrier of X} = (
the carrier of XX) \ the carrier of X by TARSKI:def 4;
thus union E = union D \/ union {{p} where p is Point of XX : not p in
the carrier of X} by ZFMISC_1:78
.= (the carrier of X) \/ ((the carrier of XX) \ the carrier of X) by A8
,EQREL_1:def 4
.= the carrier of XX by Th1,XBOOLE_1:45;
let A be Subset of XX;
assume
A9: A in E;
now
per cases by A9,XBOOLE_0:def 3;
suppose
A in D;
hence A <> {} by EQREL_1:def 4;
end;
suppose
A in {{p} where p is Point of XX : not p in the carrier of X};
then ex p being Point of XX st A ={p} & not p in the carrier of X;
hence A<>{};
end;
end;
hence A<>{};
let B be Subset of XX;
assume
A10: B in E;
now
per cases by A9,XBOOLE_0:def 3;
suppose
A11: A in D;
now
per cases by A10,XBOOLE_0:def 3;
suppose
B in D;
hence thesis by A11,EQREL_1:def 4;
end;
suppose
B in {{p} where p is Point of XX : not p in the carrier of X};
then ex p being Point of XX st B ={p} & not p in the carrier of
X;
then B misses the carrier of X by ZFMISC_1:50;
hence thesis by A11,XBOOLE_1:63;
end;
end;
hence thesis;
end;
suppose
A in {{p} where p is Point of XX : not p in the carrier of X};
then
A12: ex p being Point of XX st A ={p} & not p in the carrier of X;
then
A13: A misses the carrier of X by ZFMISC_1:50;
now
per cases by A10,XBOOLE_0:def 3;
suppose
B in D;
hence thesis by A13,XBOOLE_1:63;
end;
suppose
B in {{p} where p is Point of XX : not p in the carrier of X};
then
ex p being Point of XX st B = {p} & not p in the carrier of X;
hence thesis by A12,ZFMISC_1:11;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
correctness;
end;
theorem Th31:
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
}
proof
let XX be non empty TopSpace, X be non empty SubSpace of XX, D be non empty
a_partition of the carrier of X, A be Subset of XX;
assume
A1: A in TrivExt D;
now
per cases by A1,XBOOLE_0:def 3;
case
A in D;
hence A in D;
end;
case
A in {{p} where p is Point of XX : not p in the carrier of X};
then consider x being Point of XX such that
A2: A = {x} and
A3: not x in the carrier of X;
take x;
thus not x in [#]X by A3;
thus A = {x} by A2;
end;
end;
hence thesis;
end;
theorem Th32:
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
proof
let XX be non empty TopSpace, X be non empty SubSpace of XX, D be non empty
a_partition of the carrier of X, x be Point of XX;
union TrivExt D = the carrier of XX by EQREL_1:def 4;
then consider A being set such that
A1: x in A and
A2: A in TrivExt D by TARSKI:def 4;
assume not x in the carrier of X;
then not A in D by A1;
then A in {{p} where p is Point of XX : not p in the carrier of X} by A2,
XBOOLE_0:def 3;
then ex p being Point of XX st A = {p} & not p in the carrier of X;
hence thesis by A1,A2,TARSKI:def 1;
end;
theorem Th33:
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
proof
let XX be non empty TopSpace, X be non empty SubSpace of XX, D be non empty
a_partition of the carrier of X, W be Point of XX;
assume
A1: W in the carrier of X;
then reconsider p = W as Point of X;
D c= TrivExt D & proj D.p in D by XBOOLE_1:7;
then reconsider A = Proj D.W as Element of TrivExt D;
W in A by A1,EQREL_1:def 9;
hence thesis by EQREL_1:65;
end;
theorem Th34:
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}
proof
let XX be non empty TopSpace, X be non empty SubSpace of XX, D be non empty
a_partition of the carrier of X, W be Point of XX;
assume not W in the carrier of X;
then W in {W} & {W} in TrivExt D by Th32,TARSKI:def 1;
hence thesis by EQREL_1:65;
end;
theorem Th35:
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
proof
let XX be non empty TopSpace, X be non empty SubSpace of XX, D be non empty
a_partition of the carrier of X, W,W9 be Point of XX;
assume not W in the carrier of X;
then
A1: Proj TrivExt D.W = {W} by Th34;
W9 in Proj TrivExt D.W9 by EQREL_1:def 9;
hence thesis by A1,TARSKI:def 1;
end;
theorem Th36:
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
proof
let XX be non empty TopSpace , X be non empty SubSpace of XX;
let D be non empty a_partition of the carrier of X;
let e be Point of XX;
assume Proj TrivExt D.e in the carrier of space D;
then
A1: Proj TrivExt D.e in D by Def7;
e in Proj TrivExt D.e by EQREL_1:def 9;
hence thesis by A1;
end;
theorem Th37:
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
proof
let XX be non empty TopSpace , X be non empty SubSpace of XX;
let D be non empty a_partition of the carrier of X;
let e;
assume
A1: e in the carrier of X;
then reconsider x = e as Point of X;
the carrier of X c= the carrier of XX by Th1;
then Proj D.x = Proj TrivExt D.x by A1,Th33;
hence thesis;
end;
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:
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;
correctness
proof
take TrivDecomp X;
thus thesis by Lm1;
end;
end;
theorem Th38:
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
proof
let D be u.s.c._decomposition of X, t be Point of space D, G be
a_neighborhood of Proj D " {t};
A1: the carrier of space D = D by Def7;
then Proj D " {t} = t by EQREL_1:66;
then consider W being Subset of X such that
A2: W is open and
A3: Proj D " {t} c= W and
A4: W c= G and
A5: for B being Subset of X st B in D & B meets W holds B c= W by A1,Def10;
set Q = Proj D .:W;
A6: Proj D .: Proj D " {t} c= Q by A3,RELAT_1:123;
union Q = proj D " Q by A1,EQREL_1:67
.= W by A5,EQREL_1:69;
then union Q in the topology of X by A2;
then Q in the topology of space D by A1,Th27;
then
A7: Q is open;
rng Proj D = the carrier of space D by Th30;
then {t} c= Q by A6,FUNCT_1:77;
then
A8: t in Q by ZFMISC_1:31;
Q c= (Proj D).:G by A4,RELAT_1:123;
then t in Int((Proj D).:G) by A7,A8,TOPS_1:22;
hence thesis by CONNSP_2:def 1;
end;
theorem Th39:
TrivDecomp X is u.s.c._decomposition of X
proof
thus for A being Subset of X st A in TrivDecomp X 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 TrivDecomp X & B meets W holds B c= W by Lm1;
end;
definition
let X be TopSpace;
let IT be SubSpace of X;
attr IT is closed means
:Def11:
for A being Subset of X st A = the carrier of IT holds A is closed;
end;
Lm2: for T being TopStruct holds the TopStruct of T is SubSpace of T
proof
let T be TopStruct;
set S = the TopStruct of T;
thus [#]S c= [#]T;
let P be Subset of S;
hereby
reconsider Q = P as Subset of T;
assume
A1: P in the topology of S;
take Q;
thus Q in the topology of T by A1;
thus P = Q /\ [#]S by XBOOLE_1:28;
end;
given Q being Subset of T such that
A2: Q in the topology of T & P = Q /\ [#]S;
thus thesis by A2,XBOOLE_1:28;
end;
registration
let X be TopSpace;
cluster strict closed for SubSpace of X;
existence
proof
reconsider Y = the TopStruct of X as strict SubSpace of X by Lm2;
take Y;
Y is closed
proof
let A be Subset of X;
assume A = the carrier of Y;
then A = [#]X;
hence thesis;
end;
hence thesis;
end;
end;
registration
let X;
cluster strict closed non empty for SubSpace of X;
existence
proof
X|[#]X is closed
proof
let A be Subset of X;
assume A = the carrier of X|[#]X;
then A = [#](X|[#]X) .= [#] X by PRE_TOPC:def 5;
hence thesis;
end;
hence thesis;
end;
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; :: redefines TrivExt (BORSUK_1, definition)
correctness
proof
let A be Subset of XX such that
A1: A in TrivExt D;
let V be a_neighborhood of A;
A2: A c= Int V by CONNSP_2:def 2;
A3: Int V c= V by TOPS_1:16;
now
per cases by A1,Th31;
suppose
A4: A in D;
then reconsider C = A as Subset of X;
reconsider E = Int V /\ [#]X as Subset of X;
E is open & C c= E by A2,TOPS_2:24,XBOOLE_1:19;
then C c= Int E by TOPS_1:23;
then E is a_neighborhood of C by CONNSP_2:def 2;
then consider W being Subset of X such that
A5: W is open and
A6: C c= W and
A7: W c= E and
A8: for B being Subset of X st B in D & B meets W holds B c= W by A4,Def10;
consider G being Subset of XX such that
A9: G is open and
A10: W = G /\ [#] X by A5,TOPS_2:24;
take H = G /\ Int V;
thus H is open by A9;
A11: W c= G by A10,XBOOLE_1:17;
then C c= G by A6;
hence A c= H by A2,XBOOLE_1:19;
H c= Int V by XBOOLE_1:17;
hence H c= V by A3;
let B be Subset of XX such that
A12: B in TrivExt D and
A13: B meets H;
E c= Int V by XBOOLE_1:17;
then W c= Int V by A7;
then
A14: W c= H by A11,XBOOLE_1:19;
now
per cases by A12,Th31;
suppose
A15: B in D;
B meets G by A13,XBOOLE_1:74;
then B meets W by A10,A15,XBOOLE_1:77;
then B c= W by A8,A15;
hence B c= H by A14;
end;
suppose
ex y being Point of XX st not y in [#]X & B = {y};
then consider y being Point of XX such that
not y in [#]X and
A16: B = {y};
y in H by A13,A16,ZFMISC_1:50;
hence B c= H by A16,ZFMISC_1:31;
end;
end;
hence B c= H;
end;
suppose
A17: ex x being Point of XX st not x in [#] X & A = {x};
[#]X c= [#]XX by PRE_TOPC:def 4;
then reconsider C = [#]X as Subset of XX;
take W = Int V \ C;
C is closed by Def11;
then (Int V) /\ C` is open;
hence W is open by SUBSET_1:13;
consider x being Point of XX such that
A18: not x in [#]X and
A19: A = {x} by A17;
x in A by A19,TARSKI:def 1;
then x in W by A2,A18,XBOOLE_0:def 5;
hence A c= W by A19,ZFMISC_1:31;
W c= Int V by XBOOLE_1:36;
hence W c= V by A3;
let B be Subset of XX such that
A20: B in TrivExt D and
A21: B meets W;
now
A22: W misses C by XBOOLE_1:79;
assume B in D;
hence contradiction by A21,A22,XBOOLE_1:63;
end;
then consider y being Point of XX such that
not y in [#]X and
A23: B = {y} by A20,Th31;
y in W by A21,A23,ZFMISC_1:50;
hence B c= W by A23,ZFMISC_1:31;
end;
end;
hence thesis;
end;
end;
definition
let X be non empty TopSpace;
let IT be u.s.c._decomposition of X;
attr IT is DECOMPOSITION-like means
:Def12:
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;
existence
proof
reconsider D = TrivDecomp X as u.s.c._decomposition of X by Th39;
take D;
let A be Subset of X;
assume A in D;
then ex x being Point of X st A = {x} by Th26;
hence thesis;
end;
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; :: redefines TrivExt (BORSUK_1, definition)
correctness
proof
TrivExt D is DECOMPOSITION-like
proof
let A be Subset of XX;
assume A in TrivExt D;
then consider W being Point of XX such that
A1: A = (proj TrivExt D).W by EQREL_1:68;
A2: A = Proj TrivExt D.W by A1;
A3: the carrier of space D = D by Def7;
now
per cases;
suppose
W in the carrier of X;
then reconsider W9 = W as Point of X;
A4: A = (Proj D).W9 by A2,Th33;
then reconsider B = A as Subset of X by A3,TARSKI:def 3;
B is compact by A3,A4,Def12;
hence thesis by COMPTS_1:19;
end;
suppose
not W in the carrier of X;
then A = {W} by A2,Th34;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
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; :: redefines space (BORSUK_1, definition)
correctness
proof
A1: the topology of space TrivExt D = { A where A is Subset of TrivExt D :
union A in the topology of X} by Def7;
A2: the carrier of space TrivExt D = TrivExt D by Def7;
A3: the topology of space D = { A where A is Subset of D : union A in the
topology of Y} by Def7;
A4: the carrier of space D = D by Def7;
A5: [#] space D = D & [#] space TrivExt D = TrivExt D by Def7;
now
thus [#](space D) c= [#](space TrivExt D) by A5,XBOOLE_1:7;
let P be Subset of space D;
thus P in the topology of space D implies ex Q being Subset of space
TrivExt D st Q in the topology of space TrivExt D & P = Q /\ [#](space D)
proof
D c= TrivExt D by XBOOLE_1:7;
then
A6: P c= TrivExt D by A4;
assume P in the topology of space D;
then consider A being Subset of D such that
A7: P = A and
A8: union A in the topology of Y by A3;
reconsider B = union A as Subset of Y by A8;
consider C being Subset of X such that
A9: C in the topology of X and
A10: B = C /\ [#]Y by A8,PRE_TOPC:def 4;
{{x} where x is Point of X : x in C \ [#] Y} c= TrivExt D
proof
let e be object;
assume e in {{x} where x is Point of X : x in C \ [#] Y};
then consider x being Point of X such that
A11: e = {x} and
A12: x in C \ [#] Y;
not x in the carrier of Y by A12,XBOOLE_0:def 5;
hence thesis by A11,Th32;
end;
then reconsider
Q = P \/ {{x} where x is Point of X : x in C \ [#] Y} as
Subset of space TrivExt D by A2,A6,XBOOLE_1:8;
take Q;
now
let e be object;
thus e in C implies ex u st e in u & u in Q
proof
assume
A13: e in C;
then reconsider x = e as Point of X;
now
per cases;
case
e in [#] Y;
then e in B by A10,A13,XBOOLE_0:def 4;
then consider u such that
A14: e in u & u in P by A7,TARSKI:def 4;
take u;
thus e in u & u in Q by A14,XBOOLE_0:def 3;
end;
case
A15: not e in [#] Y;
take u = {e};
thus e in u by TARSKI:def 1;
x in C \ [#] Y by A13,A15,XBOOLE_0:def 5;
then u in {{y} where y is Point of X : y in C \ [#] Y};
hence u in Q by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
given u such that
A16: e in u and
A17: u in Q;
now
per cases by A17,XBOOLE_0:def 3;
suppose
u in P;
then e in B by A7,A16,TARSKI:def 4;
hence e in C by A10,XBOOLE_0:def 4;
end;
suppose
u in {{x} where x is Point of X : x in C \ [#] Y};
then consider x being Point of X such that
A18: u = {x} and
A19: x in C \ [#] Y;
e = x by A16,A18,TARSKI:def 1;
hence e in C by A19,XBOOLE_0:def 5;
end;
end;
hence e in C;
end;
then C = union Q by TARSKI:def 4;
hence Q in the topology of space TrivExt D by A2,A1,A9;
P c= Q by XBOOLE_1:7;
hence P c= Q /\ [#] space D by XBOOLE_1:19;
let e be object;
assume
A20: e in Q /\ [#] space D;
then
A21: e in [#] space D;
A22: now
assume e in {{x} where x is Point of X : x in C \ [#] Y};
then consider x being Point of X such that
A23: e = {x} and
A24: x in C \ [#] Y;
A25: not x in the carrier of Y by A24,XBOOLE_0:def 5;
then not Proj TrivExt D.x in the carrier of space D by Th36;
hence contradiction by A21,A23,A25,Th34;
end;
e in Q by A20,XBOOLE_0:def 4;
hence thesis by A22,XBOOLE_0:def 3;
end;
given Q being Subset of space TrivExt D such that
A26: Q in the topology of space TrivExt D and
A27: P = Q /\ [#](space D);
A28: union P is Subset of Y by A4,EQREL_1:61;
now
let e be object;
thus e in (union Q) /\ [#] Y implies ex u st e in u & u in P
proof
assume
A29: e in (union Q) /\ [#] Y;
then
A30: Proj TrivExt D.e in the carrier of space D by Th37;
e in union Q by A29,XBOOLE_0:def 4;
then consider u such that
A31: e in u and
A32: u in Q by TARSKI:def 4;
take u;
thus e in u by A31;
u is Element of TrivExt D by A32,Def7;
then u = Proj TrivExt D.e by A31,EQREL_1:65;
hence thesis by A27,A32,A30,XBOOLE_0:def 4;
end;
given u such that
A33: e in u and
A34: u in P;
u in Q by A27,A34,XBOOLE_0:def 4;
then
A35: e in union Q by A33,TARSKI:def 4;
e in union P by A33,A34,TARSKI:def 4;
hence e in (union Q) /\ [#] Y by A28,A35,XBOOLE_0:def 4;
end;
then
A36: union P = (union Q) /\ [#] Y by TARSKI:def 4;
ex A being Subset of TrivExt D st Q = A & union A in the topology
of X by A1,A26;
then union P in the topology of Y by A36,PRE_TOPC:def 4;
hence P in the topology of space D by A4,A3;
end;
then reconsider T = space D as SubSpace of space TrivExt D by
PRE_TOPC:def 4;
T is closed
proof
let A be Subset of space TrivExt D such that
A37: A = the carrier of T;
reconsider C = A` as Subset of TrivExt D by Def7;
reconsider B = union A as Subset of X by A2,EQREL_1:61;
B = the carrier of Y by A4,A37,EQREL_1:def 4;
then B is closed by Def11;
then
A38: B` in the topology of X by PRE_TOPC:def 2;
union C = B` by A2,EQREL_1:63;
then A` in the topology of space TrivExt D by A38,Th27;
then A` is open;
hence thesis by TOPS_1:3;
end;
hence thesis;
end;
end;
begin
::
:: Decomposition of retracts
::
Lm3: TopSpaceMetr RealSpace = TopStruct(#the carrier of RealSpace,
Family_open_set RealSpace#) by PCOMPS_1:def 5;
definition
func I[01] -> TopStruct means
:Def13:
for P being Subset of TopSpaceMetr(
RealSpace) st P = [.0,1.] holds it = (TopSpaceMetr RealSpace)|P;
existence
proof
reconsider P = [.0,1.] as non empty Subset of TopSpaceMetr RealSpace by Lm3
,METRIC_1:def 13,XXREAL_1:1;
take (TopSpaceMetr RealSpace)|P;
thus thesis;
end;
uniqueness
proof
reconsider P = [.0,1.] as Subset of TopSpaceMetr RealSpace by Lm3,
METRIC_1:def 13;
let I1,I2 be TopStruct such that
A1: for P being Subset of TopSpaceMetr(RealSpace) st P = [.0,1.] holds
I1 = (TopSpaceMetr RealSpace)|P and
A2: for P being Subset of TopSpaceMetr(RealSpace) st P = [.0,1.] holds
I2 = (TopSpaceMetr RealSpace)|P;
I1 = (TopSpaceMetr RealSpace)|P by A1;
hence thesis by A2;
end;
end;
registration
cluster I[01] -> strict non empty TopSpace-like;
coherence
proof
reconsider P = [.0,1.] as non empty Subset of TopSpaceMetr RealSpace by Lm3
,METRIC_1:def 13,XXREAL_1:1;
I[01] = (TopSpaceMetr RealSpace)|P by Def13;
hence thesis;
end;
end;
theorem Th40:
the carrier of I[01] = [.0,1.]
proof
reconsider P = [.0,1.] as Subset of TopSpaceMetr RealSpace by Lm3,
METRIC_1:def 13;
A1: I[01] = (TopSpaceMetr RealSpace)|P by Def13;
thus the carrier of I[01] = [#] I[01] .= [.0,1.] by A1,PRE_TOPC:def 5;
end;
definition
func 0[01] -> Point of I[01] equals
0;
coherence by Th40,XXREAL_1:1;
func 1[01] -> Point of I[01] equals
1;
coherence by Th40,XXREAL_1: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
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
ex F being continuous Function of X,Y st F is being_a_retraction;
pred Y is_an_SDR_of X means
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
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
proof
let XX be non empty TopSpace, X be closed non empty SubSpace of XX, D be
DECOMPOSITION of X;
thus X is_a_retract_of XX implies space(D) is_a_retract_of space(TrivExt D)
proof
given R being continuous Function of XX,X such that
A1: R is being_a_retraction;
now
given xx,xx9 being Point of XX such that
A2: Proj TrivExt D.xx=Proj TrivExt D.xx9 & (Proj D*R).xx<>(Proj D*R) .xx9;
xx in the carrier of X by A2,Th35;
then R.xx=xx by A1;
then
A3: Proj D.xx = (Proj D*R).xx by FUNCT_2:15;
xx9 in the carrier of X by A2,Th35;
then
A4: R.xx9=xx9 by A1;
Proj TrivExt D.xx=Proj D.xx & Proj TrivExt D.xx9=Proj D.xx9 by A2,Th33
,Th35;
hence contradiction by A2,A4,A3,FUNCT_2:15;
end;
then consider
F being Function of the carrier of space TrivExt D, the carrier
of space D such that
A5: F*(Proj TrivExt D)=(Proj D)*R by EQREL_1:56;
reconsider F as Function of space TrivExt D, space D;
F is continuous
proof
let W be Point of space TrivExt D;
let G be a_neighborhood of F.W;
reconsider GG=(Proj D*R)"G as a_neighborhood of Proj TrivExt D"{W} by A5
,Th4,EQREL_1:57;
reconsider V9=Proj TrivExt D.:GG as a_neighborhood of W by Th38;
take V=V9;
F.:V=(Proj D*R).:GG by A5,RELAT_1:126;
hence thesis by FUNCT_1:75;
end;
then reconsider F9=F as continuous Function of space TrivExt D, space D;
take F9;
let W be Point of space TrivExt D;
consider W9 being Point of XX such that
A6: Proj TrivExt D.W9=W by Th29;
assume
A7: W in the carrier of space D;
then W9 in the carrier of X by A6,Th36;
then
A8: W9=R.W9 by A1;
A9: F9.W = (F*Proj TrivExt D).W9 by A6,FUNCT_2:15;
Proj D.W9=Proj TrivExt D.W9 by A6,A7,Th33,Th36;
hence thesis by A5,A6,A8,A9,FUNCT_2:15;
end;
end;
::$N Borsuk Theorem on Decomposition of Strong Deformation Retracts
::$L https://en.wikipedia.org/wiki/Retraction_(topology) Retraction
theorem
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)
proof
let XX be non empty TopSpace, X be closed non empty SubSpace of XX, D be
DECOMPOSITION of X;
given CH1 being continuous Function of [:XX,I[01]:],XX such that
A1: for A being Point of XX holds CH1. [A,0[01]] =A & CH1. [A,1[01]] in
the carrier of X & (A in the carrier of X implies for T being Point of I[01]
holds CH1. [A,T] =A);
the carrier of [:XX,I[01]:]=[:the carrier of XX, the carrier of I[01] :]
by Def2;
then reconsider
II=[:Proj TrivExt D, id the carrier of I[01]:] as Function of the
carrier of [:XX,I[01]:], the carrier of [:space TrivExt D,I[01]:] by Def2;
now
given xx,xx9 being Point of [:XX,I[01]:] such that
A2: II.xx=II.xx9 and
A3: (Proj TrivExt D*CH1).xx<>(Proj TrivExt D*CH1).xx9;
A4: (Proj TrivExt D*CH1).xx = Proj TrivExt D.(CH1.xx) & (Proj TrivExt D*
CH1).xx9 = Proj TrivExt D.(CH1.xx9) by FUNCT_2:15;
consider x being Point of XX, t being Point of I[01] such that
A5: xx=[x,t] by Th10;
consider x9 being Point of XX, t9 being Point of I[01] such that
A6: xx9=[x9,t9] by Th10;
A7: II.(x,t)=[Proj TrivExt D.x,t] & II.(x9,t9)=[Proj TrivExt D.x9,t9] by
EQREL_1:58;
then t=t9 & Proj TrivExt D.x=Proj TrivExt D.x9 by A2,A5,A6,XTUPLE_0:1;
then CH1.xx=x & CH1.xx9=x9 by A1,A3,A5,A6,Th35;
hence contradiction by A2,A3,A5,A6,A7,A4,XTUPLE_0:1;
end;
then consider
THETA being Function of the carrier of [:space TrivExt D,I[01]:],
the carrier of space TrivExt D such that
A8: Proj TrivExt D*CH1 = THETA*II by EQREL_1:56;
reconsider THETA as Function of [:space TrivExt D,I[01]:], space TrivExt D;
THETA is continuous
proof
let WT be Point of [:space TrivExt D,I[01]:];
reconsider xt9=WT as Element of [:the carrier of space TrivExt D, the
carrier of I[01]:] by Def2;
let G be a_neighborhood of THETA.WT;
reconsider FF = Proj TrivExt D*CH1 as continuous Function of [:XX,I[01]:],
space TrivExt D;
consider W being Point of space TrivExt D, T being Point of I[01] such
that
A9: WT=[W,T] by Th10;
II"{xt9} = [:Proj TrivExt D"{W},{T}:] by A9,EQREL_1:60;
then reconsider
GG=FF"G as a_neighborhood of [:Proj TrivExt D"{W},{T}:] by A8,Th4,
EQREL_1:57;
W in the carrier of space TrivExt D;
then
A10: W in TrivExt D by Def7;
then (Proj TrivExt D)"{W} = W by EQREL_1:66;
then Proj TrivExt D"{W} is compact by A10,Def12;
then consider U being a_neighborhood of Proj TrivExt D"{W}, V being
a_neighborhood of T such that
A11: [:U,V:] c= GG by Th25;
reconsider H9=Proj(TrivExt D).:U as a_neighborhood of W by Th38;
reconsider H99=[:H9,V:] as a_neighborhood of WT by A9;
take H=H99;
II.:[:U,V:]=[:Proj TrivExt D.:U,V:] by EQREL_1:59;
then
A12: (Proj TrivExt D*CH1).:GG c= G & THETA.:H=(Proj TrivExt D*CH1).:[:U,V
:] by A8,FUNCT_1:75,RELAT_1:126;
(Proj TrivExt D*CH1).:[:U,V:] c= (Proj TrivExt D*CH1).:GG by A11,
RELAT_1:123;
hence thesis by A12;
end;
then reconsider
THETA9=THETA as continuous Function of [:space TrivExt D,I[01]:],
space TrivExt D;
take THETA99=THETA9;
let W be Point of space(TrivExt D);
consider W9 being Point of XX such that
A13: Proj(TrivExt D).W9=W by Th29;
II.(W9,0[01]) = [W,0[01]] by A13,EQREL_1:58;
then
A14: (THETA9*II). [W9,0[01]] = THETA9. [W,0[01]] by FUNCT_2:15;
CH1.(W9,0[01]) =W9 by A1;
hence THETA99. [W,0[01]] =W by A8,A13,A14,FUNCT_2:15;
A15: CH1. [W9,1[01]] in the carrier of X by A1;
II.(W9,1[01]) =[W,1[01]] by A13,EQREL_1:58;
then
A16: (THETA9*II). [W9,1[01]] = THETA9. [W,1[01]] by FUNCT_2:15;
(THETA9*II). [W9,1[01]] = Proj TrivExt D.(CH1. [W9,1[01]]) by A8,FUNCT_2:15;
hence THETA99. [W,1[01]] in the carrier of space(D) by A16,A15,Th37;
assume
A17: W in the carrier of space(D);
let T be Point of I[01];
II.(W9,T) = [W,T] by A13,EQREL_1:58;
then
A18: (THETA9*II). [W9,T] = THETA9. [W,T] by FUNCT_2:15;
CH1.(W9,T) =W9 by A1,A13,A17,Th36;
hence thesis by A8,A13,A18,FUNCT_2:15;
end;
theorem
for r being Real holds 0 <= r & r <= 1 iff r in the carrier of I[01]
proof
let r be Real;
A1: [.0,1.] = { r1 where r1 is Real: 0 <= r1 & r1 <= 1 }
by RCOMP_1:def 1;
thus 0 <= r & r <= 1 implies r in the carrier of I[01] by A1,Th40;
assume r in the carrier of I[01];
then ex r2 being Real st r2 = r & 0 <= r2 & r2 <= 1 by A1,Th40;
hence thesis;
end;