MORPH_01: Morphology for Image Processing, Part {I}

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

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;

func A (-) 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 } ;

proof end;

end;

:: deftheorem defines (-) MORPH_01:def 1 :

notation

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

end;

theorem Th1: :: 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 )

proof end;

theorem Th2: :: MORPH_01:2

for E being RealLinearSpace
for A, B being Subset of E st A <> {} & B = {} holds
B (-) A = B

proof end;

theorem Th3: :: MORPH_01:3

for E being RealLinearSpace
for A, B being Subset of E st B = the carrier of E & A <> {} holds
( A (+) B = B & B (+) A = B )

proof end;

theorem Th4: :: MORPH_01:4

for E being RealLinearSpace
for A, B being Subset of E st B = the carrier of E holds
B (-) A = B

proof end;

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 }

proof end;

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 }

proof end;

theorem Th7: :: 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 <> {} }

proof end;

theorem Th8: :: 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 }

proof end;

theorem Th9: :: 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) & ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B) )

proof end;

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

proof end;

definition

let E be non empty Abelian addLoopStr ;
let A, B be Subset of E;
:: original: +
redefine func A (+) B -> Element of K10( the carrier of E);
commutativity by Lm1;

end;

theorem Th10: :: 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)

proof end;

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

theorem Th12: :: 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 }

proof end;

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 }

proof end;

theorem Th14: :: 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 }

proof end;

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 }

proof end;

theorem Th16: :: 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

proof end;

theorem Th17: :: 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) & (v + A) (+) B = v + (A (+) B) )

proof end;

theorem Th18: :: 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 }

proof end;

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)

proof end;

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

proof end;

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 }

proof end;

theorem Th22: :: 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

proof end;

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

proof end;

theorem Th24: :: 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) & (v + A) (-) B = v + (A (-) B) )

proof end;

theorem Th25: :: 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)

proof end;

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 :Def2: :: MORPH_01:def 2
for A being binary-image of E holds it . A = A (+) B;

proof end;

proof end;

end;

:: deftheorem Def2 defines dilation MORPH_01:def 2 :

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 :Def3: :: MORPH_01:def 3
for A being binary-image of E holds it . A = A (-) B;

proof end;

proof end;

end;

:: deftheorem Def3 defines erosion MORPH_01:def 3 :

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 }

proof end;

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

proof end;

theorem :: MORPH_01:28

for E being RealLinearSpace
for v being Element of E
for A, C being non empty binary-image of E holds (dilation C) . (v + A) = v + ((dilation C) . A)

proof end;

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 }

proof end;

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

proof end;

theorem :: MORPH_01:31

for E being RealLinearSpace
for v being Element of E
for A, C being non empty binary-image of E holds (erosion C) . (v + A) = v + ((erosion C) . A)

proof end;

theorem :: MORPH_01:32

for E being RealLinearSpace
for A, C being non empty binary-image of E holds
( (dilation C) . ( the carrier of E \ A) = the carrier of E \ ((erosion C) . A) & (erosion C) . ( the carrier of E \ A) = the carrier of E \ ((dilation C) . A) )

proof end;

theorem :: MORPH_01:33

for E being RealLinearSpace
for A, B, C being non empty binary-image of E holds
( (dilation C) . ((dilation B) . A) = (dilation ((dilation C) . B)) . A & (erosion C) . ((erosion B) . A) = (erosion ((dilation C) . B)) . A )

proof end;