:: Connectedness and Continuous Sequences in Finite Topological Spaces :: by Yatsuka Nakamura :: :: Received August 18, 2006 :: Copyright (c) 2006-2021 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, XBOOLE_0, ORDERS_2, SUBSET_1, RELAT_2, FIN_TOPO, TARSKI, CONNSP_1, PRE_TOPC, STRUCT_0, RELAT_1, RCOMP_1, FINSEQ_1, ORDINAL2, XXREAL_0, NAT_1, ARYTM_3, FUNCT_1, ORDINAL4, PARTFUN1, CARD_1, ARYTM_1, BORSUK_2, RFINSEQ, FINTOPO3, FINTOPO6; notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, ORDINAL1, NUMBERS, XXREAL_0, NAT_1, DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FINSEQ_1, STRUCT_0, ORDERS_2, FIN_TOPO, FINTOPO3, NAT_D, ENUMSET1, FINTOPO4, PRE_TOPC, RFINSEQ; constructors DOMAIN_1, EQREL_1, RFINSEQ, RFUNCT_3, NAT_D, FIN_TOPO, FINTOPO3, FINTOPO4, REAL_1, RELSET_1; registrations XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, FIN_TOPO, ORDINAL1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Connectedness and Subspaces reserve FT for non empty RelStr, A,B,C for Subset of FT; registration let FT; cluster empty -> connected for Subset of FT; end; ::$CT theorem :: FINTOPO6:2 ({}FT)^b={}; registration let FT; cluster ({}FT)^b -> empty; end; theorem :: FINTOPO6:3 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; definition let FT be non empty RelStr; attr FT is connected means :: FINTOPO6:def 1 [#]FT is connected; end; theorem :: FINTOPO6:4 for A being Subset of FT holds A is connected implies for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated holds A2 = {}FT or B2 = {}FT; theorem :: FINTOPO6:5 FT is connected implies for A, B being Subset of FT st [#]FT = A \/ B & A misses B & A,B are_separated holds A = {}FT or B = {}FT; theorem :: FINTOPO6:6 for A,B being Subset of FT st FT is symmetric & A^b misses B holds A misses B^b; theorem :: FINTOPO6:7 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 holds A2 = {} FT or B2 = {}FT holds A is connected; definition let T be RelStr; mode SubSpace of T -> RelStr means :: 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; end; registration let T be RelStr; cluster strict for SubSpace of T; end; registration let T be non empty RelStr; cluster strict non empty for SubSpace of T; end; definition let T be non empty RelStr, P be non empty Subset of T; func T|P -> strict non empty SubSpace of T means :: FINTOPO6:def 3 [#]it = P; end; theorem :: FINTOPO6:8 for X being non empty SubSpace of FT st FT is filled holds X is filled; registration let FT be filled non empty RelStr; cluster -> filled for non empty SubSpace of FT; end; theorem :: FINTOPO6:9 for X being non empty SubSpace of FT st FT is symmetric holds X is symmetric; theorem :: FINTOPO6:10 for X9 being SubSpace of FT, A being Subset of X9 holds A is Subset of FT; theorem :: FINTOPO6:11 for P being Subset of FT holds P is closed iff P` is open; theorem :: FINTOPO6:12 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; theorem :: FINTOPO6:13 for X9 being non empty SubSpace of FT, A being Subset of FT, A1 being Subset of X9 st A = A1 holds A1^b = (A^b) /\ ([#]X9); theorem :: FINTOPO6:14 for X9 being non empty SubSpace of FT, P1,Q1 being Subset of FT, P,Q being Subset of X9 st P=P1 & Q=Q1 holds P,Q are_separated implies P1,Q1 are_separated; theorem :: FINTOPO6:15 for X9 being non empty SubSpace of FT, P,Q being Subset of FT, P1,Q1 being Subset of X9 st P=P1 & Q=Q1 & P \/ Q c= [#](X9) holds P,Q are_separated implies P1,Q1 are_separated; theorem :: FINTOPO6:16 for A being non empty Subset of FT holds A is connected iff FT|A is connected ; theorem :: FINTOPO6:17 for FT being filled non empty RelStr, 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 holds P = {}FT or Q = {}FT; theorem :: FINTOPO6:18 for A being Subset of FT st FT is filled connected & A <> {} & A` <> {} holds A^delta <>{}; theorem :: FINTOPO6:19 for A being Subset of FT st FT is filled symmetric & FT is connected & A <> {} & A` <> {} holds A^deltai <>{}; theorem :: FINTOPO6:20 for A being Subset of FT st FT is filled symmetric & FT is connected & A <> {} & A` <>{} holds A^deltao <>{}; theorem :: FINTOPO6:21 for A being Subset of FT holds A^deltai misses A^deltao; theorem :: FINTOPO6:22 for FT being filled non empty RelStr, A being Subset of FT holds A ^deltao=(A^b) \ A; theorem :: FINTOPO6:23 for A, B being Subset of FT st A,B are_separated holds A^deltao misses B; theorem :: FINTOPO6:24 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; theorem :: FINTOPO6:25 for x being Point of FT holds {x} is connected; registration let FT; let x be Point of FT; cluster {x} -> connected for Subset of FT; end; definition let FT be non empty RelStr, A be Subset of FT; pred A is_a_component_of FT means :: FINTOPO6:def 4 A is connected & for B being Subset of FT st B is connected holds A c= B implies A = B; end; theorem :: FINTOPO6:26 for A being Subset of FT st A is_a_component_of FT holds A <> {}FT; theorem :: FINTOPO6:27 A is closed & B is closed & A misses B implies A,B are_separated; theorem :: FINTOPO6:28 FT is filled & [#]FT = A \/ B & A,B are_separated implies A is open closed; theorem :: FINTOPO6:29 for A,B,A1,B1 being Subset of FT holds A,B are_separated & A1 c= A & B1 c= B implies A1,B1 are_separated; theorem :: FINTOPO6:30 A,B are_separated & A,C are_separated implies A,B \/ C are_separated; theorem :: FINTOPO6:31 FT is filled 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) implies FT is connected; theorem :: FINTOPO6:32 FT is connected implies 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; theorem :: FINTOPO6:33 FT is filled & A is connected & A c= B \/ C & B,C are_separated implies A c= B or A c= C; theorem :: FINTOPO6:34 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; theorem :: FINTOPO6:35 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; theorem :: FINTOPO6:36 for C being Subset of FT st FT is filled symmetric & C is connected holds C^b is connected; theorem :: FINTOPO6:37 FT is filled symmetric connected & A is connected & [#]FT \ A = B \/ C & B,C are_separated implies A \/ B is connected; theorem :: FINTOPO6:38 for X9 being non empty SubSpace of FT, A being Subset of FT, B being Subset of X9 st A = B holds A is connected iff B is connected; theorem :: FINTOPO6:39 for A being Subset of FT st FT is filled symmetric & A is_a_component_of FT holds A is closed; theorem :: FINTOPO6:40 for A,B being Subset of FT st FT is symmetric & A is_a_component_of FT & B is_a_component_of FT holds A = B or A,B are_separated; theorem :: FINTOPO6:41 for A,B being Subset of FT st FT is filled symmetric & A is_a_component_of FT & B is_a_component_of FT holds A = B or A misses B; theorem :: FINTOPO6:42 for C being Subset of FT st FT is filled symmetric & C is connected holds for S being Subset of FT st S is_a_component_of FT holds C misses S or C c= S; definition let FT be non empty RelStr, A be non empty Subset of FT, B be Subset of FT; pred B is_a_component_of A means :: FINTOPO6:def 5 ex B1 being Subset of FT|A st B1 = B & B1 is_a_component_of FT|A; end; theorem :: FINTOPO6:43 for D being non empty Subset of FT st FT is filled symmetric & D=[#]FT \ A holds FT is connected & A is connected & C is_a_component_of D implies [#] FT \ C is connected; begin ::Continuous Finite Sequences and Minimum Path definition let FT; let f be FinSequence of FT; attr f is continuous means :: FINTOPO6:def 6 1<=len f & for i being Nat,x1 being Element of FT st 1<=i & i -> continuous for FinSequence of FT; end; theorem :: FINTOPO6:44 for f being FinSequence of FT,x,y being Element of FT st f is continuous & y=f.(len f) & x in U_FT y holds f^(<*x*>) is continuous; theorem :: FINTOPO6:45 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; definition let FT; let A be Subset of FT; attr A is arcwise_connected means :: FINTOPO6:def 7 for x1,x2 being Element of FT st x1 in A & x2 in A ex f being FinSequence of FT st f is continuous & rng f c=A & f. 1=x1 & f.(len f)=x2; end; registration let FT; cluster empty -> arcwise_connected for Subset of FT; end; registration let FT; let x be Element of FT; cluster {x} -> arcwise_connected for Subset of FT; end; theorem :: FINTOPO6:46 for A being Subset of FT st FT is symmetric holds A is connected iff A is arcwise_connected; theorem :: FINTOPO6:47 for g being FinSequence of FT, k being Nat st g is continuous & 1<=k holds g|k is continuous; theorem :: FINTOPO6:48 for g being FinSequence of FT, k being Element of NAT st g is continuous & k is_minimum_path_in A,x,x; theorem :: FINTOPO6:50 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 ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2; theorem :: FINTOPO6:51 for A being Subset of FT,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 ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2; theorem :: FINTOPO6:52 for g being FinSequence of FT,A being Subset of FT, x1,x2 being Element of FT, 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; theorem :: FINTOPO6:53 for g being FinSequence of FT,A being Subset of FT, x1,x2 being Element of FT, k being Element of NAT st g is_minimum_path_in A,x1,x2 & kj & f.j in U_FT y holds i=j+1 or j=i+1; end; theorem :: FINTOPO6:56 for g being FinSequence of FT,A being Subset of FT, x1,x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds g is inv_continuous; theorem :: FINTOPO6:57 for g being FinSequence of FT,A being Subset of FT, x1,x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is filled symmetric & x1<>x2 holds (for i being Nat st 1=1 implies not g.(i+1) in Finf(B0,i-'1));