:: 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-2021 Association of Mizar Users

:: 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 -> sequence of (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
ex b₁ being sequence of (bool the carrier of T) st
( ( for n being 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 sequence of (bool the carrier of T) st ( for n being Nat
for B being Subset of T st B = b₁ . n holds
b₁ . (n + 1) = B ^b ) & b₁ . 0 = A & ( for n being 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 sequence of (bool the carrier of T) holds
( b₃ = Fcl A iff ( ( for n being 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 -> sequence of (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
ex b₁ being sequence of (bool the carrier of T) st
( ( for n being 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 sequence of (bool the carrier of T) st ( for n being Nat
for B being Subset of T st B = b₁ . n holds
b₁ . (n + 1) = B ^i ) & b₁ . 0 = A & ( for n being 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 sequence of (bool the carrier of T) holds
( b₃ = Fint A iff ( ( for n being 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 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 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 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 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 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 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 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 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 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 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 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 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 -> sequence of (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
ex b₁ being sequence of (bool the carrier of T) st
( ( for n being 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 sequence of (bool the carrier of T) st ( for n being Nat
for B being Subset of T st B = b₁ . n holds
b₁ . (n + 1) = B ^f ) & b₁ . 0 = A & ( for n being 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 sequence of (bool the carrier of T) holds
( b₃ = Finf A iff ( ( for n being 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;

:: Function of Deflation Series

definition

let T be non empty RelStr ;
let A be Subset of T;

func Fdfl A -> sequence of (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
ex b₁ being sequence of (bool the carrier of T) st
( ( for n being 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 sequence of (bool the carrier of T) st ( for n being Nat
for B being Subset of T st B = b₁ . n holds
b₁ . (n + 1) = B ^d ) & b₁ . 0 = A & ( for n being 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 sequence of (bool the carrier of T) holds
( b₃ = Fdfl A iff ( ( for n being 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 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 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 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 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 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 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 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 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 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 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 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 ) ) ) );