:: Morphology for Image Processing, Part {I}
:: by Hiroshi Yamazaki , Czes\l aw Byli\'nski and Katsumi Wasaki
::
:: Received September 21, 2011
:: Copyright (c) 2011 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, SUBSET_1, SETFAM_1, FUNCT_1, FUNCT_2, REAL_1,
STRUCT_0, ALGSTR_0, RLVECT_1, RLSUB_1, RUSUB_4, MATHMORP;
constructors SETFAM_1, REAL_1, RLSUB_1, RUSUB_4, RVSUM_1, RELSET_1, MATHMORP;
registrations SUBSET_1, RELSET_1, MEMBERED, STRUCT_0, RLVECT_1, RLSUB_1;
requirements NUMERALS, SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0, RLVECT_1, RLSUB_1, RUSUB_4, MATHMORP;
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 set;
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 LM0010:
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 AS: B = {};
hence A(+)B = B & B(+)A = B by RUSUB_5:5;
now let x be set;
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 AS;
hence x in A(-)B;
end;
then the carrier of E c= A(-)B by TARSKI:def 3;
hence the carrier of E = A(-)B by XBOOLE_0:def 10;
end;
theorem LM0010A:
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
AS: A <> {} & B = {};
then consider a be set such that
P1: a in A by XBOOLE_0:def 1;
reconsider a as Element of E by P1;
assume B(-)A <> B;
then consider ba be set such that
P2: ba in B(-)A by AS, XBOOLE_0:def 1;
consider z be Element of E such that
P3: ba = z & for a be Element of E st a in A holds z - a in B by P2;
thus contradiction by AS, P1, P3;
end;
theorem LM0020:
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
AS: B = the carrier of E & A <> {};
then consider a be set such that
P1: a in A by XBOOLE_0:def 1;
reconsider a as Element of E by P1;
now let x be set;
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 AS, P1;
end;
then
P1: the carrier of E c= A(+)B by TARSKI:def 3;
hence B = A(+)B by AS, XBOOLE_0:def 10;
thus B(+)A = A + B
.= B by P1, AS, XBOOLE_0:def 10;
end;
theorem LM0020A:
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
AS: B = the carrier of E;
now let x be set;
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 AS;
hence x in B(-)A;
end;
then the carrier of E c= B(-)A by TARSKI:def 3;
hence B = B(-)A by XBOOLE_0:def 10, AS;
end;
theorem
A(+)B = union {b + A where b is Element of E: b in B}
proof
now let x be set;
assume
P1: x in A(+)B;
consider a0, b0 be Element of E such that
P2: x = a0 + b0 & a0 in A & b0 in B by P1;
P3: x in b0 + A by P2;
b0 + A in {b + A where b is Element of E: b in B} by P2;
hence x in union {b + A where b is Element of E: b in B}
by P3, TARSKI:def 4;
end;
hence
A(+)B c= union {b + A where b is Element of E: b in B} by TARSKI:def 3;
now let x be set;
assume x in union {b + A where b is Element of E: b in B};
then consider y be set such that
P0: 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
P1: y = b + A & b in B by P0;
consider a be Element of E such that
P2: x = b + a & a in A by P1, P0;
thus x in A(+)B by P1, P2;
end;
hence thesis by TARSKI:def 3;
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 set such that
P01: g in B by XBOOLE_0:def 1;
reconsider g as Element of E by P01;
P02: g+A in {b + A where b is Element of E: b in B} by P01;
now let x be set;
assume x in A(-)B; then
consider z be Element of E such that
P1: 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
A2: Y = b + A & b in B;
A3: z - b in A by P1, A2;
z = b + (z- b) by RLVECT_4:1;
hence z in Y by A3, A2;
end;
hence x in meet {b + A where b is Element of E: b in B}
by P1, P02, SETFAM_1:def 1;
end;
hence A(-)B c= meet {b + A where b is Element of E: b in B}
by TARSKI:def 3;
now let x be set;
assume
P0: x in meet {b + A where b is Element of E: b in B};
consider S be set such that
P11: S in {b + A where b is Element of E: b in B} by P02;
consider d be Element of E such that
P12: S = d + A & d in B by P11;
x in S by P0, P11, SETFAM_1:def 1;
then
reconsider x0 = x as Element of E by P12;
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 P0, SETFAM_1:def 1;
then consider a be Element of E such that
X1: x0 = b + a & a in A;
thus thesis by X1, 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
by TARSKI:def 3;
end;
theorem Th104:
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 set;
assume
P1: x in A(+)B;
consider a0,b0 be Element of E such that
P2: x = a0 + b0 & a0 in A & b0 in B by P1;
reconsider v = x as Element of E by P1;
P3: v - b0 = a0 by P2,RLVECT_4:1;
(-1)*b0 in (-1)*B by P2;
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 P2, P3, XBOOLE_0:def 4;
hence x in {w where w is Element of E: (w + (-1)*B) /\ A <> {}};
end;
let x be set;
assume x in {v where v is Element of E: (v + (-1)*B) /\ A <> {}};
then
consider v be Element of E such that
P1: x = v & (v + (-1)*B ) /\ A <> {};
consider y be set such that
X1: y in ((v + (-1)*B) /\ A) by P1, XBOOLE_0:def 1;
X2: y in (v + (-1)*B ) & y in A by X1, XBOOLE_0:def 4;
then
consider nb be Element of E such that
X3: y = v + nb & nb in (-1)*B;
consider b be Element of E such that
X4: nb = (-1)*b & b in B by X3;
reconsider a = y as Element of E by X3;
a + b = v - b + b by X3, X4, RLVECT_1:16
.= v by RLVECT_4:1;
hence x in A(+)B by P1, X4, X2;
end;
theorem Th105:
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 set;
assume x in A(-)B; then
consider z be Element of E such that
P1: 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 set;
assume y in z + (-1)*B;
then consider nb be Element of E such that
X1: y = z + nb & nb in (-1)*B;
consider b be Element of E such that
X2: nb = (-1)*b & b in B by X1;
z - b in A by X2, P1;
hence y in A by X1, X2, RLVECT_1:16;
end;
hence x in {v where v is Element of E: v + (-1)*B c= A} by P1;
end;
let x be set;
assume x in {v where v is Element of E: v + (-1)*B c= A};
then consider v be Element of E such that
P1: 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 P1;
end;
hence x in A(-)B by P1;
end;
theorem Th106:
((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
X0: 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 X0, XBOOLE_1:37
.= {} by LM0010
.= (the carrier of E) \ (the carrier of E) by XBOOLE_1:37
.= (the carrier of E) \ (A(-)B) by X0,LM0020A;
thus ((the carrier of E) \ A) (-)B = X(-)B by X0, XBOOLE_1:37
.= {} by LM0010A
.= (the carrier of E) \ (the carrier of E) by XBOOLE_1:37
.= (the carrier of E) \ (A(+)B) by X0,LM0020;
end;
suppose
X0: A <> the carrier of E;
P1: (the carrier of E) \ A is non empty
proof
assume (the carrier of E) \ A is empty;
then (the carrier of E) c= A by XBOOLE_1:37;
hence contradiction by X0, XBOOLE_0:def 10;
end;
X1: for x be set 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 set;
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
R2: x=v & (v + (-1)*B) /\ ((the carrier of E) \ A) <> {};
thus x in (the carrier of E) by R2;
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
R4: w = x & w + (-1)*B c= A;
(v + (-1)*B) misses ((the carrier of E) \ A)
by R2, R4, XBOOLE_1:85;
hence contradiction by R2, XBOOLE_0:def 7;
end;
end;
assume
X5: 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 X5;
end;
hence x in {v where v is Element of E:
(v + (-1)*B) /\ ((the carrier of E) \ A) <> {}};
end;
X2: for x be set 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 set;
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
R2: x = v & (v + (-1)*B) c= ((the carrier of E) \ A);
thus x in (the carrier of E) by R2;
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
R4: w=x & (w + (-1)*B) /\ A <> {};
(w + (-1)*B) misses (the carrier of E) \ ((the carrier of E) \ A)
by R2, R4, 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 R4, XBOOLE_0:def 7;
end;
end;
assume
X5: 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 X5;
(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 X5;
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 Th104, P1
.= (the carrier of E) \ ({v where v is Element of E: v + (-1)*B c= A})
by X1, XBOOLE_0:def 5
.= (the carrier of E) \ (A(-)B ) by Th105;
thus ((the carrier of E) \ A)(-)B
= {v where v is Element of E: v + (-1)*B c= ((the carrier of E) \ A)}
by Th105, P1
.= (the carrier of E)
\ {v where v is Element of E: (v + (-1)*B) /\ A <> {}}
by X2, XBOOLE_0:def 5
.= (the carrier of E) \ (A(+)B) by Th104;
end;
end;
Th107:
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;
commutativity by Th107;
end;
theorem Th108A1:
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
P1: x = ab + c & ab in (A+B) & c in C;
consider a, b be Element of E such that
P2: ab = a + b & a in A & b in B by P1;
P3: x = a + (b + c) by P1, P2, RLVECT_1:def 3;
b + c in B + C by P1, P2;
hence x in A + (B + C) by P2, P3;
end;
assume x in A + (B + C);
then
consider a, bc be Element of E such that
P1: x = a + bc & a in A & bc in B + C;
consider b, c be Element of E such that
P2: bc = b + c & b in B & c in C by P1;
P3: x = (a + b) + c by P1, P2, RLVECT_1:def 3;
a + b in A + B by P1, P2;
hence x in (A +B) + C by P2, P3;
end;
hence thesis by SUBSET_1:3;
end;
theorem
A(+)B(+)C = A(+)(B(+)C) by Th108A1;
theorem Th108B:
(union F)(+)B = union {X(+)B where X is binary-image of E: X in F}
proof
for x be set
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 set;
hereby assume x in (union F)(+)B;
then consider f, b be Element of E such that
P1: x = f + b & f in (union F) & b in B;
consider Y be set such that
P2: f in Y & Y in F by P1, TARSKI:def 4;
reconsider X = Y as binary-image of E by P2;
P3: x in X(+)B by P1, P2;
X(+)B in {W(+)B where W is binary-image of E: W in F } by P2;
hence x in union {W(+)B where W is binary-image of E: W in F}
by P3, 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
P1: 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
P2: Y = W(+)B & W in F by P1;
consider f, b be Element of E such that
P3: x = f + b & f in W & b in B by P1, P2;
W c= (union F) by P2, ZFMISC_1:74;
hence x in (union F) (+)B by P3;
end;
hence thesis by TARSKI:1;
end;
theorem
A(+)(union F) = union {A(+)X where X is binary-image of E: X in F}
proof
P1: for x be set 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 set;
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
X1: x = W(+)A & W in F;
x = A(+)W & W in F by X1;
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
X1: x= A(+)W & W in F;
x= W(+)A & W in F by X1;
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 Th108B
.= union {A(+)X where X is binary-image of E: X in F}
by P1, TARSKI:1;
end;
theorem Th110:
(meet F)(+)B c= meet {X(+)B where X is binary-image of E: X in F }
proof
per cases;
suppose
G1: F = {};
reconsider Z=(meet F) as Subset of E;
(meet F) = {} by G1, SETFAM_1:def 1;
then Z(+)B ={} by LM0010;
hence (meet F)(+)B
c= meet {X(+)B where X is binary-image of E: X in F} by XBOOLE_1:2;
end;
suppose
F <> {}; then
consider W0 be set such that
P0: W0 in F by XBOOLE_0:def 1;
reconsider W0 as binary-image of E by P0;
P2: W0(+)B in {W(+)B where W is binary-image of E: W in F} by P0;
now let x be set;
assume x in (meet F)(+)B;
then consider f, b be Element of E such that
P1: 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
P3: Y = X(+)B & X in F;
meet F c= X by P3, SETFAM_1:3;
hence x in Y by P1, P3;
end;
hence x in meet {W(+)B where W is binary-image of E: W in F}
by P2, SETFAM_1:def 1;
end;
hence (meet F)(+)B c= meet {X(+)B where X is binary-image of E: X in F}
by TARSKI:def 3;
end;
end;
theorem
A(+)(meet F) c= meet { A(+)X where X is binary-image of E: X in F}
proof
P1: for x be set 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 set;
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
X1: x = W(+)A & W in F;
x = A(+)W & W in F by X1;
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
X1: x = A(+)W & W in F;
x = W(+)A & W in F by X1;
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 Th110;
hence A(+)(meet F) c= meet {A(+)X where X is binary-image of E: X in F}
by P1, TARSKI:1;
end;
theorem Th112:
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
AS1: B c= C;
let x be set;
assume x in A + B;
then consider a, b be Element of E such that
P1: x = a + b & a in A & b in B;
thus x in A + C by AS1, P1;
end;
theorem Th113:
(v + A)(+)B = A(+)(v+B) & (v+A)(+)B = v+ (A(+)B)
proof
for x be set holds x in (v+A)(+)B iff x in A(+)(v + B)
proof
let x be set;
hereby assume x in (v+A)(+)B;
then consider f, b be Element of E such that
P1: x = f + b & f in (v+A) & b in B;
consider a be Element of E such that
P2: f = v + a & a in A by P1;
P3: x = a+ (v + b) by P1, P2, RLVECT_1:def 3;
v+b in (v+B) by P1;
hence x in A(+)(v + B) by P3, P2;
end;
assume x in A(+)(v + B);
then consider a, f be Element of E such that
P1: x = a + f & a in A & f in (v + B);
consider b be Element of E such that
P2: f=v+b & b in B by P1;
P3: x = (v+a) + b by P1, P2, RLVECT_1:def 3;
v+a in (v+A) by P1;
hence x in (v+A)(+)B by P3, P2;
end;
hence (v+A)(+)B = A(+)(v+B) by TARSKI:1;
for x be set holds x in (v+A)(+) B iff x in v+(A(+)B)
proof
let x be set;
hereby assume x in (v+A)(+)B;
then consider f, b be Element of E such that
P1: x = f+b & f in (v+A) & b in B;
consider a be Element of E such that
P2: f = v+a & a in A by P1;
P3: x = v + (a+b) by P1, P2, RLVECT_1:def 3;
a+b in (A+B) by P1, P2;
hence x in v+ (A(+)B) by P3;
end;
assume x in v + (A(+)B);
then consider ab be Element of E such that
P1: x = v+ab & ab in (A(+)B);
consider a, b be Element of E such that
P2: ab = a + b & a in A & b in B by P1;
P3: x = (v+a) + b by P1, P2,RLVECT_1:def 3;
v+a in (v+A) by P2;
hence x in (v + A)(+)B by P3, P2;
end;
hence (v+A)(+)B = v + (A(+)B) by TARSKI:1;
end;
theorem Th114:
(meet F)(-)B = meet { X(-)B where X is binary-image of E: X in F}
proof
per cases;
suppose
G1: F = {};
reconsider Z=(meet F) as Subset of E;
G2: (meet F) = {} by G1, 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 set such that
S1: 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 S1;
hence contradiction by G1;
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 G2, LM0010A;
end;
suppose
G2: F <> {};
then consider W0 be set such that
P0: W0 in F by XBOOLE_0:def 1;
reconsider W0 as binary-image of E by P0;
P2: W0(-)B in { W(-)B where W is binary-image of E: W in F} by P0;
for x be set 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 set;
hereby
assume x in (meet F)(-)B;
then consider z be Element of E such that
Q1: 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
P3: Y = X(-)B & X in F;
now let b be Element of E;
assume b in B;
then
X1: z - b in (meet F) by Q1;
meet F c= X by P3, SETFAM_1:3;
hence z - b in X by X1;
end;
hence x in Y by P3, Q1;
end;
hence x in meet {W(-)B where W is binary-image of E: W in F}
by P2, SETFAM_1:def 1;
end;
assume
X1: x in meet {W(-)B where W is binary-image of E: W in F};
Q1: 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 X1, SETFAM_1:def 1;
end;
x in W0(-)B by P0, Q1;
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
D2: b in B & not z - b in meet F;
consider X be set such that
Q5: X in F & not (z-b) in X by G2,D2,SETFAM_1:def 1;
reconsider X as binary-image of E by Q5;
z in X(-)B by Q5,Q1;
then consider zz be Element of E such that
Q70: z = zz & for b be Element of E st b in B holds zz - b in X;
thus contradiction by Q70, D2, Q5;
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:1;
end;
end;
theorem
meet {B (-)X where X is binary-image of E: X in F} c= B(-)(meet F)
proof
per cases;
suppose
G1: 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 set such that
S1: 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 S1;
hence contradiction by G1;
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) by XBOOLE_1:2;
end;
suppose F <> {}; then
consider W0 be set such that
P0: W0 in F by XBOOLE_0:def 1;
reconsider W0 as binary-image of E by P0;
for x be set
holds x in meet { B(-)W where W is binary-image of E: W in F}
implies x in B(-)(meet F)
proof
let x be set;
assume
X1: x in meet { B(-)W where W is binary-image of E: W in F};
Q1: 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 X1, SETFAM_1:def 1;
end;
T1: x in B(-)W0 by P0,Q1;
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
D1: f in meet F;
D2: meet F c= W0 by P0,SETFAM_1:3;
consider zz be Element of E such that
Q7: z = zz & for w be Element of E st w in W0
holds zz - w in B by T1;
thus z - f in B by Q7, D1, D2;
end;
hence x in B(-)(meet F);
end;
hence
meet {B(-)X where X is binary-image of E: X in F} c= B(-)(meet F)
by TARSKI:def 3;
end;
end;
theorem
union {X(-)B where X is binary-image of E: X in F} c= (union F)(-)B
proof
let x be set;
assume x in union { X(-)B where X is binary-image of E: X in F};
then consider Y be set such that
P1: 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
P2: Y = W(-)B & W in F by P1;
consider z be Element of E such that
Q7: x = z & for b be Element of E st b in B holds z - b in W by P1, P2;
now let b be Element of E;
assume b in B;
then
X2: z - b in W by Q7;
W c= union F by P2,ZFMISC_1:74;
hence z - b in union F by X2;
end;
hence x in (union F) (-)B by Q7;
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 set such that
P0: W0 in F by XBOOLE_0:def 1;
reconsider W0 as binary-image of E by P0;
P2: B(-)W0 in {B(-)X where X is binary-image of E: X in F} by P0;
for x be set 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 set;
hereby
assume x in B(-) (union F);
then consider z be Element of E such that
Q1: 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
Q2: Y = B(-)X & X in F;
now
let f be Element of E;
assume f in X;
then f in (union F) by Q2, TARSKI:def 4;
hence z - f in B by Q1;
end;
hence x in Y by Q1, Q2;
end;
hence x in meet {B(-)W where W is binary-image of E: W in F}
by P2, SETFAM_1:def 1;
end;
assume
X1: x in meet {B(-)W where W is binary-image of E: W in F};
Q1: 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 X1, SETFAM_1:def 1;
end;
x in B(-)W0 by P0, Q1;
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
Q4: f in W & W in F by TARSKI:def 4;
reconsider W as binary-image of E by Q4;
z in B(-)W by Q1,Q4; then
consider w be Element of E such that
Q7: z = w & for f be Element of E st f in W holds w - f in B;
thus z - f in B by Q4, Q7;
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:1;
end;
theorem Th118:
A c= B implies A(-)C c= B(-)C
proof
assume
AS: A c= B;
let x be set;
assume x in A(-)C;
then consider w be Element of E such that
P2: x = w & for c be Element of E st c in C holds w - c in A;
now let c be Element of E;
assume c in C;
then w - c in A by P2;
hence w - c in B by AS;
end;
hence x in B(-)C by P2;
end;
theorem
A c= B implies C(-)B c= C(-)A
proof
assume
AS: A c= B;
let x be set;
assume x in C(-)B;
then consider w be Element of E such that
P2: 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 AS, P2;
hence x in C(-)A by P2;
end;
theorem Th120:
(v+A)(-)B = A(-)(v+B) & (v+A)(-)B = v+(A(-)B)
proof
for x be set holds x in (v+A)(-)B iff x in A(-)(v+B)
proof
let x be set;
hereby
assume x in (v+A)(-) B;
then consider w be Element of E such that
P1: 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
P3: vb = v+b & b in B;
w - b in (v+A) by P3,P1;
then consider a be Element of E such that
P5: w - b = v+a & a in A;
w - vb = w-b -v by P3, RLVECT_1:27
.= a by P5, RLVECT_4:1;
hence w - vb in A by P5;
end;
hence x in A(-)(v+B) by P1;
end;
assume x in A(-)(v+B);
then consider w be Element of E such that
P1: 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 P1;
then
P4: 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 RLVECT_1:14, P4;
end;
hence x in (v+A)(-) B by P1;
end;
hence (v+A)(-) B = A(-) (v+B) by TARSKI:1;
for x be set holds x in (v+A)(-) B iff x in v+ (A(-)B)
proof
let x be set;
hereby
assume x in (v+A)(-) B;
then consider w be Element of E such that
P1: 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
X2: w - b in (v+A) by P1;
consider a be Element of E such that
X3: w - b = v+a & a in A by X2;
(w - v) - b = w - (v+b) by RLVECT_1:27
.= v+a -v by RLVECT_1:27, X3
.= a by RLVECT_4:1;
hence (w - v) - b in A by X3;
end;
then
X4: w-v in A(-)B;
v+(w-v) = w by RLVECT_4:1;
hence x in v + (A(-)B) by P1, X4;
end;
assume x in v + (A(-)B);
then consider ab be Element of E such that
X1: x = v+ab & ab in (A(-)B);
reconsider w=x as Element of E by X1;
consider d be Element of E such that
Y1: ab = d & for b be Element of E st b in B holds d - b in A by X1;
now let b be Element of E;
assume b in B;
then
X2: ab - b in A by Y1;
(v+ab) - b = v +(ab-b) by RLVECT_1:28;
hence (v+ab) - b in v + A by X2;
end;
hence x in (v+A)(-)B by X1;
end;
hence (v+A)(-)B = v+(A(-)B) by TARSKI:1;
end;
theorem Th121:
(A(-)B)(-)C = A(-)(B(+)C)
proof
for x be set holds x in (A(-)B)(-)C iff x in A(-)(B(+)C)
proof
let x be set;
hereby
assume x in (A(-)B)(-)C;
then consider w be Element of E such that
P1: 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
P3: bc = b+c & b in B & c in C;
w - c in (A(-)B) by P1, P3;
then consider g be Element of E such that
P5: w - c = g & for b be Element of E st b in B holds g - b in A;
w - bc = g - b by P3, RLVECT_1:27, P5;
hence w - bc in A by P5,P3;
end;
hence x in A(-)(B(+)C) by P1;
end;
assume x in A(-)(B(+)C);
then consider w be Element of E such that
P1: 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
P2: c in C;
now let b be Element of E;
assume
P3: b in B;
b+c in B(+)C by P2, P3;
then w -(b+c) in A by P1;
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 P1;
end;
hence (A(-)B)(-)C = A(-)(B(+)C) by TARSKI:1;
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
:def020:
for A be binary-image of E holds it.A = A(+)B;
existence
proof
defpred P[set,set] means ex A be binary-image of E st $1 = A & $2 = A(+)B;
X1:
now
let x be set;
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 set 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
X2: for x be set st x in bool the carrier of E holds P[x,f.x]
from FUNCT_2:sch 1(X1);
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 X2;
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
A1: for A be binary-image of E holds f.A = A(+)B;
assume
A2: for A be binary-image of E holds g.A = A(+)B;
now
let x be set;
assume x in bool the carrier of E;
then reconsider A = x as binary-image of E;
thus f.x = A(+)B by A1
.= g.x by A2;
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
:def030:
for A be binary-image of E holds it.A = A(-)B;
existence
proof
defpred P[set,set] means ex A be binary-image of E st $1=A & $2 = A(-)B;
X1:
now
let x be set;
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 set 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
X2: for x be set st x in bool the carrier of E holds P[x,f.x]
from FUNCT_2:sch 1(X1);
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 X2;
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
A1: for A be binary-image of E holds f.A = A(-)B and
A2: for A be binary-image of E holds g.A = A(-)B;
now
let x be set;
assume x in bool (the carrier of E); then
reconsider A = x as binary-image of E;
thus f.x = A(-)B by A1
.= g.x by A2;
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
P2: for x be set 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 set;
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
P3: x = X(+)B & X in F;
x = (dilation(B)).X & X in F by P3, def020;
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
P3: x=(dilation(B)).X & X in F;
x = X(+)B & X in F by P3,def020;
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 def020
.= union { X(+)B where X is binary-image of E: X in F} by Th108B
.= union {(dilation(B)).X where X is binary-image of E: X in F}
by P2, TARSKI:1;
end;
theorem
A c= B implies (dilation(C)).A c= (dilation(C)).B
proof
assume
AS: A c= B;
P1: (dilation(C)).A = C+A by def020;
(dilation(C)).B = C+B by def020;
hence thesis by P1, AS, Th112;
end;
theorem
(dilation(C)).(v+A) = v+((dilation(C)).A)
proof
P1: (dilation(C)).(v+A) = (v+A)(+)C by def020;
v + ((dilation(C)).A) = v+(A(+)C) by def020;
hence thesis by Th113, P1;
end;
theorem
(erosion(B)).(meet F)
= meet {(erosion(B)).X where X is binary-image of E: X in F}
proof
P2: for x be set 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 set;
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
P3: x = X(-)B & X in F;
x = (erosion(B)).X & X in F by P3,def030;
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
P3: x = (erosion(B)).X & X in F;
x = X(-)B & X in F by P3, def030;
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 def030
.= meet {X(-)B where X is binary-image of E: X in F } by Th114
.= meet {(erosion(B)).X where X is binary-image of E: X in F}
by P2, TARSKI:1;
end;
theorem
A c= B implies (erosion(C)).A c= (erosion(C)).B
proof
assume
AS: A c= B;
P1: (erosion(C)).A = A(-)C by def030;
(erosion(C)).B = B(-)C by def030;
hence thesis by P1, AS, Th118;
end;
theorem
(erosion(C)).(v+A) = v+((erosion(C)).A)
proof
P1: (erosion(C)).(v+A) = (v+A)(-)C by def030;
v+((erosion(C)).A) = v+(A(-)C) by def030;
hence thesis by Th120, P1;
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 def020
.= (the carrier of E) \ (A(-)C) by Th106
.= (the carrier of E) \ ((erosion(C)).A) by def030;
thus (erosion(C)).( (the carrier of E) \ A)
= ((the carrier of E) \ A)(-)C by def030
.= (the carrier of E) \ (A(+)C) by Th106
.= (the carrier of E) \ ((dilation(C)).A) by def020;
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 def020
.= (A(+)B)(+)C by def020
.= A(+)(B(+)C) by Th108A1
.= A(+)((dilation(C)).B) by def020
.= (dilation((dilation(C)).B)).A by def020;
thus (erosion(C)).((erosion(B)).A) = (erosion(C)).(A(-)B) by def030
.= (A(-)B)(-)C by def030
.= A(-)(B(+)C) by Th121
.= A(-)((dilation(C)).B) by def020
.= (erosion((dilation(C)).B)).A by def030;
end;