:: Morphology for Image Processing, Part {I}
:: by Hiroshi Yamazaki , Czes\l aw Byli\'nski and Katsumi Wasaki
::
:: 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
}
;
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
;
proof end;
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 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
for A, B being Subset of E holds A + B = B + A
by Lm1;
end;

theorem Th10: :: MORPH_01:10
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 () (+) 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 { (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= () (-) 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 (-) () = 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;
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
proof end;
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 ) & ( for A being binary-image of E holds b2 . A = A (+) B ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 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 :Def3: :: 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
proof end;
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 ) & ( for A being binary-image of E holds b2 . A = A (-) B ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 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 () . () = union { (() . 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
() . A 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 () . (v + A) = v + (() . 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 () . (meet F) = meet { (() . 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
() . A 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 () . (v + A) = v + (() . A)
proof end;

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

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