:: Continuous Mappings between Finite and One-Dimensional Finite Topological Spaces :: by Hiroshi Imura , Masami Tanaka and Yatsuka Nakamura :: :: Received July 13, 2004 :: Copyright (c) 2004-2012 Association of Mizar Users begin definition let FT be non empty RelStr ; let A, B be Subset of FT; predA,B are_separated means :Def1: :: FINTOPO4:def 1 ( A ^b misses B & A misses B ^b ); symmetry for A, B being Subset of FT st A ^b misses B & A misses B ^b holds ( B ^b misses A & B misses A ^b ) ; end; :: deftheorem Def1 defines are_separated FINTOPO4:def_1_:_ for FT being non empty RelStr for A, B being Subset of FT holds ( A,B are_separated iff ( A ^b misses B & A misses B ^b ) ); theorem Th1: :: FINTOPO4:1 for FT being non empty filled RelStr for A being Subset of FT for n, m being Element of NAT st n <= m holds Finf (A,n) c= Finf (A,m) proofend; theorem :: FINTOPO4:2 for FT being non empty filled RelStr for A being Subset of FT for n, m being Element of NAT st n <= m holds Fcl (A,n) c= Fcl (A,m) proofend; theorem :: FINTOPO4:3 for FT being non empty filled RelStr for A being Subset of FT for n, m being Element of NAT st n <= m holds Fdfl (A,m) c= Fdfl (A,n) proofend; theorem :: FINTOPO4:4 for FT being non empty filled RelStr for A being Subset of FT for n, m being Element of NAT st n <= m holds Fint (A,m) c= Fint (A,n) proofend; theorem :: FINTOPO4:5 for FT being non empty RelStr for A, B being Subset of FT st A,B are_separated holds B,A are_separated ; theorem Th6: :: FINTOPO4:6 for FT being non empty filled RelStr for A, B being Subset of FT st A,B are_separated holds A misses B proofend; theorem :: FINTOPO4:7 for FT being non empty RelStr for A, B being Subset of FT st FT is symmetric holds ( A,B are_separated iff ( A ^f misses B & A misses B ^f ) ) proofend; theorem Th8: :: FINTOPO4:8 for FT being non empty filled RelStr for A, B being Subset of FT st FT is symmetric & A ^b misses B holds A misses B ^b proofend; theorem :: FINTOPO4:9 for FT being non empty filled RelStr for A, B being Subset of FT st FT is symmetric & A misses B ^b holds A ^b misses B by Th8; theorem :: FINTOPO4:10 for FT being non empty filled RelStr for A, B being Subset of FT st FT is symmetric holds ( A,B are_separated iff A ^b misses B ) proofend; theorem :: FINTOPO4:11 for FT being non empty filled RelStr for A, B being Subset of FT st FT is symmetric holds ( A,B are_separated iff A misses B ^b ) proofend; theorem Th12: :: FINTOPO4:12 for FT being non empty filled RelStr for IT being Subset of FT st FT is symmetric holds ( IT is connected iff for A, B being Subset of FT st IT = A \/ B & A,B are_separated & not A = IT holds B = IT ) proofend; theorem :: FINTOPO4:13 for FT being non empty filled RelStr for B being Subset of FT st FT is symmetric holds ( B is connected iff for C being Subset of FT holds ( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C ) ) proofend; definition let FT1, FT2 be non empty RelStr ; let f be Function of FT1,FT2; let n be Element of NAT ; predf is_continuous n means :Def2: :: FINTOPO4:def 2 for x being Element of FT1 for y being Element of FT2 st x in the carrier of FT1 & y = f . x holds f .: (U_FT (x,0)) c= U_FT (y,n); end; :: deftheorem Def2 defines is_continuous FINTOPO4:def_2_:_ for FT1, FT2 being non empty RelStr for f being Function of FT1,FT2 for n being Element of NAT holds ( f is_continuous n iff for x being Element of FT1 for y being Element of FT2 st x in the carrier of FT1 & y = f . x holds f .: (U_FT (x,0)) c= U_FT (y,n) ); theorem :: FINTOPO4:14 for FT1 being non empty RelStr for FT2 being non empty filled RelStr for n being Element of NAT for f being Function of FT1,FT2 st f is_continuous 0 holds f is_continuous n proofend; theorem :: FINTOPO4:15 for FT1 being non empty RelStr for FT2 being non empty filled RelStr for n0, n being Element of NAT for f being Function of FT1,FT2 st f is_continuous n0 & n0 <= n holds f is_continuous n proofend; theorem Th16: :: FINTOPO4:16 for FT1, FT2 being non empty RelStr for A being Subset of FT1 for B being Subset of FT2 for f being Function of FT1,FT2 st f is_continuous 0 & B = f .: A holds f .: (A ^b) c= B ^b proofend; theorem :: FINTOPO4:17 for FT1, FT2 being non empty RelStr for A being Subset of FT1 for B being Subset of FT2 for f being Function of FT1,FT2 st A is connected & f is_continuous 0 & B = f .: A holds B is connected proofend; ::1 dimensional linear FT_Str definition let n be Nat; func Nbdl1 n -> Relation of (Seg n) means :Def3: :: FINTOPO4:def 3 for i being Element of NAT st i in Seg n holds Im (it,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))}; existence ex b1 being Relation of (Seg n) st for i being Element of NAT st i in Seg n holds Im (b1,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} proofend; uniqueness for b1, b2 being Relation of (Seg n) st ( for i being Element of NAT st i in Seg n holds Im (b1,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ) & ( for i being Element of NAT st i in Seg n holds Im (b2,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ) holds b1 = b2 proofend; end; :: deftheorem Def3 defines Nbdl1 FINTOPO4:def_3_:_ for n being Nat for b2 being Relation of (Seg n) holds ( b2 = Nbdl1 n iff for i being Element of NAT st i in Seg n holds Im (b2,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ); definition let n be Nat; assume A1: n > 0 ; func FTSL1 n -> non empty RelStr equals :Def4: :: FINTOPO4:def 4 RelStr(# (Seg n),(Nbdl1 n) #); correctness coherence RelStr(# (Seg n),(Nbdl1 n) #) is non empty RelStr ; by A1; end; :: deftheorem Def4 defines FTSL1 FINTOPO4:def_4_:_ for n being Nat st n > 0 holds FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #); theorem :: FINTOPO4:18 for n being Nat st n > 0 holds FTSL1 n is filled proofend; theorem :: FINTOPO4:19 for n being Nat st n > 0 holds FTSL1 n is symmetric proofend; ::1 dimensional cyclic FT_Str definition let n be Nat; func Nbdc1 n -> Relation of (Seg n) means :Def5: :: FINTOPO4:def 5 for i being Element of NAT st i in Seg n holds ( ( 1 < i & i < n implies Im (it,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (it,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (it,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (it,i) = {i} ) ); existence ex b1 being Relation of (Seg n) st for i being Element of NAT st i in Seg n holds ( ( 1 < i & i < n implies Im (b1,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b1,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b1,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b1,i) = {i} ) ) proofend; uniqueness for b1, b2 being Relation of (Seg n) st ( for i being Element of NAT st i in Seg n holds ( ( 1 < i & i < n implies Im (b1,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b1,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b1,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b1,i) = {i} ) ) ) & ( for i being Element of NAT st i in Seg n holds ( ( 1 < i & i < n implies Im (b2,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b2,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b2,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b2,i) = {i} ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def5 defines Nbdc1 FINTOPO4:def_5_:_ for n being Nat for b2 being Relation of (Seg n) holds ( b2 = Nbdc1 n iff for i being Element of NAT st i in Seg n holds ( ( 1 < i & i < n implies Im (b2,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b2,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b2,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b2,i) = {i} ) ) ); definition let n be Nat; assume A1: n > 0 ; func FTSC1 n -> non empty RelStr equals :Def6: :: FINTOPO4:def 6 RelStr(# (Seg n),(Nbdc1 n) #); correctness coherence RelStr(# (Seg n),(Nbdc1 n) #) is non empty RelStr ; by A1; end; :: deftheorem Def6 defines FTSC1 FINTOPO4:def_6_:_ for n being Nat st n > 0 holds FTSC1 n = RelStr(# (Seg n),(Nbdc1 n) #); theorem :: FINTOPO4:20 for n being Element of NAT st n > 0 holds FTSC1 n is filled proofend; theorem :: FINTOPO4:21 for n being Element of NAT st n > 0 holds FTSC1 n is symmetric proofend;