:: Some Set Series in Finite Topological Spaces. {F}undamental Conceptsfor Image Processing
:: by Masami Tanaka and Yatsuka Nakamura
::
:: Received January 26, 2004
:: Copyright (c) 2004 Association of Mizar Users

begin

definition

let T be non empty RelStr ;
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
{ x where x is Element of T : for y being Element of T st y in A ` holds
not x in U_FT y } is Subset of T

proof end;

end;

:: 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: :: FINTOPO3:1

for T being non empty RelStr
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 RelStr
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 RelStr
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 RelStr
for A being Subset of T holds A ^d = ((A ` ) ^f ) `

proof end;

theorem Th5: :: FINTOPO3:5

for T being non empty RelStr
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 RelStr
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 RelStr
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 RelStr
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 RelStr
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 RelStr
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 RelStr
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 RelStr
for A, B being Subset of T holds (A ^d ) /\ (B ^d ) = (A /\ B) ^d

proof end;

definition

let T be non empty RelStr ;
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 Element of NAT
for B being Subset of T st B = it . n holds
it . (n + 1) = B ^b ) & it . 0 = A );
existence
ex b₁ being Function of NAT ,(bool the carrier of T) st
( ( for n being Element of NAT
for B being Subset of T st B = b₁ . n holds
b₁ . (n + 1) = B ^b ) & b₁ . 0 = A )

proof end;

uniqueness
for b₁, b₂ being Function of NAT ,(bool the carrier of T) st ( for n being Element of NAT
for B being Subset of T st B = b₁ . n holds
b₁ . (n + 1) = B ^b ) & b₁ . 0 = A & ( for n being Element of NAT
for B being Subset of T st B = b₂ . n holds
b₂ . (n + 1) = B ^b ) & b₂ . 0 = A holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Fcl FINTOPO3:def 2 :

for T being non empty RelStr
for A being Subset of T
for b₃ being Function of NAT ,(bool the carrier of T) holds
( b₃ = Fcl A iff ( ( for n being Element of NAT
for B being Subset of T st B = b₃ . n holds
b₃ . (n + 1) = B ^b ) & b₃ . 0 = A ) );

definition

let T be non empty RelStr ;
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
(Fcl A) . n is Subset of T

proof end;

end;

:: 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;

definition

let T be non empty RelStr ;
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 Element of NAT
for B being Subset of T st B = it . n holds
it . (n + 1) = B ^i ) & it . 0 = A );
existence
ex b₁ being Function of NAT ,(bool the carrier of T) st
( ( for n being Element of NAT
for B being Subset of T st B = b₁ . n holds
b₁ . (n + 1) = B ^i ) & b₁ . 0 = A )

proof end;

uniqueness
for b₁, b₂ being Function of NAT ,(bool the carrier of T) st ( for n being Element of NAT
for B being Subset of T st B = b₁ . n holds
b₁ . (n + 1) = B ^i ) & b₁ . 0 = A & ( for n being Element of NAT
for B being Subset of T st B = b₂ . n holds
b₂ . (n + 1) = B ^i ) & b₂ . 0 = A holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Fint FINTOPO3:def 4 :

for T being non empty RelStr
for A being Subset of T
for b₃ being Function of NAT ,(bool the carrier of T) holds
( b₃ = Fint A iff ( ( for n being Element of NAT
for B being Subset of T st B = b₃ . n holds
b₃ . (n + 1) = B ^i ) & b₃ . 0 = A ) );

definition

let T be non empty RelStr ;
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
(Fint A) . n is Subset of T

proof end;

end;

:: 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 :: FINTOPO3:13

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

theorem :: FINTOPO3:14

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

theorem Th15: :: FINTOPO3:15

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

proof end;

theorem :: FINTOPO3:16

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

proof end;

theorem Th17: :: FINTOPO3:17

for T being non empty RelStr
for A, B being Subset of T
for n being Element of NAT holds Fcl (A \/ B),n = (Fcl A,n) \/ (Fcl B,n)

proof end;

theorem :: FINTOPO3:18

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

theorem :: FINTOPO3:19

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

theorem Th20: :: FINTOPO3:20

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

proof end;

theorem :: FINTOPO3:21

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

proof end;

theorem Th22: :: FINTOPO3:22

for T being non empty RelStr
for A, B being Subset of T
for n being Element of NAT holds Fint (A /\ B),n = (Fint A,n) /\ (Fint B,n)

proof end;

theorem :: FINTOPO3:23

for T being non empty RelStr
for A being Subset of T st T is filled holds
for n being Element of NAT holds A c= Fcl A,n

proof end;

theorem :: FINTOPO3:24

for T being non empty RelStr
for A being Subset of T st T is filled holds
for n being Element of NAT holds Fint A,n c= A

proof end;

theorem :: FINTOPO3:25

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

proof end;

theorem :: FINTOPO3:26

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

proof end;

theorem Th27: :: FINTOPO3:27

for T being non empty RelStr
for A being Subset of T
for n being Element of NAT holds (Fint (A ` ),n) ` = Fcl A,n

proof end;

theorem Th28: :: FINTOPO3:28

for T being non empty RelStr
for A being Subset of T
for n being Element of NAT holds (Fcl (A ` ),n) ` = Fint A,n

proof end;

theorem :: FINTOPO3:29

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

proof end;

theorem :: FINTOPO3:30

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

proof end;

definition

let T be non empty RelStr ;
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 Element of NAT
for B being Subset of T st B = it . n holds
it . (n + 1) = B ^f ) & it . 0 = A );
existence
ex b₁ being Function of NAT ,(bool the carrier of T) st
( ( for n being Element of NAT
for B being Subset of T st B = b₁ . n holds
b₁ . (n + 1) = B ^f ) & b₁ . 0 = A )

proof end;

uniqueness
for b₁, b₂ being Function of NAT ,(bool the carrier of T) st ( for n being Element of NAT
for B being Subset of T st B = b₁ . n holds
b₁ . (n + 1) = B ^f ) & b₁ . 0 = A & ( for n being Element of NAT
for B being Subset of T st B = b₂ . n holds
b₂ . (n + 1) = B ^f ) & b₂ . 0 = A holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines Finf FINTOPO3:def 6 :

for T being non empty RelStr
for A being Subset of T
for b₃ being Function of NAT ,(bool the carrier of T) holds
( b₃ = Finf A iff ( ( for n being Element of NAT
for B being Subset of T st B = b₃ . n holds
b₃ . (n + 1) = B ^f ) & b₃ . 0 = A ) );

definition

let T be non empty RelStr ;
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
(Finf A) . n is Subset of T

proof end;

end;

:: 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;

definition

let T be non empty RelStr ;
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 Element of NAT
for B being Subset of T st B = it . n holds
it . (n + 1) = B ^d ) & it . 0 = A );
existence
ex b₁ being Function of NAT ,(bool the carrier of T) st
( ( for n being Element of NAT
for B being Subset of T st B = b₁ . n holds
b₁ . (n + 1) = B ^d ) & b₁ . 0 = A )

proof end;

uniqueness
for b₁, b₂ being Function of NAT ,(bool the carrier of T) st ( for n being Element of NAT
for B being Subset of T st B = b₁ . n holds
b₁ . (n + 1) = B ^d ) & b₁ . 0 = A & ( for n being Element of NAT
for B being Subset of T st B = b₂ . n holds
b₂ . (n + 1) = B ^d ) & b₂ . 0 = A holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines Fdfl FINTOPO3:def 8 :

for T being non empty RelStr
for A being Subset of T
for b₃ being Function of NAT ,(bool the carrier of T) holds
( b₃ = Fdfl A iff ( ( for n being Element of NAT
for B being Subset of T st B = b₃ . n holds
b₃ . (n + 1) = B ^d ) & b₃ . 0 = A ) );

definition

let T be non empty RelStr ;
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
(Fdfl A) . n is Subset of T

proof end;

end;

:: 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 :: FINTOPO3:31

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

theorem :: FINTOPO3:32

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

theorem Th33: :: FINTOPO3:33

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

proof end;

theorem :: FINTOPO3:34

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

proof end;

theorem :: FINTOPO3:35

for T being non empty RelStr
for A, B being Subset of T
for n being Element of NAT holds Finf (A \/ B),n = (Finf A,n) \/ (Finf B,n)

proof end;

theorem :: FINTOPO3:36

for T being non empty RelStr
for A being Subset of T st T is filled holds
for n being Element of NAT holds A c= Finf A,n

proof end;

theorem :: FINTOPO3:37

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

proof end;

theorem :: FINTOPO3:38

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

theorem :: FINTOPO3:39

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

theorem Th40: :: FINTOPO3:40

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

proof end;

theorem :: FINTOPO3:41

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

proof end;

theorem Th42: :: FINTOPO3:42

for T being non empty RelStr
for A, B being Subset of T
for n being Element of NAT holds Fdfl (A /\ B),n = (Fdfl A,n) /\ (Fdfl B,n)

proof end;

theorem :: FINTOPO3:43

for T being non empty RelStr
for A being Subset of T st T is filled holds
for n being Element of NAT holds Fdfl A,n c= A

proof end;

theorem :: FINTOPO3:44

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

proof end;

theorem Th45: :: FINTOPO3:45

for T being non empty RelStr
for A being Subset of T
for n being Element of NAT holds Fdfl A,n = (Finf (A ` ),n) `

proof end;

theorem :: FINTOPO3:46

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

proof end;

definition

let T be non empty RelStr ;
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
Finf (U_FT x),n is Subset of T ;

end;

:: 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 :: FINTOPO3:47

for T being non empty RelStr
for x being Element of T holds U_FT x,0 = U_FT x by Def6;

theorem :: FINTOPO3:48

for T being non empty RelStr
for x being Element of T
for n being Element of NAT holds U_FT x,(n + 1) = (U_FT x,n) ^f by Def6;

definition

let S, T be non empty RelStr ;
pred S,T are_mutually_symmetric means :: FINTOPO3:def 11
( 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 ) ) );
symmetry
for S, T being non empty RelStr st 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 ) ) holds
( the carrier of T = the carrier of S & ( for x being Element of T
for y being Element of S holds
( y in U_FT x iff x in U_FT y ) ) ) ;

end;

:: 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 ) ) ) );