:: Morphology for Image Processing, Part {I} :: by Hiroshi Yamazaki , Czes\l aw Byli\'nski and Katsumi Wasaki :: :: Received September 21, 2011 :: Copyright (c) 2011-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 TARSKI, RLVECT_1, FUNCT_1, ARYTM_1, RELAT_1, MATHMORP, SETFAM_1, ARYTM_3, ALGSTR_0, MORPH_01, ZFMISC_1, SUBSET_1, STRUCT_0, XBOOLE_0, REAL_1, SUPINF_2, VALUED_2; notations TARSKI, XBOOLE_0, ORDINAL1, SUBSET_1, SETFAM_1, FUNCT_1, FUNCT_2, XCMPLX_0, XREAL_0, REAL_1, STRUCT_0, ALGSTR_0, RLVECT_1, RUSUB_4, MATHMORP; constructors SETFAM_1, REAL_1, RUSUB_4, RVSUM_1, RELSET_1, MATHMORP; registrations SUBSET_1, RELSET_1, MEMBERED, STRUCT_0, RLVECT_1, XREAL_0; requirements NUMERALS, SUBSET, BOOLE; begin :: Minkowski set operations definition let E be non empty RLSStruct; mode binary-image of E is Subset of E; end; reserve E for RealLinearSpace; reserve A, B, C for binary-image of E; reserve a, b, v for Element of E; definition let E be RealLinearSpace; let A, B be binary-image of E; func A(-)B -> binary-image of E equals :: MORPH_01:def 1 { z where z is Element of E : for b be Element of E st b in B holds z - b in A }; end; notation let a be Real, E be RealLinearSpace, A be Subset of E; synonym a * A for a (.) A; end; theorem :: MORPH_01:1 for E be RealLinearSpace, A, B be Subset of E st B = {} holds A(+)B = B & B(+)A = B & A(-)B = the carrier of E; theorem :: MORPH_01:2 for E be RealLinearSpace, A, B be Subset of E st A <> {} & B = {} holds B(-)A = B; theorem :: MORPH_01:3 for E be RealLinearSpace, A, B be Subset of E st B = the carrier of E & A <> {} holds A(+)B = B & B(+)A = B; theorem :: MORPH_01:4 for E be RealLinearSpace, A, B be Subset of E st B = the carrier of E holds B(-)A = B; theorem :: MORPH_01:5 A(+)B = union {b + A where b is Element of E: b in B}; definition let E be non empty RLSStruct; mode binary-image-family of E is Subset-Family of the carrier of E; end; reserve F, G for binary-image-family of E; reserve A, B, C for non empty binary-image of E; theorem :: MORPH_01:6 A(-)B = meet {b + A where b is Element of E: b in B}; theorem :: MORPH_01:7 A(+)B = {v where v is Element of E: (v + (-1)*B) /\ A <> {}}; theorem :: MORPH_01:8 A(-)B = {v where v is Element of E: v + (-1)*B c= A}; theorem :: MORPH_01:9 ((the carrier of E) \ A)(+)B = (the carrier of E) \ (A(-)B) & ((the carrier of E) \ A)(-)B = (the carrier of E) \ (A(+)B); definition let E be non empty Abelian addLoopStr, A, B be Subset of E; redefine func A(+)B; commutativity; end; theorem :: MORPH_01:10 for E be non empty add-associative addLoopStr, A, B, C be Subset of E holds A + B + C = A + (B + C); theorem :: MORPH_01:11 A(+)B(+)C = A(+)(B(+)C); theorem :: MORPH_01:12 (union F)(+)B = union {X(+)B where X is binary-image of E: X in F}; theorem :: MORPH_01:13 A(+)(union F) = union {A(+)X where X is binary-image of E: X in F}; theorem :: MORPH_01:14 (meet F)(+)B c= meet {X(+)B where X is binary-image of E: X in F }; theorem :: MORPH_01:15 A(+)(meet F) c= meet { A(+)X where X is binary-image of E: X in F}; theorem :: MORPH_01:16 for E be non empty addLoopStr, A, B, C be Subset of E holds B c= C implies A + B c= A + C; theorem :: MORPH_01:17 (v + A)(+)B = A(+)(v+B) & (v+A)(+)B = v+ (A(+)B); theorem :: MORPH_01:18 (meet F)(-)B = meet { X(-)B where X is binary-image of E: X in F}; theorem :: MORPH_01:19 meet {B (-)X where X is binary-image of E: X in F} c= B(-)(meet F); theorem :: MORPH_01:20 union {X(-)B where X is binary-image of E: X in F} c= (union F)(-)B; theorem :: MORPH_01:21 F <> {} implies B(-) (union F) = meet {B(-)X where X is binary-image of E: X in F}; theorem :: MORPH_01:22 A c= B implies A(-)C c= B(-)C; theorem :: MORPH_01:23 A c= B implies C(-)B c= C(-)A; theorem :: MORPH_01:24 (v+A)(-)B = A(-)(v+B) & (v+A)(-)B = v+(A(-)B); theorem :: MORPH_01:25 (A(-)B)(-)C = A(-)(B(+)C); begin :: Dilation and erosion definition let E be RealLinearSpace; let B be binary-image of E; func dilation(B) -> Function of bool the carrier of E, bool the carrier of E means :: MORPH_01:def 2 for A be binary-image of E holds it.A = A(+)B; end; definition let E be RealLinearSpace; let B be binary-image of E; func erosion (B) -> Function of bool the carrier of E, bool the carrier of E means :: MORPH_01:def 3 for A be binary-image of E holds it.A = A(-)B; end; theorem :: MORPH_01:26 (dilation(B)).(union F) = union {(dilation(B)).X where X is binary-image of E: X in F}; theorem :: MORPH_01:27 A c= B implies (dilation(C)).A c= (dilation(C)).B; theorem :: MORPH_01:28 (dilation(C)).(v+A) = v+((dilation(C)).A); theorem :: MORPH_01:29 (erosion(B)).(meet F) = meet {(erosion(B)).X where X is binary-image of E: X in F}; theorem :: MORPH_01:30 A c= B implies (erosion(C)).A c= (erosion(C)).B; theorem :: MORPH_01:31 (erosion(C)).(v+A) = v+((erosion(C)).A); theorem :: MORPH_01:32 (dilation(C)).((the carrier of E) \ A) = (the carrier of E) \ ((erosion(C)).A) & (erosion(C)).( (the carrier of E) \ A) = (the carrier of E) \ ((dilation(C)).A ); theorem :: MORPH_01:33 (dilation(C)).((dilation(B)).A) = (dilation((dilation(C)).B)).A & (erosion(C)).((erosion(B)).A) = (erosion((dilation(C)).B)).A;