:: Components and Unions of Components :: by Yatsuka Nakamura and Andrzej Trybulec :: :: Received February 5, 1996 :: Copyright (c) 1996-2018 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 XBOOLE_0, PRE_TOPC, SUBSET_1, CONNSP_1, SETFAM_1, RELAT_2, TARSKI, STRUCT_0, ZFMISC_1, RELAT_1, RUSUB_4, RCOMP_1, CONNSP_3; notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, STRUCT_0, PRE_TOPC, CONNSP_1; constructors SETFAM_1, CONNSP_1; registrations SUBSET_1, STRUCT_0, PRE_TOPC, CONNSP_1; requirements SUBSET, BOOLE; definitions TARSKI, XBOOLE_0; equalities XBOOLE_0, STRUCT_0; expansions TARSKI, XBOOLE_0; theorems TARSKI, ZFMISC_1, SETFAM_1, PRE_TOPC, SUBSET_1, CONNSP_1, XBOOLE_0, XBOOLE_1, ORDERS_1; schemes SUBSET_1; begin :: The component of a subset in a topological space reserve x,X,X2,Y,Y2 for set; reserve GX for non empty TopSpace; reserve A2,B2 for Subset of GX; reserve B for Subset of GX; definition let GX be TopStruct, V be Subset of GX; func Component_of V -> Subset of GX means :Def1: ex F being Subset-Family of GX st (for A being Subset of GX holds A in F iff A is connected & V c= A) & union F = it; existence proof defpred P[set] means ex A1 being Subset of GX st A1 = \$1 & A1 is connected & V c= \$1; consider F being Subset-Family of GX such that A1: for A being Subset of GX holds A in F iff P[A] from SUBSET_1:sch 3; take union F, F; thus for A being Subset of GX holds A in F iff A is connected & V c= A proof let A be Subset of GX; thus A in F implies A is connected & V c= A proof assume A in F; then ex A1 being Subset of GX st A1 = A & A1 is connected & V c= A by A1; hence thesis; end; thus thesis by A1; end; thus thesis; end; uniqueness proof let S,S9 be Subset of GX; assume that A2: ex F being Subset-Family of GX st (for A being Subset of GX holds A in F iff A is connected & V c= A) & union F = S and A3: ex F9 being Subset-Family of GX st (for A being Subset of GX holds A in F9 iff A is connected & V c= A) & union F9 = S9; consider F being Subset-Family of GX such that A4: for A being Subset of GX holds A in F iff A is connected & V c= A and A5: union F = S by A2; consider F9 being Subset-Family of GX such that A6: for A being Subset of GX holds A in F9 iff A is connected & V c= A and A7: union F9 = S9 by A3; now let y be object; A8: now assume y in S9; then consider B being set such that A9: y in B and A10: B in F9 by A7,TARSKI:def 4; reconsider B as Subset of GX by A10; B is connected & V c= B by A6,A10; then B in F by A4; hence y in S by A5,A9,TARSKI:def 4; end; now assume y in S; then consider B being set such that A11: y in B and A12: B in F by A5,TARSKI:def 4; reconsider B as Subset of GX by A12; B is connected & V c= B by A4,A12; then B in F9 by A6; hence y in S9 by A7,A11,TARSKI:def 4; end; hence y in S iff y in S9 by A8; end; hence thesis by TARSKI:2; end; end; theorem Th1: for GX being TopSpace, V being Subset of GX st (ex A being Subset of GX st A is connected & V c= A) holds V c= Component_of V proof let GX be TopSpace, V be Subset of GX; given A being Subset of GX such that A1: A is connected & V c= A; consider F being Subset-Family of GX such that A2: for A being Subset of GX holds A in F iff A is connected & V c= A and A3: Component_of V = union F by Def1; A4: for A being set holds A in F implies V c= A by A2; F <> {} by A1,A2; then A5: V c= meet F by A4,SETFAM_1:5; meet F c= union F by SETFAM_1:2; hence thesis by A3,A5; end; theorem for GX being TopSpace, V being Subset of GX st (not ex A being Subset of GX st A is connected & V c= A) holds Component_of V = {} proof let GX be TopSpace, V be Subset of GX such that A1: not ex A being Subset of GX st A is connected & V c= A; consider F being Subset-Family of GX such that A2: for A being Subset of GX holds A in F iff A is connected & V c= A and A3: Component_of V = union F by Def1; now assume F <> {}; then consider A being Subset of GX such that A4: A in F by SUBSET_1:4; reconsider A as Subset of GX; A is connected & V c= A by A2,A4; hence contradiction by A1; end; hence thesis by A3,ZFMISC_1:2; end; theorem Th3: Component_of {}GX = the carrier of GX proof defpred P[set] means ex A1 being Subset of GX st A1 = \$1 & A1 is connected & {}GX c= \$1; consider F being Subset-Family of GX such that A1: for A being Subset of GX holds A in F iff P[A] from SUBSET_1:sch 3; A2: for A being Subset of GX holds A in F iff A is connected & {}GX c= A proof let A be Subset of GX; thus A in F implies A is connected & {}GX c= A proof assume A in F; then ex A1 being Subset of GX st A1 = A & A1 is connected & {}GX c= A by A1; hence thesis; end; thus thesis by A1; end; now let x be object; hereby assume x in the carrier of GX; then reconsider p = x as Point of GX; reconsider Y = Component_of p as set; take Y; thus x in Y by CONNSP_1:38; Component_of p is connected & {}GX c= Y; hence Y in F by A2; end; given Y being set such that A3: x in Y & Y in F; thus x in the carrier of GX by A3; end; then union F = the carrier of GX by TARSKI:def 4; hence thesis by A2,Def1; end; theorem for V being Subset of GX st V is connected holds Component_of V <>{} proof let V be Subset of GX such that A1: V is connected; per cases; suppose V = {}; then V = {}GX; hence thesis by Th3; end; suppose V <>{}; hence thesis by A1,Th1,XBOOLE_1:3; end; end; theorem Th5: for GX being TopSpace, V being Subset of GX st V is connected & V <> {} holds Component_of V is connected proof let GX be TopSpace; let V be Subset of GX; assume that A1: V is connected and A2: V<>{}; consider F being Subset-Family of GX such that A3: for A being Subset of GX holds A in F iff A is connected & V c= A and A4: Component_of V = union F by Def1; A5: for A being set st A in F holds V c= A by A3; F <> {} by A1,A3; then V c= meet F by A5,SETFAM_1:5; then A6: meet F<>{}(GX) by A2; for A being Subset of GX st A in F holds A is connected by A3; hence thesis by A4,A6,CONNSP_1:26; end; theorem Th6: for V,C being Subset of GX st V is connected & C is connected holds Component_of V c= C implies C = Component_of V proof let V,C be Subset of GX; assume that A1: V is connected and A2: C is connected; assume A3: Component_of V c= C; consider F being Subset-Family of GX such that A4: for A being Subset of GX holds (A in F iff A is connected & V c= A) and A5: Component_of V = union F by Def1; V c= Component_of V by A1,Th1; then V c= C by A3; then C in F by A2,A4; then C c= Component_of V by A5,ZFMISC_1:74; hence thesis by A3; end; theorem Th7: for A being Subset of GX st A is a_component holds Component_of A=A proof let A be Subset of GX; assume A1: A is a_component; then A2: A is connected; then A3: A c= Component_of A by Th1; A <>{}(GX) by A1; then Component_of A is connected by A2,Th5; hence thesis by A1,A3,CONNSP_1:def 5; end; theorem Th8: for A being Subset of GX holds A is a_component iff ex V being Subset of GX st V is connected & V <> {} & A = Component_of V proof let A be Subset of GX; A1: now assume A2: A is a_component; take V = A; thus V is connected & V<>{} & A = Component_of V by A2,Th7; end; now given V being Subset of GX such that A3: V is connected & V<>{} & A = Component_of V; A is connected & for B being Subset of GX st B is connected holds A c= B implies A = B by A3,Th5,Th6; hence A is a_component by CONNSP_1:def 5; end; hence thesis by A1; end; theorem for V being Subset of GX st V is connected & V<>{} holds Component_of V is a_component by Th8; theorem for A, V be Subset of GX st A is a_component & V is connected & V c= A & V<>{} holds A = Component_of V proof let A, V be Subset of GX; assume that A1: A is a_component and A2: V is connected and A3: V c= A and A4: V<>{}; V c= Component_of V by A2,Th1; then A5: A meets (Component_of V) by A3,A4,XBOOLE_1:67; assume A6: A <> Component_of V; Component_of V is a_component by A2,A4,Th8; hence contradiction by A1,A6,A5,CONNSP_1:1,34; end; theorem Th11: for V being Subset of GX st V is connected & V<>{} holds Component_of (Component_of V)=Component_of V proof let V be Subset of GX; assume V is connected & V<>{}; then Component_of V is a_component by Th8; hence thesis by Th7; end; theorem Th12: for A,B being Subset of GX st A is connected & B is connected & A<>{} & A c= B holds Component_of A = Component_of B proof let A,B be Subset of GX; assume that A1: A is connected and A2: B is connected and A3: A<>{} and A4: A c= B; B<>{} by A3,A4; then A5: Component_of B is connected by A2,Th5; A6: B c= Component_of B by A2,Th1; then A7: A c= Component_of B by A4; A8: Component_of B c= Component_of A proof consider F being Subset-Family of GX such that A9: for D being Subset of GX holds D in F iff D is connected & A c= D and A10: union F = Component_of A by Def1; Component_of B in F by A7,A5,A9; hence thesis by A10,ZFMISC_1:74; end; A11: Component_of A is connected by A1,A3,Th5; Component_of A c= Component_of B proof consider F being Subset-Family of GX such that A12: for D being Subset of GX holds D in F iff D is connected & B c= D and A13: union F = Component_of B by Def1; B c= Component_of A by A6,A8; then Component_of A in F by A11,A12; hence thesis by A13,ZFMISC_1:74; end; hence thesis by A8; end; theorem Th13: for A,B being Subset of GX st A is connected & B is connected & A<>{} & A c= B holds B c= Component_of A proof let A,B be Subset of GX; assume that A1: A is connected and A2: B is connected and A3: A<>{} & A c= B; Component_of A = Component_of B by A1,A2,A3,Th12; hence thesis by A2,Th1; end; theorem Th14: for A being Subset of GX,B being Subset of GX st A is connected & A \/ B is connected & A<>{} holds A \/ B c= Component_of A proof let A be Subset of GX,B be Subset of GX; assume that A1: A is connected and A2: A \/ B is connected and A3: A<>{}; Component_of (A \/ B) = Component_of A by A1,A2,A3,Th12,XBOOLE_1:7; hence thesis by A2,Th1; end; theorem Th15: for A being Subset of GX, p being Point of GX st A is connected & p in A holds Component_of p=Component_of A proof let A be Subset of GX, p be Point of GX; assume that A1: A is connected and A2: p in A; A c= Component_of A & Component_of A is a_component by A1,A2,Th1,Th8; hence thesis by A2,CONNSP_1:41; end; theorem for A,B being Subset of GX st A is connected & B is connected & A meets B holds A \/ B c= Component_of A & A \/ B c= Component_of B & A c= Component_of B & B c= Component_of A proof let A,B be Subset of GX; A1: A c= A \/ B & B c= A \/ B by XBOOLE_1:7; A2: for C,D being Subset of GX st C is connected & D is connected & C /\ D <>{} holds C \/ D c= Component_of C proof let C,D be Subset of GX; assume that A3: C is connected and A4: D is connected and A5: C /\ D <>{}; C meets D by A5; then A6: C \/ D is connected by A3,A4,CONNSP_1:1,17; C <>{} by A5; hence thesis by A3,A6,Th14; end; assume A is connected & B is connected & A /\ B <>{}; then A \/ B c= Component_of A & A \/ B c= Component_of B by A2; hence thesis by A1; end; theorem for A being Subset of GX st A is connected & A<>{} holds Cl A c= Component_of A proof let A be Subset of GX; assume that A1: A is connected and A2: A<>{}; Cl A is connected by A1,CONNSP_1:19; hence thesis by A1,A2,Th13,PRE_TOPC:18; end; theorem for A,B being Subset of GX st A is a_component & B is connected & B<>{} & A misses B holds A misses Component_of B proof let A,B be Subset of GX; assume that A1: A is a_component and A2: B is connected & B<>{} and A3: A /\ B ={}; A4: A is connected by A1; assume A /\ Component_of B <>{}; then consider x being Point of GX such that A5: x in A /\ Component_of B by SUBSET_1:4; x in A by A5,XBOOLE_0:def 4; then A6: Component_of x=Component_of A by A4,Th15; A7: x in Component_of B by A5,XBOOLE_0:def 4; Component_of A=A & Component_of B=Component_of Component_of B by A1,A2,Th7 ,Th11; then (Component_of B) /\ B={} by A2,A3,A7,A6,Th5,Th15; hence contradiction by A2,Th1,XBOOLE_1:28; end; begin :: On unions of components Lm1: now let GX be TopStruct; reconsider S={} as Subset-Family of GX by XBOOLE_1:2; for B being Subset of GX st B in S holds B is a_component; hence ex F being Subset-Family of GX st (for B being Subset of GX st B in F holds B is a_component) & {}(GX)=union F by ZFMISC_1:2; end; definition let GX be TopStruct; mode a_union_of_components of GX -> Subset of GX means :Def2: ex F being Subset-Family of GX st (for B being Subset of GX st B in F holds B is a_component) & it = union F; existence proof take {}GX; thus thesis by Lm1; end; end; theorem Th19: {}(GX) is a_union_of_components of GX proof thus ex F being Subset-Family of GX st (for B being Subset of GX st B in F holds B is a_component) & {}(GX) = union F by Lm1; end; theorem Th20: for A being Subset of GX st A=(the carrier of GX) holds A is a_union_of_components of GX proof let A be Subset of GX; {B : B is a_component} c= bool (the carrier of GX) proof let x be object; assume x in {B : B is a_component}; then ex B being Subset of GX st x=B & B is a_component; hence thesis; end; then reconsider S={B: B is a_component} as Subset-Family of GX; A1: for B being Subset of GX st B in S holds B is a_component proof let B be Subset of GX; assume B in S; then ex B2 being Subset of GX st B=B2 & B2 is a_component; hence thesis; end; the carrier of GX c= union S proof let x be object; assume x in the carrier of GX; then reconsider p=x as Point of GX; set B3=Component_of p; B3 is a_component by CONNSP_1:40; then p in Component_of p & B3 in S by CONNSP_1:38; hence thesis by TARSKI:def 4; end; then A2: the carrier of GX=union S; assume A=(the carrier of GX); hence thesis by A2,A1,Def2; end; theorem Th21: for A being Subset of GX,p being Point of GX st p in A & A is a_union_of_components of GX holds Component_of p c= A proof let A be Subset of GX,p be Point of GX; assume that A1: p in A and A2: A is a_union_of_components of GX; consider F being Subset-Family of GX such that A3: for B being Subset of GX st B in F holds B is a_component and A4: A=union F by A2,Def2; consider X such that A5: p in X and A6: X in F by A1,A4,TARSKI:def 4; reconsider B2=X as Subset of GX by A6; B2=Component_of p by A3,A5,A6,CONNSP_1:41; hence thesis by A4,A6,ZFMISC_1:74; end; theorem for A,B being Subset of GX st A is a_union_of_components of GX & B is a_union_of_components of GX holds A \/ B is a_union_of_components of GX & A /\ B is a_union_of_components of GX proof let A,B be Subset of GX; assume that A1: A is a_union_of_components of GX and A2: B is a_union_of_components of GX; consider Fa being Subset-Family of GX such that A3: for Ba being Subset of GX st Ba in Fa holds Ba is a_component and A4: A=union Fa by A1,Def2; consider Fb being Subset-Family of GX such that A5: for Bb being Subset of GX st Bb in Fb holds Bb is a_component and A6: B=union Fb by A2,Def2; A7: for B2 being Subset of GX st B2 in Fa \/ Fb holds B2 is a_component proof let B2 be Subset of GX; assume B2 in Fa \/ Fb; then B2 in Fa or B2 in Fb by XBOOLE_0:def 3; hence thesis by A3,A5; end; A8: A /\ B is a_union_of_components of GX proof reconsider Fd= Fa /\ Fb as Subset-Family of GX; A9: for B4 being Subset of GX st B4 in Fd holds B4 is a_component proof let B4 be Subset of GX; assume B4 in Fd; then B4 in Fa by XBOOLE_0:def 4; hence thesis by A3; end; A10: A /\ B c= union Fd proof let x be object; assume A11: x in A /\ B; then x in A by XBOOLE_0:def 4; then consider F1 being set such that A12: x in F1 and A13: F1 in Fa by A4,TARSKI:def 4; reconsider C1=F1 as Subset of GX by A13; x in B by A11,XBOOLE_0:def 4; then consider F2 being set such that A14: x in F2 and A15: F2 in Fb by A6,TARSKI:def 4; reconsider C2=F2 as Subset of GX by A15; A16: C2 is a_component by A5,A15; C1 is a_component by A3,A13; then A17: C1 = C2 or C1 misses C2 by A16,CONNSP_1:35; F1 /\ F2 <>{} by A12,A14,XBOOLE_0:def 4; then C1 in Fa /\ Fb by A13,A15,A17,XBOOLE_0:def 4; hence thesis by A12,TARSKI:def 4; end; union Fd c= A /\ B proof let x be object; assume x in union Fd; then consider X4 being set such that A18: x in X4 and A19: X4 in Fd by TARSKI:def 4; X4 in Fb by A19,XBOOLE_0:def 4; then A20: x in union Fb by A18,TARSKI:def 4; X4 in Fa by A19,XBOOLE_0:def 4; then x in union Fa by A18,TARSKI:def 4; hence thesis by A4,A6,A20,XBOOLE_0:def 4; end; then A /\ B =union Fd by A10; hence thesis by A9,Def2; end; reconsider Fc = Fa \/ Fb as Subset-Family of GX; A \/ B =union Fc by A4,A6,ZFMISC_1:78; hence thesis by A7,A8,Def2; end; theorem for Fu being Subset-Family of GX st (for A being Subset of GX st A in Fu holds A is a_union_of_components of GX) holds union Fu is a_union_of_components of GX proof let Fu be Subset-Family of GX; {B: ex B2 st B2 in Fu & B c= B2 & B is a_component} c= bool (the carrier of GX) proof let x be object; assume x in {B: ex B2 st B2 in Fu & B c= B2 & B is a_component}; then ex B st x=B & ex B2 st B2 in Fu & B c= B2 & B is a_component; hence thesis; end; then reconsider F2={B: ex B2 st B2 in Fu & B c= B2 & B is a_component} as Subset-Family of GX; A1: for B being Subset of GX st B in F2 holds B is a_component proof let B be Subset of GX; assume B in F2; then ex A2 being Subset of GX st B=A2 & ex B2 st B2 in Fu & A2 c= B2 & A2 is a_component; hence thesis; end; assume A2: for A being Subset of GX st A in Fu holds A is a_union_of_components of GX; A3: union Fu c= union F2 proof let x be object; assume x in union Fu; then consider X2 such that A4: x in X2 and A5: X2 in Fu by TARSKI:def 4; reconsider B3=X2 as Subset of GX by A5; B3 is a_union_of_components of GX by A2,A5; then consider F being Subset-Family of GX such that A6: for B being Subset of GX st B in F holds B is a_component and A7: B3=union F by Def2; consider Y2 such that A8: x in Y2 and A9: Y2 in F by A4,A7,TARSKI:def 4; reconsider A3=Y2 as Subset of GX by A9; A3 is a_component & Y2 c= B3 by A6,A7,A9,ZFMISC_1:74; then A3 in F2 by A5; hence thesis by A8,TARSKI:def 4; end; union F2 c= union Fu proof let x be object; assume x in union F2; then consider X such that A10: x in X and A11: X in F2 by TARSKI:def 4; ex B st X=B & ex B2 st B2 in Fu & B c= B2 & B is a_component by A11; hence thesis by A10,TARSKI:def 4; end; then union Fu = union F2 by A3; hence thesis by A1,Def2; end; theorem for Fu being Subset-Family of GX st (for A being Subset of GX st A in Fu holds A is a_union_of_components of GX) holds meet Fu is a_union_of_components of GX proof let Fu be Subset-Family of GX; assume A1: for A being Subset of GX st A in Fu holds A is a_union_of_components of GX; now per cases; case A2: Fu<>{}; {B:B is a_component & for A2 st A2 in Fu holds B c= A2} c= bool(the carrier of GX) proof let x be object; assume x in {B:B is a_component & for A2 st A2 in Fu holds B c= A2}; then ex B st x=B & B is a_component & for A2 st A2 in Fu holds B c= A2; hence thesis; end; then reconsider F1={B:B is a_component & for A2 st A2 in Fu holds B c= A2} as Subset-Family of GX; A3: meet Fu c= union F1 proof let x be object; consider Y2 being object such that A4: Y2 in Fu by A2,XBOOLE_0:def 1; reconsider Y2 as set by TARSKI:1; reconsider B2=Y2 as Subset of GX by A4; B2 is a_union_of_components of GX by A1,A4; then consider F being Subset-Family of GX such that A5: for B being Subset of GX st B in F holds B is a_component and A6: B2=union F by Def2; assume A7: x in meet Fu; then x in Y2 by A4,SETFAM_1:def 1; then consider Y3 being set such that A8: x in Y3 and A9: Y3 in F by A6,TARSKI:def 4; reconsider B3=Y3 as Subset of GX by A9; A10: for A2 st A2 in Fu holds B3 c= A2 proof reconsider p=x as Point of GX by A7; let A2; assume A11: A2 in Fu; then x in A2 by A7,SETFAM_1:def 1; then Component_of p c= A2 by A1,A11,Th21; hence thesis by A5,A8,A9,CONNSP_1:41; end; B3 is a_component by A5,A9; then Y3 in F1 by A10; hence thesis by A8,TARSKI:def 4; end; A12: for B being Subset of GX st B in F1 holds B is a_component proof let B be Subset of GX; assume B in F1; then ex B1 be Subset of GX st B=B1 & B1 is a_component & for A2 st A2 in Fu holds B1 c= A2; hence thesis; end; union F1 c= meet Fu proof let x be object; assume x in union F1; then consider X such that A13: x in X and A14: X in F1 by TARSKI:def 4; consider B such that A15: X=B and B is a_component and A16: for A2 st A2 in Fu holds B c= A2 by A14; for Y st Y in Fu holds x in Y proof let Y; assume Y in Fu; then B c= Y by A16; hence thesis by A13,A15; end; hence thesis by A2,SETFAM_1:def 1; end; then meet Fu=union F1 by A3; hence thesis by A12,Def2; end; case Fu={}; then meet Fu={}(GX) by SETFAM_1:def 1; hence thesis by Th19; end; end; hence thesis; end; theorem for A,B being Subset of GX st A is a_union_of_components of GX & B is a_union_of_components of GX holds A \ B is a_union_of_components of GX proof let A,B be Subset of GX; assume that A1: A is a_union_of_components of GX and A2: B is a_union_of_components of GX; consider Fa being Subset-Family of GX such that A3: for B2 being Subset of GX st B2 in Fa holds B2 is a_component and A4: A=union Fa by A1,Def2; consider Fb being Subset-Family of GX such that A5: for B3 being Subset of GX st B3 in Fb holds B3 is a_component and A6: B=union Fb by A2,Def2; reconsider Fd=Fa\Fb as Subset-Family of GX; A7: union Fd c= A \ B proof let x be object; assume x in union Fd; then consider X such that A8: x in X and A9: X in Fd by TARSKI:def 4; reconsider A2=X as Subset of GX by A9; A10: not X in Fb by A9,XBOOLE_0:def 5; A11: X in Fa by A9,XBOOLE_0:def 5; then A12: A2 is a_component by A3; A13: now assume x in B; then consider Y3 being set such that A14: x in Y3 and A15: Y3 in Fb by A6,TARSKI:def 4; reconsider B3=Y3 as Subset of GX by A15; A2 /\ B3 <>{} by A8,A14,XBOOLE_0:def 4; then A16: A2 meets B3; B3 is a_component by A5,A15; hence contradiction by A10,A12,A15,A16,CONNSP_1:35; end; A2 c= A by A4,A11,ZFMISC_1:74; hence thesis by A8,A13,XBOOLE_0:def 5; end; A17: for B4 being Subset of GX st B4 in Fd holds B4 is a_component proof let B4 be Subset of GX; assume B4 in Fd; then B4 in Fa by XBOOLE_0:def 5; hence thesis by A3; end; A \ B c= union Fd proof let x be object; assume A18: x in A \ B; then x in A by XBOOLE_0:def 5; then consider X such that A19: x in X and A20: X in Fa by A4,TARSKI:def 4; reconsider A2=X as Subset of GX by A20; now assume A2 in Fb; then A2 c= B by A6,ZFMISC_1:74; hence contradiction by A18,A19,XBOOLE_0:def 5; end; then A2 in Fd by A20,XBOOLE_0:def 5; hence thesis by A19,TARSKI:def 4; end; then A \ B=union Fd by A7; hence thesis by A17,Def2; end; begin :: Operations Down and Up definition let GX be TopStruct, B be Subset of GX, p be Point of GX; assume A1: p in B; func Down(p,B) -> Point of GX|B equals :Def3: p; coherence proof B=[#](GX|B) by PRE_TOPC:def 5; hence thesis by A1; end; end; definition let GX be TopStruct, B be Subset of GX, p be Point of GX|B; assume A1: B<>{}; func Up(p) -> Point of GX equals p; coherence proof B=the carrier of (GX|B) by PRE_TOPC:8; then p in B by A1; hence thesis; end; end; definition let GX be TopStruct, V,B be Subset of GX; func Down(V,B) -> Subset of GX|B equals V /\ B; coherence proof B=[#](GX|B) by PRE_TOPC:def 5; hence thesis by XBOOLE_1:17; end; end; definition let GX be TopStruct, B be Subset of GX; let V be Subset of GX|B; func Up(V) -> Subset of GX equals V; coherence proof B=the carrier of (GX|B) by PRE_TOPC:8; hence thesis by XBOOLE_1:1; end; end; definition let GX be TopStruct, B be Subset of GX, p be Point of GX; assume A1: p in B; func Component_of(p,B) -> Subset of GX means :Def7: for q being Point of GX| B st q=p holds it=Component_of q; existence proof A2: B=[#](GX|B) by PRE_TOPC:def 5; then reconsider q3=p as Point of GX|B by A1; reconsider C=Component_of q3 as Subset of GX by A2,XBOOLE_1:1; take C; thus thesis; end; uniqueness proof B=[#](GX|B) by PRE_TOPC:def 5; then reconsider q3=p as Point of GX|B by A1; let S,S9 be Subset of GX; assume that A3: for q being Point of GX|B st q=p holds S=Component_of q and A4: for q2 being Point of GX|B st q2=p holds S9=Component_of q2; S=Component_of q3 by A3; hence thesis by A4; end; end; theorem for B being Subset of GX, p be Point of GX st p in B holds p in Component_of(p,B) proof let B be Subset of GX, p be Point of GX; assume A1: p in B; then reconsider B9 = B as non empty Subset of GX; reconsider q=p as Point of GX|B9 by A1,PRE_TOPC:8; q in Component_of q by CONNSP_1:38; hence thesis by A1,Def7; end; theorem Th27: for B being Subset of GX, p be Point of GX st p in B holds Component_of(p,B)=Component_of Down(p,B) proof let B be Subset of GX, p be Point of GX; assume A1: p in B; then p=Down(p,B) by Def3; hence thesis by A1,Def7; end; theorem for GX being TopSpace for V,B being Subset of GX st V is open holds Down(V,B) is open proof let GX be TopSpace; let V,B be Subset of GX; assume V is open; then A1: V in the topology of GX by PRE_TOPC:def 2; Down(V,B)=V /\ [#](GX|B) by PRE_TOPC:def 5; then Down(V,B) in the topology of GX|B by A1,PRE_TOPC:def 4; hence thesis by PRE_TOPC:def 2; end; theorem Th29: for V,B being Subset of GX st V c= B holds Cl Down(V,B) =(Cl V) /\ B proof let V,B be Subset of GX; assume V c= B; then Down(V,B)=V by XBOOLE_1:28; then Cl Down(V,B) =(Cl V) /\ ([#](GX|B)) by PRE_TOPC:17; hence thesis by PRE_TOPC:def 5; end; theorem for B being Subset of GX,V being Subset of GX| B holds Cl V =(Cl Up(V) ) /\ B proof let B be Subset of GX, V be Subset of GX|B; A1: B=[#](GX|B) by PRE_TOPC:def 5; then Cl Down(Up(V),B)=(Cl Up(V))/\ B by Th29; hence thesis by A1,XBOOLE_1:28; end; theorem for V,B being Subset of GX st V c= B holds Cl Down(V,B) c= Cl V proof let V,B be Subset of GX; assume V c= B; then Cl Down(V,B) = (Cl V) /\ B by Th29; hence thesis by XBOOLE_1:17; end; theorem for B being Subset of GX, V being Subset of GX|B st V c= B holds Down( Up(V),B)=V by XBOOLE_1:28; theorem for B being Subset of GX, p be Point of GX st p in B holds Component_of(p,B) is connected proof let B be Subset of GX, p be Point of GX; assume A1: p in B; then reconsider B9 = B as non empty Subset of GX; Component_of Down(p,B9) is connected & Component_of(p,B)=Component_of Down(p,B) by A1,Th27; hence thesis by CONNSP_1:23; end; :: Moved from JORDAN1B, AK, 22.02.2006 registration let T be non empty TopSpace; cluster non empty for a_union_of_components of T; existence proof reconsider A = [#]T as a_union_of_components of T by Th20; A is non empty; hence thesis; end; end; theorem for T being non empty TopSpace for A being non empty a_union_of_components of T st A is connected holds A is a_component proof let T be non empty TopSpace; let A be non empty a_union_of_components of T; consider F being Subset-Family of T such that A1: for B being Subset of T st B in F holds B is a_component and A2: A = union F by Def2; consider X being set such that X <> {} and A3: X in F by A2,ORDERS_1:6; reconsider X as Subset of T by A3; assume A4: A is connected; F={X} proof thus F c= {X} proof let x be object; assume A5: x in F; then reconsider Y=x as Subset of T; A6: X is a_component & X c= A by A1,A2,A3,ZFMISC_1:74; Y is a_component & Y c= A by A1,A2,A5,ZFMISC_1:74; then Y = A by A4,CONNSP_1:def 5 .= X by A4,A6,CONNSP_1:def 5; hence thesis by TARSKI:def 1; end; let x be object; assume x in {X}; hence thesis by A3,TARSKI:def 1; end; then A = X by A2,ZFMISC_1:25; hence thesis by A1,A3; end;