begin
:: deftheorem defines ^d FINTOPO3:def 1 :
for T being non empty RelStr
for A being Subset of T holds A ^d = { x where x is Element of T : for y being Element of T st y in A ` holds
not x in U_FT y } ;
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem Th12:
:: deftheorem Def2 defines Fcl FINTOPO3:def 2 :
for T being non empty RelStr
for A being Subset of T
for b3 being Function of NAT,(bool the carrier of T) holds
( b3 = Fcl A iff ( ( for n being Element of NAT
for B being Subset of T st B = b3 . n holds
b3 . (n + 1) = B ^b ) & b3 . 0 = A ) );
:: deftheorem defines Fcl FINTOPO3:def 3 :
for T being non empty RelStr
for A being Subset of T
for n being Nat holds Fcl (A,n) = (Fcl A) . n;
:: deftheorem Def4 defines Fint FINTOPO3:def 4 :
for T being non empty RelStr
for A being Subset of T
for b3 being Function of NAT,(bool the carrier of T) holds
( b3 = Fint A iff ( ( for n being Element of NAT
for B being Subset of T st B = b3 . n holds
b3 . (n + 1) = B ^i ) & b3 . 0 = A ) );
:: deftheorem defines Fint FINTOPO3:def 5 :
for T being non empty RelStr
for A being Subset of T
for n being Nat holds Fint (A,n) = (Fint A) . n;
theorem
theorem
theorem Th15:
theorem
theorem Th17:
theorem
theorem
theorem Th20:
theorem
theorem Th22:
theorem
theorem
theorem
theorem
theorem Th27:
theorem Th28:
theorem
theorem
:: deftheorem Def6 defines Finf FINTOPO3:def 6 :
for T being non empty RelStr
for A being Subset of T
for b3 being Function of NAT,(bool the carrier of T) holds
( b3 = Finf A iff ( ( for n being Element of NAT
for B being Subset of T st B = b3 . n holds
b3 . (n + 1) = B ^f ) & b3 . 0 = A ) );
:: deftheorem defines Finf FINTOPO3:def 7 :
for T being non empty RelStr
for A being Subset of T
for n being Nat holds Finf (A,n) = (Finf A) . n;
:: deftheorem Def8 defines Fdfl FINTOPO3:def 8 :
for T being non empty RelStr
for A being Subset of T
for b3 being Function of NAT,(bool the carrier of T) holds
( b3 = Fdfl A iff ( ( for n being Element of NAT
for B being Subset of T st B = b3 . n holds
b3 . (n + 1) = B ^d ) & b3 . 0 = A ) );
:: deftheorem defines Fdfl FINTOPO3:def 9 :
for T being non empty RelStr
for A being Subset of T
for n being Nat holds Fdfl (A,n) = (Fdfl A) . n;
theorem
theorem
theorem Th33:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th40:
theorem
theorem Th42:
theorem
theorem
theorem Th45:
theorem
:: deftheorem defines U_FT FINTOPO3:def 10 :
for T being non empty RelStr
for n being Nat
for x being Element of T holds U_FT (x,n) = Finf ((U_FT x),n);
theorem
theorem
:: deftheorem defines are_mutually_symmetric FINTOPO3:def 11 :
for S, T being non empty RelStr holds
( S,T are_mutually_symmetric iff ( the carrier of S = the carrier of T & ( for x being Element of S
for y being Element of T holds
( y in U_FT x iff x in U_FT y ) ) ) );