:: 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-2012 Association of Mizar Users


begin

theorem Th1: :: FINTOPO5:1
for X being set
for Y being non empty set
for f being Function of X,Y
for A being Subset of X st f is one-to-one holds
(f ") .: (f .: A) = A
proofend;

theorem :: FINTOPO5:2
for n being Element of NAT holds
( n > 0 iff Seg n <> {} ) ;

definition
let FT1, FT2 be RelStr ;
let h be Function of FT1,FT2;
attrh is being_homeomorphism  means :Def1: :: FINTOPO5:def 1
( h is one-to-one &amp; h is onto &amp; ( for x being Element of FT1 holds h .: (U_FT x) = Im ( the InternalRel of FT2,(h . x)) ) );
end;

:: deftheorem Def1 defines being_homeomorphism FINTOPO5:def_1_:_
 for FT1, FT2 being RelStr
for h being Function of FT1,FT2 holds
( h is being_homeomorphism iff ( h is one-to-one &amp; h is onto &amp; ( for x being Element of FT1 holds h .: (U_FT x) = Im ( the InternalRel of FT2,(h . x)) ) ) );

theorem Th3: :: FINTOPO5:3
for FT1, FT2 being non empty RelStr
for h being Function of FT1,FT2 st h is being_homeomorphism holds
ex g being Function of FT2,FT1 st
( g = h " &amp; g is being_homeomorphism )
proofend;

theorem Th4: :: FINTOPO5:4
for FT1, FT2 being non empty RelStr
for h being Function of FT1,FT2
for n being Element of NAT
for x being Element of FT1
for y being Element of FT2 st h is being_homeomorphism &amp; 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) )
proofend;

theorem :: FINTOPO5:5
for FT1, FT2 being non empty RelStr
for h being Function of FT1,FT2
for n being Element of NAT
for x being Element of FT1
for y being Element of FT2 st h is being_homeomorphism &amp; 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) )
proofend;

theorem :: FINTOPO5:6
for n being non zero Element of NAT
for 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)
proofend;

theorem Th7: :: FINTOPO5:7
for T being non empty RelStr
for p being Element of T
for k being Element of NAT st T is filled holds
U_FT (p,k) c= U_FT (p,(k + 1))
proofend;

theorem Th8: :: FINTOPO5:8
for T being non empty RelStr
for p being Element of T
for k being Element of NAT st T is filled holds
U_FT (p,0) c= U_FT (p,k)
proofend;

theorem Th9: :: FINTOPO5:9
for n being non zero Nat
for jn, j, k being Nat
for p being Element of (FTSL1 n) st p = jn holds
( j in U_FT (p,k) iff ( j in Seg n &amp; abs (jn - j) <= k + 1 ) )
proofend;

:: Fixed Point Theorem
theorem :: FINTOPO5:10
for kc, km being Element of NAT
for n being non zero Element of NAT
for f being Function of (FTSL1 n),(FTSL1 n) st f is_continuous kc &amp; km = [/(kc / 2)\] holds
ex p being Element of (FTSL1 n) st f . p in U_FT (p,km)
proofend;

definition
let A, B be set ;
let R be Relation of A,B;
let x be set ;
:: original:Im
redefine func Im (R,x) ->  Subset of B;
coherence
 Im (R,x) is Subset of B
proofend;
end;

:: 2-dimensional linear FT_Str
definition
let n, m be Element of NAT ;
func Nbdl2 (n,m) ->  Relation of [:(Seg n),(Seg m):] means :Def2: :: FINTOPO5:def 2
 for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (it,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):];
existence
 ex b1 being Relation of [:(Seg n),(Seg m):] st
for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (b1,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):]
proofend;
uniqueness
 for b1, b2 being Relation of [:(Seg n),(Seg m):] st ( for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (b1,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] ) &amp; ( for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (b2,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines Nbdl2 FINTOPO5:def_2_:_
 for n, m being Element of NAT
for b3 being Relation of [:(Seg n),(Seg m):] holds
( b3 = Nbdl2 (n,m) iff for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (b3,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] );

definition
let n, m be Element of NAT ;
func FTSL2 (n,m) ->  strict RelStr  equals :: FINTOPO5:def 3
 RelStr(# [:(Seg n),(Seg m):],(Nbdl2 (n,m)) #);
coherence
 RelStr(# [:(Seg n),(Seg m):],(Nbdl2 (n,m)) #) is strict RelStr ;
end;

:: deftheorem  defines FTSL2 FINTOPO5:def_3_:_
 for n, m being Element of NAT holds FTSL2 (n,m) = RelStr(# [:(Seg n),(Seg m):],(Nbdl2 (n,m)) #);

registration
let n, m be non zero Element of NAT ;
cluster FTSL2 (n,m) ->  non empty strict ;
coherence
 not FTSL2 (n,m) is empty ;
end;

theorem :: FINTOPO5:11
for n, m being non zero Element of NAT holds FTSL2 (n,m) is filled
proofend;

theorem :: FINTOPO5:12
for n, m being non zero Element of NAT holds FTSL2 (n,m) is symmetric
proofend;

theorem :: FINTOPO5:13
for n being non zero Element of NAT ex h being Function of (FTSL2 (n,1)),(FTSL1 n) st h is being_homeomorphism
proofend;

:: 2-dimensional small FT_Str
definition
let n, m be Element of NAT ;
func Nbds2 (n,m) ->  Relation of [:(Seg n),(Seg m):] means :Def4: :: FINTOPO5:def 4
 for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (it,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:];
existence
 ex b1 being Relation of [:(Seg n),(Seg m):] st
for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (b1,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:]
proofend;
uniqueness
 for b1, b2 being Relation of [:(Seg n),(Seg m):] st ( for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (b1,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] ) &amp; ( for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (b2,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines Nbds2 FINTOPO5:def_4_:_
 for n, m being Element of NAT
for b3 being Relation of [:(Seg n),(Seg m):] holds
( b3 = Nbds2 (n,m) iff for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (b3,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] );

definition
let n, m be Element of NAT ;
func FTSS2 (n,m) ->  strict RelStr  equals :: FINTOPO5:def 5
 RelStr(# [:(Seg n),(Seg m):],(Nbds2 (n,m)) #);
coherence
 RelStr(# [:(Seg n),(Seg m):],(Nbds2 (n,m)) #) is strict RelStr ;
end;

:: deftheorem  defines FTSS2 FINTOPO5:def_5_:_
 for n, m being Element of NAT holds FTSS2 (n,m) = RelStr(# [:(Seg n),(Seg m):],(Nbds2 (n,m)) #);

registration
let n, m be non zero Element of NAT ;
cluster FTSS2 (n,m) ->  non empty strict ;
coherence
 not FTSS2 (n,m) is empty ;
end;

theorem :: FINTOPO5:14
for n, m being non zero Element of NAT holds FTSS2 (n,m) is filled
proofend;

theorem :: FINTOPO5:15
for n, m being non zero Element of NAT holds FTSS2 (n,m) is symmetric
proofend;

theorem :: FINTOPO5:16
for n being non zero Element of NAT ex h being Function of (FTSS2 (n,1)),(FTSL1 n) st h is being_homeomorphism
proofend;