:: Preliminaries to Mathematical Morphology and Its Properties
:: by Yuzhong Ding and Xiquan Liang
::
:: Received January 7, 2005
:: Copyright (c) 2005-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, ARYTM_3, STRUCT_0, REALSET1,
ARYTM_1, VALUED_2, TARSKI, SUPINF_2, XBOOLE_0, RELAT_1, CARD_1, MONOID_0,
RLVECT_1, CONVEX1, XXREAL_0, REAL_1, RLTOPSP1, MATHMORP, ALGSTR_0;
notations TARSKI, ORDINAL1, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XXREAL_0,
DOMAIN_1, STRUCT_0, ALGSTR_0, PRE_TOPC, XREAL_0, REAL_1, RLVECT_1,
RLTOPSP1, EUCLID, RUSUB_4;
constructors DOMAIN_1, REAL_1, JORDAN1, CONVEX1, BINOP_2, RUSUB_4;
registrations XXREAL_0, XREAL_0, STRUCT_0, EUCLID, RLVECT_1, ORDINAL1;
requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
begin :: 1. The definition of Erosion and Dilation and their
:: Algebraic Properties
:: Translation of X according to p
definition
let T be non empty addMagma, p be Element of T, 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};
end;
:: Reflected of X
definition
let T be non empty addLoopStr, X be Subset of T;
func X! -> Subset of T equals
:: MATHMORP:def 2
{-q where q is Point of T : q in X};
end;
:: Set Erosion
definition
let T be non empty addMagma, 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};
end;
:: Set Dilation
notation
let T be non empty addLoopStr;
let A, B be Subset of T;
synonym A(+)B for A + B;
end;
reserve T for non empty Abelian
add-associative right_zeroed right_complementable RLSStruct,
X,Y,Z,B,C,B1,B2 for Subset of T,
x,y,p for Point of T;
theorem :: MATHMORP:1
for T being add-associative right_zeroed right_complementable
non empty RLSStruct,
B being Subset of T holds
(B!)! = B;
theorem :: MATHMORP:2
{0.T} + x = {x};
theorem :: MATHMORP:3
B1 c= B2 implies B1+p c= B2+p;
theorem :: MATHMORP:4
for X st X = {} holds X+x = {};
theorem :: MATHMORP:5
X (-) {0.T} = X;
theorem :: MATHMORP:6
X (+) {0.T} = X;
theorem :: MATHMORP:7
X (+) {x} = X+x;
theorem :: MATHMORP:8
for X,Y st Y = {} holds X (-) Y = the carrier of T;
theorem :: MATHMORP:9
X c= Y implies X (-) B c= Y (-) B & X (+) B c= Y (+) B;
theorem :: MATHMORP:10
B1 c= B2 implies X (-) B2 c= X (-) B1 & X (+) B1 c= X (+) B2;
theorem :: MATHMORP:11
0.T in B implies X (-) B c= X & X c= X (+) B;
theorem :: MATHMORP:12
X (+) Y = Y (+) X;
theorem :: MATHMORP:13
Y+y c= X+x iff Y+(y-x) c= X;
theorem :: MATHMORP:14
(X+p) (-) Y = (X (-) Y)+p;
theorem :: MATHMORP:15
(X+p) (+) Y = (X (+) Y)+p;
theorem :: MATHMORP:16
(X+x)+y = X+(x+y);
theorem :: MATHMORP:17
X (-) (Y+p) = (X (-) Y)+(-p);
theorem :: MATHMORP:18
X (+) (Y+p) = (X (+) Y)+p;
theorem :: MATHMORP:19
x in X implies B+x c= B (+) X;
theorem :: MATHMORP:20
X c= (X (+) B) (-) B;
theorem :: MATHMORP:21
X+0.T = X;
theorem :: MATHMORP:22
X (-) {x} = X+(-x);
theorem :: MATHMORP:23
X (-) (Y (+) Z) = (X (-) Y) (-) Z;
theorem :: MATHMORP:24
X (-) (Y (+) Z) = (X (-) Z) (-) Y;
theorem :: MATHMORP:25
X (+) (Y (-) Z) c= (X (+) Y) (-) Z;
theorem :: MATHMORP:26
X (+) (Y (+) Z) = (X (+) Y) (+) Z;
theorem :: MATHMORP:27
(B\/C)+y = (B+y) \/ (C+y);
theorem :: MATHMORP:28
(B/\C)+y = (B+y) /\ (C+y);
theorem :: MATHMORP:29
X (-) (B\/C) = (X (-) B)/\(X (-) C);
theorem :: MATHMORP:30
X (+) (B\/C) = (X (+) B)\/(X (+) C);
theorem :: MATHMORP:31
(X (-) B)\/(Y (-) B) c= (X\/Y) (-) B;
theorem :: MATHMORP:32
(X\/Y) (+) B = (X (+) B)\/(Y (+) B);
theorem :: MATHMORP:33
(X/\Y) (-) B = (X (-) B)/\(Y (-) B);
theorem :: MATHMORP:34
(X/\Y) (+) B c= (X (+) B)/\(Y (+) B);
theorem :: MATHMORP:35
B (+) (X/\Y) c= (B (+) X)/\(B (+) Y);
theorem :: MATHMORP:36
(B (-) X)\/(B (-) Y) c= B (-) (X/\Y);
theorem :: MATHMORP:37
(X` (-) B)` = X (+) B!;
theorem :: MATHMORP:38
(X (-) B)` = X` (+) B!;
begin
:: 2. The definition of Adjunction Opening and Closing and
:: their Algebraic Properties
:: Adjunction Opening
definition
let T be non empty addLoopStr,X,B be Subset of T;
func X (O) B -> Subset of T equals
:: MATHMORP:def 4
(X (-) B) (+) B;
end;
:: Adjunction Closing
definition
let T be non empty addLoopStr,X,B be Subset of T;
func X (o) B -> Subset of T equals
:: MATHMORP:def 5
(X (+) B) (-) B;
end;
theorem :: MATHMORP:39
(X` (O) B!)` = X (o) B;
theorem :: MATHMORP:40
(X` (o) B!)` = X (O) B;
theorem :: MATHMORP:41
X (O) B c= X & X c= X (o) B;
theorem :: MATHMORP:42
X (O) X = X;
theorem :: MATHMORP:43
(X (O) B) (-) B c= X (-) B & (X (O) B) (+) B c= X (+) B;
theorem :: MATHMORP:44
X (-) B c= (X (o) B) (-) B & X (+) B c= (X (o) B) (+) B;
theorem :: MATHMORP:45
X c= Y implies X (O) B c= Y (O) B & X (o) B c= Y (o) B;
theorem :: MATHMORP:46
(X+p) (O) Y = (X (O) Y)+p;
theorem :: MATHMORP:47
(X+p) (o) Y = (X (o) Y)+p;
theorem :: MATHMORP:48
C c= B implies X (O) B c= (X (-) C) (+) B;
theorem :: MATHMORP:49
B c= C implies X (o) B c= (X (+) C) (-) B;
theorem :: MATHMORP:50
X (+) Y = (X (o) Y) (+) Y & X (-) Y = (X (O) Y) (-) Y;
theorem :: MATHMORP:51
X (+) Y = (X (+) Y) (O) Y & X (-) Y = (X (-) Y) (o) Y;
theorem :: MATHMORP:52
(X (O) B) (O) B = X (O) B;
theorem :: MATHMORP:53
(X (o) B) (o) B = X (o) B;
theorem :: MATHMORP:54
X (O) B c= (X \/ Y) (O) B;
theorem :: MATHMORP:55
B = B (O) B1 implies X (O) B c= X (O) B1;
begin
:: 3.The definition of Scaling transformation and its Algebraic Properties
:: Scaling transformation
definition
let t be Real, T be non empty RLSStruct,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};
end;
reserve t,s,r1 for Real;
theorem :: MATHMORP:56
for X being Subset of T st X = {} holds 0(.)X = {};
reserve n for Element of NAT;
reserve X,Y,B1,B2 for Subset of TOP-REAL n;
reserve x,y for Point of TOP-REAL n;
theorem :: MATHMORP:57
for X being non empty Subset of TOP-REAL n holds 0(.)X = {0.TOP-REAL n};
theorem :: MATHMORP:58
1(.)X = X;
theorem :: MATHMORP:59
2(.)X c= X (+) X;
theorem :: MATHMORP:60
(t*s)(.)X = t(.)(s(.)X);
theorem :: MATHMORP:61
X c= Y implies t(.)X c= t(.)Y;
theorem :: MATHMORP:62
t(.)(X+x) = t(.)X+t*x;
theorem :: MATHMORP:63
t(.)(X (+) Y) = t(.)X (+) t(.)Y;
theorem :: MATHMORP:64
t<>0 implies t(.)(X (-) Y) = t(.)X (-) t(.)Y;
theorem :: MATHMORP:65
t<>0 implies t(.)(X (O) Y) = t(.)X (O) t(.)Y;
theorem :: MATHMORP:66
t<>0 implies t(.)(X (o) Y) = t(.)X (o) t(.)Y;
begin :: 4. The definition of Thinning and Thickening and their
:: Algebraic Properties.
:: "Hit or Miss" Transformation
definition
let T be non empty RLSStruct,X,B1,B2 be Subset of T;
func X (*) (B1,B2) -> Subset of T equals
:: MATHMORP:def 7
(X (-) B1) /\ (X` (-) B2);
end;
:: Thickening
definition
let T be non empty RLSStruct,X,B1,B2 be Subset of T;
func X (&) (B1,B2) -> Subset of T equals
:: MATHMORP:def 8
X \/ (X (*) (B1,B2));
end;
:: Thinning
definition
let T be non empty RLSStruct,X,B1,B2 be Subset of T;
func X (@) (B1,B2) -> Subset of T equals
:: MATHMORP:def 9
X \ (X (*) (B1,B2));
end;
theorem :: MATHMORP:67
B1 = {} implies X (*) (B1,B2) = X` (-) B2;
theorem :: MATHMORP:68
B2 = {} implies X (*) (B1,B2) = X (-) B1;
theorem :: MATHMORP:69
0.TOP-REAL n in B1 implies X (*) (B1,B2) c= X;
theorem :: MATHMORP:70
0.TOP-REAL n in B2 implies (X (*) (B1,B2)) /\ X = {};
theorem :: MATHMORP:71
0.TOP-REAL n in B1 implies X (&) (B1,B2) = X;
theorem :: MATHMORP:72
0.TOP-REAL n in B2 implies X (@) (B1,B2) = X;
theorem :: MATHMORP:73
X (@) (B2,B1) = (X` (&) (B1,B2))`;
begin :: 5. Properties of Erosion, Dilation, Adjunction Opening,
:: Adjunction Closing on Convex sets
theorem :: MATHMORP:74
for V being RealLinearSpace, B being Subset of V holds
B is convex iff
for x,y be Point of V,r be Real st 0 <= r & r <= 1 & x in B &
y in B holds r*x + (1-r)*y in B;
definition
let V be RealLinearSpace, B be Subset of V;
redefine attr B is convex means
:: MATHMORP:def 10
for x,y be Point of V,r be Real st
0 <= r & r <= 1 & x in B & y in B holds r*x + (1-r)*y in B;
end;
reserve n for Element of NAT;
reserve X,B for Subset of TOP-REAL n;
theorem :: MATHMORP:75
X is convex implies X! is convex;
theorem :: MATHMORP:76
X is convex & B is convex implies X (+) B is convex & X (-) B is convex;
theorem :: MATHMORP:77
X is convex & B is convex implies X (O) B is convex & X (o) B is convex;
theorem :: MATHMORP:78
B is convex & 0 < t & 0 < s implies (s+t)(.)B = s(.)B (+) t(.)B;