:: Connectedness and Continuous Sequences in Finite Topological Spaces
:: by Yatsuka Nakamura
::
:: Received August 18, 2006
:: 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 b₁ being Subset of FT st b₁ is empty holds
b₁ 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 b₁ being RelStr st
( the carrier of b₁ c= the carrier of T & ( for x being Element of b₁ st x in the carrier of b₁ holds
U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of b₁ ) )

proof end;

end;

:: deftheorem Def2 defines SubSpace FINTOPO6:def 2 :
for T, b₂ being RelStr holds
( b₂ is SubSpace of T iff ( the carrier of b₂ c= the carrier of T & ( for x being Element of b₂ st x in the carrier of b₂ holds
U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of b₂ ) ) );

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 b₁ being SubSpace of T st b₁ is strict

proof end;

end;

registration

let T be non empty RelStr ;

cluster non empty strict for SubSpace of T;

existence
ex b₁ being SubSpace of T st
( b₁ is strict & not b₁ 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 b₁ being non empty strict SubSpace of T st [#] b₁ = P

proof end;

uniqueness
for b₁, b₂ being non empty strict SubSpace of T st [#] b₁ = P & [#] b₂ = P holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines | FINTOPO6:def 3 :
for T being non empty RelStr
for P being non empty Subset of T
for b₃ being non empty strict SubSpace of T holds
( b₃ = T | P iff [#] b₃ = 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 b₁ being non empty SubSpace of FT holds b₁ 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 b₁ being Subset of FT st b₁ = {x} holds
b₁ 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 Th39, 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 )

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 b₁ being FinSequence of FT st b₁ = <*x*> holds
b₁ 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 b₁ being Subset of FT st b₁ is empty holds
b₁ 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 b₁ being Subset of FT st b₁ = {x} holds
b₁ 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;