begin
theorem Th1:
theorem Th2:
theorem Th3:
:: deftheorem Def1 defines connected FINTOPO6:def 1 :
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
:: deftheorem Def2 defines SubSpace FINTOPO6:def 2 :
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 :
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 :
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 :
theorem
begin
:: deftheorem Def6 defines continuous FINTOPO6:def 6 :
Lm2:
for FT being non empty RelStr
for x being Element of holds <*x*> is continuous
theorem Th44:
theorem Th45:
:: deftheorem Def7 defines arcwise_connected FINTOPO6:def 7 :
Lm3:
for FT being non empty RelStr
for x being Element of holds {x} is arcwise_connected
theorem
theorem Th47:
theorem Th48:
:: deftheorem Def8 defines is_minimum_path_in FINTOPO6:def 8 :
theorem
Lm4:
for FT being non empty RelStr
for f being FinSequence of
for A being Subset of
for x1, x2 being Element of st f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 holds
ex g being FinSequence of st
( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of 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 :
theorem Th56:
theorem
theorem