:: by Yatsuka Nakamura

::

:: Received August 18, 2006

:: Copyright (c) 2006-2016 Association of Mizar Users

registration

let FT be non empty RelStr ;

coherence

for b_{1} being Subset of FT st b_{1} is empty holds

b_{1} is connected
;

end;
coherence

for b

b

::$CT

registration
end;

theorem :: FINTOPO6:3

definition
end;

:: deftheorem defines connected FINTOPO6:def 1 :

for FT being non empty RelStr holds

( FT is connected iff [#] FT is connected );

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

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

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

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

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 ;

ex b_{1} being RelStr st

( the carrier of b_{1} c= the carrier of T & ( for x being Element of b_{1} st x in the carrier of b_{1} holds

U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of b_{1} ) )

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

ex b

( the carrier of b

U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of b

proof end;

:: deftheorem Def2 defines SubSpace FINTOPO6:def 2 :

for T, b_{2} being RelStr holds

( b_{2} is SubSpace of T iff ( the carrier of b_{2} c= the carrier of T & ( for x being Element of b_{2} st x in the carrier of b_{2} holds

U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of b_{2} ) ) );

for T, b

( b

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

registration

let T be non empty RelStr ;

existence

ex b_{1} being SubSpace of T st

( b_{1} is strict & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

definition

let T be non empty RelStr ;

let P be non empty Subset of T;

existence

ex b_{1} being non empty strict SubSpace of T st [#] b_{1} = P

for b_{1}, b_{2} being non empty strict SubSpace of T st [#] b_{1} = P & [#] b_{2} = P holds

b_{1} = b_{2}

end;
let P be non empty Subset of T;

existence

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines | FINTOPO6:def 3 :

for T being non empty RelStr

for P being non empty Subset of T

for b_{3} being non empty strict SubSpace of T holds

( b_{3} = T | P iff [#] b_{3} = P );

for T being non empty RelStr

for P being non empty Subset of T

for b

( b

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

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 ;

coherence

for b_{1} being non empty SubSpace of FT holds b_{1} is filled
by Th7;

end;
coherence

for b

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

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

for X9 being SubSpace of FT

for A being Subset of X9 holds A is Subset of FT

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

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)

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

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

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 )

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 )

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 <> {}

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 <> {}

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 <> {}

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:23

for FT being non empty RelStr

for A, B being Subset of FT st A,B are_separated holds

A ^deltao misses B

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

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;

registration

let FT be non empty RelStr ;

let x be Point of FT;

coherence

for b_{1} being Subset of FT st b_{1} = {x} holds

b_{1} is connected
by Th24;

end;
let x be Point of FT;

coherence

for b

b

definition

let FT be non empty RelStr ;

let A be Subset of FT;

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

( A is connected & ( for B being Subset of FT st B is connected & A c= B holds

A = B ) );

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

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

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 )

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

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

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

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

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

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

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

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

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

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 )

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

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

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;

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 )

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;

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

ex B1 being Subset of (FT | A) st

( B1 = B & B1 is_a_component_of FT | A );

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

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

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;

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

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;

coherence

for b_{1} being FinSequence of FT st b_{1} = <*x*> holds

b_{1} is continuous
by Lm2;

end;
let x be Element of FT;

coherence

for b

b

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

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

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;

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

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

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

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 ;

coherence

for b_{1} being Subset of FT st b_{1} is empty holds

b_{1} is arcwise_connected
;

end;
coherence

for b

b

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;

coherence

for b_{1} being Subset of FT st b_{1} = {x} holds

b_{1} is arcwise_connected
by Lm3;

end;
let x be Element of FT;

coherence

for b

b

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 )

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

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

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;

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

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

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

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

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 )

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

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 )

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 )

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

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

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;

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

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

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

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

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;