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