:: Connected Spaces :: by Beata Padlewska :: :: Received May 6, 1989 :: Copyright (c) 1990-2012 Association of Mizar Users begin :: :: Separated sets :: definition let GX be TopStruct ; let A, B be Subset of GX; predA,B are_separated means :Def1: :: CONNSP_1:def 1 ( Cl A misses B & A misses Cl B ); symmetry for A, B being Subset of GX st Cl A misses B & A misses Cl B holds ( Cl B misses A & B misses Cl A ) ; end; :: deftheorem Def1 defines are_separated CONNSP_1:def_1_:_ for GX being TopStruct for A, B being Subset of GX holds ( A,B are_separated iff ( Cl A misses B & A misses Cl B ) ); theorem Th1: :: CONNSP_1:1 for TS being TopStruct for K, L being Subset of TS st K,L are_separated holds K misses L proofend; theorem Th2: :: CONNSP_1:2 for TS being TopStruct for K, L being Subset of TS st K is closed & L is closed & K misses L holds K,L are_separated proofend; theorem Th3: :: CONNSP_1:3 for GX being TopSpace for A, B being Subset of GX st [#] GX = A \/ B & A is open & B is open & A misses B holds A,B are_separated proofend; theorem Th4: :: CONNSP_1:4 for GX being TopSpace for A, B being Subset of GX st [#] GX = A \/ B & A,B are_separated holds ( A is open & A is closed & B is open & B is closed ) proofend; theorem Th5: :: CONNSP_1:5 for GX being TopSpace for X9 being SubSpace of GX for P1, Q1 being Subset of GX for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds P1,Q1 are_separated proofend; theorem Th6: :: CONNSP_1:6 for GX being TopSpace for X9 being SubSpace of GX for P, Q being Subset of GX for P1, Q1 being Subset of X9 st P = P1 & Q = Q1 & P \/ Q c= [#] X9 & P,Q are_separated holds P1,Q1 are_separated proofend; theorem Th7: :: CONNSP_1:7 for TS being TopStruct for K, L, K1, L1 being Subset of TS st K,L are_separated & K1 c= K & L1 c= L holds K1,L1 are_separated proofend; theorem Th8: :: CONNSP_1:8 for GX being TopSpace for A, B, C being Subset of GX st A,B are_separated & A,C are_separated holds A,B \/ C are_separated proofend; theorem Th9: :: CONNSP_1:9 for TS being TopStruct for K, L being Subset of TS st ( ( K is closed & L is closed ) or ( K is open & L is open ) ) holds K \ L,L \ K are_separated proofend; :: :: Connected Spaces :: definition let GX be TopStruct ; attrGX is connected means :Def2: :: CONNSP_1:def 2 for A, B being Subset of GX st [#] GX = A \/ B & A,B are_separated & not A = {} GX holds B = {} GX; end; :: deftheorem Def2 defines connected CONNSP_1:def_2_:_ for GX being TopStruct holds ( GX is connected iff for A, B being Subset of GX st [#] GX = A \/ B & A,B are_separated & not A = {} GX holds B = {} GX ); theorem Th10: :: CONNSP_1:10 for GX being TopSpace holds ( GX is connected iff for A, B being Subset of GX st [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is closed & B is closed holds A meets B ) proofend; theorem :: CONNSP_1:11 for GX being TopSpace holds ( GX is connected iff for A, B being Subset of GX st [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open holds A meets B ) proofend; theorem Th12: :: CONNSP_1:12 for GX being TopSpace holds ( GX is connected iff for A being Subset of GX st A <> {} GX & A <> [#] GX holds Cl A meets Cl (([#] GX) \ A) ) proofend; theorem :: CONNSP_1:13 for GX being TopSpace holds ( GX is connected iff for A being Subset of GX st A is open & A is closed & not A = {} GX holds A = [#] GX ) proofend; theorem :: CONNSP_1:14 for GX, GY being TopSpace for F being Function of GX,GY st F is continuous & F .: ([#] GX) = [#] GY & GX is connected holds GY is connected proofend; :: :: Connected Sets :: definition let GX be TopStruct ; let A be Subset of GX; attrA is connected means :Def3: :: CONNSP_1:def 3 GX | A is connected ; end; :: deftheorem Def3 defines connected CONNSP_1:def_3_:_ for GX being TopStruct for A being Subset of GX holds ( A is connected iff GX | A is connected ); theorem Th15: :: CONNSP_1:15 for GX being TopSpace for A being Subset of GX holds ( A is connected iff for P, Q being Subset of GX st A = P \/ Q & P,Q are_separated & not P = {} GX holds Q = {} GX ) proofend; theorem Th16: :: CONNSP_1:16 for GX being TopSpace for A, B, C being Subset of GX st A is connected & A c= B \/ C & B,C are_separated & not A c= B holds A c= C proofend; theorem Th17: :: CONNSP_1:17 for GX being TopSpace for A, B being Subset of GX st A is connected & B is connected & not A,B are_separated holds A \/ B is connected proofend; theorem Th18: :: CONNSP_1:18 for GX being TopSpace for C, A being Subset of GX st C is connected & C c= A & A c= Cl C holds A is connected proofend; theorem Th19: :: CONNSP_1:19 for GX being TopSpace for A being Subset of GX st A is connected holds Cl A is connected proofend; theorem Th20: :: CONNSP_1:20 for GX being TopSpace for A, B, C being Subset of GX st GX is connected & A is connected & ([#] GX) \ A = B \/ C & B,C are_separated holds ( A \/ B is connected & A \/ C is connected ) proofend; theorem :: CONNSP_1:21 for GX being TopSpace for A, B, C being Subset of GX st ([#] GX) \ A = B \/ C & B,C are_separated & A is closed holds ( A \/ B is closed & A \/ C is closed ) proofend; theorem :: CONNSP_1:22 for GX being TopSpace for C, A being Subset of GX st C is connected & C meets A & C \ A <> {} GX holds C meets Fr A proofend; theorem Th23: :: CONNSP_1:23 for GX being TopSpace for X9 being SubSpace of GX for A being Subset of GX for B being Subset of X9 st A = B holds ( A is connected iff B is connected ) proofend; theorem :: CONNSP_1:24 for GX being TopSpace for A, B being Subset of GX st A is closed & B is closed & A \/ B is connected & A /\ B is connected holds ( A is connected & B is connected ) proofend; theorem Th25: :: CONNSP_1:25 for GX being TopSpace for F being Subset-Family of GX st ( for A being Subset of GX st A in F holds A is connected ) & ex A being Subset of GX st ( A <> {} GX & A in F & ( for B being Subset of GX st B in F & B <> A holds not A,B are_separated ) ) holds union F is connected proofend; theorem Th26: :: CONNSP_1:26 for GX being TopSpace for F being Subset-Family of GX st ( for A being Subset of GX st A in F holds A is connected ) & meet F <> {} GX holds union F is connected proofend; theorem Th27: :: CONNSP_1:27 for GX being TopSpace holds ( [#] GX is connected iff GX is connected ) proofend; registration let GX be non empty TopSpace; let x be Point of GX; cluster{x} -> connected for Subset of GX; coherence for b1 being Subset of GX st b1 = {x} holds b1 is connected proofend; end; definition let GX be TopStruct ; let x, y be Point of GX; predx,y are_joined means :Def4: :: CONNSP_1:def 4 ex C being Subset of GX st ( C is connected & x in C & y in C ); end; :: deftheorem Def4 defines are_joined CONNSP_1:def_4_:_ for GX being TopStruct for x, y being Point of GX holds ( x,y are_joined iff ex C being Subset of GX st ( C is connected & x in C & y in C ) ); theorem Th28: :: CONNSP_1:28 for GX being non empty TopSpace st ex x being Point of GX st for y being Point of GX holds x,y are_joined holds GX is connected proofend; theorem Th29: :: CONNSP_1:29 for GX being TopSpace holds ( ex x being Point of GX st for y being Point of GX holds x,y are_joined iff for x, y being Point of GX holds x,y are_joined ) proofend; theorem :: CONNSP_1:30 for GX being non empty TopSpace st ( for x, y being Point of GX holds x,y are_joined ) holds GX is connected proofend; theorem Th31: :: CONNSP_1:31 for GX being non empty TopSpace for x being Point of GX for F being Subset-Family of GX st ( for A being Subset of GX holds ( A in F iff ( A is connected & x in A ) ) ) holds F <> {} proofend; :: :: Components of Topological Spaces :: definition let GX be TopStruct ; let A be Subset of GX; attrA is a_component means :Def5: :: CONNSP_1:def 5 ( A is connected & ( for B being Subset of GX st B is connected & A c= B holds A = B ) ); end; :: deftheorem Def5 defines a_component CONNSP_1:def_5_:_ for GX being TopStruct for A being Subset of GX holds ( A is a_component iff ( A is connected & ( for B being Subset of GX st B is connected & A c= B holds A = B ) ) ); registration let GX be TopStruct ; cluster a_component -> connected for Element of K10( the carrier of GX); coherence for b1 being Subset of GX st b1 is a_component holds b1 is connected by Def5; end; registration let GX be non empty TopSpace; cluster a_component -> non empty for Element of K10( the carrier of GX); coherence for b1 being Subset of GX st b1 is a_component holds not b1 is empty proofend; end; theorem :: CONNSP_1:32 for GX being non empty TopSpace for A being Subset of GX st A is a_component holds A <> {} GX ; registration let GX be TopSpace; cluster a_component -> closed for Element of K10( the carrier of GX); coherence for b1 being Subset of GX st b1 is a_component holds b1 is closed proofend; end; theorem :: CONNSP_1:33 for GX being TopSpace for A being Subset of GX st A is a_component holds A is closed ; theorem Th34: :: CONNSP_1:34 for GX being TopSpace for A, B being Subset of GX st A is a_component & B is a_component & not A = B holds A,B are_separated proofend; theorem :: CONNSP_1:35 for GX being TopSpace for A, B being Subset of GX st A is a_component & B is a_component & not A = B holds A misses B by Th1, Th34; theorem :: CONNSP_1:36 for GX being TopSpace for C being Subset of GX st C is connected holds for S being Subset of GX holds ( not S is a_component or C misses S or C c= S ) proofend; definition let GX be TopStruct ; let A, B be Subset of GX; predB is_a_component_of A means :Def6: :: CONNSP_1:def 6 ex B1 being Subset of (GX | A) st ( B1 = B & B1 is a_component ); end; :: deftheorem Def6 defines is_a_component_of CONNSP_1:def_6_:_ for GX being TopStruct for A, B being Subset of GX holds ( B is_a_component_of A iff ex B1 being Subset of (GX | A) st ( B1 = B & B1 is a_component ) ); theorem :: CONNSP_1:37 for GX being TopSpace for A, C being Subset of GX st GX is connected & A is connected & C is_a_component_of ([#] GX) \ A holds ([#] GX) \ C is connected proofend; :: :: A Component of a Point :: definition let GX be TopStruct ; let x be Point of GX; func Component_of x -> Subset of GX means :Def7: :: CONNSP_1:def 7 ex F being Subset-Family of GX st ( ( for A being Subset of GX holds ( A in F iff ( A is connected & x in A ) ) ) & union F = it ); existence ex b1 being Subset of GX ex F being Subset-Family of GX st ( ( for A being Subset of GX holds ( A in F iff ( A is connected & x in A ) ) ) & union F = b1 ) proofend; uniqueness for b1, b2 being Subset of GX st ex F being Subset-Family of GX st ( ( for A being Subset of GX holds ( A in F iff ( A is connected & x in A ) ) ) & union F = b1 ) & ex F being Subset-Family of GX st ( ( for A being Subset of GX holds ( A in F iff ( A is connected & x in A ) ) ) & union F = b2 ) holds b1 = b2 proofend; end; :: deftheorem Def7 defines Component_of CONNSP_1:def_7_:_ for GX being TopStruct for x being Point of GX for b3 being Subset of GX holds ( b3 = Component_of x iff ex F being Subset-Family of GX st ( ( for A being Subset of GX holds ( A in F iff ( A is connected & x in A ) ) ) & union F = b3 ) ); theorem Th38: :: CONNSP_1:38 for GX being non empty TopSpace for x being Point of GX holds x in Component_of x proofend; registration let GX be non empty TopSpace; let x be Point of GX; cluster Component_of x -> non empty connected ; coherence ( not Component_of x is empty & Component_of x is connected ) proofend; end; theorem Th39: :: CONNSP_1:39 for GX being non empty TopSpace for C being Subset of GX for x being Point of GX st C is connected & Component_of x c= C holds C = Component_of x proofend; theorem Th40: :: CONNSP_1:40 for GX being non empty TopSpace for A being Subset of GX holds ( A is a_component iff ex x being Point of GX st A = Component_of x ) proofend; theorem :: CONNSP_1:41 for GX being non empty TopSpace for A being Subset of GX for x being Point of GX st A is a_component & x in A holds A = Component_of x proofend; theorem :: CONNSP_1:42 for GX being non empty TopSpace for x, p being Point of GX st p in Component_of x holds Component_of p = Component_of x proofend; theorem :: CONNSP_1:43 for GX being non empty TopSpace for F being Subset-Family of GX st ( for A being Subset of GX holds ( A in F iff A is a_component ) ) holds F is Cover of GX proofend; begin registration let T be TopStruct ; cluster empty for Element of K10( the carrier of T); existence ex b1 being Subset of T st b1 is empty proofend; end; registration let T be TopStruct ; cluster empty -> connected for Element of K10( the carrier of T); coherence for b1 being Subset of T st b1 is empty holds b1 is connected proofend; end; theorem Th44: :: CONNSP_1:44 for T being TopSpace for X being set holds ( X is connected Subset of T iff X is connected Subset of TopStruct(# the carrier of T, the topology of T #) ) proofend; theorem :: CONNSP_1:45 for T being TopSpace for X being Subset of T for Y being Subset of TopStruct(# the carrier of T, the topology of T #) st X = Y holds ( X is a_component iff Y is a_component ) proofend; :: from JORDAN2C, 2011.07.03, A.T. theorem :: CONNSP_1:46 for G being non empty TopSpace for P, A being Subset of G for Q being Subset of (G | A) st P = Q & P is connected holds Q is connected proofend;