:: Homeomorphism between Finite Topological Spaces, Two-Dimensional LatticeSpaces and a Fixed Point Theorem
:: by Masami Tanaka , Hiroshi Imura and Yatsuka Nakamura
::
:: Received July 6, 2005
:: Copyright (c) 2005 Association of Mizar Users
theorem Th1: :: FINTOPO5:1
theorem :: FINTOPO5:2
:: deftheorem Def1 defines being_homeomorphism FINTOPO5:def 1 :
theorem Th3: :: FINTOPO5:3
theorem Th4: :: FINTOPO5:4
theorem :: FINTOPO5:5
theorem :: FINTOPO5:6
theorem Th7: :: FINTOPO5:7
theorem Th8: :: FINTOPO5:8
theorem Th9: :: FINTOPO5:9
theorem :: FINTOPO5:10
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):]
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):] ) & ( 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
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):] );
:: deftheorem defines FTSL2 FINTOPO5:def 3 :
theorem :: FINTOPO5:11
theorem :: FINTOPO5:12
theorem :: FINTOPO5:13
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}:]
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}:] ) & ( 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
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}:] );
:: deftheorem defines FTSS2 FINTOPO5:def 5 :
theorem :: FINTOPO5:14
theorem :: FINTOPO5:15
theorem :: FINTOPO5:16