:: Connectedness and Continuous Sequences in Finite Topological Spaces :: by Yatsuka Nakamura :: :: Received August 18, 2006 :: Copyright (c) 2006-2012 Association of Mizar Users begin registration let FT be non empty RelStr ; cluster empty -> connected for Element of K32( the carrier of FT); coherence for b1 being Subset of FT st b1 is empty holds b1 is connected proofend; end; theorem Th1: :: FINTOPO6:1 for FT being non empty RelStr for A, B being Subset of FT holds (A \/ B) ^b = (A ^b) \/ (B ^b) proofend; theorem Th2: :: FINTOPO6:2 for FT being non empty RelStr holds ({} FT) ^b = {} proofend; registration let FT be non empty RelStr ; cluster({} FT) ^b -> empty ; coherence ({} FT) ^b is empty by Th2; end; theorem Th3: :: FINTOPO6:3 for FT being non empty RelStr for A being Subset of FT st ( for B, C being Subset of FT st A = B \/ C & B <> {} & C <> {} & B misses C holds ( B ^b meets C & B meets C ^b ) ) holds A is connected proofend; definition let FT be non empty RelStr ; attrFT is connected means :Def1: :: FINTOPO6:def 1 [#] FT is connected ; end; :: deftheorem Def1 defines connected FINTOPO6:def_1_:_ for FT being non empty RelStr holds ( FT is connected iff [#] FT is connected ); theorem Th4: :: FINTOPO6:4 for FT being non empty RelStr for A being Subset of FT st A is connected holds for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds B2 = {} FT proofend; theorem Th5: :: FINTOPO6:5 for FT being non empty RelStr st FT is connected holds for A, B being Subset of FT st [#] FT = A \/ B & A misses B & A,B are_separated & not A = {} FT holds B = {} FT proofend; theorem Th6: :: FINTOPO6:6 for FT being non empty RelStr for A, B being Subset of FT st FT is symmetric & A ^b misses B holds A misses B ^b proofend; theorem Th7: :: FINTOPO6:7 for FT being non empty RelStr for A being Subset of FT st FT is symmetric & ( for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds B2 = {} FT ) holds A is connected proofend; definition let T be RelStr ; mode SubSpace of T -> RelStr means :Def2: :: FINTOPO6:def 2 ( the carrier of it c= the carrier of T & ( for x being Element of it st x in the carrier of it holds U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of it ) ); existence ex b1 being RelStr st ( the carrier of b1 c= the carrier of T & ( for x being Element of b1 st x in the carrier of b1 holds U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of b1 ) ) proofend; end; :: deftheorem Def2 defines SubSpace FINTOPO6:def_2_:_ for T, b2 being RelStr holds ( b2 is SubSpace of T iff ( the carrier of b2 c= the carrier of T & ( for x being Element of b2 st x in the carrier of b2 holds U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of b2 ) ) ); Lm1: for T being RelStr holds RelStr(# the carrier of T, the InternalRel of T #) is SubSpace of T proofend; registration let T be RelStr ; cluster strict for SubSpace of T; existence ex b1 being SubSpace of T st b1 is strict proofend; end; registration let T be non empty RelStr ; cluster non empty strict for SubSpace of T; existence ex b1 being SubSpace of T st ( b1 is strict & not b1 is empty ) proofend; end; definition let T be non empty RelStr ; let P be non empty Subset of T; funcT | P -> non empty strict SubSpace of T means :Def3: :: FINTOPO6:def 3 [#] it = P; existence ex b1 being non empty strict SubSpace of T st [#] b1 = P proofend; uniqueness for b1, b2 being non empty strict SubSpace of T st [#] b1 = P & [#] b2 = P holds b1 = b2 proofend; end; :: deftheorem Def3 defines | FINTOPO6:def_3_:_ for T being non empty RelStr for P being non empty Subset of T for b3 being non empty strict SubSpace of T holds ( b3 = T | P iff [#] b3 = P ); theorem Th8: :: FINTOPO6:8 for FT being non empty RelStr for X being non empty SubSpace of FT st FT is filled holds X is filled proofend; registration let FT be non empty filled RelStr ; cluster non empty -> non empty filled for SubSpace of FT; coherence for b1 being non empty SubSpace of FT holds b1 is filled by Th8; end; theorem :: FINTOPO6:9 for FT being non empty RelStr for X being non empty SubSpace of FT st FT is symmetric holds X is symmetric proofend; theorem Th10: :: FINTOPO6:10 for FT being non empty RelStr for X9 being SubSpace of FT for A being Subset of X9 holds A is Subset of FT proofend; theorem :: FINTOPO6:11 for FT being non empty RelStr for P being Subset of FT holds ( P is closed iff P ` is open ) proofend; theorem :: FINTOPO6:12 for FT being non empty RelStr for A being Subset of FT holds ( A is open iff ( ( for z being Element of FT st U_FT z c= A holds z in A ) & ( for x being Element of FT st x in A holds U_FT x c= A ) ) ) proofend; theorem Th13: :: FINTOPO6:13 for FT being non empty RelStr for X9 being non empty SubSpace of FT for A being Subset of FT for A1 being Subset of X9 st A = A1 holds A1 ^b = (A ^b) /\ ([#] X9) proofend; theorem :: FINTOPO6:14 for FT being non empty RelStr for X9 being non empty SubSpace of FT for P1, Q1 being Subset of FT for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds P1,Q1 are_separated proofend; theorem :: FINTOPO6:15 for FT being non empty RelStr for X9 being non empty SubSpace of FT for P, Q being Subset of FT 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 Th16: :: FINTOPO6:16 for FT being non empty RelStr for A being non empty Subset of FT holds ( A is connected iff FT | A is connected ) proofend; theorem :: FINTOPO6:17 for FT being non empty filled RelStr for A being non empty Subset of FT st FT is symmetric holds ( A is connected iff for P, Q being Subset of FT st A = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT holds Q = {} FT ) proofend; theorem :: FINTOPO6:18 for FT being non empty RelStr for A being Subset of FT st FT is filled & FT is connected & A <> {} & A ` <> {} holds A ^delta <> {} proofend; theorem :: FINTOPO6:19 for FT being non empty RelStr for A being Subset of FT st FT is filled & FT is symmetric & FT is connected & A <> {} & A ` <> {} holds A ^deltai <> {} proofend; theorem :: FINTOPO6:20 for FT being non empty RelStr for A being Subset of FT st FT is filled & FT is symmetric & FT is connected & A <> {} & A ` <> {} holds A ^deltao <> {} proofend; theorem :: FINTOPO6:21 for FT being non empty RelStr for A being Subset of FT holds A ^deltai misses A ^deltao proofend; theorem :: FINTOPO6:22 for FT being non empty filled RelStr for A being Subset of FT holds A ^deltao = (A ^b) \ A proofend; theorem :: FINTOPO6:23 for FT being non empty RelStr for A, B being Subset of FT st A,B are_separated holds A ^deltao misses B proofend; theorem :: FINTOPO6:24 for FT being non empty RelStr for A, B being Subset of FT st FT is filled & A misses B & A ^deltao misses B & B ^deltao misses A holds A,B are_separated proofend; theorem Th25: :: FINTOPO6:25 for FT being non empty RelStr for x being Point of FT holds {x} is connected proofend; registration let FT be non empty RelStr ; let x be Point of FT; cluster{x} -> connected for Subset of FT; coherence for b1 being Subset of FT st b1 = {x} holds b1 is connected by Th25; end; definition let FT be non empty RelStr ; let A be Subset of FT; predA is_a_component_of FT means :Def4: :: FINTOPO6:def 4 ( A is connected & ( for B being Subset of FT st B is connected & A c= B holds A = B ) ); end; :: deftheorem Def4 defines is_a_component_of FINTOPO6:def_4_:_ for FT being non empty RelStr for A being Subset of FT holds ( A is_a_component_of FT iff ( A is connected & ( for B being Subset of FT st B is connected & A c= B holds A = B ) ) ); theorem :: FINTOPO6:26 for FT being non empty RelStr for A being Subset of FT st A is_a_component_of FT holds A <> {} FT proofend; theorem Th27: :: FINTOPO6:27 for FT being non empty RelStr for A, B being Subset of FT st A is closed & B is closed & A misses B holds A,B are_separated proofend; theorem Th28: :: FINTOPO6:28 for FT being non empty RelStr for A, B being Subset of FT st FT is filled & [#] FT = A \/ B & A,B are_separated holds ( A is open & A is closed ) proofend; theorem Th29: :: FINTOPO6:29 for FT being non empty RelStr for A, B, A1, B1 being Subset of FT st A,B are_separated & A1 c= A & B1 c= B holds A1,B1 are_separated proofend; theorem Th30: :: FINTOPO6:30 for FT being non empty RelStr for A, B, C being Subset of FT st A,B are_separated & A,C are_separated holds A,B \/ C are_separated proofend; theorem :: FINTOPO6:31 for FT being non empty RelStr st FT is filled & FT is symmetric & ( for A, B being Subset of FT st [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed holds A meets B ) holds FT is connected proofend; theorem :: FINTOPO6:32 for FT being non empty RelStr st FT is connected holds for A, B being Subset of FT st [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed holds A meets B proofend; theorem Th33: :: FINTOPO6:33 for FT being non empty RelStr for A, B, C being Subset of FT st FT is filled & A is connected & A c= B \/ C & B,C are_separated & not A c= B holds A c= C proofend; theorem Th34: :: FINTOPO6:34 for FT being non empty RelStr for A, B being Subset of FT st FT is symmetric & A is connected & B is connected & not A,B are_separated holds A \/ B is connected proofend; theorem Th35: :: FINTOPO6:35 for FT being non empty RelStr for A, C being Subset of FT st FT is symmetric & C is connected & C c= A & A c= C ^b holds A is connected proofend; theorem Th36: :: FINTOPO6:36 for FT being non empty RelStr for C being Subset of FT st FT is filled & FT is symmetric & C is connected holds C ^b is connected proofend; theorem Th37: :: FINTOPO6:37 for FT being non empty RelStr for A, B, C being Subset of FT st FT is filled & FT is symmetric & FT is connected & A is connected & ([#] FT) \ A = B \/ C & B,C are_separated holds A \/ B is connected proofend; theorem Th38: :: FINTOPO6:38 for FT being non empty RelStr for X9 being non empty SubSpace of FT for A being Subset of FT for B being Subset of X9 st A = B holds ( A is connected iff B is connected ) proofend; theorem :: FINTOPO6:39 for FT being non empty RelStr for A being Subset of FT st FT is filled & FT is symmetric & A is_a_component_of FT holds A is closed proofend; theorem Th40: :: FINTOPO6:40 for FT being non empty RelStr for A, B being Subset of FT st FT is symmetric & A is_a_component_of FT & B is_a_component_of FT & not A = B holds A,B are_separated proofend; theorem :: FINTOPO6:41 for FT being non empty RelStr for A, B being Subset of FT st FT is filled & FT is symmetric & A is_a_component_of FT & B is_a_component_of FT & not A = B holds A misses B by Th40, FINTOPO4:6; theorem :: FINTOPO6:42 for FT being non empty RelStr for C being Subset of FT st FT is filled & FT is symmetric & C is connected holds for S being Subset of FT holds ( not S is_a_component_of FT or C misses S or C c= S ) proofend; definition let FT be non empty RelStr ; let A be non empty Subset of FT; let B be Subset of FT; predB is_a_component_of A means :Def5: :: FINTOPO6:def 5 ex B1 being Subset of (FT | A) st ( B1 = B & B1 is_a_component_of FT | A ); end; :: deftheorem Def5 defines is_a_component_of FINTOPO6:def_5_:_ for FT being non empty RelStr for A being non empty Subset of FT for B being Subset of FT holds ( B is_a_component_of A iff ex B1 being Subset of (FT | A) st ( B1 = B & B1 is_a_component_of FT | A ) ); theorem :: FINTOPO6:43 for FT being non empty RelStr for A, C being Subset of FT for D being non empty Subset of FT st FT is filled & FT is symmetric & D = ([#] FT) \ A & FT is connected & A is connected & C is_a_component_of D holds ([#] FT) \ C is connected proofend; begin definition let FT be non empty RelStr ; let f be FinSequence of FT; attrf is continuous means :Def6: :: FINTOPO6:def 6 ( 1 <= len f & ( for i being Nat for x1 being Element of FT st 1 <= i & i < len f & x1 = f . i holds f . (i + 1) in U_FT x1 ) ); end; :: deftheorem Def6 defines continuous FINTOPO6:def_6_:_ for FT being non empty RelStr for f being FinSequence of FT holds ( f is continuous iff ( 1 <= len f & ( for i being Nat for x1 being Element of FT st 1 <= i & i < len f & x1 = f . i holds f . (i + 1) in U_FT x1 ) ) ); Lm2: for FT being non empty RelStr for x being Element of FT holds <*x*> is continuous proofend; registration let FT be non empty RelStr ; let x be Element of FT; cluster<*x*> -> continuous for FinSequence of FT; coherence for b1 being FinSequence of FT st b1 = <*x*> holds b1 is continuous by Lm2; end; theorem Th44: :: FINTOPO6:44 for FT being non empty RelStr for f being FinSequence of FT for x, y being Element of FT st f is continuous & y = f . (len f) & x in U_FT y holds f ^ <*x*> is continuous proofend; theorem Th45: :: FINTOPO6:45 for FT being non empty RelStr for f, g being FinSequence of FT st f is continuous & g is continuous & g . 1 in U_FT (f /. (len f)) holds f ^ g is continuous proofend; definition let FT be non empty RelStr ; let A be Subset of FT; attrA is arcwise_connected means :Def7: :: FINTOPO6:def 7 for x1, x2 being Element of FT st x1 in A & x2 in A holds ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ); end; :: deftheorem Def7 defines arcwise_connected FINTOPO6:def_7_:_ for FT being non empty RelStr for A being Subset of FT holds ( A is arcwise_connected iff for x1, x2 being Element of FT st x1 in A & x2 in A holds ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) ); registration let FT be non empty RelStr ; cluster empty -> arcwise_connected for Element of K32( the carrier of FT); coherence for b1 being Subset of FT st b1 is empty holds b1 is arcwise_connected proofend; end; Lm3: for FT being non empty RelStr for x being Element of FT holds {x} is arcwise_connected proofend; registration let FT be non empty RelStr ; let x be Element of FT; cluster{x} -> arcwise_connected for Subset of FT; coherence for b1 being Subset of FT st b1 = {x} holds b1 is arcwise_connected by Lm3; end; theorem :: FINTOPO6:46 for FT being non empty RelStr for A being Subset of FT st FT is symmetric holds ( A is connected iff A is arcwise_connected ) proofend; theorem Th47: :: FINTOPO6:47 for FT being non empty RelStr for g being FinSequence of FT for k being Nat st g is continuous & 1 <= k holds g | k is continuous proofend; theorem Th48: :: FINTOPO6:48 for FT being non empty RelStr for g being FinSequence of FT for k being Element of NAT st g is continuous & k < len g holds g /^ k is continuous proofend; definition let FT be non empty RelStr ; let g be FinSequence of FT; let A be Subset of FT; let x1, x2 be Element of FT; predg is_minimum_path_in A,x1,x2 means :Def8: :: FINTOPO6:def 8 ( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds len g <= len h ) ); end; :: deftheorem Def8 defines is_minimum_path_in FINTOPO6:def_8_:_ for FT being non empty RelStr for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT holds ( g is_minimum_path_in A,x1,x2 iff ( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds len g <= len h ) ) ); theorem :: FINTOPO6:49 for FT being non empty RelStr for A being Subset of FT for x being Element of FT st x in A holds <*x*> is_minimum_path_in A,x,x proofend; Lm4: for FT being non empty RelStr for f being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT st f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 holds ex g being FinSequence of FT st ( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds len g <= len h ) ) proofend; theorem :: FINTOPO6:50 for FT being non empty RelStr for A being Subset of FT holds ( A is arcwise_connected iff for x1, x2 being Element of FT st x1 in A & x2 in A holds ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ) proofend; theorem :: FINTOPO6:51 for FT being non empty RelStr for A being Subset of FT for x1, x2 being Element of FT st ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) holds ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 proofend; theorem Th52: :: FINTOPO6:52 for FT being non empty RelStr for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT for k being Element of NAT st g is_minimum_path_in A,x1,x2 & 1 <= k & k <= len g holds ( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k ) proofend; theorem Th53: :: FINTOPO6:53 for FT being non empty RelStr for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT for k being Element of NAT st g is_minimum_path_in A,x1,x2 & k < len g holds ( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 ) proofend; theorem :: FINTOPO6:54 for FT being non empty RelStr for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds for k being Nat st 1 <= k & k <= len g holds g | k is_minimum_path_in A,x1,g /. k proofend; theorem :: FINTOPO6:55 for FT being non empty RelStr for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds g is one-to-one proofend; definition let FT be non empty RelStr ; let f be FinSequence of FT; attrf is inv_continuous means :Def9: :: FINTOPO6:def 9 ( 1 <= len f & ( for i, j being Nat for y being Element of FT st 1 <= i & i <= len f & 1 <= j & j <= len f & y = f . i & i <> j & f . j in U_FT y & not i = j + 1 holds j = i + 1 ) ); end; :: deftheorem Def9 defines inv_continuous FINTOPO6:def_9_:_ for FT being non empty RelStr for f being FinSequence of FT holds ( f is inv_continuous iff ( 1 <= len f & ( for i, j being Nat for y being Element of FT st 1 <= i & i <= len f & 1 <= j & j <= len f & y = f . i & i <> j & f . j in U_FT y & not i = j + 1 holds j = i + 1 ) ) ); theorem Th56: :: FINTOPO6:56 for FT being non empty RelStr for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds g is inv_continuous proofend; theorem :: FINTOPO6:57 for FT being non empty RelStr for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & x1 <> x2 holds ( ( for i being Nat st 1 < i & i < len g holds (rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ) & (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} ) proofend; theorem :: FINTOPO6:58 for FT being non empty RelStr for g being FinSequence of FT for A being non empty Subset of FT for x1, x2 being Element of FT for B0 being Subset of (FT | A) st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & B0 = {x1} holds for i being Element of NAT st i < len g holds ( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) ) proofend;