:: Connectedness and Continuous Sequences in Finite Topological Spaces
:: by Yatsuka Nakamura
::
:: Received August 18, 2006
:: Copyright (c) 2006 Association of Mizar Users
theorem Th1: :: FINTOPO6:1
theorem Th2: :: FINTOPO6:2
theorem Th3: :: FINTOPO6:3
:: deftheorem Def1 defines connected FINTOPO6:def 1 :
theorem Th4: :: FINTOPO6:4
theorem Th5: :: FINTOPO6:5
theorem Th6: :: FINTOPO6:6
theorem Th7: :: FINTOPO6:7
:: 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: :: FINTOPO6:8
theorem :: FINTOPO6:9
theorem Th10: :: FINTOPO6:10
theorem :: FINTOPO6:11
theorem :: FINTOPO6:12
theorem Th13: :: FINTOPO6:13
theorem :: FINTOPO6:14
theorem :: FINTOPO6:15
theorem Th16: :: FINTOPO6:16
theorem :: FINTOPO6:17
theorem :: FINTOPO6:18
theorem :: FINTOPO6:19
theorem :: FINTOPO6:20
theorem :: FINTOPO6:21
theorem :: FINTOPO6:22
theorem :: FINTOPO6:23
theorem :: FINTOPO6:24
theorem Th25: :: FINTOPO6:25
:: deftheorem Def4 defines is_a_component_of FINTOPO6:def 4 :
theorem :: FINTOPO6:26
theorem Th27: :: FINTOPO6:27
theorem Th28: :: FINTOPO6:28
theorem Th29: :: FINTOPO6:29
theorem Th30: :: FINTOPO6:30
theorem :: FINTOPO6:31
theorem :: FINTOPO6:32
theorem Th33: :: FINTOPO6:33
theorem Th34: :: FINTOPO6:34
theorem Th35: :: FINTOPO6:35
theorem Th36: :: FINTOPO6:36
theorem Th37: :: FINTOPO6:37
theorem Th38: :: FINTOPO6:38
theorem :: FINTOPO6:39
theorem Th40: :: FINTOPO6:40
theorem :: FINTOPO6:41
theorem :: FINTOPO6:42
:: deftheorem Def5 defines is_a_component_of FINTOPO6:def 5 :
theorem :: FINTOPO6:43
:: deftheorem Def6 defines continuous FINTOPO6:def 6 :
Lm2:
for FT being non empty RelStr
for x being Element of FT holds <*x*> is continuous
theorem Th44: :: FINTOPO6:44
theorem Th45: :: FINTOPO6:45
:: deftheorem Def7 defines arcwise_connected FINTOPO6:def 7 :
Lm4:
for FT being non empty RelStr
for x being Element of FT holds {x} is arcwise_connected
theorem :: FINTOPO6:46
theorem Th47: :: FINTOPO6:47
theorem Th48: :: FINTOPO6:48
:: deftheorem Def8 defines is_minimum_path_in FINTOPO6:def 8 :
theorem :: FINTOPO6:49
Lm5:
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 :: FINTOPO6:50
theorem :: FINTOPO6:51
theorem Th52: :: FINTOPO6:52
theorem Th53: :: FINTOPO6:53
theorem :: FINTOPO6:54
theorem :: FINTOPO6:55
:: deftheorem Def9 defines inv_continuous FINTOPO6:def 9 :
theorem Th56: :: FINTOPO6:56
theorem :: FINTOPO6:57
theorem :: FINTOPO6:58