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

begin

definition

let n be Element of NAT ;
let p be Point of (TOP-REAL n);
let X be Subset of (TOP-REAL n);
func X + p -> Subset of (TOP-REAL n) equals :: MATHMORP:def 1
{ (q + p) where q is Point of (TOP-REAL n) : q in X } ;
coherence
{ (q + p) where q is Point of (TOP-REAL n) : q in X } is Subset of (TOP-REAL n)

proof end;

end;

:: deftheorem defines + MATHMORP:def 1 :

for n being Element of NAT
for p being Point of (TOP-REAL n)
for X being Subset of (TOP-REAL n) holds X + p = { (q + p) where q is Point of (TOP-REAL n) : q in X } ;

definition

let n be Element of NAT ;
let X be Subset of (TOP-REAL n);
func X ! -> Subset of (TOP-REAL n) equals :: MATHMORP:def 2
{ (- q) where q is Point of (TOP-REAL n) : q in X } ;
coherence
{ (- q) where q is Point of (TOP-REAL n) : q in X } is Subset of (TOP-REAL n)

proof end;

end;

:: deftheorem defines ! MATHMORP:def 2 :

for n being Element of NAT
for X being Subset of (TOP-REAL n) holds X ! = { (- q) where q is Point of (TOP-REAL n) : q in X } ;

definition

let n be Element of NAT ;
let X, B be Subset of (TOP-REAL n);
func X (-) B -> Subset of (TOP-REAL n) equals :: MATHMORP:def 3
{ y where y is Point of (TOP-REAL n) : B + y c= X } ;
coherence
{ y where y is Point of (TOP-REAL n) : B + y c= X } is Subset of (TOP-REAL n)

proof end;

end;

:: deftheorem defines (-) MATHMORP:def 3 :

for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds X (-) B = { y where y is Point of (TOP-REAL n) : B + y c= X } ;

definition

let n be Element of NAT ;
let X, B be Subset of (TOP-REAL n);
func X (+) B -> Subset of (TOP-REAL n) equals :: MATHMORP:def 4
{ (y + b) where y, b is Point of (TOP-REAL n) : ( y in X & b in B ) } ;
coherence
{ (y + b) where y, b is Point of (TOP-REAL n) : ( y in X & b in B ) } is Subset of (TOP-REAL n)

proof end;

end;

:: deftheorem defines (+) MATHMORP:def 4 :

for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds X (+) B = { (y + b) where y, b is Point of (TOP-REAL n) : ( y in X & b in B ) } ;

theorem Th1: :: MATHMORP:1

for n being Element of NAT
for B being Subset of (TOP-REAL n) holds (B ! ) ! = B

proof end;

theorem Th2: :: MATHMORP:2

for n being Element of NAT
for x being Point of (TOP-REAL n) holds {(0. (TOP-REAL n))} + x = {x}

proof end;

theorem Th3: :: MATHMORP:3

for n being Element of NAT
for B1, B2 being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) st B1 c= B2 holds
B1 + p c= B2 + p

proof end;

theorem Th4: :: MATHMORP:4

for n being Element of NAT
for x being Point of (TOP-REAL n)
for X being Subset of (TOP-REAL n) st X = {} holds
X + x = {}

proof end;

theorem :: MATHMORP:5

for n being Element of NAT
for X being Subset of (TOP-REAL n) holds X (-) {(0. (TOP-REAL n))} = X

proof end;

Lm1: for n being Element of NAT
for x, y being Point of (TOP-REAL n) holds {x} + y = {y} + x

proof end;

theorem :: MATHMORP:6

for n being Element of NAT
for X being Subset of (TOP-REAL n) holds X (+) {(0. (TOP-REAL n))} = X

proof end;

theorem :: MATHMORP:7

for n being Element of NAT
for X being Subset of (TOP-REAL n)
for x being Point of (TOP-REAL n) holds X (+) {x} = X + x

proof end;

theorem Th8: :: MATHMORP:8

for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) st Y = {} holds
X (-) Y = REAL n

proof end;

theorem Th9: :: MATHMORP:9

for n being Element of NAT
for X, Y, B being Subset of (TOP-REAL n) st X c= Y holds
( X (-) B c= Y (-) B & X (+) B c= Y (+) B )

proof end;

theorem Th10: :: MATHMORP:10

for n being Element of NAT
for B1, B2, X being Subset of (TOP-REAL n) st B1 c= B2 holds
( X (-) B2 c= X (-) B1 & X (+) B1 c= X (+) B2 )

proof end;

theorem :: MATHMORP:11

for n being Element of NAT
for B, X being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B holds
( X (-) B c= X & X c= X (+) B )

proof end;

theorem Th12: :: MATHMORP:12

for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) holds X (+) Y = Y (+) X

proof end;

theorem Th13: :: MATHMORP:13

for n being Element of NAT
for Y, X being Subset of (TOP-REAL n)
for y, x being Point of (TOP-REAL n) holds
( Y + y c= X + x iff Y + (y - x) c= X )

proof end;

theorem Th14: :: MATHMORP:14

for n being Element of NAT
for X, Y being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) holds (X + p) (-) Y = (X (-) Y) + p

proof end;

theorem Th15: :: MATHMORP:15

for n being Element of NAT
for X, Y being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) holds (X + p) (+) Y = (X (+) Y) + p

proof end;

theorem Th16: :: MATHMORP:16

for n being Element of NAT
for X being Subset of (TOP-REAL n)
for x, y being Point of (TOP-REAL n) holds (X + x) + y = X + (x + y)

proof end;

theorem Th17: :: MATHMORP:17

for n being Element of NAT
for X, Y being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) holds X (-) (Y + p) = (X (-) Y) + (- p)

proof end;

theorem :: MATHMORP:18

for n being Element of NAT
for X, Y being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) holds X (+) (Y + p) = (X (+) Y) + p

proof end;

theorem Th19: :: MATHMORP:19

for n being Element of NAT
for X, B being Subset of (TOP-REAL n)
for x being Point of (TOP-REAL n) st x in X holds
B + x c= B (+) X

proof end;

theorem Th20: :: MATHMORP:20

for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds X c= (X (+) B) (-) B

proof end;

theorem Th21: :: MATHMORP:21

for n being Element of NAT
for X being Subset of (TOP-REAL n) holds X + (0. (TOP-REAL n)) = X

proof end;

theorem :: MATHMORP:22

for n being Element of NAT
for X being Subset of (TOP-REAL n)
for x being Point of (TOP-REAL n) holds X (-) {x} = X + (- x)

proof end;

Lm2: for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds (X (-) B) (+) B c= X

proof end;

theorem Th23: :: MATHMORP:23

for n being Element of NAT
for X, Y, Z being Subset of (TOP-REAL n) holds X (-) (Y (+) Z) = (X (-) Y) (-) Z

proof end;

theorem :: MATHMORP:24

for n being Element of NAT
for X, Y, Z being Subset of (TOP-REAL n) holds X (-) (Y (+) Z) = (X (-) Z) (-) Y

proof end;

theorem :: MATHMORP:25

for n being Element of NAT
for X, Y, Z being Subset of (TOP-REAL n) holds X (+) (Y (-) Z) c= (X (+) Y) (-) Z

proof end;

theorem :: MATHMORP:26

for n being Element of NAT
for X, Y, Z being Subset of (TOP-REAL n) holds X (+) (Y (+) Z) = (X (+) Y) (+) Z

proof end;

theorem Th27: :: MATHMORP:27

for n being Element of NAT
for B, C being Subset of (TOP-REAL n)
for y being Point of (TOP-REAL n) holds (B \/ C) + y = (B + y) \/ (C + y)

proof end;

theorem Th28: :: MATHMORP:28

for n being Element of NAT
for B, C being Subset of (TOP-REAL n)
for y being Point of (TOP-REAL n) holds (B /\ C) + y = (B + y) /\ (C + y)

proof end;

theorem :: MATHMORP:29

for n being Element of NAT
for X, B, C being Subset of (TOP-REAL n) holds X (-) (B \/ C) = (X (-) B) /\ (X (-) C)

proof end;

theorem :: MATHMORP:30

for n being Element of NAT
for X, B, C being Subset of (TOP-REAL n) holds X (+) (B \/ C) = (X (+) B) \/ (X (+) C)

proof end;

theorem :: MATHMORP:31

for n being Element of NAT
for X, B, Y being Subset of (TOP-REAL n) holds (X (-) B) \/ (Y (-) B) c= (X \/ Y) (-) B

proof end;

theorem :: MATHMORP:32

for n being Element of NAT
for X, Y, B being Subset of (TOP-REAL n) holds (X \/ Y) (+) B = (X (+) B) \/ (Y (+) B)

proof end;

theorem :: MATHMORP:33

for n being Element of NAT
for X, Y, B being Subset of (TOP-REAL n) holds (X /\ Y) (-) B = (X (-) B) /\ (Y (-) B)

proof end;

theorem Th34: :: MATHMORP:34

for n being Element of NAT
for X, Y, B being Subset of (TOP-REAL n) holds (X /\ Y) (+) B c= (X (+) B) /\ (Y (+) B)

proof end;

theorem :: MATHMORP:35

for n being Element of NAT
for B, X, Y being Subset of (TOP-REAL n) holds B (+) (X /\ Y) c= (B (+) X) /\ (B (+) Y)

proof end;

theorem :: MATHMORP:36

for n being Element of NAT
for B, X, Y being Subset of (TOP-REAL n) holds (B (-) X) \/ (B (-) Y) c= B (-) (X /\ Y)

proof end;

theorem Th37: :: MATHMORP:37

for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds ((X ` ) (-) B) ` = X (+) (B ! )

proof end;

theorem Th38: :: MATHMORP:38

for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds (X (-) B) ` = (X ` ) (+) (B ! )

proof end;

begin

definition

let n be Element of NAT ;
let X, B be Subset of (TOP-REAL n);
func X (O) B -> Subset of (TOP-REAL n) equals :: MATHMORP:def 5
(X (-) B) (+) B;
coherence
(X (-) B) (+) B is Subset of (TOP-REAL n) ;

end;

:: deftheorem defines (O) MATHMORP:def 5 :

for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds X (O) B = (X (-) B) (+) B;

definition

let n be Element of NAT ;
let X, B be Subset of (TOP-REAL n);
func X (o) B -> Subset of (TOP-REAL n) equals :: MATHMORP:def 6
(X (+) B) (-) B;
coherence
(X (+) B) (-) B is Subset of (TOP-REAL n) ;

end;

:: deftheorem defines (o) MATHMORP:def 6 :

for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds X (o) B = (X (+) B) (-) B;

theorem :: MATHMORP:39

for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds ((X ` ) (O) (B ! )) ` = X (o) B

proof end;

theorem :: MATHMORP:40

for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds ((X ` ) (o) (B ! )) ` = X (O) B

proof end;

theorem Th41: :: MATHMORP:41

for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds
( X (O) B c= X & X c= X (o) B )

proof end;

theorem Th42: :: MATHMORP:42

for n being Element of NAT
for X being Subset of (TOP-REAL n) holds X (O) X = X

proof end;

theorem :: MATHMORP:43

for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds
( (X (O) B) (-) B c= X (-) B & (X (O) B) (+) B c= X (+) B )

proof end;

theorem :: MATHMORP:44

for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds
( X (-) B c= (X (o) B) (-) B & X (+) B c= (X (o) B) (+) B )

proof end;

theorem Th45: :: MATHMORP:45

for n being Element of NAT
for X, Y, B being Subset of (TOP-REAL n) 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 n being Element of NAT
for X, Y being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) holds (X + p) (O) Y = (X (O) Y) + p

proof end;

theorem :: MATHMORP:47

for n being Element of NAT
for X, Y being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) holds (X + p) (o) Y = (X (o) Y) + p

proof end;

theorem :: MATHMORP:48

for n being Element of NAT
for C, B, X being Subset of (TOP-REAL n) st C c= B holds
X (O) B c= (X (-) C) (+) B

proof end;

theorem :: MATHMORP:49

for n being Element of NAT
for B, C, X being Subset of (TOP-REAL n) st B c= C holds
X (o) B c= (X (+) C) (-) B

proof end;

theorem Th50: :: MATHMORP:50

for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) holds
( X (+) Y = (X (o) Y) (+) Y & X (-) Y = (X (O) Y) (-) Y )

proof end;

theorem :: MATHMORP:51

for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) holds
( X (+) Y = (X (+) Y) (O) Y & X (-) Y = (X (-) Y) (o) Y )

proof end;

theorem :: MATHMORP:52

for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds (X (O) B) (O) B = X (O) B

proof end;

theorem :: MATHMORP:53

for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds (X (o) B) (o) B = X (o) B by Th50;

theorem :: MATHMORP:54

for n being Element of NAT
for X, B, Y being Subset of (TOP-REAL n) holds X (O) B c= (X \/ Y) (O) B

proof end;

theorem :: MATHMORP:55

for n being Element of NAT
for B, B1, X being Subset of (TOP-REAL n) st B = B (O) B1 holds
X (O) B c= X (O) B1

proof end;

begin

definition

let t be real number ;
let n be Element of NAT ;
let A be Subset of (TOP-REAL n);
func t (.) A -> Subset of (TOP-REAL n) equals :: MATHMORP:def 7
{ (t * a) where a is Point of (TOP-REAL n) : a in A } ;
coherence
{ (t * a) where a is Point of (TOP-REAL n) : a in A } is Subset of (TOP-REAL n)

proof end;

end;

:: deftheorem defines (.) MATHMORP:def 7 :

for t being real number
for n being Element of NAT
for A being Subset of (TOP-REAL n) holds t (.) A = { (t * a) where a is Point of (TOP-REAL n) : a in A } ;

theorem :: MATHMORP:56

for n being Element of NAT
for X being Subset of (TOP-REAL n) 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 n being Element of NAT
for X being Subset of (TOP-REAL n)
for t, s being real number holds (t * s) (.) X = t (.) (s (.) X)

proof end;

theorem Th61: :: MATHMORP:61

for n being Element of NAT
for X, Y being Subset of (TOP-REAL n)
for t being real number st X c= Y holds
t (.) X c= t (.) Y

proof end;

theorem Th62: :: MATHMORP:62

for n being Element of NAT
for X being Subset of (TOP-REAL n)
for x being Point of (TOP-REAL n)
for t being real number holds t (.) (X + x) = (t (.) X) + (t * x)

proof end;

theorem Th63: :: MATHMORP:63

for n being Element of NAT
for X, Y being Subset of (TOP-REAL n)
for t being real number holds t (.) (X (+) Y) = (t (.) X) (+) (t (.) Y)

proof end;

theorem Th64: :: MATHMORP:64

for n being Element of NAT
for X, Y being Subset of (TOP-REAL n)
for t being real number st t <> 0 holds
t (.) (X (-) Y) = (t (.) X) (-) (t (.) Y)

proof end;

theorem :: MATHMORP:65

for n being Element of NAT
for X, Y being Subset of (TOP-REAL n)
for t being real number st t <> 0 holds
t (.) (X (O) Y) = (t (.) X) (O) (t (.) Y)

proof end;

theorem :: MATHMORP:66

for n being Element of NAT
for X, Y being Subset of (TOP-REAL n)
for t being real number st t <> 0 holds
t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y)

proof end;

begin

definition

let n be Element of NAT ;
let X, B1, B2 be Subset of (TOP-REAL n);
func X (*) B1,B2 -> Subset of (TOP-REAL n) equals :: MATHMORP:def 8
(X (-) B1) /\ ((X ` ) (-) B2);
coherence
(X (-) B1) /\ ((X ` ) (-) B2) is Subset of (TOP-REAL n) ;

end;

:: deftheorem defines (*) MATHMORP:def 8 :

for n being Element of NAT
for X, B1, B2 being Subset of (TOP-REAL n) holds X (*) B1,B2 = (X (-) B1) /\ ((X ` ) (-) B2);

definition

let n be Element of NAT ;
let X, B1, B2 be Subset of (TOP-REAL n);
func X (&) B1,B2 -> Subset of (TOP-REAL n) equals :: MATHMORP:def 9
X \/ (X (*) B1,B2);
coherence
X \/ (X (*) B1,B2) is Subset of (TOP-REAL n) ;

end;

:: deftheorem defines (&) MATHMORP:def 9 :

for n being Element of NAT
for X, B1, B2 being Subset of (TOP-REAL n) holds X (&) B1,B2 = X \/ (X (*) B1,B2);

definition

let n be Element of NAT ;
let X, B1, B2 be Subset of (TOP-REAL n);
func X (@) B1,B2 -> Subset of (TOP-REAL n) equals :: MATHMORP:def 10
X \ (X (*) B1,B2);
coherence
X \ (X (*) B1,B2) is Subset of (TOP-REAL n) ;

end;

:: deftheorem defines (@) MATHMORP:def 10 :

for n being Element of NAT
for X, B1, B2 being Subset of (TOP-REAL n) holds X (@) B1,B2 = X \ (X (*) B1,B2);

theorem :: MATHMORP:67

for n being Element of NAT
for B1, X, 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 B2, X, B1 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 B1, X, 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 B2, X, B1 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 B1, X, 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 B2, X, B1 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B2 holds
X (@) B1,B2 = X

proof end;

theorem :: MATHMORP:73

canceled;

theorem :: MATHMORP:74

for n being Element of NAT
for X, B2, B1 being Subset of (TOP-REAL n) holds X (@) B2,B1 = ((X ` ) (&) B1,B2) `

proof end;

begin

theorem Th75: :: MATHMORP:75

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 number 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 :Def11: :: MATHMORP:def 11
for x, y being Point of V
for r being real number 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 number st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B ) by Th75;

end;

:: deftheorem Def11 defines convex MATHMORP:def 11 :

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

theorem :: MATHMORP:76

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 Th77: :: 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 (+) B is convex & X (-) B is convex )

proof end;

theorem :: MATHMORP:78

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

for n being Element of NAT
for B being Subset of (TOP-REAL n)
for t, s being real number st B is convex & 0 < t & 0 < s holds
(s + t) (.) B = (s (.) B) (+) (t (.) B)

proof end;