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