begin
theorem Th1:
theorem
:: 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 & h is onto & ( for x being Element of FT1 holds h .: (U_FT x) = Im ( the InternalRel of FT2,(h . x)) ) ) );
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 :
for n, m being Element of NAT holds FTSL2 (n,m) = RelStr(# [:(Seg n),(Seg m):],(Nbdl2 (n,m)) #);
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 :
for n, m being Element of NAT holds FTSS2 (n,m) = RelStr(# [:(Seg n),(Seg m):],(Nbds2 (n,m)) #);
theorem
theorem
theorem