:: FINTOPO3 semantic presentation

definition

let c₁ be non empty FT_Space_Str ;
let c₂ be Subset of c₁;
func c₂ ^d -> Subset of a₁ equals :: FINTOPO3:def 1
{ b₁ where B is Element of a₁ : for b₁ being Element of a₁ st b₂ in a₂ ` holds
not b₁ in U_FT b₂ } ;
coherence

proof end;

end;

:: deftheorem Def1 defines ^d FINTOPO3:def 1 :

theorem Th1: :: FINTOPO3:1

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ st b₁ is filled holds
b₂ c= b₂ ^f

proof end;

theorem Th2: :: FINTOPO3:2

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds
( b₃ in b₂ ^d iff for b₄ being Element of b₁ st b₄ in b₂ ` holds
not b₃ in U_FT b₄ )

proof end;

theorem Th3: :: FINTOPO3:3

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ st b₁ is filled holds
b₂ ^d c= b₂

proof end;

theorem Th4: :: FINTOPO3:4

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ holds b₂ ^d = ((b₂ ` ) ^f ) `

proof end;

theorem Th5: :: FINTOPO3:5

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
b₂ ^f c= b₃ ^f

proof end;

theorem Th6: :: FINTOPO3:6

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
b₂ ^d c= b₃ ^d

proof end;

theorem Th7: :: FINTOPO3:7

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Subset of b₁ holds (b₂ /\ b₃) ^b c= (b₂ ^b ) /\ (b₃ ^b )

proof end;

theorem Th8: :: FINTOPO3:8

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Subset of b₁ holds (b₂ \/ b₃) ^b = (b₂ ^b ) \/ (b₃ ^b )

proof end;

theorem Th9: :: FINTOPO3:9

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Subset of b₁ holds (b₂ ^i ) \/ (b₃ ^i ) c= (b₂ \/ b₃) ^i

proof end;

theorem Th10: :: FINTOPO3:10

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Subset of b₁ holds (b₂ ^i ) /\ (b₃ ^i ) = (b₂ /\ b₃) ^i

proof end;

theorem Th11: :: FINTOPO3:11

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Subset of b₁ holds (b₂ ^f ) \/ (b₃ ^f ) = (b₂ \/ b₃) ^f

proof end;

theorem Th12: :: FINTOPO3:12

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Subset of b₁ holds (b₂ ^d ) /\ (b₃ ^d ) = (b₂ /\ b₃) ^d

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Fcl FINTOPO3:def 2 :

definition

let c₁ be non empty FT_Space_Str ;
let c₂ be Subset of c₁;
let c₃ be Nat;
func Fcl c₂,c₃ -> Subset of a₁ equals :: FINTOPO3:def 3
(Fcl a₂) . a₃;
coherence ;

end;

:: deftheorem Def3 defines Fcl FINTOPO3:def 3 :

definition

let c₁ be non empty FT_Space_Str ;
let c₂ be Subset of c₁;
func Fint c₂ -> Function of NAT , bool the carrier of a₁ means :Def4: :: FINTOPO3:def 4
( ( for b₁ being Nat
for b₂ being Subset of a₁ st b₂ = a₃ . b₁ holds
a₃ . (b₁ + 1) = b₂ ^i ) & a₃ . 0 = a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Fint FINTOPO3:def 4 :

definition

let c₁ be non empty FT_Space_Str ;
let c₂ be Subset of c₁;
let c₃ be Nat;
func Fint c₂,c₃ -> Subset of a₁ equals :: FINTOPO3:def 5
(Fint a₂) . a₃;
coherence ;

end;

:: deftheorem Def5 defines Fint FINTOPO3:def 5 :

theorem Th13: :: FINTOPO3:13

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁
for b₃ being Nat holds Fcl b₂,(b₃ + 1) = (Fcl b₂,b₃) ^b by Def2;

theorem Th14: :: FINTOPO3:14

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ holds Fcl b₂,0 = b₂ by Def2;

theorem Th15: :: FINTOPO3:15

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ holds Fcl b₂,1 = b₂ ^b

proof end;

theorem Th16: :: FINTOPO3:16

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

proof end;

theorem Th17: :: FINTOPO3:17

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Subset of b₁
for b₄ being Nat holds Fcl (b₂ \/ b₃),b₄ = (Fcl b₂,b₄) \/ (Fcl b₃,b₄)

proof end;

theorem Th18: :: FINTOPO3:18

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁
for b₃ being Nat holds Fint b₂,(b₃ + 1) = (Fint b₂,b₃) ^i by Def4;

theorem Th19: :: FINTOPO3:19

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ holds Fint b₂,0 = b₂ by Def4;

theorem Th20: :: FINTOPO3:20

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ holds Fint b₂,1 = b₂ ^i

proof end;

theorem Th21: :: FINTOPO3:21

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ holds Fint b₂,2 = (b₂ ^i ) ^i

proof end;

theorem Th22: :: FINTOPO3:22

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Subset of b₁
for b₄ being Nat holds Fint (b₂ /\ b₃),b₄ = (Fint b₂,b₄) /\ (Fint b₃,b₄)

proof end;

theorem Th23: :: FINTOPO3:23

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ st b₁ is filled holds
for b₃ being Nat holds b₂ c= Fcl b₂,b₃

proof end;

theorem Th24: :: FINTOPO3:24

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ st b₁ is filled holds
for b₃ being Nat holds Fint b₂,b₃ c= b₂

proof end;

theorem Th25: :: FINTOPO3:25

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ st b₁ is filled holds
for b₃ being Nat holds Fcl b₂,b₃ c= Fcl b₂,(b₃ + 1)

proof end;

theorem Th26: :: FINTOPO3:26

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ st b₁ is filled holds
for b₃ being Nat holds Fint b₂,(b₃ + 1) c= Fint b₂,b₃

proof end;

theorem Th27: :: FINTOPO3:27

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁
for b₃ being Nat holds (Fint (b₂ ` ),b₃) ` = Fcl b₂,b₃

proof end;

theorem Th28: :: FINTOPO3:28

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁
for b₃ being Nat holds (Fcl (b₂ ` ),b₃) ` = Fint b₂,b₃

proof end;

theorem Th29: :: FINTOPO3:29

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Subset of b₁
for b₄ being Nat holds (Fcl b₂,b₄) \/ (Fcl b₃,b₄) = (Fint ((b₂ \/ b₃) ` ),b₄) `

proof end;

theorem Th30: :: FINTOPO3:30

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Subset of b₁
for b₄ being Nat holds (Fint b₂,b₄) /\ (Fint b₃,b₄) = (Fcl ((b₂ /\ b₃) ` ),b₄) `

proof end;

definition

let c₁ be non empty FT_Space_Str ;
let c₂ be Subset of c₁;
func Finf c₂ -> Function of NAT , bool the carrier of a₁ means :Def6: :: FINTOPO3:def 6
( ( for b₁ being Nat
for b₂ being Subset of a₁ st b₂ = a₃ . b₁ holds
a₃ . (b₁ + 1) = b₂ ^f ) & a₃ . 0 = a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Finf FINTOPO3:def 6 :

definition

let c₁ be non empty FT_Space_Str ;
let c₂ be Subset of c₁;
let c₃ be Nat;
func Finf c₂,c₃ -> Subset of a₁ equals :: FINTOPO3:def 7
(Finf a₂) . a₃;
coherence ;

end;

:: deftheorem Def7 defines Finf FINTOPO3:def 7 :

definition

let c₁ be non empty FT_Space_Str ;
let c₂ be Subset of c₁;
func Fdfl c₂ -> Function of NAT , bool the carrier of a₁ means :Def8: :: FINTOPO3:def 8
( ( for b₁ being Nat
for b₂ being Subset of a₁ st b₂ = a₃ . b₁ holds
a₃ . (b₁ + 1) = b₂ ^d ) & a₃ . 0 = a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines Fdfl FINTOPO3:def 8 :

definition

let c₁ be non empty FT_Space_Str ;
let c₂ be Subset of c₁;
let c₃ be Nat;
func Fdfl c₂,c₃ -> Subset of a₁ equals :: FINTOPO3:def 9
(Fdfl a₂) . a₃;
coherence ;

end;

:: deftheorem Def9 defines Fdfl FINTOPO3:def 9 :

theorem Th31: :: FINTOPO3:31

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁
for b₃ being Nat holds Finf b₂,(b₃ + 1) = (Finf b₂,b₃) ^f by Def6;

theorem Th32: :: FINTOPO3:32

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ holds Finf b₂,0 = b₂ by Def6;

theorem Th33: :: FINTOPO3:33

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ holds Finf b₂,1 = b₂ ^f

proof end;

theorem Th34: :: FINTOPO3:34

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ holds Finf b₂,2 = (b₂ ^f ) ^f

proof end;

theorem Th35: :: FINTOPO3:35

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Subset of b₁
for b₄ being Nat holds Finf (b₂ \/ b₃),b₄ = (Finf b₂,b₄) \/ (Finf b₃,b₄)

proof end;

theorem Th36: :: FINTOPO3:36

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ st b₁ is filled holds
for b₃ being Nat holds b₂ c= Finf b₂,b₃

proof end;

theorem Th37: :: FINTOPO3:37

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ st b₁ is filled holds
for b₃ being Nat holds Finf b₂,b₃ c= Finf b₂,(b₃ + 1)

proof end;

theorem Th38: :: FINTOPO3:38

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁
for b₃ being Nat holds Fdfl b₂,(b₃ + 1) = (Fdfl b₂,b₃) ^d by Def8;

theorem Th39: :: FINTOPO3:39

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ holds Fdfl b₂,0 = b₂ by Def8;

theorem Th40: :: FINTOPO3:40

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ holds Fdfl b₂,1 = b₂ ^d

proof end;

theorem Th41: :: FINTOPO3:41

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ holds Fdfl b₂,2 = (b₂ ^d ) ^d

proof end;

theorem Th42: :: FINTOPO3:42

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Subset of b₁
for b₄ being Nat holds Fdfl (b₂ /\ b₃),b₄ = (Fdfl b₂,b₄) /\ (Fdfl b₃,b₄)

proof end;

theorem Th43: :: FINTOPO3:43

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ st b₁ is filled holds
for b₃ being Nat holds Fdfl b₂,b₃ c= b₂

proof end;

theorem Th44: :: FINTOPO3:44

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ st b₁ is filled holds
for b₃ being Nat holds Fdfl b₂,(b₃ + 1) c= Fdfl b₂,b₃

proof end;

theorem Th45: :: FINTOPO3:45

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁
for b₃ being Nat holds Fdfl b₂,b₃ = (Finf (b₂ ` ),b₃) `

proof end;

theorem Th46: :: FINTOPO3:46

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Subset of b₁
for b₄ being Nat holds (Fdfl b₂,b₄) /\ (Fdfl b₃,b₄) = (Finf ((b₂ /\ b₃) ` ),b₄) `

proof end;

definition

let c₁ be non empty FT_Space_Str ;
let c₂ be Nat;
let c₃ be Element of c₁;
func U_FT c₃,c₂ -> Subset of a₁ equals :: FINTOPO3:def 10
Finf (U_FT a₃),a₂;
coherence ;

end;

:: deftheorem Def10 defines U_FT FINTOPO3:def 10 :

theorem Th47: :: FINTOPO3:47

for b₁ being non empty FT_Space_Str
for b₂ being Element of b₁ holds U_FT b₂,0 = U_FT b₂ by Th32;

theorem Th48: :: FINTOPO3:48

for b₁ being non empty FT_Space_Str
for b₂ being Element of b₁
for b₃ being Nat holds U_FT b₂,(b₃ + 1) = (U_FT b₂,b₃) ^f by Th31;

definition

let c₁, c₂ be non empty FT_Space_Str ;
pred c₁,c₂ are_mutually_symmetric means :: FINTOPO3:def 11
( the carrier of a₁ = the carrier of a₂ & ( for b₁, b₂ being set st b₁ in the carrier of a₁ & b₂ in the carrier of a₂ holds
( b₂ in the Nbd of a₁ . b₁ iff b₁ in the Nbd of a₂ . b₂ ) ) );
symmetry ;

end;

:: deftheorem Def11 defines are_mutually_symmetric FINTOPO3:def 11 :