:: Connectedness and Continuous Sequences in Finite Topological Spaces
:: by Yatsuka Nakamura
::
:: Copyright (c) 2006-2021 Association of Mizar Users

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
;
end;

theorem :: FINTOPO6:1
canceled;

::\$CT
theorem Th1: :: FINTOPO6:2
for FT being non empty RelStr holds ({} FT) ^b = {}
proof end;

registration
let FT be non empty RelStr ;
cluster ({} FT) ^b -> empty ;
coherence
({} FT) ^b is empty
by Th1;
end;

theorem :: 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 ;

definition
let FT be non empty RelStr ;
attr FT is connected means :: FINTOPO6:def 1
[#] FT is connected ;
end;

:: deftheorem defines connected FINTOPO6:def 1 :
for FT being non empty RelStr holds
( FT is connected iff [#] FT is connected );

theorem Th3: :: 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
proof end;

theorem Th4: :: 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
proof end;

theorem Th5: :: 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
proof end;

theorem Th6: :: 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
proof end;

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 ) )
proof end;
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
proof end;

registration
let T be RelStr ;
cluster strict for SubSpace of T;
existence
ex b1 being SubSpace of T st b1 is strict
proof end;
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 )
proof end;
end;

definition
let T be non empty RelStr ;
let P be non empty Subset of T;
func T | 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
proof end;
uniqueness
for b1, b2 being non empty strict SubSpace of T st [#] b1 = P & [#] b2 = P holds
b1 = b2
proof end;
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 Th7: :: FINTOPO6:8
for FT being non empty RelStr
for X being non empty SubSpace of FT st FT is filled holds
X is filled
proof end;

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 Th7;
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
proof end;

theorem Th9: :: 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
proof end;

theorem :: FINTOPO6:11
for FT being non empty RelStr
for P being Subset of FT holds
( P is closed iff P  is open )
proof end;

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 ) ) )
proof end;

theorem Th12: :: 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)
proof end;

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
proof end;

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
proof end;

theorem Th15: :: 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 )
proof end;

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 )
proof end;

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 <> {}
proof end;

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 <> {}
proof end;

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 <> {}
proof end;

theorem :: FINTOPO6:21
for FT being non empty RelStr
for A being Subset of FT holds A ^deltai misses A ^deltao
proof end;

theorem :: FINTOPO6:22
for FT being non empty filled RelStr
for A being Subset of FT holds A ^deltao = (A ^b) \ A
proof end;

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
proof end;

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
proof end;

theorem Th24: :: FINTOPO6:25
for FT being non empty RelStr
for x being Point of FT holds {x} is connected
proof end;

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 Th24;
end;

definition
let FT be non empty RelStr ;
let 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 & A c= B holds
A = B ) );
end;

:: deftheorem 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
proof end;

theorem :: 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 by FINTOPO4:def 1;

theorem Th27: :: 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 )
proof end;

theorem Th28: :: 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
proof end;

theorem Th29: :: 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
proof end;

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
proof end;

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
proof end;

theorem Th32: :: 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
proof end;

theorem Th33: :: 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
proof end;

theorem Th34: :: 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
proof end;

theorem Th35: :: 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
proof end;

theorem Th36: :: 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
proof end;

theorem Th37: :: 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 )
proof end;

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
proof end;

theorem Th39: :: 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
proof end;

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 ;

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 )
proof end;

definition
let FT be non empty RelStr ;
let A be non empty Subset of FT;
let 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;

:: deftheorem 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
proof end;

definition
let FT be non empty RelStr ;
let f be FinSequence of FT;
attr f is continuous means :: 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 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

by FINSEQ_1:39;

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 Th43: :: 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
proof end;

theorem Th44: :: 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
proof end;

definition
let FT be non empty RelStr ;
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 holds
ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 );
end;

:: deftheorem 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
;
end;

Lm3: for FT being non empty RelStr
for x being Element of FT holds {x} is arcwise_connected

proof end;

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 )
proof end;

theorem Th46: :: 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
proof end;

theorem Th47: :: 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
proof end;

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;
pred g is_minimum_path_in A,x1,x2 means :: 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 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
proof end;

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 ) )

proof end;

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 )
proof end;

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
proof end;

theorem Th51: :: 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 )
proof end;

theorem Th52: :: 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 )
proof end;

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
proof end;

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
proof end;

definition
let FT be non empty RelStr ;
let f be FinSequence of FT;
attr f is inv_continuous means :: 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 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 Th55: :: 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
proof end;

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))} )
proof end;

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)) ) )
proof end;