:: Connectedness and Continuous Sequences in Finite Topological Spaces
:: by Yatsuka Nakamura
::
:: Received August 18, 2006
:: Copyright (c) 2006-2017 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));
*