begin
theorem Th1:
theorem Th2:
theorem Th3:
:: deftheorem Def1 defines connected FINTOPO6:def 1 :
for FT being non empty RelStr holds
( FT is connected iff [#] FT is connected );
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
:: 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
:: 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 Th8:
theorem
theorem Th10:
theorem
theorem
theorem Th13:
theorem
theorem
theorem Th16:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th25:
:: deftheorem Def4 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
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem
theorem
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem
theorem Th40:
theorem
theorem
:: deftheorem Def5 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
begin
:: deftheorem Def6 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
theorem Th44:
theorem Th45:
:: deftheorem Def7 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 ) );
Lm3:
for FT being non empty RelStr
for x being Element of FT holds {x} is arcwise_connected
theorem
theorem Th47:
theorem Th48:
:: deftheorem Def8 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
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 ) )
theorem
theorem
theorem Th52:
theorem Th53:
theorem
theorem
:: deftheorem Def9 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 Th56:
theorem
theorem