begin
theorem Th1:
theorem
:: deftheorem Def1 defines being_homeomorphism FINTOPO5:def 1 :
theorem Th3:
theorem Th4:
theorem
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem
definition
let n,
m be
Element of
NAT ;
func Nbdl2 n,
m -> Relation of
[:(Seg n),(Seg m):] means :
Def2:
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
theorem
theorem
definition
let n,
m be
Element of
NAT ;
func Nbds2 n,
m -> Relation of
[:(Seg n),(Seg m):] means :
Def4:
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
theorem
theorem