:: Homeomorphism between Finite Topological Spaces, Two-Dimensional Lattice :: Spaces and a Fixed Point Theorem :: by Masami Tanaka , Hiroshi Imura and Yatsuka Nakamura :: :: Received July 6, 2005 :: Copyright (c) 2005-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, FUNCT_1, SUBSET_1, RELAT_1, XXREAL_0, CARD_1, FINSEQ_1, ORDERS_2, TOPS_2, FUNCT_2, FIN_TOPO, STRUCT_0, ARYTM_3, EQREL_1, XCMPLX_0, FINTOPO4, NAT_1, ARYTM_1, TARSKI, COMPLEX1, INT_1, ZFMISC_1, RELAT_2, FINTOPO5; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, RELAT_1, FUNCT_1, RELSET_1, EQREL_1, FUNCT_2, FINSEQ_1, STRUCT_0, FIN_TOPO, FINTOPO3, ENUMSET1, ORDERS_2, FINTOPO4, COMPLEX1, INT_1; constructors ENUMSET1, REAL_1, NAT_1, EQREL_1, FIN_TOPO, FINTOPO3, FINTOPO4, NAT_D, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, STRUCT_0, FIN_TOPO, ORDINAL1, FINSEQ_1, CARD_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin theorem :: FINTOPO5:1 for X being set, Y being non empty set, f being Function of X,Y, A being Subset of X st f is one-to-one holds f".:(f.:A)=A; theorem :: FINTOPO5:2 for n being Nat holds n>0 iff Seg n<>{}; definition let FT1,FT2 be RelStr, h be Function of FT1, FT2; attr h is being_homeomorphism means :: FINTOPO5:def 1 h is one-to-one onto & for x being Element of FT1 holds h.:U_FT x = Im(the InternalRel of FT2,h.x); end; theorem :: FINTOPO5:3 for FT1,FT2 being non empty RelStr, h being Function of FT1, FT2 st h is being_homeomorphism ex g being Function of FT2, FT1 st g=h" & g is being_homeomorphism; theorem :: FINTOPO5:4 for FT1,FT2 being non empty RelStr, h being Function of FT1, FT2, n being Nat, x being Element of FT1, y being Element of FT2 st h is being_homeomorphism & y=h.x holds for z being Element of FT1 holds z in U_FT(x, n) iff h.z in U_FT(y,n); theorem :: FINTOPO5:5 for FT1,FT2 being non empty RelStr, h being Function of FT1, FT2, n being Nat,x being Element of FT1,y being Element of FT2 st h is being_homeomorphism & y=h.x holds for v being Element of FT2 holds h".v in U_FT (x,n) iff v in U_FT(y,n); theorem :: FINTOPO5:6 for n being non zero Nat, f being Function of FTSL1 n, FTSL1 n st f is_continuous 0 holds ex p being Element of FTSL1 n st f.p in U_FT (p,0); theorem :: FINTOPO5:7 for T being non empty RelStr, p being Element of T, k being Nat st T is filled holds U_FT(p,k) c= U_FT(p,k+1); theorem :: FINTOPO5:8 for T being non empty RelStr, p being Element of T, k being Nat st T is filled holds U_FT(p,0) c= U_FT(p,k); theorem :: FINTOPO5:9 for n being non zero Nat, jn,j,k being Nat, p being Element of FTSL1 n st p=jn holds j in U_FT(p,k) iff j in Seg n & |.jn-j.|<= k+1; :: Fixed Point Theorem theorem :: FINTOPO5:10 for kc,km being Nat, n being non zero Nat, f being Function of FTSL1 n, FTSL1 n st f is_continuous kc & km=[/ (kc/2) \] holds ex p being Element of FTSL1 n st f.p in U_FT(p,km); definition let A,B be set; let R be Relation of A,B, x be set; redefine func Im(R,x) -> Subset of B; end; :: 2-dimensional linear FT_Str definition let n,m be Nat; func Nbdl2(n,m) -> Relation of [:Seg n, Seg m:] means :: FINTOPO5:def 2 for x being set st x in [:Seg n, Seg m:] holds for i,j being Nat st x=[i,j] holds Im (it,x) = [:Im(Nbdl1 n,i), Im(Nbdl1 m,j):]; end; definition let n,m be Nat; func FTSL2(n,m) -> strict RelStr equals :: FINTOPO5:def 3 RelStr(# [:Seg n, Seg m:], Nbdl2(n,m ) #); end; registration let n,m be non zero Nat; cluster FTSL2(n,m) -> non empty; end; theorem :: FINTOPO5:11 for n,m being non zero Nat holds FTSL2(n,m) is filled; theorem :: FINTOPO5:12 for n,m being non zero Nat holds FTSL2(n,m) is symmetric; theorem :: FINTOPO5:13 for n being non zero Nat ex h being Function of FTSL2(n,1), FTSL1 n st h is being_homeomorphism; :: 2-dimensional small FT_Str definition let n,m be Nat; func Nbds2(n,m) -> Relation of [:Seg n, Seg m:] means :: FINTOPO5:def 4 for x being set st x in [:Seg n, Seg m:] holds for i,j being Nat st x=[i,j] holds Im (it,x) = [:{i}, Im(Nbdl1 m,j):] \/ [:Im(Nbdl1 n,i),{j}:]; end; definition let n,m be Nat; func FTSS2(n,m) -> strict RelStr equals :: FINTOPO5:def 5 RelStr(# [:Seg n, Seg m:], Nbds2(n,m ) #); end; registration let n,m be non zero Nat; cluster FTSS2(n,m) -> non empty; end; theorem :: FINTOPO5:14 for n,m being non zero Nat holds FTSS2(n,m) is filled; theorem :: FINTOPO5:15 for n,m being non zero Nat holds FTSS2(n,m) is symmetric; theorem :: FINTOPO5:16 for n being non zero Nat ex h being Function of FTSS2(n,1), FTSL1 n st h is being_homeomorphism;