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