:: The Formal Construction of Fuzzy Numbers :: by Adam Grabowski :: :: Received December 31, 2014 :: Copyright (c) 2014-2018 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, XBOOLE_0, SUBSET_1, XXREAL_1, CARD_1, RELAT_1, TARSKI, FUNCT_1, XXREAL_0, PARTFUN1, ARYTM_1, ARYTM_3, COMPLEX1, FUZZY_1, GRAPH_2, MEASURE5, MSALIMIT, FUZNUM_1, REAL_1, ORDINAL2, XXREAL_2, TREES_1, RCOMP_1, ZFMISC_1, NUMPOLY1, JGRAPH_2, FUNCT_4, PRE_TOPC, FCONT_1; notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, XCMPLX_0, XXREAL_2, COMPLEX1, XREAL_0, FUNCT_1, PARTFUN1, FCONT_1, RELSET_1, FUNCT_4, RCOMP_1, MEASURE5, FUZZY_1; constructors COMPLEX1, RFUNCT_1, INTEGRA1, SEQ_4, RELSET_1, FUZZY_1, FCONT_1, FUNCT_4; registrations RELSET_1, NUMBERS, XXREAL_0, MEMBERED, XBOOLE_0, VALUED_0, FUNCT_2, XREAL_0, ORDINAL1, FCONT_1, RELAT_1, TOPREALB, FUNCT_4, FUNCT_1, XCMPLX_0, NAT_1, RCOMP_1; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; definitions XBOOLE_0, TARSKI, XXREAL_2; equalities FUZZY_1, RCOMP_1; expansions TARSKI, FCONT_1; theorems TARSKI, FUNCT_1, FUNCT_3, ABSVALUE, PARTFUN1, ZFMISC_1, XBOOLE_0, XBOOLE_1, COMPLEX1, XREAL_1, XXREAL_0, XXREAL_1, FUNCT_2, RELAT_1, MEASURE5, XREAL_0, XXREAL_2, FCONT_1, XCMPLX_1, FUZZY_2, FUNCT_4, RCOMP_1, ENUMSET1; begin :: Preliminaries: Affine Maps theorem RealNon: for a,b being Real st a <= b holds REAL \ ].a,b.[ <> {} proof let a,b be Real; assume a <= b; consider c being Real such that A1: c < a by XREAL_1:2; A2: not c in ].a,b.[ by A1,XXREAL_1:4; c in REAL by XREAL_0:def 1; hence thesis by A2,XBOOLE_0:def 5; end; reserve a,b,c,x for Real; theorem Ah1: AffineMap (1/(b-a),-a/(b-a)).a = 0 proof AffineMap (1/(b-a),-a/(b-a)).a = (1/(b-a))*a+-a/(b-a) by FCONT_1:def 4 .= (1/(b-a))*a+(-a)/(b-a) by XCMPLX_1:187 .= (1/(b-a))*a+a*((-1))/(b-a) .= a*(1/(b-a))+a*((-1)/(b-a)) by XCMPLX_1:74 .= a*(1/(b-a)+(-1)/(b-a)) .= a*(1/(b-a)+-1/(b-a)) by XCMPLX_1:187 .= 0; hence thesis; end; theorem Ab1: b - a <> 0 implies AffineMap (1/(b-a),-a/(b-a)).b = 1 proof assume A1: b - a <> 0; AffineMap (1/(b-a),-a/(b-a)).b = (1/(b-a))*b+-a/(b-a) by FCONT_1:def 4 .= (b/(b-a))+-a/(b-a) by XCMPLX_1:99 .= (b/(b-a))+(-a)/(b-a) by XCMPLX_1:187 .= (b+-a)/(b-a) by XCMPLX_1:62 .= (1/(b-a))*(b+-a) by XCMPLX_1:99 .= 1 by XCMPLX_1:106,A1; hence thesis; end; theorem Cb1: c - b <> 0 implies AffineMap (-1/(c-b),c/(c-b)).b = 1 proof assume A1: c - b <> 0; AffineMap (-1/(c-b),c/(c-b)).b = (-1/(c-b))*b+c/(c-b) by FCONT_1:def 4 .= ((-1)/(c-b))*b+c/(c-b) by XCMPLX_1:187 .= (((-1)*b)/(c-b))+c/(c-b) by XCMPLX_1:74 .= (-b+c)/(c-b) by XCMPLX_1:62 .= 1 by A1,XCMPLX_1:60; hence thesis; end; theorem Cb2: AffineMap (-1/(c-b),c/(c-b)).c = 0 proof AffineMap (-1/(c-b),c/(c-b)).c = (-1/(c-b))*c+c/(c-b) by FCONT_1:def 4 .= ((-1)/(c-b))*c+c/(c-b) by XCMPLX_1:187 .= (((-1)*c)/(c-b))+c/(c-b) by XCMPLX_1:74 .= (-c+c)/(c-b) by XCMPLX_1:62 .= 0; hence thesis; end; theorem Hope3: b - a <> 0 & AffineMap (1/(b-a),-a/(b-a)).x = 1 implies x = b proof assume that A0: b - a <> 0 and A1: AffineMap (1/(b-a),-a/(b-a)).x = 1; x in REAL & b in REAL by XREAL_0:def 1; then A3: x in dom AffineMap (1/(b-a),-a/(b-a)) & b in dom AffineMap (1/(b-a),-a/(b-a)) by FUNCT_2:def 1; AffineMap (1/(b-a),-a/(b-a)).b = 1 by A0,Ab1; hence thesis by A1,FUNCT_1:def 4,A3,A0; end; theorem Hope4: c - b <> 0 & AffineMap (-1/(c-b),c/(c-b)).x = 1 implies x = b proof assume that A0: c - b <> 0 and A1: AffineMap (-1/(c-b),c/(c-b)).x = 1; x in REAL & b in REAL by XREAL_0:def 1; then A3: x in dom AffineMap (-1/(c-b),c/(c-b)) & b in dom AffineMap (-1/(c-b),c/(c-b)) by FUNCT_2:def 1; AffineMap (-1/(c-b),c/(c-b)).b = 1 by A0,Cb1; hence thesis by A1,FUNCT_1:def 4,A3,A0; end; theorem rng AffineMap (0,a) = {a} proof set f = AffineMap (0,a); thus rng f c= {a} proof let y be object; assume y in rng f; then consider x being object such that A1: x in dom f & y = f.x by FUNCT_1:def 3; reconsider x as Real by A1; y = 0 * x + a by A1,FCONT_1:def 4 .= a; hence thesis by TARSKI:def 1; end; let y be object; assume a0: y in {a}; 0 in REAL by XREAL_0:def 1; then A1: 0 in dom f by FUNCT_2:def 1; y = 0 * 0 + a by a0,TARSKI:def 1 .= f.0 by FCONT_1:def 4; hence thesis by FUNCT_1:def 3,A1; end; theorem Andr1a: for C being non empty Subset of REAL holds rng (AffineMap (0,a) | C) = {a} proof let C be non empty Subset of REAL; set f = AffineMap (0,a) | C; thus rng f c= {a} proof let y be object; assume y in rng f; then consider x being object such that A1: x in dom f & y = f.x by FUNCT_1:def 3; reconsider x as Real by A1; y = AffineMap (0,a).x by A1,FUNCT_1:49; then y = 0 * x + a by FCONT_1:def 4 .= a; hence thesis by TARSKI:def 1; end; let y be object; assume a0: y in {a}; reconsider o = the Element of C as Real; C c= REAL; then C c= dom AffineMap(0,a) by FUNCT_2:def 1; then a1: dom f = C by RELAT_1:62; y = 0 * o + a by a0,TARSKI:def 1 .= AffineMap (0,a).o by FCONT_1:def 4 .= f.o by FUNCT_1:49; hence thesis by FUNCT_1:def 3,a1; end; theorem Hope1: b - a > 0 implies rng ((AffineMap (1/(b-a),-a/(b-a)) | [.a,b.])) = [.0,1.] proof set f = AffineMap (1/(b-a),-a/(b-a)); set g = f | [.a,b.]; assume A0: b - a > 0; thus rng g c= [.0,1.] proof let y be object; assume Y0: y in rng g; then consider x being object such that A1: x in dom g and A2: y = g.x by FUNCT_1:def 3; Y1: x in [.a,b.] by A1,RELAT_1:57; reconsider xx = x as Real by A1; reconsider yy = y as Real by Y0; S4: y = f.xx by FUNCT_1:47,A1,A2; A4: a <= xx by Y1,XXREAL_1:1; S2: f.a = 0 by Ah1; S5: f.a <= f.xx by A4,FCONT_1:53,A0; xx <= b by Y1,XXREAL_1:1; then S6: f.xx <= f.b by A0,FCONT_1:53; f.b = 1 by Ab1,A0; hence thesis by S4,S2,S5,S6; end; let y be object; assume V1: y in [.0,1.]; then reconsider yy = y as Real; set A = 1 / (b-a); set B = -a / (b-a); L2: (f qua Function)" = AffineMap (A",-B/A) by A0,FCONT_1:56; then L3: (f qua Function)".0 = A" * 0 + -B/A by FCONT_1:def 4 .= -(((-a) / (b-a))/(1 / (b-a))) by XCMPLX_1:187 .= -((-a) / 1) by XCMPLX_1:55,A0 .= a; set x = (f qua Function)".yy; reconsider xx = x as Real by L2; X1: -B/A = -(((-a) / (b-a))/(1 / (b-a))) by XCMPLX_1:187 .= -((-a) / 1) by XCMPLX_1:55,A0 .= a; L4: (f qua Function)".1 = A" * 1 + -B/A by FCONT_1:def 4,L2 .= 1/A + -B/A by XCMPLX_1:215 .= b-a + a by XCMPLX_1:52,X1 .= b; J2: 0 <= yy & yy <= 1 by XXREAL_1:1,V1; then J3: a <= xx by FCONT_1:53,L2,A0,L3; xx <= b by FCONT_1:53,L2,A0,J2,L4; then J4: x in [.a,b.] by J3; j5: dom f = REAL by FUNCT_2:def 1; T1: x in dom g by J4,j5,RELAT_1:57; rng f = REAL by FCONT_1:55,A0; then S2: yy in rng f by XREAL_0:def 1; g.((f qua Function)".yy) = f.((f qua Function)".yy) by FUNCT_1:49,J4 .= yy by A0,S2,FUNCT_1:35; hence thesis by T1,FUNCT_1:def 3; end; theorem c - b > 0 implies rng ((AffineMap (-1/(c-b),c/(c-b)) | ].b,c.])) = [.0,1.[ proof set f = AffineMap (-1/(c-b),c/(c-b)); set g = f | ].b,c.]; assume A0: c - b > 0; thus rng g c= [.0,1.[ proof let y be object; assume Y0: y in rng g; then consider x being object such that A1: x in dom g and A2: y = g.x by FUNCT_1:def 3; Y1: x in ].b,c.] by A1,RELAT_1:57; reconsider xx = x as Real by A1; reconsider yy = y as Real by Y0; S4: y = f.xx by FUNCT_1:47,A1,A2; A4: b < xx by Y1,XXREAL_1:2; S2: f.b = 1 by Cb1,A0; S5: f.b > f.xx by A4,FCONT_1:52,A0; xx <= c by Y1,XXREAL_1:2; then S6: f.xx >= f.c by A0,FCONT_1:54; f.c = 0 by Cb2; hence thesis by S4,S2,S5,S6; end; let y be object; assume V1: y in [.0,1.[; then reconsider yy = y as Real; set A = -1 / (c-b); set B = c / (c-b); L2: (f qua Function)" = AffineMap (A",-B/A) by A0,FCONT_1:56; then L3: (f qua Function)".0 = A" * 0 + -B/A by FCONT_1:def 4 .= -((c / (c-b))/((-1) / (c-b))) by XCMPLX_1:187 .= -(c / -1) by XCMPLX_1:55,A0 .= c; X1: -B/A = -((c / (c-b))/((-1) / (c-b))) by XCMPLX_1:187 .= -(c / -1) by XCMPLX_1:55,A0 .= c; L4: (f qua Function)".1 = A" * 1 + -B/A by FCONT_1:def 4,L2 .= 1/A + -B/A by XCMPLX_1:215 .= 1/((-1)/(c-b)) + c by XCMPLX_1:187,X1 .= (c-b)/(-1) + c by XCMPLX_1:57 .= b; set x = (f qua Function)".yy; reconsider xx = x as Real by L2; J2: 0 <= yy & yy < 1 by XXREAL_1:3,V1; then J3: c >= xx by FCONT_1:54,L2,A0,L3; xx > b by FCONT_1:52,L2,A0,J2,L4; then J4: x in ].b,c.] by J3; j5: dom f = REAL by FUNCT_2:def 1; T1: x in dom g by J4,j5,RELAT_1:57; rng f = REAL by FCONT_1:55,A0; then S2: yy in rng f by XREAL_0:def 1; set ff = (f qua Function)"; g.(ff.yy) = f.(ff.yy) by FUNCT_1:49,J4 .= yy by A0,S2,FUNCT_1:35; hence thesis by T1,FUNCT_1:def 3; end; theorem Hope2a: c - b > 0 implies rng ((AffineMap (-1/(c-b),c/(c-b)) | [.b,c.])) = [.0,1.] proof set f = AffineMap (-1/(c-b),c/(c-b)); set g = f | [.b,c.]; assume A0: c - b > 0; thus rng g c= [.0,1.] proof let y be object; assume Y0: y in rng g; then consider x being object such that A1: x in dom g and A2: y = g.x by FUNCT_1:def 3; Y1: x in [.b,c.] by A1,RELAT_1:57; reconsider xx = x as Real by A1; reconsider yy = y as Real by Y0; S4: y = f.xx by FUNCT_1:47,A1,A2; A4: b <= xx by Y1,XXREAL_1:1; S2: f.b = 1 by Cb1,A0; S5: f.b >= f.xx by A4,FCONT_1:54,A0; xx <= c by Y1,XXREAL_1:1; then S6: f.xx >= f.c by A0,FCONT_1:54; f.c = 0 by Cb2; hence thesis by S4,S2,S5,S6; end; let y be object; assume V1: y in [.0,1.]; then reconsider yy = y as Real; set A = -1 / (c-b); set B = c / (c-b); L2: (f qua Function)" = AffineMap (A",-B/A) by FCONT_1:56,A0; then L3: (f qua Function)".0 = A" * 0 + -B/A by FCONT_1:def 4 .= -((c / (c-b))/((-1) / (c-b))) by XCMPLX_1:187 .= -(c / -1) by XCMPLX_1:55,A0 .= c; X1: -B/A = -((c / (c-b))/((-1) / (c-b))) by XCMPLX_1:187 .= -(c / -1) by XCMPLX_1:55,A0 .= c; L4: (f qua Function)".1 = A" * 1 + -B/A by FCONT_1:def 4,L2 .= 1/A + -B/A by XCMPLX_1:215 .= 1/((-1)/(c-b)) + c by XCMPLX_1:187,X1 .= (c-b)/(-1) + c by XCMPLX_1:57 .= b; set x = (f qua Function)".yy; reconsider xx = x as Real by L2; J2: 0 <= yy & yy <= 1 by XXREAL_1:1,V1; then J3: c >= xx by FCONT_1:54,L2,A0,L3; xx >= b by FCONT_1:54,L2,A0,J2,L4; then J4: x in [.b,c.] by J3; jj: dom f = REAL by FUNCT_2:def 1; T1: x in dom g by J4,jj,RELAT_1:57; rng f = REAL by FCONT_1:55,A0; then S2: yy in rng f by XREAL_0:def 1; set ff = (f qua Function)"; g.(ff.yy) = f.(ff.yy) by FUNCT_1:49,J4 .= yy by A0,S2,FUNCT_1:35; hence thesis by T1,FUNCT_1:def 3; end; theorem Hope5: (AffineMap (0,0)).x <> 1 proof (AffineMap (0,0)).x = 0 * x + 0 by FCONT_1:def 4 .= 0; hence thesis; end; theorem AffineMap (0,1).b = 1 proof AffineMap (0,1).b = 0*b + 1 by FCONT_1:def 4 .= 1; hence thesis; end; theorem Kici1: for a being Real holds AffineMap (0,b).a = b proof let a be Real; AffineMap (0,b).a = 0 * a + b by FCONT_1:def 4 .= b; hence thesis; end; begin :: Towards Development of Fuzzy Numbers reserve C for non empty set; definition let C be non empty set; mode FuzzySet of C is Membership_Func of C; end; definition let C be non empty set; let F be FuzzySet of C; attr F is normalized means ex x being Element of C st F.x = 1; end; notation let C be non empty set; let F be FuzzySet of C; synonym F is normal for F is normalized; end; notation let C be non empty set; let F be FuzzySet of C; antonym F is subnormal for F is normal; end; definition let C be non empty set; let F be FuzzySet of C; attr F is strictly-normalized means ex x being Element of C st F.x = 1 & for y being Element of C st F.y = 1 holds y = x; end; registration let C be non empty set; cluster strictly-normalized -> normalized for FuzzySet of C; coherence; end; definition let C be non empty set; let F be FuzzySet of C; let alpha be Real; func alpha-cut F -> Subset of C equals { x where x is Element of C : F.x >= alpha }; coherence proof set H = { x where x is Element of C : F.x >= alpha }; H c= C proof let y be object; assume y in H; then consider x being Element of C such that A1: y = x & F.x >= alpha; thus thesis by A1; end; hence thesis; end; end; theorem AlphaCut1: for F being FuzzySet of C, alpha being Real holds alpha-cut F = F " ([. alpha, 1 .]) proof let F be FuzzySet of C, alpha be Real; thus alpha-cut F c= F " ([. alpha, 1 .]) proof let x be object; assume x in alpha-cut F; then consider y being Element of C such that A1: x = y & F.y >= alpha; x in C by A1; then A2: x in dom F by FUNCT_2:def 1; then F.y in [. 0, 1 .] by A1,PARTFUN1:4; then 0 <= F.y & F.y <= 1 by XXREAL_1:1; then F.y in [. alpha, 1 .] by A1; hence thesis by A1,FUNCT_1:def 7,A2; end; let x be object; assume c2: x in F"([. alpha, 1 .]); then x in dom F & F.x in [. alpha, 1 .] by FUNCT_1:def 7; then alpha <= F.x & F.x <= 1 by XXREAL_1:1; hence thesis by c2; end; registration let C; cluster UMF C -> normalized; coherence proof ex x being Element of C st (UMF C).x = 1 proof take x = the Element of C; thus thesis by FUNCT_3:def 3; end; hence thesis; end; end; registration let C; cluster normalized for FuzzySet of C; existence proof take UMF C; thus thesis; end; end; definition let C; let F be FuzzySet of C; func Core F -> Subset of C equals { x where x is Element of C : F.x = 1 }; coherence proof set H = { x where x is Element of C : F.x = 1 }; H c= C proof let y be object; assume y in H; then consider x being Element of C such that A1: y = x & F.x = 1; thus thesis by A1; end; hence thesis; end; end; theorem Core UMF C = C proof thus Core UMF C c= C; let x be object; assume x in C; then reconsider xx = x as Element of C; (UMF C).xx = 1 by FUNCT_3:def 3; hence thesis; end; theorem CEmpty: Core EMF C = {} proof thus Core EMF C c= {} proof let x be object; assume x in Core EMF C; then consider xx being Element of C such that A1: x = xx & (EMF C).xx = 1; thus thesis by A1,FUNCT_3:def 3; end; thus thesis; end; registration let C; cluster Core EMF C -> empty; coherence by CEmpty; end; theorem CCounter: for F being FuzzySet of C holds Core F = F " {1} proof let F be FuzzySet of C; thus Core F c= F " {1} proof let x be object; assume x in Core F; then consider xx being Element of C such that A1: x = xx & F.xx = 1; A2: F.xx in {1} by TARSKI:def 1,A1; dom F = C by FUNCT_2:def 1; hence thesis by A1,FUNCT_1:def 7,A2; end; let x be object; assume a1: x in F " {1}; then A1: x in dom F & F.x in {1} by FUNCT_1:def 7; reconsider xx = x as Element of C by a1; F.xx = 1 by A1,TARSKI:def 1; hence thesis; end; theorem for F being FuzzySet of C holds Core F = 1-cut F proof let F be FuzzySet of C; 1-cut F = F " ([. 1, 1 .]) by AlphaCut1 .= F " {1} by XXREAL_1:17; hence thesis by CCounter; end; begin :: Convexity and the Height of a Fuzzy Set definition let F be FuzzySet of REAL; attr F is f-convex means for x1, x2 being Real, l being Real st 0 <= l & l <= 1 holds F.(l*x1 + (1-l)*x2) >= min(F.x1,F.x2); end; UCon: UMF REAL is f-convex proof for x1, x2 being Real, l being Real st 0 <= l & l <= 1 holds (UMF REAL).(l*x1 + (1-l)*x2) >= min((UMF REAL).x1,(UMF REAL).x2) proof let x1, x2 be Real, l be Real; set F = UMF REAL; assume 0 <= l & l <= 1; x1 in REAL & x2 in REAL by XREAL_0:def 1; then A1: F.x1 = 1 & F.x2 = 1 by FUNCT_3:def 3; l*x1 + (1-l)*x2 in REAL by XREAL_0:def 1; hence thesis by A1,FUNCT_3:def 3; end; hence thesis; end; ECon: EMF REAL is f-convex proof for x1, x2 being Real, l being Real st 0 <= l & l <= 1 holds (EMF REAL).(l*x1 + (1-l)*x2) >= min((EMF REAL).x1,(EMF REAL).x2) proof let x1, x2 be Real, l be Real; set F = EMF REAL; assume 0 <= l & l <= 1; A3: x1 in REAL & x2 in REAL by XREAL_0:def 1; A1: F.x1 = {} & F.x2 = {} by FUNCT_3:def 3,A3; l*x1 + (1-l)*x2 in REAL by XREAL_0:def 1; hence thesis by A1,FUNCT_3:def 3; end; hence thesis; end; registration cluster UMF REAL -> f-convex; coherence by UCon; cluster EMF REAL -> f-convex; coherence by ECon; end; definition let C be non empty set; let F be FuzzySet of C; func height F -> ExtReal equals sup rng F; coherence; end; theorem HgtBnd: for F being FuzzySet of C holds 0 <= height F & height F <= 1 proof let F be FuzzySet of C; B0: 0 is LowerBound of rng F proof let x be ExtReal; assume x in rng F; then consider xx being object such that B1: xx in dom F & x = F.xx by FUNCT_1:def 3; reconsider xx as Element of C by B1; thus thesis by B1,FUZZY_2:1; end; b2: 1 is UpperBound of rng F proof let x be ExtReal; assume x in rng F; then consider xx being object such that B1: xx in dom F & x = F.xx by FUNCT_1:def 3; reconsider xx as Element of C by B1; thus thesis by B1,FUZZY_2:1; end; inf rng F <= sup rng F by XXREAL_2:40; hence thesis by b2,B0,XXREAL_2:def 4,XXREAL_2:def 3; end; theorem for F being FuzzySet of C st F is normalized holds height F = 1 proof let F be FuzzySet of C; assume F is normalized; then consider x being Element of C such that A1: F.x = 1; x in C; then x in dom F by FUNCT_2:def 1; then A2: 1 <= height F by XXREAL_2:4,FUNCT_1:3,A1; height F <= 1 by HgtBnd; hence height F = 1 by A2,XXREAL_0:1; end; begin :: Pasting aka Glueing Lemmas theorem for f,g being PartFunc of REAL, REAL st f is continuous & g is continuous & ex x being object st dom f /\ dom g = {x} & for x being object st x in dom f /\ dom g holds f.x = g.x holds ex h being PartFunc of REAL, REAL st h = f +* g & for x being Real st x in dom f /\ dom g holds h is_continuous_in x proof let f,g be PartFunc of REAL, REAL; assume A1: f is continuous & g is continuous & ex x being object st dom f /\ dom g = {x} & for x being object st x in dom f /\ dom g holds f.x = g.x; reconsider h = f +* g as PartFunc of REAL, REAL; take h; thus h = f +* g; let x be Real; J2: h | dom f = (g +* f) | dom f by FUNCT_4:34,PARTFUN1:def 4,A1 .= f by FUNCT_4:23; j2: h | dom g = g by FUNCT_4:23; assume x in dom f /\ dom g; then ZR: x in dom f & x in dom g by XBOOLE_0:def 4; then JJ: x in dom h by FUNCT_4:12; for r being Real st 0 < r ex s being Real st 0 < s & for x1 being Real st x1 in dom h & |.x1-x.| {} & dom gg <> {}; then Ab: a <= b & b <= c by XXREAL_1:29,AB; AA: dom f /\ dom g = {b} by XXREAL_1:418,Ab,AB; reconsider h = f +* g as PartFunc of REAL, REAL; take h; thus h = f +* g; let x be Real; J2: h | dom f = (g +* f) | dom f by FUNCT_4:34,A1 .= f by FUNCT_4:23; j2: h | dom g = g by FUNCT_4:23; assume JJ: x in dom h; then per cases by FUNCT_4:12; suppose J1: x in dom f; set hf = h |dom f; set hg = h |dom g; for r being Real st 0 < r ex s being Real st 0 < s & for x1 being Real st x1 in dom h & |.x1-x.| < s holds |.h.x1-h.x.| < r proof let r be Real; dom f c= dom h & dom g c= dom h by FUNCT_4:10; then XX: dom hf = dom f & dom hg = dom g by RELAT_1:62; SF: x in dom hf by RELAT_1:57,J1,JJ; assume R0: 0 < r; then consider s2 being Real such that SB: 0 < s2 & for x1 being Real st x1 in dom hf & |.x1-x.|= b by XXREAL_1:1,J1,AB; M7: a <= x1 & x1 <= b by XXREAL_1:1,P1,AB; m0: x1 + 0 <= x by M7,XXREAL_0:2,M3; b - 0 >= x1 by XXREAL_1:1,P1,AB; then M1: |.b - x1.| = b - x1 by ABSVALUE:def 1,XREAL_1:11; M2: |.x - b.| = x - b by ABSVALUE:def 1,M3,XREAL_1:11; M8: |.x - x1.| = |.b-x1.| + |.x-b.| by M1,M2,m0,ABSVALUE:def 1,XREAL_1:19; then |.b - x1.| <= |.x - x1.| by COMPLEX1:46,XREAL_1:31; then |.b - x1.| < s1 by P6,XXREAL_0:2; then |.x1 - b.| < s1 by COMPLEX1:60; then KJ: |.hf.x1 - hf.b.| < r / 2 by Sb,P1,RELAT_1:57,SC; LK: |.b - x.| = |.x - b.| by COMPLEX1:60; |.x - b.| <= |.x - x1.| by M8,XREAL_1:31,COMPLEX1:46; then |.b - x.| <= |.x1 - x.| by COMPLEX1:60,LK; then |.b - x.| < s2 by H1,XXREAL_0:2; then |.hg.b - hg.x.| < r / 2 by SB,KI; then WW: |.hf.x1 - hf.b.| + |.hg.b - hg.x.| < r / 2 + r / 2 by KJ,XREAL_1:8; |.hf.x1-hg.x.| <= |.hf.x1-hf.b.| + |.hf.b-hg.x.| by COMPLEX1:63; hence thesis by P2,P3,WA,XXREAL_0:2,WW; end; end; hence thesis by FCONT_1:3; end; end; theorem Glue: for f,g being PartFunc of REAL, REAL st f is continuous non empty & g is continuous non empty & (ex a,b,c being Real st dom f = [.a,b.] & dom g = [.b,c.]) & f tolerates g holds f +* g is continuous proof let f,g be PartFunc of REAL, REAL; assume f is continuous non empty & g is continuous non empty & (ex a,b,c being Real st dom f = [.a,b.] & dom g = [.b,c.]) & f tolerates g; then consider h being PartFunc of REAL, REAL such that A2: h = f +* g & for x being Real st x in dom h holds h is_continuous_in x by LemGlue; thus thesis by A2; end; theorem Asi1: for f, g being PartFunc of REAL, REAL st g is non empty & f = AffineMap (0,0) | (REAL \ ].a,b.[) & dom g = [.a,b.] & g.a = 0 & g.b = 0 holds f tolerates g proof let f, g be PartFunc of REAL, REAL; assume A1: g is non empty & f = (AffineMap (0,0)) | (REAL \ ].a,b.[) & dom g = [.a,b.] & g.a = 0 & g.b = 0; REAL \ ].a,b.[ c= REAL; then REAL \ ].a,b.[ c= dom AffineMap (0,0) by FUNCT_2:def 1; then A2: dom f = REAL \ ].a,b.[ by RELAT_1:62,A1 .= ].-infty,a.] \/ [.b,+infty.[ by XXREAL_1:398; for x being object st x in dom f /\ dom g holds f.x = g.x proof let x be object; K2: b < +infty by XXREAL_0:9,XREAL_0:def 1; K3: -infty < a by XXREAL_0:12,XREAL_0:def 1; assume P1: x in dom f /\ dom g; then x in ([.a,b.] /\ ].-infty,a.]) \/ ([.a,b.] /\ [.b,+infty.[) by XBOOLE_1:23,A1,A2; then x in {a} \/ ([.a,b.] /\ [.b,+infty.[) by XXREAL_1:417,A1,XXREAL_1:29,K3; then x in {a} \/ {b} by XXREAL_1:416,A1,XXREAL_1:29,K2; then x in {a,b} by ENUMSET1:1; then W1: g.x = 0 by A1,TARSKI:def 2; reconsider xx = x as Real by P1; x in dom f by P1,XBOOLE_0:def 4; then f.x = AffineMap(0,0).xx by A1,FUNCT_1:47; hence thesis by Kici1, W1; end; hence thesis by PARTFUN1:def 4; end; theorem Kluczyk: for f, g being PartFunc of REAL, REAL st g is continuous non empty & f = AffineMap (0,0) | (REAL \ ].a,b.[) & dom g = [.a,b.] & g.a = 0 & g.b = 0 holds ex h being PartFunc of REAL, REAL st h = f +* g & for x being Real st x in dom h holds h is_continuous_in x proof let f, g be PartFunc of REAL, REAL; assume A1: g is continuous non empty & f = (AffineMap (0,0)) | (REAL \ ].a,b.[) & dom g = [.a,b.] & g.a = 0 & g.b = 0; then KK: f tolerates g by Asi1; set c = b; take h = f +* g; thus h = f +* g; let x be Real; U1: -infty < a by XXREAL_0:12,XREAL_0:def 1; U3: b < +infty by XXREAL_0:9,XREAL_0:def 1; REAL \ ].a,b.[ c= REAL; then REAL \ ].a,b.[ c= dom AffineMap(0,0) by FUNCT_2:def 1; then S1: dom f = REAL \ ].a,b.[ by A1,RELAT_1:62; aa: (REAL \ ].a,b.[) /\ [.a,b.] = (].-infty,a.] \/ [.b,+infty.[) /\ [.a,b.] by XXREAL_1:398 .= (].-infty,a.] /\ [.a,b.]) \/ ([.b,+infty.[ /\ [.a,b.]) by XBOOLE_1:23 .= {a} \/ ([.b,+infty.[ /\ [.a,b.]) by XXREAL_1:417,U1,XXREAL_1:29,A1 .= {a} \/ {b} by XXREAL_1:416,XXREAL_1:29,A1,U3 .= {a,b} by ENUMSET1:1; a in dom f /\ dom g by aa,S1,A1,TARSKI:def 2; then sx: a in dom f & a in dom g by XBOOLE_0:def 4; nn: f.a = AffineMap(0,0).a by FUNCT_1:47,A1,sx .= 0*a+0 by FCONT_1:def 4 .= 0; b in dom f /\ dom g by aa,S1,A1,TARSKI:def 2; then sy: b in dom f & b in dom g by XBOOLE_0:def 4; then mn: f.b = AffineMap(0,0).b by FUNCT_1:47,A1 .= 0*b+0 by FCONT_1:def 4 .= 0; Z7: dom f = ].-infty,a.] \/ [.b,+infty.[ by S1,XXREAL_1:398; Z8: ].-infty,a.[ c= ].-infty,a.] by XXREAL_1:21; xz: ].-infty,a.] c= dom f by XBOOLE_1:7,Z7; then Z6: ].-infty,a.[ c= dom f by Z8; z8: ].b,+infty.[ c= [.b,+infty.[ by XXREAL_1:22; wz: [.b,+infty.[ c= dom f by XBOOLE_1:7,Z7; then z6: ].b,+infty.[ c= dom f by z8; assume x in dom h; then R1: x in dom f or x in dom g by FUNCT_4:12; set xx0 = x; b2: ].a,b.[ c= [.a,b.] by XXREAL_1:25; b1: ].a,b.[ c= dom g by A1,XXREAL_1:25; x in ].-infty,a.] or x in [.b,+infty.[ or x in [.a,b.] by A1,R1,Z7,XBOOLE_0:def 3; then x in ].-infty,a.[ \/ {a} or x in [.b,+infty.[ or x in [.a,b.] by XXREAL_1:423; then x in ].-infty,a.[ or x in {a} or x in [.b,+infty.[ or x in [.a,b.] by XBOOLE_0:def 3; then x in ].-infty,a.[ or x = a or x in {b} \/ ].b,+infty.[ or x in [.a,b.] by XXREAL_1:427,TARSKI:def 1; then x in ].-infty,a.[ or x = a or x in {b} or x in ].b,+infty.[ or x in [.a,b.] by XBOOLE_0:def 3; then x in ].-infty,a.[ or x = a or x = b or x in ].b,+infty.[ or x in {a,b} \/ ].a,b.[ by XXREAL_1:29,XXREAL_1:128,TARSKI:def 1; then x in ].-infty,a.[ or x = a or x = b or x in ].b,+infty.[ or x in {a,b} or x in {a,b} or x in ].a,b.[ by XBOOLE_0:def 3; then per cases by TARSKI:def 2; suppose FT: x = a; for r being Real st 0 < r ex s being Real st 0 < s & for x1 being Real st x1 in dom h & |.x1-x.| 0 by XREAL_1:20; set rr2 = rr / 2; set P1 = ].xx0-rr2, xx0+rr2.[; xx0 / 2 < a / 2 by Zz,XREAL_1:74; then z5:xx0 / 2 + a / 2 < a / 2 + a / 2 by XREAL_1:8; P1 c= ].-infty,a.[ by XXREAL_1:263,z5; then Y1:P1 c= dom f by Z8,xz; reconsider P1 as Neighbourhood of xx0 by Z1,RCOMP_1:def 6; consider N being Neighbourhood of xx0 such that Y2:N c= Nx & N c= P1 by RCOMP_1:17; take N; let x1 be Real; assume D1:x1 in dom h & x1 in N; then f.x1 in N2 by D0,Y2,Y1; hence thesis by FUNCT_4:15,Y2,Y1,D1,KK; end; hence thesis by FCONT_1:4; end; suppose B0: xx0 in ].a,b.[; for N1 being Neighbourhood of h.xx0 ex N being Neighbourhood of xx0 st for x1 being Real st x1 in dom h & x1 in N holds h.x1 in N1 proof let N1 be Neighbourhood of h.xx0; set r = h.xx0; reconsider N2 = N1 as Neighbourhood of g.xx0 by B0,A1,b2,FUNCT_4:13; consider Nx being Neighbourhood of xx0 such that D0: for x1 being Real st x1 in dom g & x1 in Nx holds g.x1 in N2 by FCONT_1:4,B0,b2,A1; set rr = min (xx0-a,b-xx0); Zw: a < xx0 & xx0 < b by B0,XXREAL_1:4; a - a < xx0 - a & b - xx0 > xx0 - xx0 by XREAL_1:14,Zw; then Z1: rr > 0 by XXREAL_0:15; set rr2 = rr / 2; set P1 = ].xx0-rr2, xx0+rr2.[; u1: rr2 < rr by Z1,XREAL_1:216; u2: rr <= b - xx0 by XXREAL_0:17; u3: xx0 + rr2 < xx0 + rr by u1,XREAL_1:8; xx0 + rr <= xx0 + (b - xx0) by u2,XREAL_1:7; then Z5: xx0 + rr2 < b by u3,XXREAL_0:2; rr <= xx0 - a by XXREAL_0:17; then rr2 < xx0 - a by XXREAL_0:2,u1; then h1: xx0 - rr2 > xx0 - (xx0 - a) by XREAL_1:15; y1: P1 c= ].a,b.[ by XXREAL_1:46,Z5,h1; reconsider P1 as Neighbourhood of xx0 by Z1,RCOMP_1:def 6; consider N being Neighbourhood of xx0 such that Y2: N c= Nx & N c= P1 by RCOMP_1:17; XX: N c= dom g by Y2,y1,b1; take N; let x1 be Real; assume D1: x1 in dom h & x1 in N; x1 in Nx & x1 in dom g by Y2,y1,b1,D1; then g.x1 in N2 by D0; hence thesis by FUNCT_4:13,XX,D1; end; hence thesis by FCONT_1:4; end; suppose B0: xx0 in ].b,+infty.[; for N1 being Neighbourhood of h.xx0 ex N being Neighbourhood of xx0 st for x1 being Real st x1 in dom h & x1 in N holds h.x1 in N1 proof let N1 be Neighbourhood of h.xx0; set r = h.xx0; reconsider N2 = N1 as Neighbourhood of f.xx0 by B0,z6,FUNCT_4:15,A1,Asi1; T1: f is continuous by A1; consider Nx being Neighbourhood of xx0 such that D0: for x1 being Real st x1 in dom f & x1 in Nx holds f.x1 in N2 by FCONT_1:4,B0,z6,T1; set rr = xx0 - b; Zz: b + 0 < xx0 by B0,XXREAL_1:235; then Z1: rr > 0 by XREAL_1:20; set rr2 = rr / 2; set P1 = ].xx0-rr2, xx0+rr2.[; Z3: b / 2 < xx0 / 2 by Zz,XREAL_1:74; xx0 / 2 + b / 2 > b / 2 + b / 2 by Z3,XREAL_1:8; then P1 c= ].b,+infty.[ by XXREAL_1:247; then Y1: P1 c= dom f by z8,wz; reconsider P1 as Neighbourhood of xx0 by Z1,RCOMP_1:def 6; consider N being Neighbourhood of xx0 such that Y2: N c= Nx & N c= P1 by RCOMP_1:17; take N; let x1 be Real; assume D1: x1 in dom h & x1 in N; then f.x1 in N2 by D0,Y2,Y1; hence thesis by FUNCT_4:15,Y2,Y1,D1,KK; end; hence thesis by FCONT_1:4; end; end; theorem for f, g being PartFunc of REAL, REAL st g is continuous non empty & f = AffineMap (0,0) | (REAL \ ].a,b.[) & dom g = [.a,b.] & g.a = 0 & g.b = 0 holds f +* g is continuous proof let f, g be PartFunc of REAL, REAL; assume g is continuous non empty & f = AffineMap (0,0) | (REAL \ ].a,b.[) & dom g = [.a,b.] & g.a = 0 & g.b = 0; then consider h being PartFunc of REAL, REAL such that A2: h = f +* g & for x being Real st x in dom h holds h is_continuous_in x by Kluczyk; thus thesis by A2; end; registration cluster non trivial closed_interval closed for Subset of REAL; existence proof take A = [.0,1.]; 0 in A & 1 in A; hence thesis by MEASURE5:def 3,ZFMISC_1:def 10; end; end; begin :: Triangular and Trapezoidal Fuzzy Sets definition let a,b,c be Real; assume that Z1: a < b and Z2: b < c; func TriangularFS (a,b,c) -> FuzzySet of REAL equals :TrDef: AffineMap (0,0) | (REAL \ ].a,c.[) +* (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.]) +* (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.]); coherence proof k1: a + 0 < b by Z1; k2: b + 0 < c by Z2; set f1 = AffineMap (0,0) | (REAL \ ].a,c.[), f2 = (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.]), f3 = (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.]); set f = f1 +* f2 +* f3; REAL \ ].a,c.[ <> {} by RealNon,Z1,Z2,XXREAL_0:2; then L1: rng f1 = {0} by Andr1a; L2: rng f2 = [.0,1.] by k1,Hope1,XREAL_1:20; L3: rng f3 = [.0,1.] by Hope2a,k2,XREAL_1:20; rng (f1 +* f2) c= rng f1 \/ rng f2 by FUNCT_4:17; then L5: rng (f1 +* f2) \/ rng f3 c= ({0} \/ [.0,1.]) \/ rng f3 by XBOOLE_1:13,L1,L2; l6: rng f c= rng (f1 +* f2) \/ rng f3 by FUNCT_4:17; [.0,0.] c= [.0,1.] by XXREAL_1:34; then {0} c= [.0,1.] by XXREAL_1:17; then {0} \/ [.0,1.] = [.0,1.] by XBOOLE_1:12; then I3: rng f c= [.0,1.] by l6,L3,L5; I5: dom f = dom (f1 +* f2) \/ dom f3 by FUNCT_4:def 1 .= dom f1 \/ dom f2 \/ dom f3 by FUNCT_4:def 1; REAL \ ].a,c.[ c= REAL; then i7: REAL \ ].a,c.[ c= dom AffineMap (0,0) by FUNCT_2:def 1; O4: a < +infty & c < +infty by XXREAL_0:9,XREAL_0:def 1; O3: a < c by Z1,Z2,XXREAL_0:2; O5: -infty < a by XXREAL_0:12,XREAL_0:def 1; [.a,b.] c= REAL; then O1: [.a,b.] c= dom AffineMap (1/(b-a),-a/(b-a)) by FUNCT_2:def 1; [.b,c.] c= REAL; then O2: [.b,c.] c= dom AffineMap (-1/(c-b),c/(c-b)) by FUNCT_2:def 1; dom f2 \/ dom f3 = [.a,b.] \/ dom f3 by RELAT_1:62,O1 .= [.a,b.] \/ [.b,c.] by RELAT_1:62,O2 .= [.a,c.] by XXREAL_1:165,Z1,Z2; then dom f1 \/ (dom f2 \/ dom f3) = (REAL \ ].a,c.[) \/ [.a,c.] by i7,RELAT_1:62 .= (].-infty,a.] \/ [.c,+infty.[) \/ [.a,c.] by XXREAL_1:398 .= ].-infty,a.] \/ ([.c,+infty.[ \/ [.a,c.]) by XBOOLE_1:4 .= ].-infty,a.] \/ [.a,+infty.[ by XXREAL_1:176,O3,O4 .= ].-infty,+infty.[ by XXREAL_1:172,O4,O5; then dom f1 \/ dom f2 \/ dom f3 = REAL by XBOOLE_1:4,XXREAL_1:224; hence thesis by FUNCT_2:2,I5,I3; end; end; ::definition let C; let a,b,c be Real; :: func TriangularFS (C,a,b,c) -> FuzzySet of C means :: for x being Real st x in C holds :: ((x <= a or c <= x) implies it.x = 0) & :: (a <= x & x <= b implies it.x = (x-a)/(b-a)) & :: (b <= x & x <= c implies it.x = (c-x)/(c-b)); :: correctness; ::end; theorem for a,b,c being Real st a < b & b < c holds TriangularFS (a,b,c) is strictly-normalized proof let a,b,c be Real; set F = TriangularFS (a,b,c); reconsider bb = b as Element of REAL by XREAL_0:def 1; assume Z1: a < b & b < c; s0: bb in [.b,c.] by Z1; S1: F = AffineMap (0,0) | (REAL \ ].a,c.[) +* (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.]) +* (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.]) by Z1,TrDef; s2: dom AffineMap (-1/(c-b),c/(c-b)) = REAL by FUNCT_2:def 1; a + 0 < b by Z1; then T1: b - a > 0 by XREAL_1:20; b + 0 < c by Z1; then t1: c - b > 0 by XREAL_1:20; bb in [.b,c.] by Z1; then bb in dom (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.]) by s2,RELAT_1:57; then A1: F.bb = (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.]).bb by FUNCT_4:13,S1 .= (AffineMap (-1/(c-b),c/(c-b))).bb by FUNCT_1:49,s0 .= 1 by Cb1,t1; for y being Element of REAL st F.y = 1 holds y = bb proof let y be Element of REAL; assume X0: F.y = 1; per cases; suppose X1: y in [.a,b.]; then per cases by XXREAL_1:7; suppose x1: y in [.a,b.[; y in REAL; then X3: y in dom AffineMap (1/(b-a),-a/(b-a)) by FUNCT_2:def 1; X2: y in dom (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.]) by X3,X1,RELAT_1:57; not y in [.b,c.] by x1,XBOOLE_0:3,XXREAL_1:95; then not y in dom (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.]) by RELAT_1:57; then F.y = (AffineMap (0,0) | (REAL \ ].a,c.[) +* (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.])).y by FUNCT_4:11,S1 .= (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.]).y by FUNCT_4:13,X2; then (AffineMap (1/(b-a),-a/(b-a))).y = 1 by X1,FUNCT_1:49,X0; hence thesis by Hope3,T1; end; suppose y = b; hence thesis; end; end; suppose X1: y in [.b,c.]; y in REAL; then y in dom AffineMap (-1/(c-b),c/(c-b)) by FUNCT_2:def 1; then y in dom (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.]) by X1,RELAT_1:57; then F.y = (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.]).y by FUNCT_4:13,S1; then (AffineMap (-1/(c-b),c/(c-b))).y = 1 by X1,FUNCT_1:49,X0; hence thesis by Hope4,t1; end; suppose so: not (y in [.a,b.] or y in [.b,c.]); then s1: not y in dom (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.]) & not y in dom (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.]) by RELAT_1:57; s8: ].a,c.[ c= [.a,c.] by XXREAL_1:25; not y in [.a,b.] \/ [.b,c.] by so,XBOOLE_0:def 3; then not y in [.a,c.] by XXREAL_1:165,Z1; then s7: not y in ].a,c.[ by s8; ss: y in REAL \ ].a,c.[ by s7,XBOOLE_0:def 5; F.y = ((AffineMap (0,0) | (REAL \ ].a,c.[) +* (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.]))).y by FUNCT_4:11,s1,S1 .= (AffineMap (0,0) | (REAL \ ].a,c.[)).y by FUNCT_4:11,s1 .= (AffineMap (0,0)).y by FUNCT_1:49,ss; hence thesis by Hope5,X0; end; end; hence thesis by A1; end; theorem for a,b,c being Real st a < b & b < c holds TriangularFS (a,b,c) is continuous proof let a,b,c be Real; assume that Z1: a < b and Z2: b < c; set F = TriangularFS (a,b,c); S1: F = AffineMap (0,0) | (REAL \ ].a,c.[) +* (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.]) +* (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.]) by Z1,Z2,TrDef; set f1 = AffineMap (0,0); set f = f1 | (REAL \ ].a,c.[); set g1 = AffineMap (1/(b-a),-a/(b-a)); reconsider g = g1 | [.a,b.] as PartFunc of REAL, REAL; set h1 = AffineMap (-1/(c-b),c/(c-b)); reconsider h = h1 | [.b,c.] as PartFunc of REAL, REAL; [.a,b.] c= REAL; then [.a,b.] c= dom g1 by FUNCT_2:def 1; then J2: dom g = [.a,b.] by RELAT_1:62; [.b,c.] c= REAL; then h1: [.b,c.] c= dom h1 by FUNCT_2:def 1; then J3: dom h = [.b,c.] by RELAT_1:62; b in dom g by J2,Z1; then j2: g is non empty; b in dom h by J3,Z2; then j3: h is non empty; ff: for x being object st x in dom g /\ dom h holds g.x = h.x proof let x be object; assume x in dom g /\ dom h; then i1: x in {b} by XXREAL_1:418,Z1,Z2,J2,J3; II: b in [.a,b.] & b in [.b,c.] by Z1,Z2; a + 0 < b by Z1; then I0: b - a > 0 by XREAL_1:20; b + 0 < c by Z2; then I2: c - b > 0 by XREAL_1:20; h.x = h.b by i1,TARSKI:def 1 .= h1.b by FUNCT_1:49,II .= 1 by Cb1, I2 .= g1.b by I0,Ab1 .= g.b by FUNCT_1:49,II .= g.x by i1,TARSKI:def 1; hence thesis; end; then fF: g tolerates h by PARTFUN1:def 4; set gh = g +* h; z1: dom gh = dom g \/ dom h by FUNCT_4:def 1 .= [.a,b.] \/ [.b,c.] by J2,h1,RELAT_1:62 .= [.a,c.] by XXREAL_1:165,Z1,Z2; K2: a in [.a,b.] by Z1; then W3: gh.a = g.a by FUNCT_4:15,PARTFUN1:def 4,ff,J2 .= g1.a by FUNCT_1:49,K2 .= 0 by Ah1; K1: c in [.b,c.] by Z2; c in dom h by J3,Z2; then gh.c = h.c by FUNCT_4:13 .= h1.c by K1,FUNCT_1:49 .= 0 by Cb2; then consider hh being PartFunc of REAL, REAL such that TT: hh = f +* gh & for x being Real st x in dom hh holds hh is_continuous_in x by W3,Kluczyk,fF,z1,Glue,J2,j2,j3,J3; hh = F by TT,FUNCT_4:14,S1; hence thesis by TT; end; definition let a,b,c,d be Real; assume that Z1: a < b and Z2: b < c and Z3: c < d; func TrapezoidalFS (a,b,c,d) -> FuzzySet of REAL equals :TPDef: AffineMap (0,0) | (REAL \ ].a,d.[) +* (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.]) +* (AffineMap (0,1) | [.b,c.]) +* (AffineMap (-1/(d-c),d/(d-c)) | [.c,d.]); coherence proof k1: a + 0 < b by Z1; k3: b < d by Z2,Z3,XXREAL_0:2; set f1 = AffineMap (0,0) | (REAL \ ].a,d.[), f2 = (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.]), f3 = (AffineMap (0,1) | [.b,c.]), f4 = (AffineMap (-1/(d-c),d/(d-c)) | [.c,d.]); set f = f1 +* f2 +* f3 +* f4; a < c by Z1,Z2,XXREAL_0:2; then REAL \ ].a,d.[ <> {} by RealNon,Z3,XXREAL_0:2; then L1: rng f1 = {0} by Andr1a; L2: rng f2 = [.0,1.] by k1,Hope1,XREAL_1:20; b in [.b,c.] by Z2; then L3: rng f3 = {1} by Andr1a; c + 0 < d by Z3; then L4: rng f4 = [.0,1.] by Hope2a,XREAL_1:20; Ss: rng (f1 +* f2) c= rng f1 \/ rng f2 by FUNCT_4:17; rng (f1 +* f2 +* f3) c= rng (f1 +* f2) \/ rng f3 by FUNCT_4:17; then d6: rng (f1 +* f2 +* f3) \/ rng f4 c= rng (f1 +* f2) \/ rng f3 \/ rng f4 by XBOOLE_1:13; rng f c= rng (f1 +* f2 +* f3) \/ rng f4 by FUNCT_4:17; then l6: rng f c= rng (f1 +* f2) \/ rng f3 \/ rng f4 by d6; [.0,0.] c= [.0,1.] by XXREAL_1:34; then Hh: {0} c= [.0,1.] by XXREAL_1:17; [.1,1.] c= [.0,1.] by XXREAL_1:34; then {1} c= [.0,1.] by XXREAL_1:17; then hx: {1} \/ [.0,1.] = [.0,1.] by XBOOLE_1:12; ss: rng (f1 +* f2) c= [.0,1.] by Hh,Ss,L1,L2,XBOOLE_1:12; sk: rng f c= rng (f1 +* f2) \/ [.0,1.] by hx,L3,XBOOLE_1:4,L4,l6; rng (f1 +* f2) \/ [.0,1.] c= [.0,1.] \/ [.0,1.] by ss,XBOOLE_1:13; then I3: rng f c= [.0,1.] by sk; I5: dom f = dom (f1 +* f2 +* f3) \/ dom f4 by FUNCT_4:def 1 .= dom (f1 +* f2) \/ dom f3 \/ dom f4 by FUNCT_4:def 1 .= dom f1 \/ dom f2 \/ dom f3 \/ dom f4 by FUNCT_4:def 1; REAL \ ].a,d.[ c= REAL; then i7: REAL \ ].a,d.[ c= dom AffineMap (0,0) by FUNCT_2:def 1; O4: a < +infty & c < +infty & d < +infty by XXREAL_0:9,XREAL_0:def 1; a < c by Z1,Z2,XXREAL_0:2; then O6: a < d by Z3,XXREAL_0:2; O5: -infty < a by XXREAL_0:12,XREAL_0:def 1; [.a,b.] c= REAL; then O1: [.a,b.] c= dom AffineMap (1/(b-a),-a/(b-a)) by FUNCT_2:def 1; [.b,c.] c= REAL; then j1: [.b,c.] c= dom AffineMap (0,1) by FUNCT_2:def 1; [.c,d.] c= REAL; then OO: [.c,d.] c= dom AffineMap (-1/(d-c),d/(d-c)) by FUNCT_2:def 1; d2: dom f3 \/ dom f4 = [.b,c.] \/ dom f4 by j1,RELAT_1:62 .= [.b,c.] \/ [.c,d.] by RELAT_1:62,OO .= [.b,d.] by XXREAL_1:165,Z2,Z3; d3: dom f2 \/ dom f3 \/ dom f4 = dom f2 \/ (dom f3 \/ dom f4) by XBOOLE_1:4 .= [.a,b.] \/ [.b,d.] by d2,O1,RELAT_1:62 .= [.a,d.] by XXREAL_1:165,k3,Z1; dom f1 \/ (dom f2 \/ dom f3) \/ dom f4 = dom f1 \/ ((dom f2 \/ dom f3) \/ dom f4) by XBOOLE_1:4 .= (REAL \ ].a,d.[) \/ [.a,d.] by d3,i7,RELAT_1:62 .= (].-infty,a.] \/ [.d,+infty.[) \/ [.a,d.] by XXREAL_1:398 .= ].-infty,a.] \/ ([.d,+infty.[ \/ [.a,d.]) by XBOOLE_1:4 .= ].-infty,a.] \/ [.a,+infty.[ by XXREAL_1:176,O4,O6 .= ].-infty,+infty.[ by XXREAL_1:172,O4,O5; then dom f1 \/ dom f2 \/ dom f3 \/ dom f4 = REAL by XBOOLE_1:4,XXREAL_1:224; hence thesis by FUNCT_2:2,I5,I3; end; end; theorem for a,b,c,d being Real st a < b & b < c & c < d holds TrapezoidalFS (a,b,c,d) is normalized proof let a,b,c,d be Real; set F = TrapezoidalFS (a,b,c,d); reconsider bb = c as Element of REAL by XREAL_0:def 1; assume Z1: a < b & b < c & c < d; s0: bb in [.c,d.] by Z1; S1: F = AffineMap (0,0) | (REAL \ ].a,d.[) +* (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.]) +* (AffineMap (0,1) | [.b,c.]) +* (AffineMap (-1/(d-c),d/(d-c)) | [.c,d.]) by Z1,TPDef; s2: dom AffineMap (-1/(d-c),d/(d-c)) = REAL by FUNCT_2:def 1; c + 0 < d by Z1; then t1: d - c > 0 by XREAL_1:20; bb in [.c,d.] by Z1; then bb in dom (AffineMap (-1/(d-c),d/(d-c)) | [.c,d.]) by s2,RELAT_1:57; then F.bb = (AffineMap (-1/(d-c),d/(d-c)) | [.c,d.]).bb by FUNCT_4:13,S1 .= (AffineMap (-1/(d-c),d/(d-c))).bb by FUNCT_1:49,s0 .= 1 by Cb1,t1; hence thesis; end; theorem for a,b,c,d being Real st a < b & b < c & c < d holds TrapezoidalFS (a,b,c,d) is continuous proof let a,b,c,d be Real; assume that Z1: a < b and Z2: b < c and Z3: c < d; set F = TrapezoidalFS (a,b,c,d); S1: F = AffineMap (0,0) | (REAL \ ].a,d.[) +* (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.]) +* (AffineMap (0,1) | [.b,c.]) +* (AffineMap (-1/(d-c),d/(d-c)) | [.c,d.]) by Z1,Z2,Z3,TPDef; set f1 = AffineMap (0,0); set f = f1 | (REAL \ ].a,d.[); set g1 = AffineMap (1/(b-a),-a/(b-a)); reconsider g = g1 | [.a,b.] as PartFunc of REAL, REAL; set h1 = AffineMap (-1/(d-c),d/(d-c)); reconsider h = h1 | [.c,d.] as PartFunc of REAL, REAL; set i1 = AffineMap (0,1); reconsider i = i1 | [.b,c.] as PartFunc of REAL, REAL; [.a,b.] c= REAL; then d9: [.a,b.] c= dom g1 by FUNCT_2:def 1; then J2: dom g = [.a,b.] by RELAT_1:62; [.c,d.] c= REAL; then d3: [.c,d.] c= dom h1 by FUNCT_2:def 1; then J3: dom h = [.c,d.] by RELAT_1:62; [.b,c.] c= REAL; then d8: [.b,c.] c= dom i1 by FUNCT_2:def 1; then JW: dom i = [.b,c.] by RELAT_1:62; b in dom g by J2,Z1; then j2: g is non empty; c in dom h by J3,Z3; then j3: h is non empty; ff: for x being object st x in dom g /\ dom i holds g.x = i.x proof let x be object; assume x in dom g /\ dom i; then i1: x in {b} by XXREAL_1:418,Z1,Z2,J2,JW; II: b in [.a,b.] & b in [.b,c.] by Z1,Z2; a + 0 < b by Z1; then I0: b - a > 0 by XREAL_1:20; i.x = i.b by i1,TARSKI:def 1 .= i1.b by FUNCT_1:49,II .= 1 by Kici1 .= g1.b by I0,Ab1 .= g.b by FUNCT_1:49,II .= g.x by i1,TARSKI:def 1; hence thesis; end; set gh = g +* i; z1: dom gh = dom g \/ dom i by FUNCT_4:def 1 .= [.a,b.] \/ [.b,c.] by d9,RELAT_1:62,JW .= [.a,c.] by XXREAL_1:165,Z1,Z2; V5: a < c by XXREAL_0:2,Z1,Z2; then PS: a in dom gh by z1; then reconsider gh as non empty PartFunc of REAL, REAL; K2: a in [.a,b.] by Z1; then W3: gh.a = g.a by FUNCT_4:15,PARTFUN1:def 4,ff,J2 .= g1.a by FUNCT_1:49,K2 .= 0 by Ah1; P3: c in [.b,c.] by Z2; K1: c in [.c,d.] by Z3; N3: dom h = [.c,d.] by d3,RELAT_1:62; c + 0 < d by Z3; then MN: d - c > 0 by XREAL_1:20; N4: h.c = h1.c by FUNCT_1:49,K1 .= 1 by Cb1,MN; KK: d in [.c,d.] by Z3; then N5: h.d = h1.d by FUNCT_1:49 .= 0 by Cb2; NN: gh is continuous by Glue,ff,j2,J2,JW,d8,P3,PARTFUN1:def 4; M1: for x being object st x in dom gh /\ dom h holds gh.x = h.x proof let x be object; assume x in dom gh /\ dom h; then ll: x in {c} by XXREAL_1:418,Z3,V5,J3,z1; then gh.x = gh.c by TARSKI:def 1 .= i.c by FUNCT_4:13,P3,JW .= i1.c by FUNCT_1:49,P3 .= h.c by N4,Kici1 .= h.x by ll,TARSKI:def 1; hence thesis; end; then fG: gh tolerates h by PARTFUN1:def 4; set ghi = gh +* h; V3: dom ghi = dom gh \/ dom h by FUNCT_4:def 1 .= [.a,c.] \/ [.c,d.] by z1,d3,RELAT_1:62 .= [.a,d.] by XXREAL_1:165,Z3,V5; V4: ghi.a = 0 by FUNCT_4:15,M1,PARTFUN1:def 4,PS,W3; ghi.d = 0 by N3,FUNCT_4:13,KK,N5; then consider hh being PartFunc of REAL, REAL such that TT: hh = f +* ghi & for x being Real st x in dom hh holds hh is_continuous_in x by Kluczyk,V3,V4,Glue,NN,j3,z1,J3,fG; hh = f +* (g +* i) +* h by FUNCT_4:14,TT .= f +* g +* i +* h by FUNCT_4:14; hence thesis by TT,S1; end; definition let F be FuzzySet of REAL; attr F is triangular means ex a,b,c being Real st F = TriangularFS (a,b,c); attr F is trapezoidal means ex a,b,c,d being Real st F = TrapezoidalFS (a,b,c,d); end; registration cluster triangular for FuzzySet of REAL; existence proof take TriangularFS (0,1,2); thus thesis; end; cluster trapezoidal for FuzzySet of REAL; existence proof take TrapezoidalFS (0,1,2,3); thus thesis; end; end;