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