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


:: 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;
func X + 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
proof end;
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;
func X ! -> 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
proof end;
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;
func X (-) 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
proof end;
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
proof end;

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}
proof end;

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
proof end;

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 = {}
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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 )
proof end;

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

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

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
proof end;

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

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

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
proof end;

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
proof end;

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)
proof end;

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)
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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)
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

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

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)
proof end;

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)
proof end;

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)
proof end;

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

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

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 !)
proof end;

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 !)
proof end;

:: 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;
func X (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;
func X (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
proof end;

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
proof end;

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 )
proof end;

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
proof end;

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 )
proof end;

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 )
proof end;

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 )
proof end;

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
proof end;

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
proof end;

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

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

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 )
proof end;

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 )
proof end;

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
proof end;

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, Y, B being Subset of T holds X (O) B c= (X \/ Y) (O) B
proof end;

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

:: 3.The definition of Scaling transformation and its Algebraic Properties
:: Scaling transformation
definition
let t be Real;
let T be non empty RLSStruct ;
let A be Subset of T;
func t (.) 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
proof end;
end;

:: deftheorem defines (.) MATHMORP:def 6 :
for t being Real
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 = {}
proof end;

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))}
proof end;

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

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

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

theorem Th61: :: MATHMORP:61
for t being Real
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
proof end;

theorem Th62: :: MATHMORP:62
for t being Real
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)
proof end;

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

theorem Th64: :: MATHMORP:64
for t being Real
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)
proof end;

theorem :: MATHMORP:65
for t being Real
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)
proof end;

theorem :: MATHMORP:66
for t being Real
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)
proof end;

:: Algebraic Properties.
:: "Hit or Miss" Transformation
definition
let T be non empty RLSStruct ;
let X, B1, B2 be Subset of T;
func X (*) (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;
func X (&) (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 (&) MATHMORP:def 8 :
for T being non empty RLSStruct
for X, B1, B2 being Subset of T holds X (&) (B1,B2) = X \/ (X (*) (B1,B2));

:: Thinning
definition
let T be non empty RLSStruct ;
let X, B1, B2 be Subset of T;
func X (@) (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 X, B1, B2 being Subset of (TOP-REAL n) st B1 = {} holds
X (*) (B1,B2) = (X `) (-) B2
proof end;

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

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

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

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

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

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

:: 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 st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B )
proof end;

definition
let V be RealLinearSpace;
let B be Subset of V;
redefine attr B is convex means :: MATHMORP:def 10
 for x, y being Point of V
for r being Real st 0 <= r & r <= 1 & x in B & 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 st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B ) by Th74;
end;

:: deftheorem 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 st 0 <= r & r <= 1 & x in B & 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
proof end;

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

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

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