:: FINTOPO5 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: FINTOPO5:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: FINTOPO5:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds
( n > 0 iff Seg n <> {} )
proof end;

definition
let FT1, FT2 be FT_Space_Str ;
let h be Function of FT1,FT2;
pred h is_homeomorphism means :Def1: :: FINTOPO5:def 1
( h is one-to-one & h is onto & ( for x being Element of FT1 holds h .: (the Nbd of FT1 . x) = the Nbd of FT2 . (h . x) ) );
end;

:: deftheorem Def1 defines is_homeomorphism FINTOPO5:def 1 :
for FT1, FT2 being FT_Space_Str
for h being Function of FT1,FT2 holds
( h is_homeomorphism iff ( h is one-to-one & h is onto & ( for x being Element of FT1 holds h .: (the Nbd of FT1 . x) = the Nbd of FT2 . (h . x) ) ) );

theorem Th3: :: FINTOPO5:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT1, FT2 being non empty FT_Space_Str
for h being Function of FT1,FT2 st h is_homeomorphism holds
ex g being Function of FT2,FT1 st
( g = h " & g is_homeomorphism )
proof end;

theorem Th4: :: FINTOPO5:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT1, FT2 being non empty FT_Space_Str
for h being Function of FT1,FT2
for n being Nat
for x being Element of FT1
for y being Element of FT2 st h is_homeomorphism & 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 )
proof end;

theorem :: FINTOPO5:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT1, FT2 being non empty FT_Space_Str
for h being Function of FT1,FT2
for n being Nat
for x being Element of FT1
for y being Element of FT2 st h is_homeomorphism & 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 )
proof end;

theorem :: FINTOPO5:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non zero 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
proof end;

theorem Th7: :: FINTOPO5:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty FT_Space_Str
for p being Element of T
for k being Nat st T is filled holds
U_FT p,k c= U_FT p,(k + 1)
proof end;

theorem Th8: :: FINTOPO5:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty FT_Space_Str
for p being Element of T
for k being Nat st T is filled holds
U_FT p,0 c= U_FT p,k
proof end;

theorem Th9: :: FINTOPO5:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & abs (jn - j) <= k + 1 ) )
proof end;

theorem :: FINTOPO5:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for kc, km being Nat
for n being non zero Nat
for f being Function of (FTSL1 n),(FTSL1 n) st f is_continuous kc & km = [/(kc / 2)\] holds
ex p being Element of (FTSL1 n) st f . p in U_FT p,km
proof end;

definition
let n, m be Nat;
func Nbdl2 n,m -> Function of [:(Seg n),(Seg m):], bool [:(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 Nat st x = [i,j] holds
it . x = [:((Nbdl1 n) . i),((Nbdl1 m) . j):];
existence
ex b1 being Function of [:(Seg n),(Seg m):], bool [:(Seg n),(Seg m):] st
for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Nat st x = [i,j] holds
b1 . x = [:((Nbdl1 n) . i),((Nbdl1 m) . j):]
proof end;
uniqueness
for b1, b2 being Function of [:(Seg n),(Seg m):], bool [:(Seg n),(Seg m):] st ( for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Nat st x = [i,j] holds
b1 . x = [:((Nbdl1 n) . i),((Nbdl1 m) . j):] ) & ( for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Nat st x = [i,j] holds
b2 . x = [:((Nbdl1 n) . i),((Nbdl1 m) . j):] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Nbdl2 FINTOPO5:def 2 :
for n, m being Nat
for b3 being Function of [:(Seg n),(Seg m):], bool [:(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 Nat st x = [i,j] holds
b3 . x = [:((Nbdl1 n) . i),((Nbdl1 m) . j):] );

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

:: deftheorem defines FTSL2 FINTOPO5:def 3 :
for n, m being Nat holds FTSL2 n,m = FT_Space_Str(# [:(Seg n),(Seg m):],(Nbdl2 n,m) #);

registration
let n, m be non zero Nat;
cluster FTSL2 n,m -> non empty strict ;
coherence
not FTSL2 n,m is empty
proof end;
end;

theorem :: FINTOPO5:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being non zero Nat holds FTSL2 n,m is filled
proof end;

theorem :: FINTOPO5:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being non zero Nat holds FTSL2 n,m is symmetric
proof end;

theorem :: FINTOPO5:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non zero Nat ex h being Function of (FTSL2 n,1),(FTSL1 n) st h is_homeomorphism
proof end;

definition
let n, m be Nat;
func Nbds2 n,m -> Function of [:(Seg n),(Seg m):], bool [:(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 Nat st x = [i,j] holds
it . x = [:{i},((Nbdl1 m) . j):] \/ [:((Nbdl1 n) . i),{j}:];
existence
ex b1 being Function of [:(Seg n),(Seg m):], bool [:(Seg n),(Seg m):] st
for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Nat st x = [i,j] holds
b1 . x = [:{i},((Nbdl1 m) . j):] \/ [:((Nbdl1 n) . i),{j}:]
proof end;
uniqueness
for b1, b2 being Function of [:(Seg n),(Seg m):], bool [:(Seg n),(Seg m):] st ( for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Nat st x = [i,j] holds
b1 . x = [:{i},((Nbdl1 m) . j):] \/ [:((Nbdl1 n) . i),{j}:] ) & ( for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Nat st x = [i,j] holds
b2 . x = [:{i},((Nbdl1 m) . j):] \/ [:((Nbdl1 n) . i),{j}:] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Nbds2 FINTOPO5:def 4 :
for n, m being Nat
for b3 being Function of [:(Seg n),(Seg m):], bool [:(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 Nat st x = [i,j] holds
b3 . x = [:{i},((Nbdl1 m) . j):] \/ [:((Nbdl1 n) . i),{j}:] );

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

:: deftheorem defines FTSS2 FINTOPO5:def 5 :
for n, m being Nat holds FTSS2 n,m = FT_Space_Str(# [:(Seg n),(Seg m):],(Nbds2 n,m) #);

registration
let n, m be non zero Nat;
cluster FTSS2 n,m -> non empty strict ;
coherence
not FTSS2 n,m is empty
proof end;
end;

theorem :: FINTOPO5:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being non zero Nat holds FTSS2 n,m is filled
proof end;

theorem :: FINTOPO5:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being non zero Nat holds FTSS2 n,m is symmetric
proof end;

theorem :: FINTOPO5:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non zero Nat ex h being Function of (FTSS2 n,1),(FTSL1 n) st h is_homeomorphism
proof end;