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


begin

:: The following is definition of "deflation of a set A"
:: (A^f is an inflation of A).
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 b1 being Function of NAT,(bool the carrier of T) st
( ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^b ) & b1 . 0 = A )
proof end;
uniqueness
for b1, b2 being Function of NAT,(bool the carrier of T) st ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^b ) & b1 . 0 = A & ( for n being Element of NAT
for B being Subset of T st B = b2 . n holds
b2 . (n + 1) = B ^b ) & b2 . 0 = A holds
b1 = b2
proof end;
end;

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

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 b1 being Function of NAT,(bool the carrier of T) st
( ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^i ) & b1 . 0 = A )
proof end;
uniqueness
for b1, b2 being Function of NAT,(bool the carrier of T) st ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^i ) & b1 . 0 = A & ( for n being Element of NAT
for B being Subset of T st B = b2 . n holds
b2 . (n + 1) = B ^i ) & b2 . 0 = A holds
b1 = b2
proof end;
end;

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

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;

:: Function of Inflation Series
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 b1 being Function of NAT,(bool the carrier of T) st
( ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^f ) & b1 . 0 = A )
proof end;
uniqueness
for b1, b2 being Function of NAT,(bool the carrier of T) st ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^f ) & b1 . 0 = A & ( for n being Element of NAT
for B being Subset of T st B = b2 . n holds
b2 . (n + 1) = B ^f ) & b2 . 0 = A holds
b1 = b2
proof end;
end;

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

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;

:: Function of Deflation Series
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 b1 being Function of NAT,(bool the carrier of T) st
( ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^d ) & b1 . 0 = A )
proof end;
uniqueness
for b1, b2 being Function of NAT,(bool the carrier of T) st ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^d ) & b1 . 0 = A & ( for n being Element of NAT
for B being Subset of T st B = b2 . n holds
b2 . (n + 1) = B ^d ) & b2 . 0 = A holds
b1 = b2
proof end;
end;

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

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