:: 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-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, ORDERS_2, SUBSET_1, CONNSP_1, FIN_TOPO, XXREAL_0, FINTOPO3, TARSKI, ARYTM_3, ARYTM_1, CARD_1, RELAT_2, FUNCT_1, STRUCT_0, RELAT_1, NAT_1, FINSEQ_1, ZFMISC_1, FINTOPO4; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, FUNCT_1, RELSET_1, FUNCT_2, FINSEQ_1, STRUCT_0, ORDERS_2, FIN_TOPO, FINTOPO3, NAT_D, ENUMSET1; constructors ENUMSET1, NAT_1, EQREL_1, NAT_D, FIN_TOPO, FINTOPO3, FINSEQ_1, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, STRUCT_0, FIN_TOPO, ORDINAL1, FINSEQ_1, RELAT_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin definition let FT be non empty RelStr, A,B be Subset of FT; pred A,B are_separated means :: FINTOPO4:def 1 A^b misses B & A misses B^b; symmetry; end; theorem :: FINTOPO4:1 for FT being filled non empty RelStr, A being Subset of FT, n,m being Element of NAT st n<=m holds Finf(A,n) c= Finf(A,m); theorem :: FINTOPO4:2 for FT being filled non empty RelStr, A being Subset of FT, n,m being Element of NAT st n<=m holds Fcl(A,n) c= Fcl(A,m); theorem :: FINTOPO4:3 for FT being filled non empty RelStr, A being Subset of FT, n,m being Element of NAT st n<=m holds Fdfl(A,m) c= Fdfl(A,n); theorem :: FINTOPO4:4 for FT being filled non empty RelStr, A being Subset of FT, n,m being Element of NAT st n<=m holds Fint(A,m) c= Fint(A,n); theorem :: FINTOPO4:5 for FT being non empty RelStr,A,B being Subset of FT st A,B are_separated holds B,A are_separated; theorem :: FINTOPO4:6 for FT being filled non empty RelStr, A,B being Subset of FT st A,B are_separated holds A misses B; theorem :: FINTOPO4:7 for FT being non empty RelStr, A,B being Subset of FT st FT is symmetric holds A,B are_separated iff A^f misses B & A misses (B^f); theorem :: FINTOPO4:8 for FT being filled non empty RelStr, A,B being Subset of FT st FT is symmetric & A^b misses B holds A misses (B^b); theorem :: FINTOPO4:9 for FT being filled non empty RelStr, A,B being Subset of FT st FT is symmetric & A misses (B^b) holds A^b misses B; theorem :: FINTOPO4:10 for FT being filled non empty RelStr, A,B being Subset of FT st FT is symmetric holds A,B are_separated iff A^b misses B; theorem :: FINTOPO4:11 for FT being filled non empty RelStr, A,B being Subset of FT st FT is symmetric holds A,B are_separated iff A misses (B^b); theorem :: FINTOPO4:12 for FT being filled non empty RelStr, 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 holds A = IT or B = IT); theorem :: FINTOPO4:13 for FT being filled non empty RelStr, B being Subset of FT st FT is symmetric holds B is connected iff not (ex C being Subset of FT st C<>{} & B\C <>{} & C c= B & (C^b) misses (B\C)); definition let FT1,FT2 be non empty RelStr, f be Function of FT1, FT2, n be Nat; pred f is_continuous n means :: FINTOPO4:def 2 for x being Element of FT1,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; theorem :: FINTOPO4:14 for FT1 being non empty RelStr, FT2 being filled non empty RelStr, n being Element of NAT, f being Function of FT1, FT2 st f is_continuous 0 holds f is_continuous n; theorem :: FINTOPO4:15 for FT1 being non empty RelStr, FT2 being filled non empty RelStr, n0,n being Element of NAT, f being Function of FT1, FT2 st f is_continuous n0 & n0<=n holds f is_continuous n; theorem :: FINTOPO4:16 for FT1,FT2 being non empty RelStr, A being Subset of FT1,B being Subset of FT2, f being Function of FT1, FT2 st f is_continuous 0 & B=f.:A holds f.:(A^b) c= B^b; theorem :: FINTOPO4:17 for FT1,FT2 being non empty RelStr,A being Subset of FT1, B being Subset of FT2, f being Function of FT1, FT2 st A is connected & f is_continuous 0 & B=f.:A holds B is connected; ::1 dimensional linear FT_Str definition let n be Nat; func Nbdl1 n -> Relation of Seg n means :: 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)}; end; definition let n be Nat; assume n>0; func FTSL1 n -> non empty RelStr equals :: FINTOPO4:def 4 RelStr(# Seg n,Nbdl1 n #); end; theorem :: FINTOPO4:18 for n being Nat st n>0 holds FTSL1 n is filled; theorem :: FINTOPO4:19 for n being Nat st n>0 holds FTSL1 n is symmetric; ::1 dimensional cyclic FT_Str definition let n be Nat; func Nbdc1 n -> Relation of Seg n means :: FINTOPO4:def 5 for i being Element of NAT st i in Seg n holds (10; func FTSC1 n -> non empty RelStr equals :: FINTOPO4:def 6 RelStr(# Seg n,Nbdc1 n #); end; theorem :: FINTOPO4:20 for n being Element of NAT st n>0 holds FTSC1 n is filled; theorem :: FINTOPO4:21 for n being Element of NAT st n>0 holds FTSC1 n is symmetric;