:: Morphology for Image Processing, Part {I}
:: by Hiroshi Yamazaki , Czes\l aw Byli\'nski and Katsumi Wasaki
::
:: Received September 21, 2011
:: Copyright (c) 2011-2012 Association of Mizar Users


begin

definition
let E be non empty RLSStruct ;
mode binary-image of E is Subset of E;
end;

definition
let E be RealLinearSpace;
let A, B be binary-image of E;
funcA (-) B ->  binary-image of E equals :: MORPH_01:def 1
 {  z where z is Element of E : for b being Element of E st b in B holds
z - b in A  }  ;
correctness
coherence
{  z where z is Element of E : for b being Element of E st b in B holds
z - b in A  }  is binary-image of E;
proofend;
end;

:: deftheorem  defines (-) MORPH_01:def_1_:_
 for E being RealLinearSpace
for A, B being binary-image of E holds A (-) B =  {  z where z is Element of E : for b being Element of E st b in B holds
z - b in A  }  ;

notation
let a be Real;
let E be RealLinearSpace;
let A be Subset of E;
synonym a * A for a (.) A;
end;

theorem LM0010: :: MORPH_01:1
for E being RealLinearSpace
for A, B being Subset of E st B = {} holds
( A (+) B = B & B (+) A = B & A (-) B = the carrier of E )
proofend;

theorem LM0010A: :: MORPH_01:2
for E being RealLinearSpace
for A, B being Subset of E st A <> {} &amp; B = {} holds
B (-) A = B
proofend;

theorem LM0020: :: MORPH_01:3
for E being RealLinearSpace
for A, B being Subset of E st B = the carrier of E &amp; A <> {} holds
( A (+) B = B &amp; B (+) A = B )
proofend;

theorem LM0020A: :: MORPH_01:4
for E being RealLinearSpace
for A, B being Subset of E st B = the carrier of E holds
B (-) A = B
proofend;

theorem :: MORPH_01:5
for E being RealLinearSpace
for A, B being binary-image of E holds A (+) B = union  {  (b + A) where b is Element of E : b in B  }
proofend;

definition
let E be non empty RLSStruct ;
mode binary-image-family of E is Subset-Family of the carrier of E;
end;

theorem :: MORPH_01:6
for E being RealLinearSpace
for A, B being non empty binary-image of E holds A (-) B = meet  {  (b + A) where b is Element of E : b in B  }
proofend;

theorem Th104: :: MORPH_01:7
for E being RealLinearSpace
for A, B being non empty binary-image of E holds A (+) B =  {  v where v is Element of E : (v + ((- 1) * B)) /\ A <> {}  }
proofend;

theorem Th105: :: MORPH_01:8
for E being RealLinearSpace
for A, B being non empty binary-image of E holds A (-) B =  {  v where v is Element of E : v + ((- 1) * B) c= A  }
proofend;

theorem Th106: :: MORPH_01:9
for E being RealLinearSpace
for A, B being non empty binary-image of E holds
( ( the carrier of E \ A) (+) B = the carrier of E \ (A (-) B) &amp; ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B) )
proofend;

Th107:  for E being non empty Abelian addLoopStr
for A, B being Subset of E holds A (+) B = B (+) A
proofend;

definition
let E be non empty Abelian addLoopStr ;
let A, B be Subset of E;
:: original:+
redefine funcA (+) B ->  Element of K10( the carrier of E);
commutativity
 for A, B being Subset of E holds A + B = B + A by Th107;
end;

theorem Th108A1: :: MORPH_01:10
for E being non empty add-associative addLoopStr
for A, B, C being Subset of E holds (A + B) + C = A + (B + C)
proofend;

theorem :: MORPH_01:11
for E being RealLinearSpace
for A, B, C being non empty binary-image of E holds (A (+) B) (+) C = A (+) (B (+) C) by Th108A1;

theorem Th108B: :: MORPH_01:12
for E being RealLinearSpace
for F being binary-image-family of E
for B being non empty binary-image of E holds (union F) (+) B = union  {  (X (+) B) where X is binary-image of E : X in F  }
proofend;

theorem :: MORPH_01:13
for E being RealLinearSpace
for F being binary-image-family of E
for A being non empty binary-image of E holds A (+) (union F) = union  {  (A (+) X) where X is binary-image of E : X in F  }
proofend;

theorem Th110: :: MORPH_01:14
for E being RealLinearSpace
for F being binary-image-family of E
for B being non empty binary-image of E holds (meet F) (+) B c= meet  {  (X (+) B) where X is binary-image of E : X in F  }
proofend;

theorem :: MORPH_01:15
for E being RealLinearSpace
for F being binary-image-family of E
for A being non empty binary-image of E holds A (+) (meet F) c= meet  {  (A (+) X) where X is binary-image of E : X in F  }
proofend;

theorem Th112: :: MORPH_01:16
for E being non empty addLoopStr
for A, B, C being Subset of E st B c= C holds
A + B c= A + C
proofend;

theorem Th113: :: MORPH_01:17
for E being RealLinearSpace
for v being Element of E
for A, B being non empty binary-image of E holds
( (v + A) (+) B = A (+) (v + B) &amp; (v + A) (+) B = v + (A (+) B) )
proofend;

theorem Th114: :: MORPH_01:18
for E being RealLinearSpace
for F being binary-image-family of E
for B being non empty binary-image of E holds (meet F) (-) B = meet  {  (X (-) B) where X is binary-image of E : X in F  }
proofend;

theorem :: MORPH_01:19
for E being RealLinearSpace
for F being binary-image-family of E
for B being non empty binary-image of E holds meet  {  (B (-) X) where X is binary-image of E : X in F  }  c= B (-) (meet F)
proofend;

theorem :: MORPH_01:20
for E being RealLinearSpace
for F being binary-image-family of E
for B being non empty binary-image of E holds union  {  (X (-) B) where X is binary-image of E : X in F  }  c= (union F) (-) B
proofend;

theorem :: MORPH_01:21
for E being RealLinearSpace
for F being binary-image-family of E
for B being non empty binary-image of E st F <> {} holds
B (-) (union F) = meet  {  (B (-) X) where X is binary-image of E : X in F  }
proofend;

theorem Th118: :: MORPH_01:22
for E being RealLinearSpace
for A, B, C being non empty binary-image of E st A c= B holds
A (-) C c= B (-) C
proofend;

theorem :: MORPH_01:23
for E being RealLinearSpace
for A, B, C being non empty binary-image of E st A c= B holds
C (-) B c= C (-) A
proofend;

theorem Th120: :: MORPH_01:24
for E being RealLinearSpace
for v being Element of E
for A, B being non empty binary-image of E holds
( (v + A) (-) B = A (-) (v + B) &amp; (v + A) (-) B = v + (A (-) B) )
proofend;

theorem Th121: :: MORPH_01:25
for E being RealLinearSpace
for A, B, C being non empty binary-image of E holds (A (-) B) (-) C = A (-) (B (+) C)
proofend;

begin

definition
let E be RealLinearSpace;
let B be binary-image of E;
func dilation B ->  Function of (bool the carrier of E),(bool the carrier of E) means :def020: :: MORPH_01:def 2
 for A being binary-image of E holds it . A = A (+) B;
existence
 ex b1 being Function of (bool the carrier of E),(bool the carrier of E) st
for A being binary-image of E holds b1 . A = A (+) B
proofend;
uniqueness
 for b1, b2 being Function of (bool the carrier of E),(bool the carrier of E) st ( for A being binary-image of E holds b1 . A = A (+) B ) &amp; ( for A being binary-image of E holds b2 . A = A (+) B ) holds
b1 = b2
proofend;
end;

:: deftheorem def020 defines dilation MORPH_01:def_2_:_
 for E being RealLinearSpace
for B being binary-image of E
for b3 being Function of (bool the carrier of E),(bool the carrier of E) holds
( b3 = dilation B iff for A being binary-image of E holds b3 . A = A (+) B );

definition
let E be RealLinearSpace;
let B be binary-image of E;
func erosion B ->  Function of (bool the carrier of E),(bool the carrier of E) means :def030: :: MORPH_01:def 3
 for A being binary-image of E holds it . A = A (-) B;
existence
 ex b1 being Function of (bool the carrier of E),(bool the carrier of E) st
for A being binary-image of E holds b1 . A = A (-) B
proofend;
uniqueness
 for b1, b2 being Function of (bool the carrier of E),(bool the carrier of E) st ( for A being binary-image of E holds b1 . A = A (-) B ) &amp; ( for A being binary-image of E holds b2 . A = A (-) B ) holds
b1 = b2
proofend;
end;

:: deftheorem def030 defines erosion MORPH_01:def_3_:_
 for E being RealLinearSpace
for B being binary-image of E
for b3 being Function of (bool the carrier of E),(bool the carrier of E) holds
( b3 = erosion B iff for A being binary-image of E holds b3 . A = A (-) B );

theorem :: MORPH_01:26
for E being RealLinearSpace
for F being binary-image-family of E
for B being non empty binary-image of E holds (dilation B) . (union F) = union  {  ((dilation B) . X) where X is binary-image of E : X in F  }
proofend;

theorem :: MORPH_01:27
for E being RealLinearSpace
for A, B, C being non empty binary-image of E st A c= B holds
(dilation C) . A c= (dilation C) . B
proofend;

theorem :: MORPH_01:28
for E being RealLinearSpace
for v being Element of E
for C, A being non empty binary-image of E holds (dilation C) . (v + A) = v + ((dilation C) . A)
proofend;

theorem :: MORPH_01:29
for E being RealLinearSpace
for F being binary-image-family of E
for B being non empty binary-image of E holds (erosion B) . (meet F) = meet  {  ((erosion B) . X) where X is binary-image of E : X in F  }
proofend;

theorem :: MORPH_01:30
for E being RealLinearSpace
for A, B, C being non empty binary-image of E st A c= B holds
(erosion C) . A c= (erosion C) . B
proofend;

theorem :: MORPH_01:31
for E being RealLinearSpace
for v being Element of E
for C, A being non empty binary-image of E holds (erosion C) . (v + A) = v + ((erosion C) . A)
proofend;

theorem :: MORPH_01:32
for E being RealLinearSpace
for C, A being non empty binary-image of E holds
( (dilation C) . ( the carrier of E \ A) = the carrier of E \ ((erosion C) . A) &amp; (erosion C) . ( the carrier of E \ A) = the carrier of E \ ((dilation C) . A) )
proofend;

theorem :: MORPH_01:33
for E being RealLinearSpace
for C, B, A being non empty binary-image of E holds
( (dilation C) . ((dilation B) . A) = (dilation ((dilation C) . B)) . A &amp; (erosion C) . ((erosion B) . A) = (erosion ((dilation C) . B)) . A )
proofend;