:: Morphology for Image Processing, Part {I}
:: by Hiroshi Yamazaki , Czes\l aw Byli\'nski and Katsumi Wasaki
::
:: Received September 21, 2011
:: Copyright (c) 2011-2026 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;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, RLVECT_1, RUSUB_4, MATHMORP;
expansions TARSKI, XBOOLE_0;
theorems SUBSET_1, RLVECT_1, TARSKI, ZFMISC_1, XBOOLE_0, SETFAM_1, RUSUB_5,
XBOOLE_1, FUNCT_2, RLVECT_4;
schemes FUNCT_2;
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
{ z where z is Element of E :
for b be Element of E st b in B holds z - b in A };
correctness
proof
now let x be object;
assume x in {z where z is Element of E : for b be Element of E
st b in B holds z - b in A}; then
ex z be Element of E st x=z &
for b be Element of E st b in B holds z - b in A;
hence x in the carrier of E;
end;
hence thesis by TARSKI:def 3;
end;
end;
notation
let a be Real, E be RealLinearSpace,
A be Subset of E;
synonym a * A for a (.) A;
end;
theorem Th1:
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
proof
let E be RealLinearSpace,
A, B be Subset of E;
assume A1: B = {};
hence A(+)B = B & B(+)A = B by RUSUB_5:5;
now let x be object;
assume x in the carrier of E;
then reconsider z = x as Element of E;
for b be Element of E st b in B
holds z - b in A by A1;
hence x in A(-)B;
end;
then the carrier of E c= A(-)B;
hence the carrier of E = A(-)B;
end;
theorem Th2:
for E be RealLinearSpace, A, B be Subset of E st A <> {} & B = {}
holds B(-)A = B
proof
let E be RealLinearSpace,
A, B be Subset of E;
assume
A1: A <> {} & B = {};
then consider a be object such that
A2: a in A by XBOOLE_0:def 1;
reconsider a as Element of E by A2;
assume B(-)A <> B;
then consider ba be object such that
A3: ba in B(-)A by A1,XBOOLE_0:def 1;
consider z be Element of E such that
A4: ba = z & for a be Element of E st a in A holds z - a in B by A3;
thus contradiction by A1,A2,A4;
end;
theorem Th3:
for E be RealLinearSpace,
A, B be Subset of E st B = the carrier of E & A <> {}
holds A(+)B = B & B(+)A = B
proof
let E be RealLinearSpace, A, B be Subset of E;
assume
A1: B = the carrier of E & A <> {};
then consider a be object such that
A2: a in A by XBOOLE_0:def 1;
reconsider a as Element of E by A2;
now let x be object;
assume x in the carrier of E;
then reconsider z = x as Element of E;
a+(z-a) =z by RLVECT_4:1;
hence x in A(+)B by A1,A2;
end;
then
A3: the carrier of E c= A(+)B;
hence B = A(+)B by A1;
thus B(+)A = A + B
.= B by A3,A1;
end;
theorem Th4:
for E be RealLinearSpace,
A, B be Subset of E st B = the carrier of E
holds B(-)A = B
proof
let E be RealLinearSpace, A,B be Subset of E;
assume
A1: B = the carrier of E;
now let x be object;
assume x in the carrier of E;
then reconsider z = x as Element of E;
for a be Element of E st a in A holds z-a in B by A1;
hence x in B(-)A;
end;
then the carrier of E c= B(-)A;
hence B = B(-)A by A1;
end;
theorem
A(+)B = union {b + A where b is Element of E: b in B}
proof
now let x be object;
assume
A1: x in A(+)B;
consider a0, b0 be Element of E such that
A2: x = a0 + b0 & a0 in A & b0 in B by A1;
A3: x in b0 + A by A2;
b0 + A in {b + A where b is Element of E: b in B} by A2;
hence x in union {b + A where b is Element of E: b in B}
by A3,TARSKI:def 4;
end;
hence
A(+)B c= union {b + A where b is Element of E: b in B};
now let x be object;
assume x in union {b + A where b is Element of E: b in B};
then consider y be set such that
A4: x in y & y in {b + A where b is Element of E: b in B}
by TARSKI:def 4;
consider b be Element of E such that
A5: y = b + A & b in B by A4;
consider a be Element of E such that
A6: x = b + a & a in A by A5,A4;
thus x in A(+)B by A5,A6;
end;
hence thesis;
end;
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
A(-)B = meet {b + A where b is Element of E: b in B}
proof
consider g be object such that
A1: g in B by XBOOLE_0:def 1;
reconsider g as Element of E by A1;
A2: g+A in {b + A where b is Element of E: b in B} by A1;
now let x be object;
assume x in A(-)B; then
consider z be Element of E such that
A3: x = z & for b be Element of E st b in B
holds z - b in A;
for Y be set st Y in {b + A where b is Element of E: b in B}
holds z in Y
proof
let Y be set;
assume Y in {b + A where b is Element of E: b in B};
then
consider b be Element of E such that
A4: Y = b + A & b in B;
A5: z - b in A by A3,A4;
z = b + (z- b) by RLVECT_4:1;
hence z in Y by A5,A4;
end;
hence x in meet {b + A where b is Element of E: b in B}
by A3,A2,SETFAM_1:def 1;
end;
hence A(-)B c= meet {b + A where b is Element of E: b in B};
now let x be object;
assume
A6: x in meet {b + A where b is Element of E: b in B};
consider S be set such that
A7: S in {b + A where b is Element of E: b in B} by A2;
consider d be Element of E such that
A8: S = d + A & d in B by A7;
x in S by A6,A7,SETFAM_1:def 1;
then
reconsider x0 = x as Element of E by A8;
for b be Element of E st b in B holds x0 - b in A
proof
let b be Element of E;
assume b in B;
then b + A in {f + A where f is Element of E :f in B};
then x in b + A by A6,SETFAM_1:def 1;
then consider a be Element of E such that
A9: x0 = b + a & a in A;
thus thesis by A9,RLVECT_4:1;
end;
hence x in A(-)B;
end;
hence meet {b + A where b is Element of E: b in B} c= A(-)B;
end;
theorem Th7:
A(+)B = {v where v is Element of E: (v + (-1)*B) /\ A <> {}}
proof
thus A(+)B c= {v where v is Element of E: (v + (-1)*B ) /\ A <> {}}
proof let x be object;
assume
A1: x in A(+)B;
consider a0,b0 be Element of E such that
A2: x = a0 + b0 & a0 in A & b0 in B by A1;
reconsider v = x as Element of E by A1;
A3: v - b0 = a0 by A2,RLVECT_4:1;
(-1)*b0 in (-1)*B by A2;
then v + (-1)*b0 in v + (-1)*B;
then v - b0 in v + (-1)*B by RLVECT_1:16;
then (v + (-1)*B) /\ A <> {} by A2,A3,XBOOLE_0:def 4;
hence x in {w where w is Element of E: (w + (-1)*B) /\ A <> {}};
end;
let x be object;
assume x in {v where v is Element of E: (v + (-1)*B) /\ A <> {}};
then
consider v be Element of E such that
A4: x = v & (v + (-1)*B ) /\ A <> {};
consider y be object such that
A5: y in ((v + (-1)*B) /\ A) by A4,XBOOLE_0:def 1;
A6: y in (v + (-1)*B ) & y in A by A5,XBOOLE_0:def 4;
then
consider nb be Element of E such that
A7: y = v + nb & nb in (-1)*B;
consider b be Element of E such that
A8: nb = (-1)*b & b in B by A7;
reconsider a = y as Element of E by A7;
a + b = v - b + b by A7,A8,RLVECT_1:16
.= v by RLVECT_4:1;
hence x in A(+)B by A4,A8,A6;
end;
theorem Th8:
A(-)B = {v where v is Element of E: v + (-1)*B c= A}
proof
thus A(-)B c= {v where v is Element of E: v + (-1)*B c= A}
proof let x be object;
assume x in A(-)B; then
consider z be Element of E such that
A1: x = z & for b be Element of E st b in B holds z - b in A;
z + (-1)*B c= A
proof
let y be object;
assume y in z + (-1)*B;
then consider nb be Element of E such that
A2: y = z + nb & nb in (-1)*B;
consider b be Element of E such that
A3: nb = (-1)*b & b in B by A2;
z - b in A by A3,A1;
hence y in A by A2,A3,RLVECT_1:16;
end;
hence x in {v where v is Element of E: v + (-1)*B c= A} by A1;
end;
let x be object;
assume x in {v where v is Element of E: v + (-1)*B c= A};
then consider v be Element of E such that
A4: x = v & v + (-1)*B c= A;
for b be Element of E st b in B holds v - b in A
proof
let b be Element of E;
assume b in B;
then (-1)*b in (-1)*B;
then v + (-1)*b in v + (-1)*B;
then v-b in v + (-1)*B by RLVECT_1:16;
hence thesis by A4;
end;
hence x in A(-)B by A4;
end;
theorem Th9:
((the carrier of E) \ A)(+)B = (the carrier of E) \ (A(-)B)
& ((the carrier of E) \ A)(-)B = (the carrier of E) \ (A(+)B)
proof
per cases;
suppose
A1: A = the carrier of E;
reconsider X = {} as Subset of E by XBOOLE_1:2;
thus ((the carrier of E) \ A)(+)B = X(+)B by A1,XBOOLE_1:37
.= {} by Th1
.= (the carrier of E) \ (the carrier of E) by XBOOLE_1:37
.= (the carrier of E) \ (A(-)B) by A1,Th4;
thus ((the carrier of E) \ A) (-)B = X(-)B by A1,XBOOLE_1:37
.= {} by Th2
.= (the carrier of E) \ (the carrier of E) by XBOOLE_1:37
.= (the carrier of E) \ (A(+)B) by A1,Th3;
end;
suppose
A2: A <> the carrier of E;
A3: (the carrier of E) \ A is non empty
by XBOOLE_1:37,A2;
A4: for x be object holds x in {v where v is Element of E:
(v + (-1)*B) /\ ((the carrier of E) \ A) <> {}}
iff x in (the carrier of E)
& not x in ({v where v is Element of E: v + (-1)*B c= A })
proof
let x be object;
hereby
assume x in {v where v is Element of E:
(v + (-1)*B) /\ ( (the carrier of E) \ A) <> {}};
then
consider v be Element of E such that
A5: x=v & (v + (-1)*B) /\ ((the carrier of E) \ A) <> {};
thus x in (the carrier of E) by A5;
thus not x in ({ w where w is Element of E: w + (-1)*B c= A })
proof
assume x in ({w where w is Element of E: w + (-1)*B c= A});
then
consider w be Element of E such that
A6: w = x & w + (-1)*B c= A;
(v + (-1)*B) misses ((the carrier of E) \ A)
by A5,A6,XBOOLE_1:85;
hence contradiction by A5;
end;
end;
assume
A7: x in (the carrier of E)
& not x in ({v where v is Element of E: v + (-1)*B c= A });
then
reconsider w=x as Element of E;
now assume (w + (-1)*B) /\ ((the carrier of E) \ A) = {};
then {} = ((w + (-1)*B) /\ (the carrier of E)) \ A by XBOOLE_1:49
.= (w + (-1)*B) \ A by XBOOLE_1:28;
then (w + (-1)*B) c= A by XBOOLE_1:37;
hence contradiction by A7;
end;
hence x in {v where v is Element of E:
(v + (-1)*B) /\ ((the carrier of E) \ A) <> {}};
end;
A8: for x be object holds
x in {v where v is Element of E: v + (-1)*B c= ((the carrier of E) \ A)}
iff
x in the carrier of E
& not x in {v where v is Element of E: (v + (-1)*B) /\ A <> {}}
proof
let x be object;
hereby
assume x in {v where v is Element of E:
(v + (-1)*B) c= ((the carrier of E) \ A)};
then consider v be Element of E such that
A9: x = v & (v + (-1)*B) c= ((the carrier of E) \ A);
thus x in (the carrier of E) by A9;
thus not x in
{w where w is Element of E: (w + (-1)*B) /\ A <> {}}
proof
assume x in {w where w is Element of E: (w + (-1)*B) /\ A <> {}};
then
consider w be Element of E such that
A10: w=x & (w + (-1)*B) /\ A <> {};
(w + (-1)*B) misses (the carrier of E) \ ((the carrier of E) \ A)
by A9,A10,XBOOLE_1:85;
then (w + (-1)*B) misses (the carrier of E) /\ A by XBOOLE_1:48;
then (w + (-1)*B) misses A by XBOOLE_1:28;
hence contradiction by A10;
end;
end;
assume
A11: x in (the carrier of E)
& not x in ({v where v is Element of E: (v + (-1)*B) /\ A <> {}});
then reconsider w = x as Element of E;
reconsider w = x as Element of E by A11;
(w + (-1)*B) \ ((the carrier of E) \ A)
= ((w + (-1)*B) \ (the carrier of E)) \/ ((w + (-1)*B) /\ A)
by XBOOLE_1:52
.= {} \/ ((w + (-1)*B) /\ A) by XBOOLE_1:37
.= {} by A11;
then w + (-1)*B c= ((the carrier of E) \ A) by XBOOLE_1:37;
hence
x in ({v where v is Element of E: v + (-1)*B
c= ((the carrier of E) \ A)});
end;
thus ((the carrier of E) \ A)(+)B = {v where v is Element of E:
(v + (-1)*B) /\ ((the carrier of E) \ A) <> {}} by Th7,A3
.= (the carrier of E) \ ({v where v is Element of E: v + (-1)*B c= A})
by A4,XBOOLE_0:def 5
.= (the carrier of E) \ (A(-)B ) by Th8;
thus ((the carrier of E) \ A)(-)B
= {v where v is Element of E: v + (-1)*B c= ((the carrier of E) \ A)}
by Th8,A3
.= (the carrier of E)
\ {v where v is Element of E: (v + (-1)*B) /\ A <> {}}
by A8,XBOOLE_0:def 5
.= (the carrier of E) \ (A(+)B) by Th7;
end;
end;
Lm1:
for E be non empty Abelian addLoopStr, A, B be Subset of E
holds A(+)B = B(+)A
proof
let E be non empty Abelian addLoopStr, A, B be Subset of E;
thus A(+)B = B + A
.= B(+)A;
end;
definition let E be non empty Abelian addLoopStr, A, B be Subset of E;
redefine func A(+)B; :: redefines (+) (MATHMORP, synonym) → + (RUSUB_4, definition)
commutativity by Lm1;
end;
theorem Th10:
for E be non empty add-associative addLoopStr, A, B, C be Subset of E
holds A + B + C = A + (B + C)
proof
let E be non empty add-associative addLoopStr, A, B, C be Subset of E;
for x be Element of E
holds x in (A + B + C) iff x in A + (B + C)
proof
let x be Element of E;
hereby assume x in (A + B + C);
then
consider ab, c be Element of E such that
A1: x = ab + c & ab in (A+B) & c in C;
consider a, b be Element of E such that
A2: ab = a + b & a in A & b in B by A1;
A3: x = a + (b + c) by A1,A2,RLVECT_1:def 3;
b + c in B + C by A1,A2;
hence x in A + (B + C) by A2,A3;
end;
assume x in A + (B + C);
then
consider a, bc be Element of E such that
A4: x = a + bc & a in A & bc in B + C;
consider b, c be Element of E such that
A5: bc = b + c & b in B & c in C by A4;
A6: x = (a + b) + c by A4,A5,RLVECT_1:def 3;
a + b in A + B by A4,A5;
hence x in (A +B) + C by A5,A6;
end;
hence thesis by SUBSET_1:3;
end;
theorem
A(+)B(+)C = A(+)(B(+)C) by Th10;
theorem Th12:
(union F)(+)B = union {X(+)B where X is binary-image of E: X in F}
proof
for x be object
holds x in (union F)(+)B
iff x in union {X(+)B where X is binary-image of E: X in F}
proof
let x be object;
hereby assume x in (union F)(+)B;
then consider f, b be Element of E such that
A1: x = f + b & f in (union F) & b in B;
consider Y be set such that
A2: f in Y & Y in F by A1,TARSKI:def 4;
reconsider X = Y as binary-image of E by A2;
A3: x in X(+)B by A1,A2;
X(+)B in {W(+)B where W is binary-image of E: W in F } by A2;
hence x in union {W(+)B where W is binary-image of E: W in F}
by A3,TARSKI:def 4;
end;
assume x in union {X(+)B where X is binary-image of E: X in F};
then consider Y be set such that
A4: x in Y & Y in {X(+)B where X is binary-image of E: X in F}
by TARSKI:def 4;
consider W be binary-image of E such that
A5: Y = W(+)B & W in F by A4;
consider f, b be Element of E such that
A6: x = f + b & f in W & b in B by A4,A5;
W c= (union F) by A5,ZFMISC_1:74;
hence x in (union F) (+)B by A6;
end;
hence thesis by TARSKI:2;
end;
theorem
A(+)(union F) = union {A(+)X where X is binary-image of E: X in F}
proof
A1: for x be object
holds x in {X(+)A where X is binary-image of E: X in F}
iff x in {A(+)X where X is binary-image of E: X in F}
proof
let x be object;
hereby assume x in {X(+)A where X is binary-image of E: X in F};
then consider W be binary-image of E such that
A2: x = W(+)A & W in F;
x = A(+)W & W in F by A2;
hence x in {A(+)X where X is binary-image of E: X in F};
end;
assume x in {A(+)X where X is binary-image of E: X in F};
then consider W be binary-image of E such that
A3: x= A(+)W & W in F;
x= W(+)A & W in F by A3;
hence x in {X(+)A where X is binary-image of E: X in F};
end;
thus A(+)(union F) = (union F)(+)A
.= union {X(+)A where X is binary-image of E: X in F} by Th12
.= union {A(+)X where X is binary-image of E: X in F}
by A1,TARSKI:2;
end;
theorem Th14:
(meet F)(+)B c= meet {X(+)B where X is binary-image of E: X in F }
proof
per cases;
suppose
A1: F = {};
reconsider Z=(meet F) as Subset of E;
(meet F) = {} by A1,SETFAM_1:def 1;
then Z(+)B ={} by Th1;
hence (meet F)(+)B
c= meet {X(+)B where X is binary-image of E: X in F};
end;
suppose
F <> {}; then
consider W0 be object such that
A2: W0 in F by XBOOLE_0:def 1;
reconsider W0 as binary-image of E by A2;
A3: W0(+)B in {W(+)B where W is binary-image of E: W in F} by A2;
let x be object;
assume x in (meet F)(+)B;
then consider f, b be Element of E such that
A4: x = f + b & f in (meet F) & b in B;
now let Y be set;
assume Y in {X(+)B where X is binary-image of E: X in F};
then consider X be binary-image of E such that
A5: Y = X(+)B & X in F;
meet F c= X by A5,SETFAM_1:3;
hence x in Y by A4,A5;
end;
hence x in meet {W(+)B where W is binary-image of E: W in F}
by A3,SETFAM_1:def 1;
end;
end;
theorem
A(+)(meet F) c= meet { A(+)X where X is binary-image of E: X in F}
proof
A1: for x be object
holds x in {X(+)A where X is binary-image of E: X in F}
iff x in { A(+)X where X is binary-image of E: X in F}
proof
let x be object;
hereby assume x in {X(+)A where X is binary-image of E: X in F };
then
consider W be binary-image of E such that
A2: x = W(+)A & W in F;
x = A(+)W & W in F by A2;
hence x in {A(+)X where X is binary-image of E: X in F};
end;
assume x in {A(+)X where X is binary-image of E: X in F};
then consider W be binary-image of E such that
A3: x = A(+)W & W in F;
x = W(+)A & W in F by A3;
hence x in {X(+)A where X is binary-image of E: X in F};
end;
A(+)(meet F) c= meet {X(+)A where X is binary-image of E: X in F}
by Th14;
hence A(+)(meet F) c= meet {A(+)X where X is binary-image of E: X in F}
by A1,TARSKI:2;
end;
theorem Th16:
for E be non empty addLoopStr, A, B, C be Subset of E
holds B c= C implies A + B c= A + C
proof
let E be non empty addLoopStr,
A, B, C be Subset of E;
assume
A1: B c= C;
let x be object;
assume x in A + B;
then consider a, b be Element of E such that
A2: x = a + b & a in A & b in B;
thus x in A + C by A1,A2;
end;
theorem Th17:
(v + A)(+)B = A(+)(v+B) & (v+A)(+)B = v+ (A(+)B)
proof
for x be object holds x in (v+A)(+)B iff x in A(+)(v + B)
proof
let x be object;
hereby assume x in (v+A)(+)B;
then consider f, b be Element of E such that
A1: x = f + b & f in (v+A) & b in B;
consider a be Element of E such that
A2: f = v + a & a in A by A1;
A3: x = a+ (v + b) by A1,A2,RLVECT_1:def 3;
v+b in (v+B) by A1;
hence x in A(+)(v + B) by A3,A2;
end;
assume x in A(+)(v + B);
then consider a, f be Element of E such that
A4: x = a + f & a in A & f in (v + B);
consider b be Element of E such that
A5: f=v+b & b in B by A4;
A6: x = (v+a) + b by A4,A5,RLVECT_1:def 3;
v+a in (v+A) by A4;
hence x in (v+A)(+)B by A6,A5;
end;
hence (v+A)(+)B = A(+)(v+B) by TARSKI:2;
for x be object holds x in (v+A)(+) B iff x in v+(A(+)B)
proof
let x be object;
hereby assume x in (v+A)(+)B;
then consider f, b be Element of E such that
A7: x = f+b & f in (v+A) & b in B;
consider a be Element of E such that
A8: f = v+a & a in A by A7;
A9: x = v + (a+b) by A7,A8,RLVECT_1:def 3;
a+b in (A+B) by A7,A8;
hence x in v+ (A(+)B) by A9;
end;
assume x in v + (A(+)B);
then consider ab be Element of E such that
A10: x = v+ab & ab in (A(+)B);
consider a, b be Element of E such that
A11: ab = a + b & a in A & b in B by A10;
A12: x = (v+a) + b by A10,A11,RLVECT_1:def 3;
v+a in (v+A) by A11;
hence x in (v + A)(+)B by A12,A11;
end;
hence (v+A)(+)B = v + (A(+)B) by TARSKI:2;
end;
theorem Th18:
(meet F)(-)B = meet { X(-)B where X is binary-image of E: X in F}
proof
per cases;
suppose
A1: F = {};
reconsider Z=(meet F) as Subset of E;
A2: (meet F) = {} by A1,SETFAM_1:def 1;
{X(-)B where X is binary-image of E: X in F} = {}
proof
assume {X(-)B where X is binary-image of E: X in F} <> {};
then consider x be object such that
A3: x in {X(-)B where X is binary-image of E: X in F}
by XBOOLE_0:def 1;
ex X be binary-image of E st x = X(-)B & X in F by A3;
hence contradiction by A1;
end;
then {} = meet {X(-)B where X is binary-image of E: X in F}
by SETFAM_1:def 1;
hence (meet F)(-)B = meet {X(-)B where X is binary-image of E: X in F}
by A2,Th2;
end;
suppose
A4: F <> {};
then consider W0 be object such that
A5: W0 in F by XBOOLE_0:def 1;
reconsider W0 as binary-image of E by A5;
A6: W0(-)B in { W(-)B where W is binary-image of E: W in F} by A5;
for x be object holds x in (meet F)(-)B
iff x in meet {W(-)B where W is binary-image of E: W in F}
proof
let x be object;
hereby
assume x in (meet F)(-)B;
then consider z be Element of E such that
A7: x = z & for b be Element of E st b in B holds z - b in (meet F);
now let Y be set;
assume Y in { X(-)B where X is binary-image of E: X in F};
then consider X be binary-image of E such that
A8: Y = X(-)B & X in F;
now let b be Element of E;
assume b in B;
then
A9: z - b in (meet F) by A7;
meet F c= X by A8,SETFAM_1:3;
hence z - b in X by A9;
end;
hence x in Y by A8,A7;
end;
hence x in meet {W(-)B where W is binary-image of E: W in F}
by A6,SETFAM_1:def 1;
end;
assume
A10: x in meet {W(-)B where W is binary-image of E: W in F};
A11: for W be binary-image of E st W in F holds x in W(-)B
proof
let W be binary-image of E;
assume W in F;
then W(-)B in {D(-)B where D is binary-image of E: D in F};
hence x in W(-)B by A10,SETFAM_1:def 1;
end;
x in W0(-)B by A5,A11;
then
reconsider z=x as Element of E;
for b be Element of E st b in B holds z - b in meet F
proof
assume not for b be Element of E st b in B holds z - b in meet F;
then consider b be Element of E such that
A12: b in B & not z - b in meet F;
consider X be set such that
A13: X in F & not (z-b) in X by A4,A12,SETFAM_1:def 1;
reconsider X as binary-image of E by A13;
z in X(-)B by A13,A11;
then consider zz be Element of E such that
A14: z = zz & for b be Element of E st b in B holds zz - b in X;
thus contradiction by A14,A12,A13;
end;
hence x in (meet F)(-)B;
end;
hence (meet F)(-)B = meet {X(-)B where X is binary-image of E: X in F}
by TARSKI:2;
end;
end;
theorem
meet {B (-)X where X is binary-image of E: X in F} c= B(-)(meet F)
proof
per cases;
suppose
A1: F = {};
reconsider Z = meet F as Subset of E;
{B(-)X where X is binary-image of E: X in F} = {}
proof
assume { B(-)X where X is binary-image of E: X in F} <> {};
then consider x be object such that
A2: x in {B(-)X where X is binary-image of E: X in F}
by XBOOLE_0:def 1;
ex X be binary-image of E st x = B(-)X & X in F by A2;
hence contradiction by A1;
end;
then {} = meet {B(-)X where X is binary-image of E: X in F}
by SETFAM_1:def 1;
hence meet {B(-)X where X is binary-image of E: X in F}
c= B (-)(meet F);
end;
suppose F <> {}; then
consider W0 be object such that
A3: W0 in F by XBOOLE_0:def 1;
reconsider W0 as binary-image of E by A3;
let x be object;
assume
A4: x in meet { B(-)W where W is binary-image of E: W in F};
A5: for W be binary-image of E st W in F holds x in B(-)W
proof
let W be binary-image of E;
assume W in F;
then B(-)W in { B(-)D where D is binary-image of E: D in F};
hence x in B(-)W by A4,SETFAM_1:def 1;
end;
A6: x in B(-)W0 by A3,A5;
then reconsider z=x as Element of E;
for f be Element of E st f in meet F holds z - f in B
proof
let f be Element of E;
assume
A7: f in meet F;
A8: meet F c= W0 by A3,SETFAM_1:3;
consider zz be Element of E such that
A9: z = zz & for w be Element of E st w in W0
holds zz - w in B by A6;
thus z - f in B by A9,A7,A8;
end;
hence x in B(-)(meet F);
end;
end;
theorem
union {X(-)B where X is binary-image of E: X in F} c= (union F)(-)B
proof
let x be object;
assume x in union { X(-)B where X is binary-image of E: X in F};
then consider Y be set such that
A1: x in Y & Y in {X(-)B where X is binary-image of E: X in F}
by TARSKI:def 4;
consider W be binary-image of E such that
A2: Y = W(-)B & W in F by A1;
consider z be Element of E such that
A3: x = z & for b be Element of E st b in B holds z - b in W by A1,A2;
now let b be Element of E;
assume b in B;
then
A4: z - b in W by A3;
W c= union F by A2,ZFMISC_1:74;
hence z - b in union F by A4;
end;
hence x in (union F) (-)B by A3;
end;
theorem
F <> {}
implies B(-) (union F) = meet {B(-)X where X is binary-image of E: X in F}
proof
assume F <> {};
then consider W0 be object such that
A1: W0 in F by XBOOLE_0:def 1;
reconsider W0 as binary-image of E by A1;
A2: B(-)W0 in {B(-)X where X is binary-image of E: X in F} by A1;
for x be object holds x in B(-) (union F)
iff x in meet {B(-)X where X is binary-image of E: X in F}
proof
let x be object;
hereby
assume x in B(-) (union F);
then consider z be Element of E such that
A3: x = z & for f be Element of E st f in (union F) holds z - f in B;
now
let Y be set;
assume Y in {B(-)X where X is binary-image of E: X in F};
then consider X be binary-image of E such that
A4: Y = B(-)X & X in F;
now
let f be Element of E;
assume f in X;
then f in (union F) by A4,TARSKI:def 4;
hence z - f in B by A3;
end;
hence x in Y by A3,A4;
end;
hence x in meet {B(-)W where W is binary-image of E: W in F}
by A2,SETFAM_1:def 1;
end;
assume
A5: x in meet {B(-)W where W is binary-image of E: W in F};
A6: for W be binary-image of E st W in F holds x in B(-)W
proof
let W be binary-image of E;
assume W in F;
then B(-)W in {B(-)D where D is binary-image of E: D in F};
hence x in B(-)W by A5,SETFAM_1:def 1;
end;
x in B(-)W0 by A1,A6;
then reconsider z=x as Element of E;
for f be Element of E st f in (union F) holds z - f in B
proof
let f be Element of E;
assume f in (union F);
then consider W be set such that
A7: f in W & W in F by TARSKI:def 4;
reconsider W as binary-image of E by A7;
z in B(-)W by A6,A7; then
consider w be Element of E such that
A8: z = w & for f be Element of E st f in W holds w - f in B;
thus z - f in B by A7,A8;
end;
hence x in B(-)(union F);
end;
hence B(-)(union F) = meet {B(-)X where X is binary-image of E: X in F}
by TARSKI:2;
end;
theorem Th22:
A c= B implies A(-)C c= B(-)C
proof
assume
A1: A c= B;
let x be object;
assume x in A(-)C;
then consider w be Element of E such that
A2: x = w & for c be Element of E st c in C holds w - c in A;
for c being Element of E st c in C holds w - c in B by A1,A2;
hence x in B(-)C by A2;
end;
theorem
A c= B implies C(-)B c= C(-)A
proof
assume
A1: A c= B;
let x be object;
assume x in C(-)B;
then consider w be Element of E such that
A2: x = w & for b be Element of E st b in B holds w - b in C;
for a be Element of E st a in A holds w - a in C by A1,A2;
hence x in C(-)A by A2;
end;
theorem Th24:
(v+A)(-)B = A(-)(v+B) & (v+A)(-)B = v+(A(-)B)
proof
for x be object holds x in (v+A)(-)B iff x in A(-)(v+B)
proof
let x be object;
hereby
assume x in (v+A)(-) B;
then consider w be Element of E such that
A1: x = w & for b be Element of E st b in B holds w - b in (v+A);
now let vb be Element of E;
assume vb in (v+B); then
consider b be Element of E such that
A2: vb = v+b & b in B;
w - b in (v+A) by A2,A1;
then consider a be Element of E such that
A3: w - b = v+a & a in A;
w - vb = w-b -v by A2,RLVECT_1:27
.= a by A3,RLVECT_4:1;
hence w - vb in A by A3;
end;
hence x in A(-)(v+B) by A1;
end;
assume x in A(-)(v+B);
then consider w be Element of E such that
A4: x = w & for vb be Element of E st vb in (v+B) holds w - vb in A;
now let b be Element of E;
assume b in B;
then (v+b) in (v+B);
then w -(v+b) in A by A4;
then
A5: v + (w -(v+b)) in v+A;
v + (w -(v+b)) = v+w -(v+b) by RLVECT_1:28
.=w+(v-(v+b)) by RLVECT_1:28
.=w+ (v -v - b) by RLVECT_1:27
.=w + (0.E - b) by RLVECT_1:15;
hence w - b in v+A by A5;
end;
hence x in (v+A)(-) B by A4;
end;
hence (v+A)(-) B = A(-) (v+B) by TARSKI:2;
for x be object holds x in (v+A)(-) B iff x in v+ (A(-)B)
proof
let x be object;
hereby
assume x in (v+A)(-) B;
then consider w be Element of E such that
A6: x = w & for b be Element of E st b in B holds w - b in (v+A);
now let b be Element of E;
assume b in B;
then
A7: w - b in (v+A) by A6;
consider a be Element of E such that
A8: w - b = v+a & a in A by A7;
(w - v) - b = w - (v+b) by RLVECT_1:27
.= v+a -v by A8,RLVECT_1:27
.= a by RLVECT_4:1;
hence (w - v) - b in A by A8;
end;
then
A9: w-v in A(-)B;
v+(w-v) = w by RLVECT_4:1;
hence x in v + (A(-)B) by A6,A9;
end;
assume x in v + (A(-)B);
then consider ab be Element of E such that
A10: x = v+ab & ab in (A(-)B);
reconsider w=x as Element of E by A10;
consider d be Element of E such that
A11: ab = d & for b be Element of E st b in B holds d - b in A by A10;
now let b be Element of E;
assume b in B;
then
A12: ab - b in A by A11;
(v+ab) - b = v +(ab-b) by RLVECT_1:28;
hence (v+ab) - b in v + A by A12;
end;
hence x in (v+A)(-)B by A10;
end;
hence (v+A)(-)B = v+(A(-)B) by TARSKI:2;
end;
theorem Th25:
(A(-)B)(-)C = A(-)(B(+)C)
proof
for x be object holds x in (A(-)B)(-)C iff x in A(-)(B(+)C)
proof
let x be object;
hereby
assume x in (A(-)B)(-)C;
then consider w be Element of E such that
A1: x = w & for c be Element of E st c in C
holds w - c in (A(-)B);
now
let bc be Element of E;
assume bc in (B(+)C);
then consider b, c be Element of E such that
A2: bc = b+c & b in B & c in C;
w - c in (A(-)B) by A1,A2;
then consider g be Element of E such that
A3: w - c = g & for b be Element of E st b in B holds g - b in A;
w - bc = g - b by A2,A3,RLVECT_1:27;
hence w - bc in A by A3,A2;
end;
hence x in A(-)(B(+)C) by A1;
end;
assume x in A(-)(B(+)C);
then consider w be Element of E such that
A4: x = w & for bc be Element of E st bc in B(+)C holds w - bc in A;
now let c be Element of E;
assume
A5: c in C;
now let b be Element of E;
assume
A6: b in B;
b+c in B(+)C by A5,A6;
then w -(b+c) in A by A4;
hence (w -c) -b in A by RLVECT_1:27;
end;
hence w-c in A(-)B;
end;
hence x in (A(-)B)(-)C by A4;
end;
hence (A(-)B)(-)C = A(-)(B(+)C) by TARSKI:2;
end;
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
:Def2:
for A be binary-image of E holds it.A = A(+)B;
existence
proof
defpred P[object,object] means
ex A be binary-image of E st $1 = A & $2 = A(+)B;
A1:
now
let x be object;
assume x in bool (the carrier of E);
then reconsider A = x as binary-image of E;
set y = A(+)B;
A(+)B c= the carrier of E;
hence ex y be object st y in bool (the carrier of E) & P[x,y];
end;
consider f be Function of bool the carrier of E, bool the carrier of E
such that
A2: for x be object st x in bool the carrier of E holds P[x,f.x]
from FUNCT_2:sch 1(A1);
take f;
now
let A be binary-image of E;
ex X be binary-image of E st A = X & f.A = X(+)B by A2;
hence f.A = A(+)B;
end;
hence thesis;
end;
uniqueness
proof
let f, g be Function of bool (the carrier of E), bool (the carrier of E);
assume
A3: for A be binary-image of E holds f.A = A(+)B;
assume
A4: for A be binary-image of E holds g.A = A(+)B;
now
let x be object;
assume x in bool the carrier of E;
then reconsider A = x as binary-image of E;
thus f.x = A(+)B by A3
.= g.x by A4;
end;
hence f=g by FUNCT_2:12;
end;
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
:Def3:
for A be binary-image of E holds it.A = A(-)B;
existence
proof
defpred P[object,object] means
ex A be binary-image of E st $1=A & $2 = A(-)B;
A1:
now
let x be object;
assume x in bool the carrier of E;
then reconsider A = x as binary-image of E;
set y = A(-)B;
A(-)B c= the carrier of E;
hence ex y be object st y in bool the carrier of E & P[x,y];
end;
consider f be Function of bool the carrier of E, bool the carrier of E
such that
A2: for x be object st x in bool the carrier of E holds P[x,f.x]
from FUNCT_2:sch 1(A1);
take f;
now let A be binary-image of E;
ex X be binary-image of E st A=X & f.A = X(-)B by A2;
hence f.A = A(-)B;
end;
hence thesis;
end;
uniqueness
proof
let f, g be Function of bool (the carrier of E), bool (the carrier of E);
assume that
A3: for A be binary-image of E holds f.A = A(-)B and
A4: for A be binary-image of E holds g.A = A(-)B;
now
let x be object;
assume x in bool (the carrier of E); then
reconsider A = x as binary-image of E;
thus f.x = A(-)B by A3
.= g.x by A4;
end;
hence f = g by FUNCT_2:12;
end;
end;
theorem
(dilation(B)).(union F)
= union {(dilation(B)).X where X is binary-image of E: X in F}
proof
A1: for x be object holds x in {X(+)B where X is binary-image of E: X in F}
iff x in {(dilation(B)).X where X is binary-image of E: X in F}
proof
let x be object;
hereby assume x in {X(+)B where X is binary-image of E: X in F};
then consider X be binary-image of E such that
A2: x = X(+)B & X in F;
x = (dilation(B)).X & X in F by A2,Def2;
hence x in {(dilation(B)).W where W is binary-image of E: W in F};
end;
assume x in {(dilation(B)).X where X is binary-image of E: X in F};
then consider X be binary-image of E such that
A3: x=(dilation(B)).X & X in F;
x = X(+)B & X in F by A3,Def2;
hence x in { W(+)B where W is binary-image of E: W in F};
end;
thus (dilation(B)).(union F) = (union F)(+)B by Def2
.= union { X(+)B where X is binary-image of E: X in F} by Th12
.= union {(dilation(B)).X where X is binary-image of E: X in F}
by A1,TARSKI:2;
end;
theorem
A c= B implies (dilation(C)).A c= (dilation(C)).B
proof
assume
A1: A c= B;
A2: (dilation(C)).A = C+A by Def2;
(dilation(C)).B = C+B by Def2;
hence thesis by A2,A1,Th16;
end;
theorem
(dilation(C)).(v+A) = v+((dilation(C)).A)
proof
A1: (dilation(C)).(v+A) = (v+A)(+)C by Def2;
v + ((dilation(C)).A) = v+(A(+)C) by Def2;
hence thesis by Th17,A1;
end;
theorem
(erosion(B)).(meet F)
= meet {(erosion(B)).X where X is binary-image of E: X in F}
proof
A1: for x be object
holds x in {X(-)B where X is binary-image of E: X in F}
iff x in {(erosion(B)).X where X is binary-image of E: X in F}
proof
let x be object;
hereby
assume x in {X(-)B where X is binary-image of E: X in F};
then consider X be binary-image of E such that
A2: x = X(-)B & X in F;
x = (erosion(B)).X & X in F by A2,Def3;
hence x in {(erosion(B)).W where W is binary-image of E: W in F};
end;
assume x in {(erosion(B)).X where X is binary-image of E: X in F};
then consider X be binary-image of E such that
A3: x = (erosion(B)).X & X in F;
x = X(-)B & X in F by A3,Def3;
hence x in { W(-)B where W is binary-image of E: W in F};
end;
thus (erosion(B)).(meet F) = (meet F)(-)B by Def3
.= meet {X(-)B where X is binary-image of E: X in F } by Th18
.= meet {(erosion(B)).X where X is binary-image of E: X in F}
by A1,TARSKI:2;
end;
theorem
A c= B implies (erosion(C)).A c= (erosion(C)).B
proof
assume
A1: A c= B;
A2: (erosion(C)).A = A(-)C by Def3;
(erosion(C)).B = B(-)C by Def3;
hence thesis by A2,A1,Th22;
end;
theorem
(erosion(C)).(v+A) = v+((erosion(C)).A)
proof
A1: (erosion(C)).(v+A) = (v+A)(-)C by Def3;
v+((erosion(C)).A) = v+(A(-)C) by Def3;
hence thesis by Th24,A1;
end;
theorem
(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 )
proof
thus (dilation(C)).((the carrier of E) \ A)
= ((the carrier of E) \ A)(+)C by Def2
.= (the carrier of E) \ (A(-)C) by Th9
.= (the carrier of E) \ ((erosion(C)).A) by Def3;
thus (erosion(C)).( (the carrier of E) \ A)
= ((the carrier of E) \ A)(-)C by Def3
.= (the carrier of E) \ (A(+)C) by Th9
.= (the carrier of E) \ ((dilation(C)).A) by Def2;
end;
theorem
(dilation(C)).((dilation(B)).A) = (dilation((dilation(C)).B)).A
& (erosion(C)).((erosion(B)).A) = (erosion((dilation(C)).B)).A
proof
thus (dilation(C)).((dilation(B)).A) = (dilation(C)).(A(+)B) by Def2
.= (A(+)B)(+)C by Def2
.= A(+)(B(+)C) by Th10
.= A(+)((dilation(C)).B) by Def2
.= (dilation((dilation(C)).B)).A by Def2;
thus (erosion(C)).((erosion(B)).A) = (erosion(C)).(A(-)B) by Def3
.= (A(-)B)(-)C by Def3
.= A(-)(B(+)C) by Th25
.= A(-)((dilation(C)).B) by Def2
.= (erosion((dilation(C)).B)).A by Def3;
end;