:: Preliminaries to Mathematical Morphology and Its Properties
:: by Yuzhong Ding and Xiquan Liang
::
:: Received January 7, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users


begin

:: Algebraic Properties
:: Translation of X according to p
definition
let T be non empty addMagma ;
let p be Element of T;
let X be Subset of T;
funcX + p ->  Subset of T equals :: MATHMORP:def 1
 {  (q + p) where q is Element of T : q in X  }  ;
coherence
  {  (q + p) where q is Element of T : q in X  }  is Subset of T
proofend;
end;

:: deftheorem  defines + MATHMORP:def_1_:_
 for T being non empty addMagma
for p being Element of T
for X being Subset of T holds X + p =  {  (q + p) where q is Element of T : q in X  }  ;

:: Reflected of X
definition
let T be non empty addLoopStr ;
let X be Subset of T;
funcX !  ->  Subset of T equals :: MATHMORP:def 2
 {  (- q) where q is Point of T : q in X  }  ;
coherence
  {  (- q) where q is Point of T : q in X  }  is Subset of T
proofend;
end;

:: deftheorem  defines ! MATHMORP:def_2_:_
 for T being non empty addLoopStr
for X being Subset of T holds X ! =  {  (- q) where q is Point of T : q in X  }  ;

:: Set Erosion
definition
let T be non empty addMagma ;
let X, B be Subset of T;
funcX (-) B ->  Subset of T equals :: MATHMORP:def 3
 {  y where y is Point of T : B + y c= X  }  ;
coherence
  {  y where y is Point of T : B + y c= X  }  is Subset of T
proofend;
end;

:: deftheorem  defines (-) MATHMORP:def_3_:_
 for T being non empty addMagma
for X, B being Subset of T holds X (-) B =  {  y where y is Point of T : B + y c= X  }  ;

notation
let T be non empty addLoopStr ;
let A, B be Subset of T;
synonym A (+) B for A + B;
end;

theorem Th1: :: MATHMORP:1
for T being non empty right_complementable add-associative right_zeroed RLSStruct
for B being Subset of T holds (B !) ! = B
proofend;

theorem Th2: :: MATHMORP:2
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for x being Point of T holds {(0. T)} + x = {x}
proofend;

theorem Th3: :: MATHMORP:3
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for B1, B2 being Subset of T
for p being Point of T st B1 c= B2 holds
B1 + p c= B2 + p
proofend;

theorem Th4: :: MATHMORP:4
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for x being Point of T
for X being Subset of T st X = {} holds
X + x = {}
proofend;

theorem :: MATHMORP:5
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X being Subset of T holds X (-) {(0. T)} = X
proofend;

Lm1:  for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for x, y being Point of T holds {x} + y = {y} + x
proofend;

theorem :: MATHMORP:6
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X being Subset of T holds X (+) {(0. T)} = X
proofend;

theorem :: MATHMORP:7
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X being Subset of T
for x being Point of T holds X (+) {x} = X + x
proofend;

theorem Th8: :: MATHMORP:8
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T st Y = {} holds
X (-) Y = the carrier of T
proofend;

theorem Th9: :: MATHMORP:9
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, B being Subset of T st X c= Y holds
( X (-) B c= Y (-) B & X (+) B c= Y (+) B )
proofend;

theorem Th10: :: MATHMORP:10
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for B1, B2, X being Subset of T st B1 c= B2 holds
( X (-) B2 c= X (-) B1 & X (+) B1 c= X (+) B2 )
proofend;

theorem :: MATHMORP:11
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for B, X being Subset of T st 0. T in B holds
( X (-) B c= X & X c= X (+) B )
proofend;

theorem Th12: :: MATHMORP:12
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T holds X (+) Y = Y (+) X
proofend;

Lm2:  for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for p, x being Point of T holds
( (p - x) + x = p & (p + x) - x = p )
proofend;

theorem Th13: :: MATHMORP:13
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for Y, X being Subset of T
for y, x being Point of T holds
( Y + y c= X + x iff Y + (y - x) c= X )
proofend;

theorem Th14: :: MATHMORP:14
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T
for p being Point of T holds (X + p) (-) Y = (X (-) Y) + p
proofend;

theorem Th15: :: MATHMORP:15
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T
for p being Point of T holds (X + p) (+) Y = (X (+) Y) + p
proofend;

theorem Th16: :: MATHMORP:16
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X being Subset of T
for x, y being Point of T holds (X + x) + y = X + (x + y)
proofend;

theorem Th17: :: MATHMORP:17
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T
for p being Point of T holds X (-) (Y + p) = (X (-) Y) + (- p)
proofend;

theorem :: MATHMORP:18
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T
for p being Point of T holds X (+) (Y + p) = (X (+) Y) + p
proofend;

theorem Th19: :: MATHMORP:19
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T
for x being Point of T st x in X holds
B + x c= B (+) X
proofend;

theorem Th20: :: MATHMORP:20
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds X c= (X (+) B) (-) B
proofend;

theorem Th21: :: MATHMORP:21
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X being Subset of T holds X + (0. T) = X
proofend;

theorem :: MATHMORP:22
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X being Subset of T
for x being Point of T holds X (-) {x} = X + (- x)
proofend;

Lm3:  for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds (X (-) B) (+) B c= X
proofend;

theorem Th23: :: MATHMORP:23
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, Z being Subset of T holds X (-) (Y (+) Z) = (X (-) Y) (-) Z
proofend;

theorem :: MATHMORP:24
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, Z being Subset of T holds X (-) (Y (+) Z) = (X (-) Z) (-) Y
proofend;

theorem :: MATHMORP:25
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, Z being Subset of T holds X (+) (Y (-) Z) c= (X (+) Y) (-) Z
proofend;

theorem :: MATHMORP:26
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, Z being Subset of T holds X (+) (Y (+) Z) = (X (+) Y) (+) Z
proofend;

theorem Th27: :: MATHMORP:27
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for B, C being Subset of T
for y being Point of T holds (B \/ C) + y = (B + y) \/ (C + y)
proofend;

theorem Th28: :: MATHMORP:28
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for B, C being Subset of T
for y being Point of T holds (B /\ C) + y = (B + y) /\ (C + y)
proofend;

theorem :: MATHMORP:29
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B, C being Subset of T holds X (-) (B \/ C) = (X (-) B) /\ (X (-) C)
proofend;

theorem :: MATHMORP:30
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B, C being Subset of T holds X (+) (B \/ C) = (X (+) B) \/ (X (+) C)
proofend;

theorem :: MATHMORP:31
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B, Y being Subset of T holds (X (-) B) \/ (Y (-) B) c= (X \/ Y) (-) B
proofend;

theorem :: MATHMORP:32
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, B being Subset of T holds (X \/ Y) (+) B = (X (+) B) \/ (Y (+) B)
proofend;

theorem :: MATHMORP:33
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, B being Subset of T holds (X /\ Y) (-) B = (X (-) B) /\ (Y (-) B)
proofend;

theorem Th34: :: MATHMORP:34
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, B being Subset of T holds (X /\ Y) (+) B c= (X (+) B) /\ (Y (+) B)
proofend;

theorem :: MATHMORP:35
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for B, X, Y being Subset of T holds B (+) (X /\ Y) c= (B (+) X) /\ (B (+) Y)
proofend;

theorem :: MATHMORP:36
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for B, X, Y being Subset of T holds (B (-) X) \/ (B (-) Y) c= B (-) (X /\ Y)
proofend;

theorem Th37: :: MATHMORP:37
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds ((X `) (-) B) ` = X (+) (B !)
proofend;

theorem Th38: :: MATHMORP:38
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds (X (-) B) ` = (X `) (+) (B !)
proofend;

begin

:: 2. The definition of Adjunction Opening and Closing and
:: their Algebraic Properties
:: Adjunction Opening
definition
let T be non empty addLoopStr ;
let X, B be Subset of T;
funcX (O) B ->  Subset of T equals :: MATHMORP:def 4
(X (-) B) (+) B;
coherence
 (X (-) B) (+) B is Subset of T ;
end;

:: deftheorem  defines (O) MATHMORP:def_4_:_
 for T being non empty addLoopStr
for X, B being Subset of T holds X (O) B = (X (-) B) (+) B;

:: Adjunction Closing
definition
let T be non empty addLoopStr ;
let X, B be Subset of T;
funcX (o) B ->  Subset of T equals :: MATHMORP:def 5
(X (+) B) (-) B;
coherence
 (X (+) B) (-) B is Subset of T ;
end;

:: deftheorem  defines (o) MATHMORP:def_5_:_
 for T being non empty addLoopStr
for X, B being Subset of T holds X (o) B = (X (+) B) (-) B;

theorem :: MATHMORP:39
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds ((X `) (O) (B !)) ` = X (o) B
proofend;

theorem :: MATHMORP:40
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds ((X `) (o) (B !)) ` = X (O) B
proofend;

theorem Th41: :: MATHMORP:41
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds
( X (O) B c= X & X c= X (o) B )
proofend;

theorem Th42: :: MATHMORP:42
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X being Subset of T holds X (O) X = X
proofend;

theorem :: MATHMORP:43
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds
( (X (O) B) (-) B c= X (-) B & (X (O) B) (+) B c= X (+) B )
proofend;

theorem :: MATHMORP:44
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds
( X (-) B c= (X (o) B) (-) B & X (+) B c= (X (o) B) (+) B )
proofend;

theorem Th45: :: MATHMORP:45
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, B being Subset of T st X c= Y holds
( X (O) B c= Y (O) B & X (o) B c= Y (o) B )
proofend;

theorem Th46: :: MATHMORP:46
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T
for p being Point of T holds (X + p) (O) Y = (X (O) Y) + p
proofend;

theorem :: MATHMORP:47
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T
for p being Point of T holds (X + p) (o) Y = (X (o) Y) + p
proofend;

theorem :: MATHMORP:48
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for C, B, X being Subset of T st C c= B holds
X (O) B c= (X (-) C) (+) B
proofend;

theorem :: MATHMORP:49
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for B, C, X being Subset of T st B c= C holds
X (o) B c= (X (+) C) (-) B
proofend;

theorem Th50: :: MATHMORP:50
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T holds
( X (+) Y = (X (o) Y) (+) Y & X (-) Y = (X (O) Y) (-) Y )
proofend;

theorem :: MATHMORP:51
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T holds
( X (+) Y = (X (+) Y) (O) Y & X (-) Y = (X (-) Y) (o) Y )
proofend;

theorem :: MATHMORP:52
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds (X (O) B) (O) B = X (O) B
proofend;

theorem :: MATHMORP:53
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds (X (o) B) (o) B = X (o) B by Th50;

theorem :: MATHMORP:54
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B, Y being Subset of T holds X (O) B c= (X \/ Y) (O) B
proofend;

theorem :: MATHMORP:55
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for B, B1, X being Subset of T st B = B (O) B1 holds
X (O) B c= X (O) B1
proofend;

begin

:: 3.The definition of Scaling transformation and its Algebraic Properties
:: Scaling transformation
definition
let t be real number ;
let T be non empty RLSStruct ;
let A be Subset of T;
funct (.) A ->  Subset of T equals :: MATHMORP:def 6
 {  (t * a) where a is Point of T : a in A  }  ;
coherence
  {  (t * a) where a is Point of T : a in A  }  is Subset of T
proofend;
end;

:: deftheorem  defines (.) MATHMORP:def_6_:_
 for t being real number
for T being non empty RLSStruct
for A being Subset of T holds t (.) A =  {  (t * a) where a is Point of T : a in A  }  ;

theorem :: MATHMORP:56
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X being Subset of T st X = {} holds
0 (.) X = {}
proofend;

theorem :: MATHMORP:57
for n being Element of NAT
for X being non empty Subset of (TOP-REAL n) holds 0 (.) X = {(0. (TOP-REAL n))}
proofend;

theorem Th58: :: MATHMORP:58
for n being Element of NAT
for X being Subset of (TOP-REAL n) holds 1 (.) X = X
proofend;

theorem :: MATHMORP:59
for n being Element of NAT
for X being Subset of (TOP-REAL n) holds 2 (.) X c= X (+) X
proofend;

theorem Th60: :: MATHMORP:60
for t, s being real number
for n being Element of NAT
for X being Subset of (TOP-REAL n) holds (t * s) (.) X = t (.) (s (.) X)
proofend;

theorem Th61: :: MATHMORP:61
for t being real number
for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) st X c= Y holds
t (.) X c= t (.) Y
proofend;

theorem Th62: :: MATHMORP:62
for t being real number
for n being Element of NAT
for X being Subset of (TOP-REAL n)
for x being Point of (TOP-REAL n) holds t (.) (X + x) = (t (.) X) + (t * x)
proofend;

theorem Th63: :: MATHMORP:63
for t being real number
for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) holds t (.) (X (+) Y) = (t (.) X) (+) (t (.) Y)
proofend;

theorem Th64: :: MATHMORP:64
for t being real number
for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) st t <> 0 holds
t (.) (X (-) Y) = (t (.) X) (-) (t (.) Y)
proofend;

theorem :: MATHMORP:65
for t being real number
for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) st t <> 0 holds
t (.) (X (O) Y) = (t (.) X) (O) (t (.) Y)
proofend;

theorem :: MATHMORP:66
for t being real number
for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) st t <> 0 holds
t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y)
proofend;

begin

:: Algebraic Properties.
:: "Hit or Miss" Transformation
definition
let T be non empty RLSStruct ;
let X, B1, B2 be Subset of T;
funcX (*) (B1,B2) ->  Subset of T equals :: MATHMORP:def 7
(X (-) B1) /\ ((X `) (-) B2);
coherence
 (X (-) B1) /\ ((X `) (-) B2) is Subset of T ;
end;

:: deftheorem  defines (*) MATHMORP:def_7_:_
 for T being non empty RLSStruct
for X, B1, B2 being Subset of T holds X (*) (B1,B2) = (X (-) B1) /\ ((X `) (-) B2);

:: Thickening
definition
let T be non empty RLSStruct ;
let X, B1, B2 be Subset of T;
funcX (&amp;) (B1,B2) ->  Subset of T equals :: MATHMORP:def 8
X \/ (X (*) (B1,B2));
coherence
 X \/ (X (*) (B1,B2)) is Subset of T ;
end;

:: deftheorem  defines (&amp;) MATHMORP:def_8_:_
 for T being non empty RLSStruct
for X, B1, B2 being Subset of T holds X (&amp;) (B1,B2) = X \/ (X (*) (B1,B2));

:: Thinning
definition
let T be non empty RLSStruct ;
let X, B1, B2 be Subset of T;
funcX (@) (B1,B2) ->  Subset of T equals :: MATHMORP:def 9
X \ (X (*) (B1,B2));
coherence
 X \ (X (*) (B1,B2)) is Subset of T ;
end;

:: deftheorem  defines (@) MATHMORP:def_9_:_
 for T being non empty RLSStruct
for X, B1, B2 being Subset of T holds X (@) (B1,B2) = X \ (X (*) (B1,B2));

theorem :: MATHMORP:67
for n being Element of NAT
for B1, X, B2 being Subset of (TOP-REAL n) st B1 = {} holds
X (*) (B1,B2) = (X `) (-) B2
proofend;

theorem :: MATHMORP:68
for n being Element of NAT
for B2, X, B1 being Subset of (TOP-REAL n) st B2 = {} holds
X (*) (B1,B2) = X (-) B1
proofend;

theorem :: MATHMORP:69
for n being Element of NAT
for B1, X, B2 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B1 holds
X (*) (B1,B2) c= X
proofend;

theorem :: MATHMORP:70
for n being Element of NAT
for B2, X, B1 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B2 holds
(X (*) (B1,B2)) /\ X = {}
proofend;

theorem :: MATHMORP:71
for n being Element of NAT
for B1, X, B2 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B1 holds
X (&amp;) (B1,B2) = X
proofend;

theorem :: MATHMORP:72
for n being Element of NAT
for B2, X, B1 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B2 holds
X (@) (B1,B2) = X
proofend;

theorem :: MATHMORP:73
for n being Element of NAT
for X, B2, B1 being Subset of (TOP-REAL n) holds X (@) (B2,B1) = ((X `) (&amp;) (B1,B2)) `
proofend;

begin

:: Adjunction Closing on Convex sets
theorem Th74: :: MATHMORP:74
for V being RealLinearSpace
for B being Subset of V holds
( B is convex iff for x, y being Point of V
for r being real number st 0 <= r &amp; r <= 1 &amp; x in B &amp; y in B holds
(r * x) + ((1 - r) * y) in B )
proofend;

definition
let V be RealLinearSpace;
let B be Subset of V;
redefine attr B is convex  means :Def10: :: MATHMORP:def 10
 for x, y being Point of V
for r being real number st 0 <= r &amp; r <= 1 &amp; x in B &amp; y in B holds
(r * x) + ((1 - r) * y) in B;
compatibility
 ( B is convex iff for x, y being Point of V
for r being real number st 0 <= r &amp; r <= 1 &amp; x in B &amp; y in B holds
(r * x) + ((1 - r) * y) in B ) by Th74;
end;

:: deftheorem Def10 defines convex MATHMORP:def_10_:_
 for V being RealLinearSpace
for B being Subset of V holds
( B is convex iff for x, y being Point of V
for r being real number st 0 <= r &amp; r <= 1 &amp; x in B &amp; y in B holds
(r * x) + ((1 - r) * y) in B );

theorem :: MATHMORP:75
for n being Element of NAT
for X being Subset of (TOP-REAL n) st X is convex holds
X ! is convex
proofend;

theorem Th76: :: MATHMORP:76
for n being Element of NAT
for X, B being Subset of (TOP-REAL n) st X is convex &amp; B is convex holds
( X (+) B is convex &amp; X (-) B is convex )
proofend;

theorem :: MATHMORP:77
for n being Element of NAT
for X, B being Subset of (TOP-REAL n) st X is convex &amp; B is convex holds
( X (O) B is convex &amp; X (o) B is convex )
proofend;

theorem :: MATHMORP:78
for t, s being real number
for n being Element of NAT
for B being Subset of (TOP-REAL n) st B is convex &amp; 0 < t &amp; 0 < s holds
(s + t) (.) B = (s (.) B) (+) (t (.) B)
proofend;