:: 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;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, SUBSET_1, ALGSTR_0, RUSUB_4;
expansions TARSKI, XBOOLE_0;
theorems XBOOLE_1, XCMPLX_1, TARSKI, SUBSET_1, ZFMISC_1, XBOOLE_0, JORDAN1,
XREAL_1, RLTOPSP1, RLVECT_1, RLVECT_4;
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
{q + p where q is Element of T : q in X};
coherence
proof
now
let x be object;
assume x in {q+p where q is Point of T : q in X};
then ex q being Point of T st x = q + p & q in X;
hence x in the carrier of T;
end;
hence thesis by TARSKI:def 3;
end;
end;
:: Reflected of X
definition
let T be non empty addLoopStr, X be Subset of T;
func X! -> Subset of T equals
{-q where q is Point of T : q in X};
coherence
proof
now
let x be object;
assume x in {-q where q is Point of T : q in X};
then ex q being Point of T st x = -q & q in X;
hence x in the carrier of T;
end;
hence thesis by TARSKI:def 3;
end;
end;
:: Set Erosion
definition
let T be non empty addMagma, X,B be Subset of T;
func X (-) B -> Subset of T equals
{y where y is Point of T : B+y c= X};
coherence
proof
now
let x be object;
assume x in {y where y is Point of T : B+y c= X};
then ex q being Point of T st x = q & B+q c= X;
hence x in the carrier of T;
end;
hence thesis by TARSKI:def 3;
end;
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 Th1:
for T being add-associative right_zeroed right_complementable
non empty RLSStruct,
B being Subset of T holds
(B!)! = B
proof
let T be add-associative right_zeroed right_complementable
non empty RLSStruct,
B be Subset of T;
thus (B!)! c= B
proof
let x be object;
assume x in (B!)!;
then consider q being Element of T such that
A1: x = -q and
A2: q in B!;
ex q1 being Element of T st q = -q1 & q1 in B by A2;
hence thesis by A1,RLVECT_1:17;
end;
let x be object;
assume
A3: x in B;
then reconsider xx = x as Point of T;
-xx in {-q where q is Point of T : q in B}by A3;
then -(-xx) in {-q where q is Point of T : q in B!};
hence thesis by RLVECT_1:17;
end;
theorem Th2:
{0.T} + x = {x}
proof
thus {0.T} + x c= {x}
proof
let a be object;
assume a in {0.T} + x;
then consider q being Point of T such that
A1: a=q+x and
A2: q in {0.T};
{q} c= {0.T} by A2,ZFMISC_1:31;
then q = 0.T by ZFMISC_1:18;
then {a} c= {x} by A1;
hence thesis by ZFMISC_1:31;
end;
let a be object;
assume a in {x};
then {a} c= {x} by ZFMISC_1:31;
then a = x by ZFMISC_1:18;
then
A3: a = 0.T + x;
0.T in {0.T} by ZFMISC_1:31;
hence thesis by A3;
end;
theorem Th3:
B1 c= B2 implies B1+p c= B2+p
proof
assume
A1: B1 c= B2;
let p1 be object;
assume p1 in B1+p;
then ex p2 being Point of T st p1 =p2+p & p2 in B1;
hence thesis by A1;
end;
theorem Th4:
for X st X = {} holds X+x = {}
proof
let X;
assume
A1: X = {};
now
given y being object such that
A2: y in X+x;
ex y1 being Point of T st y = y1+x & y1 in X by A2;
hence contradiction by A1;
end;
hence thesis by XBOOLE_0:def 1;
end;
theorem
X (-) {0.T} = X
proof
thus X (-) {0.T} c= X
proof
let x be object;
assume x in X (-) {0.T};
then ex y being Point of T st x=y & {0.T}+y c= X;
then {x} c= X by Th2;
hence thesis by ZFMISC_1:31;
end;
let x be object;
assume
A1: x in X;
then reconsider xx=x as Point of T;
{x} c= X by A1,ZFMISC_1:31;
then {0.T}+xx c= X by Th2;
hence thesis;
end;
Lm1: {x}+y = {y}+x
proof
thus {x}+y c= {y}+x
proof
let x1 be object;
assume x1 in {x}+y;
then consider p1 being Point of T such that
A1: x1=p1+y and
A2: p1 in {x};
{p1} c= {x} by A2,ZFMISC_1:31; then
A3: x1=x+y by A1,ZFMISC_1:18;
y in {y} by TARSKI:def 1;
hence thesis by A3;
end;
let x1 be object;
assume x1 in {y}+x;
then consider p1 being Point of T such that
A4: x1=p1+x and
A5: p1 in {y};
{p1} c= {y} by A5,ZFMISC_1:31;
then
A6: x1=x+y by A4,ZFMISC_1:18;
x in {x}by TARSKI:def 1;
hence thesis by A6;
end;
theorem
X (+) {0.T} = X
proof
thus X (+) {0.T} c= X
proof
let x be object;
assume x in X (+) {0.T};
then consider y,z being Point of T such that
A1: x=y+z & y in X and
A2: z in {0.T};
{z} c= {0.T} by A2,ZFMISC_1:31;
then z = 0.T by ZFMISC_1:18;
hence thesis by A1;
end;
let x be object;
assume
A3: x in X;
then reconsider x as Point of T;
0.T in {0.T} by TARSKI:def 1;
then
x+0.T in {y+z where y,z is Point of T : y in X & z in {0.T}} by A3;
hence thesis;
end;
theorem
X (+) {x} = X+x
proof
thus X (+) {x} c= X+x
proof
let p be object;
assume p in X (+) {x};
then consider y,z being Point of T such that
A1: p=y+z and
A2: y in X and
A3: z in {x};
{z} c= {x} by A3,ZFMISC_1:31;
then p=y+x by A1,ZFMISC_1:18;
hence thesis by A2;
end;
let p be object;
assume p in X+x;
then
A4: ex q being Point of T st p=q+x & q in X;
x in {x} by TARSKI:def 1;
hence thesis by A4;
end;
theorem Th8:
for X,Y st Y = {} holds X (-) Y = the carrier of T
proof
let X,Y;
assume
A1: Y = {};
{y where y is Point of T:Y+y c= X} = the carrier of T
proof
thus {y where y is Point of T:Y+y c= X} c= the carrier of T
proof
let x be object;
assume x in {y where y is Point of T:Y+y c= X};
then ex y being Point of T st x=y & Y+y c= X;
hence thesis;
end;
let x be object;
assume x in the carrier of T;
then reconsider a=x as Point of T;
Y+a = {} by A1,Th4;
then Y+a c= X;
hence thesis;
end;
hence thesis;
end;
theorem Th9:
X c= Y implies X (-) B c= Y (-) B & X (+) B c= Y (+) B
proof
assume
A1: X c= Y;
thus X (-) B c= Y (-) B
proof
let p be object;
assume p in X (-) B;
then consider p1 being Point of T such that
A2: p = p1 and
A3: B+p1 c= X;
B+p1 c= Y by A1,A3;
hence thesis by A2;
end;
let p be object;
assume p in X (+) B;
then ex p1,p2 being Point of T st p = p1+p2 & p1 in X & p2 in B;
hence thesis by A1;
end;
theorem Th10:
B1 c= B2 implies X (-) B2 c= X (-) B1 & X (+) B1 c= X (+) B2
proof
assume
A1: B1 c= B2;
thus X (-) B2 c= X (-) B1
proof
let p be object;
assume p in X (-) B2;
then consider p1 being Point of T such that
A2: p = p1 and
A3: B2+p1 c= X;
B1+p1 c= B2 + p1 by A1,Th3;
then B1+p1 c= X by A3;
hence thesis by A2;
end;
let p be object;
assume p in X (+) B1;
then ex x,b being Point of T st p = x+b & x in X & b in B1;
hence thesis by A1;
end;
theorem
0.T in B implies X (-) B c= X & X c= X (+) B
proof
assume
A1: 0.T in B;
thus X (-) B c= X
proof
let p be object;
assume p in X (-) B;
then consider p1 being Point of T such that
A2: p = p1 and
A3: B+p1 c= X;
0.T+p1 in {q+p1 where q is Point of T:q in B} by A1;
then 0.T+p1 in X by A3;
hence thesis by A2;
end;
let p be object;
assume
A4: p in X;
then reconsider p as Point of T;
p + 0.T in {x+b where x,b is Point of T:x in X & b in B} by A1,A4;
hence thesis;
end;
theorem Th12:
X (+) Y = Y (+) X
proof
thus X (+) Y c= Y (+) X
proof
let p be object;
assume p in X (+) Y; then
ex p1,p2 being Point of T st p = p1+p2 & p1 in X & p2 in Y;
hence thesis;
end;
let p be object;
assume p in Y (+) X;
then ex p1,p2 being Point of T st p = p1+p2 & p1 in Y & p2 in X;
hence thesis;
end;
Lm2:
p - x + x = p & p + x - x = p
proof
p + x - x = p + (x - x) by RLVECT_1:def 3
.= p + 0.T by RLVECT_1:15
.= p;
hence thesis by RLVECT_1:28;
end;
theorem Th13:
Y+y c= X+x iff Y+(y-x) c= X
proof
thus Y+y c= X+x implies Y+(y-x) c= X
proof
assume
A1: Y+y c= X+x;
let p be object;
assume p in Y+(y-x);
then consider q1 being Point of T such that
A2: p = q1 + (y-x) and
A3: q1 in Y;
reconsider p as Point of T by A2;
p = q1 + y - x by A2,RLVECT_1:28; then
A4: p + x = q1 + y by Lm2;
q1 + y in {q+y where q is Point of T:q in Y} by A3;
then p + x in X + x by A1,A4;
then consider p1 being Point of T such that
A5: p+x =p1+x and
A6: p1 in X;
p +x-x= p1 by A5,Lm2;
hence thesis by A6,Lm2;
end;
assume
A7: Y+(y-x) c= X;
let p be object;
assume p in Y+y;
then consider q1 being Point of T such that
A8: p = q1 + y and
A9: q1 in Y;
reconsider p as Point of T by A8;
p-x = q1 + (y -x) & q1+(y-x) in {q+(y-x) where q is Point of T
:q in Y} by A8,A9,RLVECT_1:28;
then (p-x)+x in {q+x where q is Point of T:q in X}by A7;
hence thesis by Lm2;
end;
theorem Th14:
(X+p) (-) Y = (X (-) Y)+p
proof
thus (X+p) (-) Y c= (X (-) Y)+p
proof
let x be object;
assume x in (X+p) (-) Y;
then consider y being Point of T such that
A1: x = y and
A2: Y+y c= X+p;
Y+(y-p) c= X by A2,Th13;
then y-p in {y1 where y1 is Point of T:Y+y1 c= X};
then (y-p)+p in {q+p where q is Point of T:q in X (-) Y};
hence thesis by A1,Lm2;
end;
let x be object;
assume x in (X (-) Y)+p;
then consider y being Point of T such that
A3: x = y+p and
A4: y in X (-) Y;
reconsider x as Point of T by A3;
x-p = y & ex y2 being Point of T st y = y2 & Y+y2 c= X by A3,A4,Lm2;
then Y + x c= X + p by Th13;
hence thesis;
end;
theorem Th15:
(X+p) (+) Y = (X (+) Y)+p
proof
thus (X+p) (+) Y c= (X (+) Y)+p
proof
let x be object;
assume x in (X+p) (+) Y;
then consider x2,y2 being Point of T such that
A1: x = x2+y2 and
A2: x2 in X+p and
A3: y2 in Y;
consider x3 being Point of T such that
A4: x2 = x3+p & x3 in X by A2;
x=x3+y2+p & x3+y2 in X (+) Y by A1,A3,A4,RLVECT_1:def 3;
hence thesis;
end;
let x be object;
assume x in (X (+) Y)+p;
then consider x2 being Point of T such that
A5: x = x2+p and
A6: x2 in X (+) Y;
consider x3,y3 being Point of T such that
A7: x2 = x3+y3 and
A8: x3 in X and
A9: y3 in Y by A6;
A10: x3+p in X+p by A8;
x=x3+p+y3 by A5,A7,RLVECT_1:def 3;
hence thesis by A9,A10;
end;
theorem Th16:
(X+x)+y = X+(x+y)
proof
thus X+x+y c= X+(x+y)
proof
let p be object;
assume p in (X+x)+y;
then consider x2 being Point of T such that
A1: p = x2+y and
A2: x2 in X+x;
consider x3 being Point of T such that
A3: x2 = x3+x and
A4: x3 in X by A2;
p=x3+(x+y) by A1,A3,RLVECT_1:def 3;
hence thesis by A4;
end;
let p be object;
assume p in X+(x+y);
then consider x2 being Point of T such that
A5: p = x2+(x+y) & x2 in X;
p = x2 + x + y & x2+x in X+x by A5,RLVECT_1:def 3;
hence thesis;
end;
theorem Th17:
X (-) (Y+p) = (X (-) Y)+(-p)
proof
thus X (-) (Y+p) c= (X (-) Y)+(-p)
proof
let x be object;
assume x in X (-) (Y+p);
then consider y being Point of T such that
A1: x = y and
A2: (Y+p)+y c= X;
Y+(y+p) c= X by A2,Th16;
then y+p in {y1 where y1 is Point of T:Y+y1 c= X};
then y+p-p in (X (-) Y)+(-p);
hence thesis by A1,Lm2;
end;
let x be object;
assume x in (X (-) Y)+(-p);
then consider y being Point of T such that
A3: x = y+(-p) and
A4: y in X (-) Y;
reconsider x as Point of T by A3;
x+p = y-p+p by A3; then
A5: x+p =y by Lm2;
ex y2 being Point of T st y = y2 & Y+y2 c= X by A4;
then Y+p+x c= X by A5,Th16;
hence thesis;
end;
theorem
X (+) (Y+p) = (X (+) Y)+p
proof
thus X (+) (Y+p) c= (X (+) Y)+p
proof
let x be object;
assume x in X (+) (Y+p);
then consider x2,y2 being Point of T such that
A1: x = x2+y2 & x2 in X and
A2: y2 in Y+p;
consider y3 being Point of T such that
A3: y2 = y3+p & y3 in Y by A2;
x=x2+y3+p & x2+y3 in X (+) Y by A1,A3,RLVECT_1:def 3;
hence thesis;
end;
let x be object;
assume x in (X (+) Y)+p;
then consider x2 being Point of T such that
A4: x = x2+p and
A5: x2 in X (+) Y;
consider x3,y3 being Point of T such that
A6: x2 = x3+y3 and
A7: x3 in X and
A8: y3 in Y by A5;
A9: y3+p in Y+p by A8;
x=x3+(y3+p) by A4,A6,RLVECT_1:def 3;
hence thesis by A7,A9;
end;
theorem Th19:
x in X implies B+x c= B (+) X
proof
assume
A1: x in X;
let y be object;
assume y in B+x;
then ex y1 being Point of T st y = y1+x & y1 in B;
hence thesis by A1;
end;
theorem Th20:
X c= (X (+) B) (-) B
proof
let x be object;
assume
A1: x in X;
then consider x1 being Point of T such that
A2: x1=x;
B+x1 c= B (+) X by A1,A2,Th19;
then x in (B (+) X) (-) B by A2;
hence thesis by Th12;
end;
theorem Th21:
X+0.T = X
proof
thus X+0.T c= X
proof
let x be object;
assume x in X+0.T;
then ex q being Point of T st x = q + 0.T & q in X;
hence thesis;
end;
let x be object;
assume
A1: x in X;
then reconsider x1=x as Point of T;
x1=x1+0.T;
hence thesis by A1;
end;
theorem
X (-) {x} = X+(-x)
proof
thus X (-) {x} c= X+(-x)
proof
let y be object;
assume y in X (-) {x};
then consider p being Point of T such that
A1: p=y and
A2: {x}+p c= X;
{p}+x c= X by A2,Lm1;
then {p}+x+(-x) c= X+(-x) by Th3;
then {p}+(x+(-x)) c= X+(-x) by Th16;
then {p}+0.T c= X+(-x) by RLVECT_1:5;
then {p} c= X+(-x) by Th21;
hence thesis by A1,ZFMISC_1:31;
end;
let y be object;
assume y in X+(-x);
then consider p being Point of T such that
A3: y=p+(-x) and
A4: p in X;
reconsider y as Point of T by A3;
y = p - x by A3;
then
A5: y+x = p by Lm2;
{x}+y c= X
proof
let q be object;
assume q in {x}+y;
then consider qq being Point of T such that
A6: q=qq+y and
A7: qq in {x};
{qq} c= {x} by A7,ZFMISC_1:31;
hence thesis by A4,A5,A6,ZFMISC_1:18;
end;
hence thesis;
end;
Lm3: (X (-) B) (+) B c= X
proof
let x be object;
assume x in (X (-) B) (+) B;
then consider y1,y2 being Point of T such that
A1: x=y1+y2 and
A2: y1 in X (-) B and
A3: y2 in B;
consider y being Point of T such that
A4: y1=y and
A5: B+y c= X by A2;
x in B+y by A1,A3,A4;
hence thesis by A5;
end;
theorem Th23:
X (-) (Y (+) Z) = (X (-) Y) (-) Z
proof
A1: (X (-) Y) (+) Y c= X by Lm3;
thus X (-) (Y (+) Z) c= (X (-) Y) (-) Z
proof
let p be object;
assume p in X (-) (Y (+) Z);
then consider x being Point of T such that
A2: p = x and
A3: (Y (+) Z)+x c= X;
(Y+x) (+) Z c= X by A3,Th15;
then Z (+) (Y+x) c= X by Th12;
then
A4: (Z (+) (Y+x)) (-) (Y+x) c= X (-) (Y+x) by Th9;
Z c= (Z (+) (Y+x)) (-) (Y+x) by Th20;
then Z c= X (-) (Y+x) by A4;
then Z c= (X (-) Y)+(-x) by Th17;
then Z+x c= (X (-) Y)+(-x)+x by Th3;
then Z+x c= (X (-) Y)+((-x)+x) by Th16;
then Z+x c= (X (-) Y)+(x-x);
then Z+x c= (X (-) Y)+0.T by RLVECT_1:15;
then Z+x c= X (-) Y by Th21;
hence thesis by A2;
end;
let p be object;
assume p in (X (-) Y) (-) Z;
then consider y being Point of T such that
A5: p = y and
A6: Z+y c= X (-) Y;
(Z+y) (+) Y c= (X (-) Y) (+) Y by A6,Th9;
then (Z+y) (+) Y c= X by A1;
then (Z (+) Y)+y c= X by Th15;
then p in X (-) (Z (+) Y) by A5;
hence thesis by Th12;
end;
theorem
X (-) (Y (+) Z) = (X (-) Z) (-) Y
proof
X (-) (Y (+) Z) = X (-) (Z (+) Y) by Th12
.=X (-) Z (-) Y by Th23;
hence thesis;
end;
theorem
X (+) (Y (-) Z) c= (X (+) Y) (-) Z
proof
let x be object;
assume x in X (+) (Y (-) Z);
then consider a,b being Point of T such that
A1: x=a+b and
A2: a in X and
A3: b in Y (-) Z;
ex c being Point of T st b=c & Z+c c= Y by A3;
then Z+b+a c= Y+a by Th3;
then
A4: Z+(b+a) c= Y+a by Th16;
Y+a c= Y (+) X by A2,Th19;
then Z+(b+a) c= Y (+) X by A4;
then x in (Y (+) X) (-) Z by A1;
hence thesis by Th12;
end;
theorem
X (+) (Y (+) Z) = (X (+) Y) (+) Z
proof
thus X (+) ( Y (+) Z) c= (X (+) Y) (+) Z
proof
let p be object;
assume p in X (+) ( Y (+) Z);
then consider x1,p2 being Point of T such that
A1: p = x1+p2 & x1 in X and
A2: p2 in Y (+) Z;
consider y,z being Point of T such that
A3: p2=y+z & y in Y and
A4: z in Z by A2;
set p3=x1+y;
p=x1+y+z & p3 in X (+) Y by A1,A3,RLVECT_1:def 3;
hence thesis by A4;
end;
let p be object;
assume p in (X (+) Y) (+) Z;
then consider x1,p2 being Point of T such that
A5: p = x1+p2 and
A6: x1 in X (+) Y and
A7: p2 in Z;
consider y,z being Point of T such that
A8: x1=y+z and
A9: y in X and
A10: z in Y by A6;
set p3=z+p2;
p=y+(z+p2) & p3 in Y (+) Z by A5,A7,A8,A10,RLVECT_1:def 3;
hence thesis by A9;
end;
theorem Th27:
(B\/C)+y = (B+y) \/ (C+y)
proof
thus (B\/C)+y c= (B+y) \/ (C+y)
proof
let x be object;
assume x in (B\/C)+y;
then consider y2 being Point of T such that
A1: x=y2+y and
A2: y2 in B\/C;
y2 in B or y2 in C by A2,XBOOLE_0:def 3;
then x in {y1+y where y1 is Point of T : y1 in B} or x in {y1+y
where y1 is Point of T:y1 in C} by A1;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume x in (B+y) \/ (C+y);
then x in B+y or x in C+y by XBOOLE_0:def 3;
then consider y2 being Point of T such that
A3: x=y2+y & y2 in B or x=y2+y & y2 in C;
y2 in B\/C by A3,XBOOLE_0:def 3;
hence thesis by A3;
end;
theorem Th28:
(B/\C)+y = (B+y) /\ (C+y)
proof
thus (B/\C)+y c= (B+y) /\ (C+y)
proof
let x be object;
assume x in (B/\C)+y;
then consider y2 being Point of T such that
A1: x=y2+y and
A2: y2 in B/\C;
y2 in C by A2,XBOOLE_0:def 4;
then
A3: x in {y1+y where y1 is Point of T:y1 in C} by A1;
y2 in B by A2,XBOOLE_0:def 4;
then x in {y1+y where y1 is Point of T:y1 in B} by A1;
hence thesis by A3,XBOOLE_0:def 4;
end;
let x be object;
assume
A4: x in (B+y) /\ (C+y);
then x in B+y by XBOOLE_0:def 4;
then consider y3 being Point of T such that
A5: x=y3+y and
A6: y3 in B;
x in C+y by A4,XBOOLE_0:def 4;
then consider y2 being Point of T such that
A7: x=y2+y and
A8: y2 in C;
y2+y-y=y3 by A5,A7,Lm2; then
A9: y2=y3 by Lm2;
then y2 in B/\C by A6,A8,XBOOLE_0:def 4;
hence thesis by A5,A9;
end;
theorem
X (-) (B\/C) = (X (-) B)/\(X (-) C)
proof
thus X (-) (B\/C) c= (X (-) B)/\(X (-) C)
proof
let x be object;
assume x in X (-) (B\/C);
then consider y being Point of T such that
A1: x = y and
A2: (B\/C)+y c= X;
A3: (B+y)\/(C+y) c= X by A2,Th27;
then C+y c= X by XBOOLE_1:11;
then
A4: x in {y1 where y1 is Point of T:C+y1 c= X} by A1;
B+y c= X by A3,XBOOLE_1:11;
then x in {y1 where y1 is Point of T:B+y1 c= X} by A1;
hence thesis by A4,XBOOLE_0:def 4;
end;
let x be object;
assume
A5: x in (X (-) B)/\(X (-) C);
then x in X (-) B by XBOOLE_0:def 4;
then consider y being Point of T such that
A6: x = y and
A7: B+y c= X;
x in X (-) C by A5,XBOOLE_0:def 4;
then ex y2 being Point of T st x = y2 & C+y2 c= X;
then (B+y)\/(C+y) c= X by A6,A7,XBOOLE_1:8;
then (B\/C)+y c= X by Th27;
hence thesis by A6;
end;
theorem
X (+) (B\/C) = (X (+) B)\/(X (+) C)
proof
thus X (+) (B\/C) c= (X (+) B)\/(X (+) C)
proof
let x be object;
assume x in X (+) (B\/C);
then consider y3,y4 being Point of T such that
A1: x = y3+y4 & y3 in X and
A2: y4 in (B\/C);
y4 in B or y4 in C by A2,XBOOLE_0:def 3;
then
x in {y1+y2 where y1,y2 is Point of T :y1 in X & y2 in B} or x
in {y1+y2 where y1,y2 is Point of T:y1 in X & y2 in C} by A1;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume x in (X (+) B)\/(X (+) C);
then x in X (+) B or x in X (+) C by XBOOLE_0:def 3;
then consider y3,y4 being Point of T such that
A3: x=y3+y4 & y3 in X & y4 in B or x=y3+y4 & y3 in X & y4 in C;
y4 in B\/C by A3,XBOOLE_0:def 3;
hence thesis by A3;
end;
theorem
(X (-) B)\/(Y (-) B) c= (X\/Y) (-) B
proof
let x be object;
assume x in (X (-) B)\/(Y (-) B);
then x in X (-) B or x in Y (-) B by XBOOLE_0:def 3;
then consider y being Point of T such that
A1: x=y & B+y c= X or x=y & B+y c= Y;
B+y c= X \/ Y
by A1,XBOOLE_0:def 3;
hence thesis by A1;
end;
theorem
(X\/Y) (+) B = (X (+) B)\/(Y (+) B)
proof
thus (X\/Y) (+) B c= (X (+) B)\/(Y (+) B)
proof
let x be object;
assume x in (X\/Y) (+) B;
then consider y1,y2 being Point of T such that
A1: x=y1+y2 and
A2: y1 in X\/Y and
A3: y2 in B;
y1 in X or y1 in Y by A2,XBOOLE_0:def 3;
then
x in {y3+y4 where y3,y4 is Point of T:y3 in X & y4 in B} or x
in {y3+y4 where y3,y4 is Point of T:y3 in Y & y4 in B} by A1,A3;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume x in (X (+) B)\/(Y (+) B);
then x in X (+) B or x in Y (+) B by XBOOLE_0:def 3;
then consider y1,y2 being Point of T such that
A4: x=y1+y2 & y1 in X & y2 in B or x=y1+y2 & y1 in Y & y2 in B;
y1 in X\/Y by A4,XBOOLE_0:def 3;
hence thesis by A4;
end;
theorem
(X/\Y) (-) B = (X (-) B)/\(Y (-) B)
proof
thus (X/\Y) (-) B c= (X (-) B)/\(Y (-) B)
proof
let x be object;
assume x in (X/\Y) (-) B;
then consider y being Point of T such that
A1: x=y and
A2: B+y c= X/\Y;
B+y c= Y by A2,XBOOLE_1:18;
then
A3: x in {y1 where y1 is Point of T:B+y1 c= Y} by A1;
B+y c= X by A2,XBOOLE_1:18;
then x in {y1 where y1 is Point of T:B+y1 c= X} by A1;
hence thesis by A3,XBOOLE_0:def 4;
end;
let x be object;
assume
A4: x in (X (-) B)/\(Y (-) B);
then x in X (-) B by XBOOLE_0:def 4;
then consider y being Point of T such that
A5: x=y and
A6: B+y c= X;
x in Y (-) B by A4,XBOOLE_0:def 4;
then
A7: ex y2 being Point of T st x=y2 & B+y2 c= Y;
B+y c= X/\Y
by A5,A6,A7,XBOOLE_0:def 4;
hence thesis by A5;
end;
theorem Th34:
(X/\Y) (+) B c= (X (+) B)/\(Y (+) B)
proof
let x be object;
assume x in (X/\Y) (+) B;
then consider y1,y2 being Point of T such that
A1: x=y1+y2 and
A2: y1 in X/\Y and
A3: y2 in B;
y1 in Y by A2,XBOOLE_0:def 4;
then
A4: x in {y3+y4 where y3,y4 is Point of T:y3 in Y & y4 in B} by A1,A3;
y1 in X by A2,XBOOLE_0:def 4;
then
x in {y3+y4 where y3,y4 is Point of T:y3 in X & y4 in B} by A1,A3;
hence thesis by A4,XBOOLE_0:def 4;
end;
theorem
B (+) (X/\Y) c= (B (+) X)/\(B (+) Y)
proof
B (+) (X/\Y) = (X/\Y) (+) B by Th12;
then B (+) (X/\Y) c= (X (+) B)/\(Y (+) B) by Th34;
then B (+) (X/\Y) c= (B (+) X)/\(Y (+) B) by Th12;
hence thesis by Th12;
end;
theorem
(B (-) X)\/(B (-) Y) c= B (-) (X/\Y)
proof
let x be object;
assume x in (B (-) X)\/(B (-) Y);
then x in B (-) X or x in B (-) Y by XBOOLE_0:def 3;
then consider y being Point of T such that
A1: x=y & X+y c= B or x=y & Y+y c= B;
(X+y)/\(Y+y) c= B
proof
let a be object;
assume
A2: a in (X+y)/\(Y+y);
then
A3: a in X+y by XBOOLE_0:def 4;
A4: a in Y+y by A2,XBOOLE_0:def 4;
per cases by A1;
suppose
X+y c= B;
hence thesis by A3;
end;
suppose
Y+y c= B;
hence thesis by A4;
end;
end;
then (X/\Y)+y c= B by Th28;
hence thesis by A1;
end;
theorem Th37:
(X` (-) B)` = X (+) B!
proof
thus ((X`) (-) B)` c= X (+) B!
proof
let x be object;
assume
A1: x in ((X`) (-) B)`;
then reconsider x1=x as Point of T;
not x in (X`) (-) B by A1,XBOOLE_0:def 5;
then not B+x1 c= X`;
then B+x1 meets X by SUBSET_1:23;
then consider y being object such that
A2: y in (B+x1) and
A3: y in X by XBOOLE_0:3;
reconsider y1=y as Point of T by A2;
consider b1 being Point of T such that
A4: y = b1+x1 & b1 in B by A2;
x1 = y1 - b1 & -b1 in B! by A4,Lm2;
hence thesis by A3;
end;
let x be object;
assume x in X (+) B!;
then consider x1,b1 being Point of T such that
A5: x=x1+b1 and
A6: x1 in X and
A7: b1 in B!;
reconsider xx=x as Point of T by A5;
consider b2 being Point of T such that
A8: b1=-b2 and
A9: b2 in B by A7;
x=x1-b2 by A5,A8;
then
A10: xx+b2=x1 by Lm2;
b2+xx in {pb+xx where pb is Point of T:pb in B}by A9;
then
A11: B+xx meets X by A6,A10,XBOOLE_0:3;
not xx in ((X`) (-) B)
proof
assume xx in ((X`) (-) B);
then ex yy being Point of T st xx=yy & B+yy c= X`;
hence contradiction by A11,SUBSET_1:23;
end;
hence thesis by XBOOLE_0:def 5;
end;
theorem Th38:
(X (-) B)` = X` (+) B!
proof
thus (X (-) B)` c= X` (+) B!
proof
let x be object;
assume
A1: x in (X (-) B)`;
then reconsider x1=x as Point of T;
not x in X (-) B by A1,XBOOLE_0:def 5;
then not B+x1 c= X;
then B+x1 meets X` by SUBSET_1:24;
then consider y being object such that
A2: y in B+x1 and
A3: y in X` by XBOOLE_0:3;
reconsider y1=y as Point of T by A2;
consider b1 being Point of T such that
A4: y = b1+x1 & b1 in B by A2;
x1 = y1 - b1 & -b1 in B! by A4,Lm2;
hence thesis by A3;
end;
let x be object;
assume x in X` (+) B!;
then consider x1,b1 being Point of T such that
A5: x=x1+b1 and
A6: x1 in X` and
A7: b1 in B!;
reconsider xx=x as Point of T by A5;
consider q being Point of T such that
A8: b1=-q and
A9: q in B by A7;
xx=x1-q by A5,A8;
then
A10: xx+q=x1 by Lm2;
q+xx in {q1+xx where q1 is Point of T:q1 in B}by A9;
then
A11: B+xx meets X` by A6,A10,XBOOLE_0:3;
not xx in (X (-) B)
proof
assume xx in (X (-) B);
then ex yy being Point of T st xx=yy & B+yy c= X;
hence contradiction by A11,SUBSET_1:24;
end;
hence thesis by XBOOLE_0:def 5;
end;
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
(X (-) B) (+) B;
coherence;
end;
:: Adjunction Closing
definition
let T be non empty addLoopStr,X,B be Subset of T;
func X (o) B -> Subset of T equals
(X (+) B) (-) B;
coherence;
end;
theorem
(X` (O) B!)` = X (o) B
proof
(X` (O) B!)` =(((X` (-) B!)` (-) B)`)` by Th37
.=X (+) (B!)! (-) B by Th37
.=X (+) B (-) B by Th1;
hence thesis;
end;
theorem
(X` (o) B!)` = X (O) B
proof
(X` (o) B!)` =(X` (+) B!)` (+) (B!)! by Th38
.=(X` (+) B!)` (+) B by Th1
.=(X (-) B)`` (+) B by Th38;
hence thesis;
end;
theorem Th41:
X (O) B c= X & X c= X (o) B
proof
thus X (O) B c= X
proof
let x be object;
assume x in X (O) B;
then consider y1,y2 being Point of T such that
A1: x=y1+y2 and
A2: y1 in X (-) B and
A3: y2 in B;
consider y being Point of T such that
A4: y1=y and
A5: B+y c= X by A2;
x in B+y by A1,A3,A4;
hence thesis by A5;
end;
thus thesis by Th20;
end;
theorem Th42:
X (O) X = X
proof
thus X (O) X c= X by Th41;
let x be object;
assume
A1: x in X;
then reconsider x1=x as Point of T;
X+0.T c= X by Th21;
then 0.T in X (-) X;
then x1+0.T in (X (-) X) (+) X by A1;
hence thesis;
end;
theorem
(X (O) B) (-) B c= X (-) B & (X (O) B) (+) B c= X (+) B
proof
X (O) B c= X by Th41;
hence thesis by Th9;
end;
theorem
X (-) B c= (X (o) B) (-) B & X (+) B c= (X (o) B) (+) B
proof
X c= X (o) B by Th41;
hence thesis by Th9;
end;
theorem Th45:
X c= Y implies X (O) B c= Y (O) B & X (o) B c= Y (o) B
proof
assume
A1: X c= Y;
thus X (O) B c= Y (O) B
proof
let x be object;
assume x in X (O) B;
then consider x2,b2 being Point of T such that
A2: x=x2+b2 and
A3: x2 in X (-) B and
A4: b2 in B;
consider y being Point of T such that
A5: x2=y and
A6: B+y c= X by A3;
B+y c= Y by A1,A6;
then x2 in {y1 where y1 is Point of T:B+y1 c= Y}by A5;
hence thesis by A2,A4;
end;
let x be object;
assume x in X (o) B;
then consider x2 being Point of T such that
A7: x=x2 and
A8: B+x2 c= X (+) B;
X (+) B c= Y (+) B by A1,Th9;
then B+x2 c= Y (+) B by A8;
hence thesis by A7;
end;
theorem Th46:
(X+p) (O) Y = (X (O) Y)+p
proof
thus (X+p) (O) Y = ((X (-) Y)+p) (+) Y by Th14
.= (X (O) Y)+p by Th15;
end;
theorem
(X+p) (o) Y = (X (o) Y)+p
proof
thus (X+p) (o) Y = ((X (+) Y)+p) (-) Y by Th15
.= (X (o) Y)+p by Th14;
end;
theorem
C c= B implies X (O) B c= (X (-) C) (+) B
proof
assume
A1: C c= B;
let x be object;
assume x in X (O) B;
then consider x1,b1 being Point of T such that
A2: x=x1+b1 and
A3: x1 in X (-) B and
A4: b1 in B;
consider x2 being Point of T such that
A5: x1=x2 and
A6: B+x2 c= X by A3;
C+x2 c= B+x2 by A1,Th3;
then C+x2 c= X by A6;
then x1 in X (-) C by A5;
hence thesis by A2,A4;
end;
theorem
B c= C implies X (o) B c= (X (+) C) (-) B
proof
assume B c= C;
then
A1: X (+) B c= X (+) C by Th10;
let x be object;
assume x in X (o) B;
then consider x2 being Point of T such that
A2: x=x2 and
A3: B+x2 c= X (+) B;
B+x2 c= X (+) C by A3,A1;
hence thesis by A2;
end;
theorem Th50:
X (+) Y = (X (o) Y) (+) Y & X (-) Y = (X (O) Y) (-) Y
proof
(X (o) Y) (+) Y =(X (+) Y) (O) Y;
then
A1: (X (o) Y) (+) Y c= X (+) Y by Th41;
X c= X (o) Y by Th41;
then X (+) Y c= (X (o) Y) (+) Y by Th9;
hence X (+) Y = (X (o) Y) (+) Y by A1;
(X (O) Y) (-) Y = (X (-) Y) (o) Y;
hence X (-) Y c= (X (O) Y) (-) Y by Th41;
X (O) Y c= X by Th41;
hence thesis by Th9;
end;
theorem
X (+) Y = (X (+) Y) (O) Y & X (-) Y = (X (-) Y) (o) Y
proof
(X (+) Y) (O) Y =(X (o) Y) (+) Y;
hence X (+) Y = (X (+) Y) (O) Y by Th50;
(X (-) Y) (o) Y =(X (O) Y) (-) Y;
hence thesis by Th50;
end;
theorem
(X (O) B) (O) B = X (O) B
proof
thus (X (O) B) (O) B c= X (O) B by Th41;
let x be object;
assume x in X (O) B;
then consider x1,b1 being Point of T such that
A1: x=x1+b1 and
A2: x1 in X (-) B and
A3: b1 in B;
consider x2 being Point of T such that
A4: x1=x2 and
A5: B+x2 c= X by A2;
(B+x2) (O) B c= X (O) B by A5,Th45;
then (B (O) B)+x2 c= X (O) B by Th46;
then B+x2 c= X (O) B by Th42;
then x1 in {x4 where x4 is Point of T:B+x4 c= X (O) B}by A4;
hence thesis by A1,A3;
end;
theorem
(X (o) B) (o) B = X (o) B by Th50;
theorem
X (O) B c= (X \/ Y) (O) B
proof
X c= X \/ Y by XBOOLE_1:7;
hence thesis by Th45;
end;
theorem
B = B (O) B1 implies X (O) B c= X (O) B1
proof
assume
A1: B = B (O) B1;
let x be object;
assume x in X (O) B;
then consider x1,b1 being Point of T such that
A2: x=x1+b1 and
A3: x1 in X (-) B and
A4: b1 in B;
consider x2 being Point of T such that
A5: x1=x2 & B+x2 c= X by A3;
consider x3,b2 being Point of T such that
A6: b1=x3+b2 and
A7: x3 in B (-) B1 and
A8: b2 in B1 by A1,A4;
consider x4 being Point of T such that
A9: x3=x4 and
A10: B1+x4 c= B by A7;
B1+x4+x2 c= B+x2 by A10,Th3;
then B1+x3+x1 c= X by A5,A9;
then B1+(x3+x1) c= X by Th16;
then x1+x3 in X (-) B1;
then x1+x3+b2 in (X (-) B1) (+) B1 by A8;
hence thesis by A2,A6,RLVECT_1:def 3;
end;
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
{t*a where a is Point of T : a in A};
coherence
proof
now
let x be object;
assume x in {t*a where a is Point of T:a in A};
then ex q being Point of T st x = t*q & q in A;
hence x in the carrier of T;
end;
hence thesis by TARSKI:def 3;
end;
end;
reserve t,s,r1 for Real;
theorem
for X being Subset of T st X = {} holds 0(.)X = {}
proof
let X be Subset of T;
assume
A1: X = {};
now
given x being object such that
A2: x in 0(.)X;
ex a being Point of T st x = 0 * a & a in X by A2;
hence contradiction by A1;
end;
hence thesis by XBOOLE_0:def 1;
end;
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
for X being non empty Subset of TOP-REAL n holds 0(.)X = {0.TOP-REAL n}
proof
set T = TOP-REAL n;
let X be non empty Subset of TOP-REAL n;
thus 0(.)X c= {0.T}
proof
let x be object;
assume x in 0(.)X;
then ex a being Point of T st x=0 * a & a in X;
then x = 0.T by RLVECT_1:10;
hence thesis by ZFMISC_1:31;
end;
let x be object;
set d = the Element of X;
reconsider d1=d as Point of T;
assume x in {0.T};
then {x} c= {0.T} by ZFMISC_1:31;
then x = 0.T by ZFMISC_1:18;
then x = 0 * d1 by RLVECT_1:10;
hence thesis;
end;
theorem Th58:
1(.)X = X
proof
thus 1(.)X c= X
proof
let x be object;
assume x in 1(.)X;
then ex z being Point of TOP-REAL n st x=1*z & z in X;
hence thesis by RLVECT_1:def 8;
end;
let x be object;
assume
A1: x in X;
then reconsider x1=x as Point of TOP-REAL n;
x1=1*x1 by RLVECT_1:def 8;
hence thesis by A1;
end;
theorem
2(.)X c= X (+) X
proof
let x be object;
assume x in 2(.)X;
then consider z being Point of TOP-REAL n such that
A1: x=2*z and
A2: z in X;
x = (1+1)*z by A1
.= 1*z+1*z by RLVECT_1:def 6
.= z + 1*z by RLVECT_1:def 8
.= z + z by RLVECT_1:def 8;
hence thesis by A2;
end;
theorem Th60:
(t*s)(.)X = t(.)(s(.)X)
proof
thus (t*s)(.)X c= t(.)(s(.)X)
proof
let x be object;
assume x in (t*s)(.)X;
then consider z being Point of TOP-REAL n such that
A1: x = (t*s) * z & z in X;
x = t*(s*z) & s*z in s(.)X by A1,RLVECT_1:def 7;
hence thesis;
end;
let x be object;
assume x in t(.)(s(.)X);
then consider z being Point of TOP-REAL n such that
A2: x = t * z and
A3: z in s(.)X;
consider z1 being Point of TOP-REAL n such that
A4: z = s * z1 and
A5: z1 in X by A3;
x = (t*s)*z1 by A2,A4,RLVECT_1:def 7;
hence thesis by A5;
end;
theorem Th61:
X c= Y implies t(.)X c= t(.)Y
proof
assume
A1: X c= Y;
let x be object;
assume x in t(.)X;
then ex a being Point of TOP-REAL n st x = t*a & a in X;
hence thesis by A1;
end;
theorem Th62:
t(.)(X+x) = t(.)X+t*x
proof
thus t(.)(X+x) c= t(.)X+t*x
proof
let b be object;
assume b in t(.)(X+x);
then consider a being Point of TOP-REAL n such that
A1: b = t*a and
A2: a in X+x;
consider x1 being Point of TOP-REAL n such that
A3: a=x1+x and
A4: x1 in X by A2;
A5: t*x1 in t(.)X by A4;
b=t*x1+t*x by A1,A3,RLVECT_1:def 5;
hence thesis by A5;
end;
let b be object;
assume b in t(.)X+t*x;
then consider x1 being Point of TOP-REAL n such that
A6: b = x1+t*x and
A7: x1 in t(.)X;
consider a being Point of TOP-REAL n such that
A8: x1=t*a and
A9: a in X by A7;
A10: a+x in X+x by A9;
b=t*(a+x) by A6,A8,RLVECT_1:def 5;
hence thesis by A10;
end;
theorem Th63:
t(.)(X (+) Y) = t(.)X (+) t(.)Y
proof
thus t(.)(X (+) Y) c= t(.)X (+) t(.)Y
proof
let b be object;
assume b in t(.)(X (+) Y);
then consider a being Point of TOP-REAL n such that
A1: b = t*a and
A2: a in X (+) Y;
consider x,y being Point of TOP-REAL n such that
A3: a=x+y and
A4: x in X & y in Y by A2;
A5: t*x in t(.)X & t*y in t(.)Y by A4;
b=t*x+t*y by A1,A3,RLVECT_1:def 5;
hence thesis by A5;
end;
let b be object;
assume b in t(.)X (+) t(.)Y;
then consider x,y being Point of TOP-REAL n such that
A6: b = x+y and
A7: x in t(.)X and
A8: y in t(.)Y;
consider y1 being Point of TOP-REAL n such that
A9: y=t*y1 and
A10: y1 in Y by A8;
consider x1 being Point of TOP-REAL n such that
A11: x=t*x1 and
A12: x1 in X by A7;
A13: x1+y1 in X (+) Y by A12,A10;
b=t*(x1+y1) by A6,A11,A9,RLVECT_1:def 5;
hence thesis by A13;
end;
theorem Th64:
t<>0 implies t(.)(X (-) Y) = t(.)X (-) t(.)Y
proof
assume
A1: t<>0;
thus t(.)(X (-) Y) c= t(.)X (-) t(.)Y
proof
let b be object;
assume b in t(.)(X (-) Y);
then consider a being Point of TOP-REAL n such that
A2: b = t*a and
A3: a in X (-) Y;
consider x being Point of TOP-REAL n such that
A4: a=x and
A5: Y+x c= X by A3;
t(.)(Y+x) c= t(.)X by A5,Th61;
then t(.)Y+t*x c= t(.)X by Th62;
hence thesis by A2,A4;
end;
let b be object;
assume b in t(.)X (-) t(.)Y;
then consider x being Point of TOP-REAL n such that
A6: b = x and
A7: t(.)Y+x c= t(.)X;
(1/t)(.)(t(.)Y+x) c= (1/t)(.)(t(.)X) by A7,Th61;
then (1/t)(.)(t(.)Y+x) c= (1/t*t)(.)X by Th60;
then (1/t)(.)(t(.)Y)+(1/t)*x c= (1/t*t)(.)X by Th62;
then (1/t*t)(.)Y+(1/t)*x c= (1/t*t)(.)X by Th60;
then 1(.)Y+(1/t)*x c= (1/t*t)(.)X by A1,XCMPLX_1:87;
then 1(.)Y+(1/t)*x c= 1(.)X by A1,XCMPLX_1:87;
then Y+(1/t)*x c= 1(.)X by Th58;
then Y+(1/t)*x c= X by Th58;
then (1/t)*x in {z where z is Point of TOP-REAL n :Y+z c= X};
then t*((1/t)*x) in {t*a1 where a1 is Point of TOP-REAL n :a1 in X (-) Y};
then (1/t*t)*x in t(.)(X (-) Y) by RLVECT_1:def 7;
then 1*x in t(.)(X (-) Y) by A1,XCMPLX_1:87;
hence thesis by A6,RLVECT_1:def 8;
end;
theorem
t<>0 implies t(.)(X (O) Y) = t(.)X (O) t(.)Y
proof
assume
A1: t<>0;
t(.)(X (O) Y) =t(.)(X (-) Y) (+) t(.)Y by Th63
.=t(.)X (-) t(.)Y (+) t(.)Y by A1,Th64;
hence thesis;
end;
theorem
t<>0 implies t(.)(X (o) Y) = t(.)X (o) t(.)Y
proof
assume t<>0;
then t(.)(X (o) Y) =t(.)(X (+) Y) (-) t(.)Y by Th64
.=t(.)X (+) t(.)Y (-) t(.)Y by Th63;
hence thesis;
end;
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
(X (-) B1) /\ (X` (-) B2);
coherence;
end;
:: Thickening
definition
let T be non empty RLSStruct,X,B1,B2 be Subset of T;
func X (&) (B1,B2) -> Subset of T equals
X \/ (X (*) (B1,B2));
coherence;
end;
:: Thinning
definition
let T be non empty RLSStruct,X,B1,B2 be Subset of T;
func X (@) (B1,B2) -> Subset of T equals
X \ (X (*) (B1,B2));
coherence;
end;
theorem
B1 = {} implies X (*) (B1,B2) = X` (-) B2
proof
assume B1 = {};
then X (*) (B1,B2) = (X` (-) B2) /\ the carrier of TOP-REAL n by Th8;
hence thesis by XBOOLE_1:28;
end;
theorem
B2 = {} implies X (*) (B1,B2) = X (-) B1
proof
assume B2 = {};
then X (*) (B1,B2) = (X (-) B1)/\(the carrier of TOP-REAL n) by Th8;
hence thesis by XBOOLE_1:28;
end;
theorem
0.TOP-REAL n in B1 implies X (*) (B1,B2) c= X
proof
assume
A1: 0.TOP-REAL n in B1;
let x be object;
assume x in X (*) (B1,B2);
then x in X (-) B1 by XBOOLE_0:def 4;
then consider y being Point of TOP-REAL n such that
A2: x=y and
A3: B1+y c= X;
0.TOP-REAL n + y in {z+y where z is Point of TOP-REAL n:z in B1} by A1;
then x in B1+y by A2;
hence thesis by A3;
end;
theorem
0.TOP-REAL n in B2 implies (X (*) (B1,B2)) /\ X = {}
proof
assume
A1: 0.TOP-REAL n in B2;
now
given x being object such that
A2: x in (X (*) (B1,B2)) /\ X;
A3: x in X by A2,XBOOLE_0:def 4;
x in (X (*) (B1,B2)) by A2,XBOOLE_0:def 4;
then x in X` (-) B2 by XBOOLE_0:def 4;
then consider y being Point of TOP-REAL n such that
A4: x=y and
A5: B2+y c= X`;
0.TOP-REAL n + y in {z+y where z is Point of TOP-REAL n :z in B2} by A1;
then x in B2+y by A4;
hence contradiction by A3,A5,XBOOLE_0:def 5;
end;
hence thesis by XBOOLE_0:def 1;
end;
theorem
0.TOP-REAL n in B1 implies X (&) (B1,B2) = X
proof
assume
A1: 0.TOP-REAL n in B1;
thus X (&) (B1,B2) c= X
proof
let x be object;
assume
A2: x in X (&) (B1,B2);
per cases by A2,XBOOLE_0:def 3;
suppose
x in X;
hence thesis;
end;
suppose
x in X (*) (B1,B2);
then x in X (-) B1 by XBOOLE_0:def 4;
then consider y being Point of TOP-REAL n such that
A3: x=y and
A4: B1+y c= X;
0.TOP-REAL n + y in {z+y where z is Point of TOP-REAL n:z in B1} by A1;
then x in B1+y by A3;
hence thesis by A4;
end;
end;
thus thesis by XBOOLE_1:7;
end;
theorem
0.TOP-REAL n in B2 implies X (@) (B1,B2) = X
proof
assume
A1: 0.TOP-REAL n in B2;
thus X (@) (B1,B2) c= X
by XBOOLE_0:def 5;
let x be object;
assume
A2: x in X;
not x in (X (*) (B1,B2))
proof
assume x in (X (*) (B1,B2));
then x in X` (-) B2 by XBOOLE_0:def 4;
then consider y being Point of TOP-REAL n such that
A3: x=y and
A4: B2+y c= X`;
0.TOP-REAL n + y in {z+y where z is Point of TOP-REAL n:z in B2} by A1;
then x in B2+y by A3;
hence contradiction by A2,A4,XBOOLE_0:def 5;
end;
hence thesis by A2,XBOOLE_0:def 5;
end;
theorem
X (@) (B2,B1) = (X` (&) (B1,B2))`
proof
(X` (&) (B1,B2))` =((X \ ((X` (-) B1) /\ ((X`)` (-) B2)))`)` by SUBSET_1:14
.=X \ (X (*) (B2,B1));
hence thesis;
end;
begin :: 5. Properties of Erosion, Dilation, Adjunction Opening,
:: Adjunction Closing on Convex sets
theorem Th74:
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
proof
let V be RealLinearSpace, B be Subset of V;
thus B is convex implies 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
proof
assume
A1: B is convex;
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
proof
let x,y be Point of V,r be Real;
assume that
A2: 0 <= r & r <= 1 and
A3: x in B & y in B;
(1-r)*y + r*x in {(1-r1)*y+r1*x where r1 is Real:0<=r1&r1<=1}
by A2;
then
A4: (1-r)*y + r*x in LSeg(x,y) by RLTOPSP1:def 2;
LSeg(x,y) c= B by A1,A3,JORDAN1:def 1;
hence thesis by A4;
end;
hence thesis;
end;
(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) implies B is convex
proof
assume
A5: 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;
for x,y being Point of V st x in B & y in B holds LSeg(x,y) c= B
proof
let x,y be Point of V;
assume
A6: x in B & y in B;
let p be object;
assume p in LSeg(x,y);
then p in {(1-r1) * y + r1*x where r1 is Real:0<=r1&r1<=1} by
RLTOPSP1:def 2;
then ex r1 being Real
st p = (1-r1) * y + r1 * x & 0<=r1 & r1<=1;
hence thesis by A5,A6;
end;
hence thesis by RLTOPSP1:22;
end;
hence thesis;
end;
definition
let V be RealLinearSpace, B be Subset of V;
redefine attr B is convex means
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;
compatibility by Th74;
end;
reserve n for Element of NAT;
reserve X,B for Subset of TOP-REAL n;
theorem
X is convex implies X! is convex
proof
assume
A1: X is convex;
for x,y be Point of TOP-REAL n,r be Real st 0 <= r & r <= 1 & x
in X! & y in X! holds r*x + (1-r)*y in X!
proof
let x,y be Point of TOP-REAL n,r be Real;
assume that
A2: 0 <= r & r <= 1 and
A3: x in X! and
A4: y in X!;
consider x2 being Point of TOP-REAL n such that
A5: y=-x2 and
A6: x2 in X by A4;
consider x1 being Point of TOP-REAL n such that
A7: x=-x1 and
A8: x1 in X by A3;
r*x1 + (1-r)*x2 in X by A1,A2,A8,A6;
then -(r*x1 + (1-r)*x2) in X!;
then -(r*x1) - ((1-r)*x2) in X! by RLVECT_1:30;
then r*(-x1) + -((1-r)*x2) in X! by RLVECT_1:25;
hence thesis by A7,A5,RLVECT_1:25;
end;
hence thesis;
end;
theorem Th76:
X is convex & B is convex implies X (+) B is convex & X (-) B is convex
proof
assume that
A1: X is convex and
A2: B is convex;
for x,y be Point of TOP-REAL n,r be Real st 0 <= r & r <= 1 & x
in X (+) B & y in X (+) B holds r*x + (1-r)*y in X (+) B
proof
let x,y be Point of TOP-REAL n,r be Real;
assume that
A3: 0 <= r & r <= 1 and
A4: x in X (+) B and
A5: y in X (+) B;
consider x2,b2 being Point of TOP-REAL n such that
A6: y=x2+b2 and
A7: x2 in X & b2 in B by A5;
consider x1,b1 being Point of TOP-REAL n such that
A8: x=x1+b1 and
A9: x1 in X & b1 in B by A4;
r*x1 + (1-r)*x2 in X & r*b1 + (1-r)*b2 in B by A1,A2,A3,A9,A7;
then
(r*x1 + (1-r)*x2)+(r*b1 + (1-r)*b2) in {x3+b3 where x3,b3 is Point of
TOP-REAL n:x3 in X&b3 in B};
then (r*x1 + (1-r)*x2)+r*b1 + (1-r)*b2 in X (+) B by RLVECT_1:def 3;
then r*x1 + r*b1+(1-r)*x2 + (1-r)*b2 in X (+) B by RLVECT_1:def 3;
then (r*x1 + r*b1)+((1-r)*x2 + (1-r)*b2) in X (+) B by RLVECT_1:def 3;
then r*(x1 + b1)+((1-r)*x2 + (1-r)*b2) in X (+) B by RLVECT_1:def 5;
hence thesis by A8,A6,RLVECT_1:def 5;
end;
hence X (+) B is convex;
for x,y be Point of TOP-REAL n,r be Real st 0 <= r & r <= 1 & x
in X (-) B & y in X (-) B holds r*x + (1-r)*y in X (-) B
proof
let x,y be Point of TOP-REAL n,r be Real;
assume that
A10: 0 <= r & r <= 1 and
A11: x in X (-) B & y in X (-) B;
A12: (ex x1 being Point of TOP-REAL n st x=x1 & B+x1 c= X )& ex y1 being
Point of TOP-REAL n st y=y1 & B+y1 c= X by A11;
B+(r*x + (1-r)*y) c= X
proof
let b1 be object;
assume b1 in B+(r*x + (1-r)*y);
then consider b being Point of TOP-REAL n such that
A13: b1=b+(r*x + (1-r)*y) and
A14: b in B;
b+x in B+x & b+y in {b2+y where b2 is Point of TOP-REAL n:b2 in B}
by A14;
then r*(b+x) + (1-r)*(b+y) in X by A1,A10,A12;
then r*b+r*x + (1-r)*(b+y) in X by RLVECT_1:def 5;
then r*b+r*x + ((1-r)*b+(1-r)*y) in X by RLVECT_1:def 5;
then r*b+r*x + (1-r)*b+(1-r)*y in X by RLVECT_1:def 3;
then r*b+r*x + (1*b-r*b)+(1-r)*y in X by RLVECT_1:35;
then r*b+r*x + 1*b-r*b+(1-r)*y in X by RLVECT_1:def 3;
then r*x+1*b + r*b-r*b+(1-r)*y in X by RLVECT_1:def 3;
then r*x+1*b +(1-r)*y in X by RLVECT_4:1;
then 1*b +(r*x+(1-r)*y) in X by RLVECT_1:def 3;
hence thesis by A13,RLVECT_1:def 8;
end;
hence thesis;
end;
hence thesis;
end;
theorem
X is convex & B is convex implies X (O) B is convex & X (o) B is convex
proof
assume that
A1: X is convex and
A2: B is convex;
X (-) B is convex by A1,A2,Th76;
hence X (O) B is convex by A2,Th76;
X (+) B is convex by A1,A2,Th76;
hence thesis by A2,Th76;
end;
theorem
B is convex & 0 < t & 0 < s implies (s+t)(.)B = s(.)B (+) t(.)B
proof
assume that
A1: B is convex and
A2: 0 < t & 0 < s;
thus (s+t)(.)B c= s(.)B (+) t(.)B
proof
let x be object;
assume x in (s+t)(.)B;
then consider b being Point of TOP-REAL n such that
A3: x=(s+t)*b and
A4: b in B;
A5: t*b in t(.)B by A4;
x = s*b +t*b & s*b in s(.)B by A3,A4,RLVECT_1:def 6;
hence thesis by A5;
end;
let x be object;
assume x in s(.)B (+) t(.)B;
then consider s1,s2 being Point of TOP-REAL n such that
A6: x=s1+s2 and
A7: s1 in s(.)B and
A8: s2 in t(.)B;
consider b2 being Point of TOP-REAL n such that
A9: s2=t*b2 and
A10: b2 in B by A8;
consider b1 being Point of TOP-REAL n such that
A11: s1=s*b1 and
A12: b1 in B by A7;
s/(s+t) < (s+t)/(s+t) by A2,XREAL_1:29,74;
then s/(s+t) < 1 by A2,XCMPLX_1:60;
then (s/(s+t))*b1 +(1-s/(s+t))*b2 in B by A1,A2,A12,A10;
then (s+t)*((s/(s+t))*b1 +(1-s/(s+t))*b2) in {(s+t)*zz where zz is Point of
TOP-REAL n: zz in B};
then (s+t)*((s/(s+t))*b1) +(s+t)*((1-s/(s+t))*b2) in (s+t)(.)B by
RLVECT_1:def 5;
then (s+t)*(s/(s+t))*b1 +(s+t)*((1-s/(s+t))*b2) in (s+t)(.)B by
RLVECT_1:def 7;
then (s+t)*(s/(s+t))*b1 +(s+t)*(1-s/(s+t))*b2 in (s+t)(.)B by RLVECT_1:def 7;
then s*b1 +(s+t)*(1-s/(s+t))*b2 in (s+t)(.)B by A2,XCMPLX_1:87;
then s*b1 +(s+t)*((s+t)/(s+t)-s/(s+t))*b2 in (s+t)(.)B by A2,XCMPLX_1:60;
then s*b1 +(s+t)*((s+t-s)/(s+t))*b2 in (s+t)(.)B by XCMPLX_1:120;
hence thesis by A2,A6,A11,A9,XCMPLX_1:87;
end;