:: FINTOPO3 semantic presentation

definition

let T be non empty FT_Space_Str ;
let A be Subset of T;
func A ^d -> Subset of T equals :: FINTOPO3:def 1
{ x where x is Element of T : for y being Element of T st y in A ` holds
not x in U_FT y } ;
coherence

proof end;

end;

:: deftheorem defines ^d FINTOPO3:def 1 :

theorem Th1: :: FINTOPO3:1

for T being non empty FT_Space_Str
for A being Subset of T st T is filled holds
A c= A ^f

proof end;

theorem Th2: :: FINTOPO3:2

for T being non empty FT_Space_Str
for A being Subset of T
for x being Element of T holds
( x in A ^d iff for y being Element of T st y in A ` holds
not x in U_FT y )

proof end;

theorem Th3: :: FINTOPO3:3

for T being non empty FT_Space_Str
for A being Subset of T st T is filled holds
A ^d c= A

proof end;

theorem Th4: :: FINTOPO3:4

for T being non empty FT_Space_Str
for A being Subset of T holds A ^d = ((A ` ) ^f ) `

proof end;

theorem Th5: :: FINTOPO3:5

for T being non empty FT_Space_Str
for A, B being Subset of T st A c= B holds
A ^f c= B ^f

proof end;

theorem Th6: :: FINTOPO3:6

for T being non empty FT_Space_Str
for A, B being Subset of T st A c= B holds
A ^d c= B ^d

proof end;

theorem :: FINTOPO3:7

for T being non empty FT_Space_Str
for A, B being Subset of T holds (A /\ B) ^b c= (A ^b ) /\ (B ^b )

proof end;

theorem Th8: :: FINTOPO3:8

for T being non empty FT_Space_Str
for A, B being Subset of T holds (A \/ B) ^b = (A ^b ) \/ (B ^b )

proof end;

theorem :: FINTOPO3:9

for T being non empty FT_Space_Str
for A, B being Subset of T holds (A ^i ) \/ (B ^i ) c= (A \/ B) ^i

proof end;

theorem Th10: :: FINTOPO3:10

for T being non empty FT_Space_Str
for A, B being Subset of T holds (A ^i ) /\ (B ^i ) = (A /\ B) ^i

proof end;

theorem Th11: :: FINTOPO3:11

for T being non empty FT_Space_Str
for A, B being Subset of T holds (A ^f ) \/ (B ^f ) = (A \/ B) ^f

proof end;

theorem Th12: :: FINTOPO3:12

for T being non empty FT_Space_Str
for A, B being Subset of T holds (A ^d ) /\ (B ^d ) = (A /\ B) ^d

proof end;

definition

let T be non empty FT_Space_Str ;
let A be Subset of T;
func Fcl A -> Function of NAT , bool the carrier of T means :Def2: :: FINTOPO3:def 2
( ( for n being Nat
for B being Subset of T st B = it . n holds
it . (n + 1) = B ^b ) & it . 0 = A );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Fcl FINTOPO3:def 2 :

definition

let T be non empty FT_Space_Str ;
let A be Subset of T;
let n be Nat;
func Fcl A,n -> Subset of T equals :: FINTOPO3:def 3
(Fcl A) . n;
coherence ;

end;

:: deftheorem defines Fcl FINTOPO3:def 3 :

definition

let T be non empty FT_Space_Str ;
let A be Subset of T;
func Fint A -> Function of NAT , bool the carrier of T means :Def4: :: FINTOPO3:def 4
( ( for n being Nat
for B being Subset of T st B = it . n holds
it . (n + 1) = B ^i ) & it . 0 = A );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Fint FINTOPO3:def 4 :

definition

let T be non empty FT_Space_Str ;
let A be Subset of T;
let n be Nat;
func Fint A,n -> Subset of T equals :: FINTOPO3:def 5
(Fint A) . n;
coherence ;

end;

:: deftheorem defines Fint FINTOPO3:def 5 :

theorem Th13: :: FINTOPO3:13

for T being non empty FT_Space_Str
for A being Subset of T
for n being Nat holds Fcl A,(n + 1) = (Fcl A,n) ^b by Def2;

theorem :: FINTOPO3:14

for T being non empty FT_Space_Str
for A being Subset of T holds Fcl A,0 = A by Def2;

theorem Th15: :: FINTOPO3:15

for T being non empty FT_Space_Str
for A being Subset of T holds Fcl A,1 = A ^b

proof end;

theorem :: FINTOPO3:16

for T being non empty FT_Space_Str
for A being Subset of T holds Fcl A,2 = (A ^b ) ^b

proof end;

theorem Th17: :: FINTOPO3:17

for T being non empty FT_Space_Str
for A, B being Subset of T
for n being Nat holds Fcl (A \/ B),n = (Fcl A,n) \/ (Fcl B,n)

proof end;

theorem Th18: :: FINTOPO3:18

for T being non empty FT_Space_Str
for A being Subset of T
for n being Nat holds Fint A,(n + 1) = (Fint A,n) ^i by Def4;

theorem :: FINTOPO3:19

for T being non empty FT_Space_Str
for A being Subset of T holds Fint A,0 = A by Def4;

theorem Th20: :: FINTOPO3:20

for T being non empty FT_Space_Str
for A being Subset of T holds Fint A,1 = A ^i

proof end;

theorem :: FINTOPO3:21

for T being non empty FT_Space_Str
for A being Subset of T holds Fint A,2 = (A ^i ) ^i

proof end;

theorem Th22: :: FINTOPO3:22

for T being non empty FT_Space_Str
for A, B being Subset of T
for n being Nat holds Fint (A /\ B),n = (Fint A,n) /\ (Fint B,n)

proof end;

theorem :: FINTOPO3:23

for T being non empty FT_Space_Str
for A being Subset of T st T is filled holds
for n being Nat holds A c= Fcl A,n

proof end;

theorem :: FINTOPO3:24

for T being non empty FT_Space_Str
for A being Subset of T st T is filled holds
for n being Nat holds Fint A,n c= A

proof end;

theorem :: FINTOPO3:25

for T being non empty FT_Space_Str
for A being Subset of T st T is filled holds
for n being Nat holds Fcl A,n c= Fcl A,(n + 1)

proof end;

theorem :: FINTOPO3:26

for T being non empty FT_Space_Str
for A being Subset of T st T is filled holds
for n being Nat holds Fint A,(n + 1) c= Fint A,n

proof end;

theorem Th27: :: FINTOPO3:27

for T being non empty FT_Space_Str
for A being Subset of T
for n being Nat holds (Fint (A ` ),n) ` = Fcl A,n

proof end;

theorem Th28: :: FINTOPO3:28

for T being non empty FT_Space_Str
for A being Subset of T
for n being Nat holds (Fcl (A ` ),n) ` = Fint A,n

proof end;

theorem :: FINTOPO3:29

for T being non empty FT_Space_Str
for A, B being Subset of T
for n being Nat holds (Fcl A,n) \/ (Fcl B,n) = (Fint ((A \/ B) ` ),n) `

proof end;

theorem :: FINTOPO3:30

for T being non empty FT_Space_Str
for A, B being Subset of T
for n being Nat holds (Fint A,n) /\ (Fint B,n) = (Fcl ((A /\ B) ` ),n) `

proof end;

definition

let T be non empty FT_Space_Str ;
let A be Subset of T;
func Finf A -> Function of NAT , bool the carrier of T means :Def6: :: FINTOPO3:def 6
( ( for n being Nat
for B being Subset of T st B = it . n holds
it . (n + 1) = B ^f ) & it . 0 = A );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Finf FINTOPO3:def 6 :

definition

let T be non empty FT_Space_Str ;
let A be Subset of T;
let n be Nat;
func Finf A,n -> Subset of T equals :: FINTOPO3:def 7
(Finf A) . n;
coherence ;

end;

:: deftheorem defines Finf FINTOPO3:def 7 :

definition

let T be non empty FT_Space_Str ;
let A be Subset of T;
func Fdfl A -> Function of NAT , bool the carrier of T means :Def8: :: FINTOPO3:def 8
( ( for n being Nat
for B being Subset of T st B = it . n holds
it . (n + 1) = B ^d ) & it . 0 = A );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines Fdfl FINTOPO3:def 8 :

definition

let T be non empty FT_Space_Str ;
let A be Subset of T;
let n be Nat;
func Fdfl A,n -> Subset of T equals :: FINTOPO3:def 9
(Fdfl A) . n;
coherence ;

end;

:: deftheorem defines Fdfl FINTOPO3:def 9 :

theorem Th31: :: FINTOPO3:31

for T being non empty FT_Space_Str
for A being Subset of T
for n being Nat holds Finf A,(n + 1) = (Finf A,n) ^f by Def6;

theorem Th32: :: FINTOPO3:32

for T being non empty FT_Space_Str
for A being Subset of T holds Finf A,0 = A by Def6;

theorem Th33: :: FINTOPO3:33

for T being non empty FT_Space_Str
for A being Subset of T holds Finf A,1 = A ^f

proof end;

theorem :: FINTOPO3:34

for T being non empty FT_Space_Str
for A being Subset of T holds Finf A,2 = (A ^f ) ^f

proof end;

theorem :: FINTOPO3:35

for T being non empty FT_Space_Str
for A, B being Subset of T
for n being Nat holds Finf (A \/ B),n = (Finf A,n) \/ (Finf B,n)

proof end;

theorem :: FINTOPO3:36

for T being non empty FT_Space_Str
for A being Subset of T st T is filled holds
for n being Nat holds A c= Finf A,n

proof end;

theorem :: FINTOPO3:37

for T being non empty FT_Space_Str
for A being Subset of T st T is filled holds
for n being Nat holds Finf A,n c= Finf A,(n + 1)

proof end;

theorem Th38: :: FINTOPO3:38

for T being non empty FT_Space_Str
for A being Subset of T
for n being Nat holds Fdfl A,(n + 1) = (Fdfl A,n) ^d by Def8;

theorem :: FINTOPO3:39

for T being non empty FT_Space_Str
for A being Subset of T holds Fdfl A,0 = A by Def8;

theorem Th40: :: FINTOPO3:40

for T being non empty FT_Space_Str
for A being Subset of T holds Fdfl A,1 = A ^d

proof end;

theorem :: FINTOPO3:41

for T being non empty FT_Space_Str
for A being Subset of T holds Fdfl A,2 = (A ^d ) ^d

proof end;

theorem Th42: :: FINTOPO3:42

for T being non empty FT_Space_Str
for A, B being Subset of T
for n being Nat holds Fdfl (A /\ B),n = (Fdfl A,n) /\ (Fdfl B,n)

proof end;

theorem :: FINTOPO3:43

for T being non empty FT_Space_Str
for A being Subset of T st T is filled holds
for n being Nat holds Fdfl A,n c= A

proof end;

theorem :: FINTOPO3:44

for T being non empty FT_Space_Str
for A being Subset of T st T is filled holds
for n being Nat holds Fdfl A,(n + 1) c= Fdfl A,n

proof end;

theorem Th45: :: FINTOPO3:45

for T being non empty FT_Space_Str
for A being Subset of T
for n being Nat holds Fdfl A,n = (Finf (A ` ),n) `

proof end;

theorem :: FINTOPO3:46

for T being non empty FT_Space_Str
for A, B being Subset of T
for n being Nat holds (Fdfl A,n) /\ (Fdfl B,n) = (Finf ((A /\ B) ` ),n) `

proof end;

definition

let T be non empty FT_Space_Str ;
let n be Nat;
let x be Element of T;
func U_FT x,n -> Subset of T equals :: FINTOPO3:def 10
Finf (U_FT x),n;
coherence ;

end;

:: deftheorem defines U_FT FINTOPO3:def 10 :

theorem :: FINTOPO3:47

for T being non empty FT_Space_Str
for x being Element of T holds U_FT x,0 = U_FT x by Th32;

theorem :: FINTOPO3:48

for T being non empty FT_Space_Str
for x being Element of T
for n being Nat holds U_FT x,(n + 1) = (U_FT x,n) ^f by Th31;

definition

let S, T be non empty FT_Space_Str ;
pred S,T are_mutually_symmetric means :: FINTOPO3:def 11
( the carrier of S = the carrier of T & ( for x, y being set st x in the carrier of S & y in the carrier of T holds
( y in the Nbd of S . x iff x in the Nbd of T . y ) ) );
symmetry ;

end;

:: deftheorem defines are_mutually_symmetric FINTOPO3:def 11 :