:: Concept of Fuzzy Set and Membership Function and Basic :: Properties of Fuzzy Set Operation :: by Takashi Mitsuishi , Noboru Endou and Yasunari Shidama :: :: Received May 18, 2000 :: Copyright (c) 2000-2019 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, FUNCT_3, XXREAL_1, CARD_1, RELAT_1, TARSKI, FUNCT_1, VALUED_0, LATTICE3, XXREAL_0, PARTFUN1, SEQ_4, ARYTM_1, ARYTM_3, COMPLEX1, FUZZY_1, MEASURE5, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, COMPLEX1, XREAL_0, RELAT_1, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, VALUED_0, SEQ_4, RFUNCT_1, MEASURE5, INTEGRA1, RCOMP_1; constructors REAL_1, SQUARE_1, COMPLEX1, RFUNCT_1, INTEGRA1, SEQ_4, RELSET_1, NUMBERS; registrations RELSET_1, NUMBERS, XXREAL_0, MEMBERED, XBOOLE_0, VALUED_0, RFUNCT_1, FUNCT_2, MEASURE5, XREAL_0, ORDINAL1; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; definitions RELAT_1; equalities ORDINAL1; theorems TARSKI, FUNCT_1, FUNCT_3, ABSVALUE, PARTFUN1, ZFMISC_1, INTEGRA1, INTEGRA2, XBOOLE_0, XBOOLE_1, COMPLEX1, XREAL_1, XXREAL_0, XXREAL_1, FUNCT_2, RELAT_1, MEASURE5, XREAL_0; schemes SEQ_1, PARTFUN1; begin reserve x,y,y1,y2 for set; reserve C for non empty set; reserve c for Element of C; :: Definition of Membership Function and Fuzzy Set registration let x,y; cluster chi(x,y) -> [.0,1.]-valued; coherence proof 1 in [.0,1.] & 0 in [.0,1.] by XXREAL_1:1; then rng chi(x,y) c= {0,1} & {0,1} c= [.0,1.] by FUNCT_3:39,ZFMISC_1:32; hence rng chi(x,y) c= [.0,1.] by XBOOLE_1:1; end; end; registration let C; cluster [.0,1.]-valued for Function of C,REAL; existence proof take chi(C,C); thus rng chi(C,C) c= [.0,1.] by RELAT_1:def 19; end; end; definition let C; mode Membership_Func of C is [.0,1.]-valued Function of C,REAL; end; theorem chi(C,C) is Membership_Func of C; reserve f,h,g,h1 for Membership_Func of C; registration let X be non empty set; cluster -> real-valued for Membership_Func of X; coherence; end; definition let f,g be real-valued Function; pred f is_less_than g means dom f c= dom g & for x being set st x in dom f holds f.x <= g.x; reflexivity; end; notation let X be non empty set; let f,g be Membership_Func of X; synonym f c= g for f is_less_than g; end; definition let X be non empty set; let f,g be Membership_Func of X; redefine pred f is_less_than g means :Def2: for x being Element of X holds f .x <= g.x; compatibility proof thus f is_less_than g iff for x being Element of X holds f.x <= g.x proof hereby assume A1: f is_less_than g; thus for x being Element of X holds f.x <= g.x proof let x be Element of X; dom f = X by FUNCT_2:def 1; hence thesis by A1; end; end; assume for x being Element of X holds f.x <= g.x; then dom g = X & for x being set st x in dom f holds f.x <= g.x by FUNCT_2:def 1; hence thesis; end; end; end; Lm1: f c= g & g c= f implies f = g proof set A = f, B = g; assume A1: A c= B & B c= A; A2: for c being Element of C st c in C holds f.c = g.c proof let c be Element of C; f.c <= g.c & g.c <= f.c by A1; hence thesis by XXREAL_0:1; end; C = dom f & C = dom g by FUNCT_2:def 1; hence thesis by A2,PARTFUN1:5; end; theorem f = g iff f c= g & g c= f by Lm1; theorem f c= f; theorem f c= g & g c= h implies g c= h; begin :: Intersection,Union and Complement reconsider jj=1 as Element of REAL by XREAL_0:def 1; definition let C be non empty set; let h,g be Membership_Func of C; func min(h,g) -> Membership_Func of C means :Def3: for c being Element of C holds it.c = min(h.c,g.c); existence proof defpred P[object,object] means \$2 = min(h.\$1,g.\$1); A1: for x,y1,y2 being object st x in C & P[x,y1] & P[x,y2] holds y1=y2; A2: for x,y being object st x in C & P[x,y] holds y in REAL by XREAL_0:def 1; consider IT being PartFunc of C,REAL such that A3: (for x being object holds x in dom IT iff x in C & ex y being object st P[x,y]) & for x being object st x in dom IT holds P[x,IT.x] from PARTFUN1:sch 2(A2,A1); for x being object st x in C holds x in dom IT proof let x be object; min(h.x,g.x) is set by TARSKI:1; hence thesis by A3; end; then C c= dom IT by TARSKI:def 3; then A5: dom IT = C by XBOOLE_0:def 10; then A6: for c being Element of C holds IT.c = min(h.c,g.c) by A3; A7: rng h c= [.0,1.] by RELAT_1:def 19; A8: rng g c= [.0,1.] by RELAT_1:def 19; for y being object st y in rng IT holds y in [.0,1.] proof reconsider A=[.0,jj.] as non empty closed_interval Subset of REAL by MEASURE5:14; let y be object; assume y in rng IT; then consider x being Element of C such that A9: x in dom IT and A10: y = IT.x by PARTFUN1:3; A11: h.x >= min(h.x,g.x) by XXREAL_0:17; A12: A = [. lower_bound A, upper_bound A .] by INTEGRA1:4; then A13: 0=lower_bound A by INTEGRA1:5; A14: x in C; then x in dom h by FUNCT_2:def 1; then A15: h.x in rng h by FUNCT_1:def 3; A16: 1=upper_bound A by A12,INTEGRA1:5; then h.x <= 1 by A7,A15,INTEGRA2:1; then min(h.x,g.x) <= 1 by A11,XXREAL_0:2; then A17: IT.x <= 1 by A3,A9; x in dom g by A14,FUNCT_2:def 1; then g.x in rng g by FUNCT_1:def 3; then A18: 0 <= g.x by A8,A13,INTEGRA2:1; 0 <= h.x by A7,A13,A15,INTEGRA2:1; then 0 <= min(h.x,g.x) by A18,XXREAL_0:20; then 0 <= IT.x by A3,A9; hence thesis by A10,A13,A16,A17,INTEGRA2:1; end; then A19: rng IT c= [.0,1.] by TARSKI:def 3; IT is total by A5,PARTFUN1:def 2; then IT is Membership_Func of C by A19,RELAT_1:def 19; hence thesis by A6; end; uniqueness proof let F,G be Membership_Func of C; assume that A20: for c being Element of C holds F.c = min(h.c,g.c) and A21: for c being Element of C holds G.c = min(h.c,g.c); A22: for c being Element of C st c in C holds F.c = G.c proof let c be Element of C; F.c = min(h.c,g.c) by A20; hence thesis by A21; end; C = dom F & C = dom G by FUNCT_2:def 1; hence thesis by A22,PARTFUN1:5; end; idempotence; commutativity; end; definition let C be non empty set; let h,g be Membership_Func of C; func max(h,g) -> Membership_Func of C means :Def4: for c being Element of C holds it.c = max(h.c,g.c); existence proof defpred P[object,object] means \$2 = max(h.\$1,g.\$1); A1: for x,y1,y2 being object st x in C & P[x,y1] & P[x,y2] holds y1=y2; A2: for x,y being object st x in C & P[x,y] holds y in REAL by XREAL_0:def 1; consider IT being PartFunc of C,REAL such that A3: (for x being object holds x in dom IT iff x in C & ex y being object st P[x,y]) & for x being object st x in dom IT holds P[x,IT.x] from PARTFUN1:sch 2(A2,A1); for x being object st x in C holds x in dom IT proof let x be object; max(h.x,g.x) is set by TARSKI:1; hence thesis by A3; end; then C c= dom IT by TARSKI:def 3; then A5: dom IT = C by XBOOLE_0:def 10; then A6: for c being Element of C holds IT.c = max(h.c,g.c) by A3; A7: rng h c= [.0,1.] by RELAT_1:def 19; A8: rng g c= [.0,1.] by RELAT_1:def 19; for y being object st y in rng IT holds y in [.0,1.] proof reconsider A=[.0,jj.] as non empty closed_interval Subset of REAL by MEASURE5:14; let y be object; assume y in rng IT; then consider x being Element of C such that A9: x in dom IT and A10: y = IT.x by PARTFUN1:3; A11: A = [. lower_bound A, upper_bound A .] by INTEGRA1:4; then A12: 0=lower_bound A by INTEGRA1:5; A13: x in C; then x in dom h by FUNCT_2:def 1; then A14: h.x in rng h by FUNCT_1:def 3; then 0 <= h.x by A7,A12,INTEGRA2:1; then 0 <= max(h.x,g.x) by XXREAL_0:30; then A15: 0 <= IT.x by A3,A9; A16: 1=upper_bound A by A11,INTEGRA1:5; x in dom g by A13,FUNCT_2:def 1; then g.x in rng g by FUNCT_1:def 3; then A17: g.x <= 1 by A8,A16,INTEGRA2:1; h.x <= 1 by A7,A16,A14,INTEGRA2:1; then max(h.x,g.x) <= 1 by A17,XXREAL_0:28; then IT.x <= 1 by A3,A9; hence thesis by A10,A12,A16,A15,INTEGRA2:1; end; then A18: rng IT c= [.0,1.] by TARSKI:def 3; IT is total by A5,PARTFUN1:def 2; then IT is Membership_Func of C by A18,RELAT_1:def 19; hence thesis by A6; end; uniqueness proof let F,G be Membership_Func of C; assume that A19: for c being Element of C holds F.c = max(h.c,g.c) and A20: for c being Element of C holds G.c = max(h.c,g.c); A21: for c being Element of C st c in C holds F.c = G.c proof let c be Element of C; F.c = max(h.c,g.c) by A19; hence thesis by A20; end; C = dom F & C = dom G by FUNCT_2:def 1; hence thesis by A21,PARTFUN1:5; end; idempotence; commutativity; end; definition let C be non empty set; let h be Membership_Func of C; func 1_minus h -> Membership_Func of C means :Def5: for c being Element of C holds it.c = 1-h.c; existence proof deffunc F(set) = In(1 - h.\$1,REAL); defpred P[set] means \$1 in dom h; consider IT being PartFunc of C,REAL such that A1: (for x be Element of C holds x in dom IT iff P[x]) & for x be Element of C st x in dom IT holds IT.x = F(x) from SEQ_1:sch 3; for x being object st x in C holds x in dom IT proof let x be object; A2: dom h = C by FUNCT_2:def 1; assume x in C; hence thesis by A1,A2; end; then C c= dom IT by TARSKI:def 3; then A3: dom IT = C by XBOOLE_0:def 10; then A4: for c being Element of C holds IT.c = F(c) by A1; A5: rng h c= [.0,1.] by RELAT_1:def 19; for y being object st y in rng IT holds y in [.0,1.] proof reconsider A=[.0,jj.] as non empty closed_interval Subset of REAL by MEASURE5:14; let y be object; assume y in rng IT; then consider x being Element of C such that A6: x in dom IT and A7: y = IT.x by PARTFUN1:3; A8: A = [. lower_bound A, upper_bound A .] by INTEGRA1:4; then A9: 0=lower_bound A by INTEGRA1:5; x in C; then x in dom h by FUNCT_2:def 1; then A10: h.x in rng h by FUNCT_1:def 3; then 0 <= h.x by A5,A9,INTEGRA2:1; then 0+1 <= 1+h.x by XREAL_1:6; then F(x) <= 1 by XREAL_1:20; then A11: IT.x <= 1 by A1,A6; A12: 1=upper_bound A by A8,INTEGRA1:5; then h.x <= 1 by A5,A10,INTEGRA2:1; then 0 <= F(x) by XREAL_1:48; then 0 <= IT.x by A1,A6; hence thesis by A7,A9,A12,A11,INTEGRA2:1; end; then A13: rng IT c= [.0,1.] by TARSKI:def 3; IT is total by A3,PARTFUN1:def 2; then reconsider IT as Membership_Func of C by A13,RELAT_1:def 19; take IT; let c be Element of C; IT.c = F(c) by A4; hence thesis; end; uniqueness proof let F,G be Membership_Func of C; assume that A14: for c being Element of C holds F.c = 1-h.c and A15: for c being Element of C holds G.c = 1-h.c; A16: for c being Element of C st c in C holds F.c = G.c proof let c be Element of C; F.c = 1-h.c by A14; hence thesis by A15; end; C = dom F & C = dom G by FUNCT_2:def 1; hence thesis by A16,PARTFUN1:5; end; involutiveness proof let h1,h2 be Membership_Func of C; assume A17: for c being Element of C holds h1.c = 1-h2.c; let c be Element of C; thus h2.c = 1-(1-h2.c) .= 1-h1.c by A17; end; end; theorem min(h.c,g.c) = min(h,g).c & max(h.c,g.c) = max(h,g).c by Def3,Def4; theorem max(h,h) = h & min(h,h) = h & max(h,h) = min(h,h) & min(f,g) = min(g,f ) & max(f,g) = max(g,f); theorem Th7: max(max(f,g),h) = max(f,max(g,h)) & min(min(f,g),h) = min(f,min(g ,h)) proof A1: C = dom min(min(f,g),h) & C = dom min(f,min(g,h)) by FUNCT_2:def 1; A2: for x being Element of C st x in C holds max(max(f,g),h).x = max(f,max(g ,h)).x proof let x be Element of C; max(max(f,g),h).x = max(max(f,g).x,h.x) by Def4 .= max(max(f.x,g.x),h.x) by Def4 .= max(f.x,max(g.x,h.x)) by XXREAL_0:34 .= max(f.x,max(g,h).x) by Def4 .= max(f,max(g,h)).x by Def4; hence thesis; end; A3: for x being Element of C st x in C holds min(min(f,g),h).x = min(f,min(g ,h)).x proof let x be Element of C; min(min(f,g),h).x = min(min(f,g).x,h.x) by Def3 .= min(min(f.x,g.x),h.x) by Def3 .= min(f.x,min(g.x,h.x)) by XXREAL_0:33 .= min(f.x,min(g,h).x) by Def3 .= min(f,min(g,h)).x by Def3; hence thesis; end; C = dom max(max(f,g),h) & C = dom max(f,max(g,h)) by FUNCT_2:def 1; hence thesis by A1,A2,A3,PARTFUN1:5; end; theorem Th8: max(f,min(f,g)) = f & min(f,max(f,g)) = f proof A1: C = dom min(f,max(f,g)) by FUNCT_2:def 1; A2: for x being Element of C st x in C holds max(f,min(f,g)).x = f.x proof let x be Element of C; max(f,min(f,g)).x = max(f.x,min(f,g).x) by Def4 .= max(f.x,min(f.x,g.x)) by Def3 .= f.x by XXREAL_0:36; hence thesis; end; A3: for x being Element of C st x in C holds min(f,max(f,g)).x = f.x proof let x be Element of C; min(f,max(f,g)).x = min(f.x,max(f,g).x) by Def3 .= min(f.x,max(f.x,g.x)) by Def4 .= f.x by XXREAL_0:35; hence thesis; end; C = dom max(f,min(f,g)) & C = dom f by FUNCT_2:def 1; hence thesis by A1,A2,A3,PARTFUN1:5; end; theorem Th9: min(f,max(g,h)) = max(min(f,g),min(f,h)) & max(f,min(g,h)) = min (max(f,g),max(f,h)) proof A1: C = dom max(f,min(g,h)) & C = dom min(max(f,g),max(f,h)) by FUNCT_2:def 1; A2: for x being Element of C st x in C holds min(f,max(g,h)).x = max(min(f,g ),min(f,h)).x proof let x be Element of C; min(f,max(g,h)).x = min(f.x,max(g,h).x) by Def3 .= min(f.x,max(g.x,h.x)) by Def4 .= max(min(f.x,g.x),min(f.x,h.x)) by XXREAL_0:38 .= max(min(f,g).x,min(f.x,h.x)) by Def3 .= max(min(f,g).x,min(f,h).x) by Def3 .= max(min(f,g),min(f,h)).x by Def4; hence thesis; end; A3: for x being Element of C st x in C holds max(f,min(g,h)).x = min(max(f,g ),max(f,h)).x proof let x be Element of C; max(f,min(g,h)).x = max(f.x,min(g,h).x) by Def4 .= max(f.x,min(g.x,h.x)) by Def3 .= min(max(f.x,g.x),max(f.x,h.x)) by XXREAL_0:39 .= min(max(f,g).x,max(f.x,h.x)) by Def4 .= min(max(f,g).x,max(f,h).x) by Def4 .= min(max(f,g),max(f,h)).x by Def3; hence thesis; end; C = dom min(f,max(g,h)) & C = dom max(min(f,g),min(f,h)) by FUNCT_2:def 1; hence thesis by A1,A2,A3,PARTFUN1:5; end; ::\$CT theorem Th10: 1_minus(max(f,g)) = min(1_minus(f),1_minus(g)) & 1_minus(min(f,g )) = max(1_minus(f),1_minus(g)) proof A1: C = dom 1_minus(min(f,g)) & C = dom max(1_minus(f),1_minus(g)) by FUNCT_2:def 1; A2: for x being Element of C st x in C holds (1_minus(max(f,g))).x = min( 1_minus(f),1_minus(g)).x proof let x be Element of C; A3: (1_minus(max(f,g))).x =1 - max(f,g).x by Def5 .=1 - max(f.x,g.x) by Def4 .=1 - (f.x + g.x + |.f.x - g.x.|)/2 by COMPLEX1:74; min(1_minus(f),1_minus(g)).x =min((1_minus(f)).x,(1_minus(g)).x) by Def3 .=min((1 - f.x),(1_minus(g)).x) by Def5 .=min((1 - f.x),(1- g.x)) by Def5 .=((1-f.x) + (1-g.x) - |.(1-f.x) - (1-g.x).|)/2 by COMPLEX1:73 .=(2-f.x -g.x- |.-(f.x-g.x).|)/2 .=(2-(f.x + g.x) - |.f.x-g.x.|)/2 by COMPLEX1:52 .=1 - ((f.x + g.x) + |.f.x-g.x.|)/2; hence thesis by A3; end; A4: for x being Element of C st x in C holds (1_minus(min(f,g))).x = max( 1_minus(f),1_minus(g)).x proof let x be Element of C; A5: (1_minus(min(f,g))).x =1 - min(f,g).x by Def5 .=1 - min(f.x,g.x) by Def3 .=1 - (f.x + g.x - |.f.x-g.x.|)/2 by COMPLEX1:73; max(1_minus(f),1_minus(g)).x =max((1_minus(f)).x,(1_minus(g)).x) by Def4 .=max((1 - f.x),(1_minus(g)).x) by Def5 .=max((1 - f.x),(1- g.x)) by Def5 .=((1-f.x) + (1-g.x) + |.(1-f.x) - (1-g.x).|)/2 by COMPLEX1:74 .=(2-f.x -g.x + |.-(f.x-g.x).|)/2 .=(2-(f.x + g.x) + |.f.x-g.x.|)/2 by COMPLEX1:52 .=1 - ((f.x + g.x) - |.f.x-g.x.|)/2; hence thesis by A5; end; C = dom 1_minus(max(f,g)) & C = dom min(1_minus(f),1_minus(g)) by FUNCT_2:def 1; hence thesis by A1,A2,A4,PARTFUN1:5; end; begin :: Empty Fuzzy Set and Universal Fuzzy Set theorem chi({},C) is Membership_Func of C; definition let C be non empty set; func EMF(C) -> Membership_Func of C equals chi({},C); correctness; end; definition let C be non empty set; func UMF(C) -> Membership_Func of C equals chi(C,C); correctness; end; theorem Th12: for a,b be Element of REAL, f be PartFunc of C,REAL st rng f c= [.a,b.] & a <= b holds for x being Element of C st x in dom f holds a <= f.x & f.x <= b proof let a,b be Element of REAL; let f be PartFunc of C,REAL; assume that A1: rng f c= [.a,b.] and A2: a <= b; for x being Element of C st x in dom f holds a <= f.x & f.x <= b proof reconsider A=[.a,b.] as non empty closed_interval Subset of REAL by A2,MEASURE5:14; let x be Element of C; A = [. lower_bound A, upper_bound A .] by INTEGRA1:4; then A3: a=lower_bound A & b=upper_bound A by INTEGRA1:5; assume x in dom f; then f.x in rng f by FUNCT_1:def 3; hence thesis by A1,A3,INTEGRA2:1; end; hence thesis; end; theorem Th13: EMF(C) c= f proof let x be Element of C; A1: rng f c= [.0,jj.] by RELAT_1:def 19; dom f = C & (EMF(C)).x = 0 by FUNCT_2:def 1,FUNCT_3:def 3; hence thesis by A1,Th12; end; theorem Th14: f c= UMF(C) proof let x be Element of C; A1: 0 in REAL by XREAL_0:def 1; A2: rng f c= [.0,1.] by RELAT_1:def 19; dom f = C & (UMF(C)).x = 1 by FUNCT_2:def 1,FUNCT_3:def 3; hence thesis by A2,Th12,A1; end; theorem Th15: for x be Element of C,h be Membership_Func of C holds (EMF(C)).x <= h.x & h.x <= (UMF(C)).x by Th13,Th14,Def2; theorem Th16: min(f,g) c= f & f c= max(f,g) proof thus min(f,g) c= f proof let x be Element of C; min(f,g).x = min(f.x,g.x) by Def3; hence thesis by XXREAL_0:17; end; let x be Element of C; max(f,g).x = max(f.x,g.x) by Def4; hence thesis by XXREAL_0:25; end; theorem Th17: max(f,UMF(C)) = UMF(C) & min(f,UMF(C)) = f & max(f,EMF(C)) = f & min(f,EMF(C)) = EMF(C) proof A1: C = dom max(f,EMF(C)) & C = dom min(f,EMF(C)) by FUNCT_2:def 1; A2: for x being Element of C st x in C holds min(f,UMF(C)).x = f.x proof let x be Element of C; A3: f.x <= (UMF(C)).x by Th15; min(f,UMF(C)).x = min(f.x,(UMF(C)).x) by Def3 .=f.x by A3,XXREAL_0:def 9; hence thesis; end; A4: for x being Element of C st x in C holds min(f,EMF(C)).x = (EMF(C)).x proof let x be Element of C; A5: (EMF(C)).x <= f.x by Th15; min(f,EMF(C)).x = min(f.x,(EMF(C)).x) by Def3 .=(EMF(C)).x by A5,XXREAL_0:def 9; hence thesis; end; A6: for x being Element of C st x in C holds max(f,EMF(C)).x = f.x proof let x be Element of C; A7: (EMF(C)).x <= f.x by Th15; max(f,EMF(C)).x = max(f.x,(EMF(C)).x) by Def4 .=f.x by A7,XXREAL_0:def 10; hence thesis; end; max(f,UMF(C)) c= UMF(C) & UMF(C) c= max(f,UMF(C)) by Th14,Th16; hence max(f,UMF(C)) = UMF(C) by Lm1; A8: C = dom EMF(C) by FUNCT_2:def 1; C = dom min(f,UMF(C)) & C = dom f by FUNCT_2:def 1; hence thesis by A2,A6,A1,A8,A4,PARTFUN1:5; end; theorem Th18: f c= h & g c= h implies max(f,g) c= h proof assume A1: f c= h & g c= h; let x be Element of C; A2: max(f.x,g.x) = max(f,g).x by Def4; f.x <= h.x & g.x <= h.x by A1; hence thesis by A2,XXREAL_0:28; end; theorem f c= g implies max(f,h) c= max(g,h) proof assume A1: f c= g; let x be Element of C; f.x <= g.x by A1; then max(f.x,h.x) <= max(g.x,h.x) by XXREAL_0:26; then max(f.x,h.x) <= max(g,h).x by Def4; hence thesis by Def4; end; theorem f c= g & h c= h1 implies max(f,h) c= max(g,h1) proof assume A1: f c= g & h c= h1; let x be Element of C; f.x <= g.x & h.x <= h1.x by A1; then max(f.x,h.x) <= max(g.x,h1.x) by XXREAL_0:26; then max(f,h).x <= max(g.x,h1.x) by Def4; hence thesis by Def4; end; theorem f c= g implies max(f,g) = g proof assume f c= g; then A1: max(f,g) c= g by Th18; g c= max(f,g) by Th16; hence thesis by A1,Lm1; end; theorem min(f,g) c= max(f,g) proof let x be Element of C; min(f.x,g.x) <= f.x & f.x <= max(f.x,g.x) by XXREAL_0:17,25; then min(f.x,g.x) <= max(f.x,g.x) by XXREAL_0:2; then min(f.x,g.x) <= max(f,g).x by Def4; hence thesis by Def3; end; theorem Th23: h c= f & h c= g implies h c= min(f,g) proof assume A1: h c= f & h c= g; let x be Element of C; h.x <= f.x & h.x <= g.x by A1; then h.x <= min(f.x,g.x) by XXREAL_0:20; hence thesis by Def3; end; theorem f c= g implies min(f,h) c= min(g,h) proof assume A1: f c= g; let x be Element of C; f.x <= g.x by A1; then min(f.x,h.x) <= min(g.x,h.x) by XXREAL_0:18; then min(f,h).x <= min(g.x,h.x) by Def3; hence thesis by Def3; end; theorem f c= g & h c= h1 implies min(f,h) c= min(g,h1) proof assume A1: f c= g & h c= h1; let x be Element of C; f.x <= g.x & h.x <= h1.x by A1; then min(f.x,h.x) <= min(g.x,h1.x) by XXREAL_0:18; then min(f,h).x <= min(g.x,h1.x) by Def3; hence thesis by Def3; end; theorem Th26: f c= g implies min(f,g) = f proof assume A1: f c= g; A2: for x being Element of C st x in C holds min(f,g).x = f.x proof let x be Element of C; f.x <= g.x by A1; then f.x = min(f.x,g.x) by XXREAL_0:def 9 .= min(f,g).x by Def3; hence thesis; end; C = dom min(f,g) & C = dom f by FUNCT_2:def 1; hence thesis by A2,PARTFUN1:5; end; theorem f c= g & f c= h & min(g,h) = EMF(C) implies f = EMF(C) proof assume that A1: f c= g & f c= h and A2: min(g,h)= EMF(C); A3: for x being Element of C st x in C holds f.x = (EMF(C)).x proof let x be Element of C; f.x <= g.x & f.x <= h.x by A1; then f.x <= min(g.x,h.x) by XXREAL_0:20; then A4: f.x <= min(g,h).x by Def3; (EMF(C)).x <= f.x by Th15; hence thesis by A2,A4,XXREAL_0:1; end; C = dom f & C = dom EMF(C) by FUNCT_2:def 1; hence thesis by A3,PARTFUN1:5; end; theorem max(min(f,g),min(f,h)) = f implies f c= max(g,h) proof assume A1: max(min(f,g),min(f,h)) = f; let x be Element of C; max(min(f,g),min(f,h)).x = max(min(f,g).x,min(f,h).x) by Def4 .=max(min(f,g).x,min(f.x,h.x)) by Def3 .=max(min(f.x,g.x),min(f.x,h.x)) by Def3 .=min(f.x,max(g.x,h.x)) by XXREAL_0:38; then f.x <= max(g.x,h.x) by A1,XXREAL_0:def 9; hence thesis by Def4; end; theorem f c= g & min(g,h) = EMF(C) implies min(f,h) = EMF(C) proof assume that A1: f c= g and A2: min(g,h) = EMF(C); A3: for x being Element of C st x in C holds min(f,h).x = (EMF(C)).x proof let x be Element of C; f.x <= g.x by A1; then min(f.x,h.x) <= min(g.x,h.x) by XXREAL_0:18; then min(f.x,h.x) <= min(g,h).x by Def3; then A4: min(f,h).x <= min(g,h).x by Def3; (EMF(C)).x <= min(f,h).x by Th15; hence thesis by A2,A4,XXREAL_0:1; end; C = dom min(f,h) & C = dom EMF(C) by FUNCT_2:def 1; hence thesis by A3,PARTFUN1:5; end; theorem f c= EMF(C) implies f = EMF(C) proof EMF(C) c= f by Th13; hence thesis by Lm1; end; theorem max(f,g) = EMF(C) iff f = EMF(C) & g = EMF(C) proof thus max(f,g) = EMF(C) implies f = EMF(C) & g = EMF(C) proof assume A1: max(f,g) = EMF(C); A2: for x being Element of C st x in C holds f.x = (EMF(C)).x proof let x be Element of C; max(f.x,g.x) =(EMF(C)).x by A1,Def4; then A3: f.x <= (EMF(C)).x by XXREAL_0:25; (EMF(C)).x <= f.x by Th15; hence thesis by A3,XXREAL_0:1; end; A4: for x being Element of C st x in C holds g.x = (EMF(C)).x proof let x be Element of C; max(f.x,g.x) =(EMF(C)).x by A1,Def4; then A5: g.x <= (EMF(C)).x by XXREAL_0:25; (EMF(C)).x <= g.x by Th15; hence thesis by A5,XXREAL_0:1; end; C = dom f & C = dom EMF(C) by FUNCT_2:def 1; hence f = EMF(C) by A2,PARTFUN1:5; C = dom g & C = dom EMF(C) by FUNCT_2:def 1; hence g = EMF(C) by A4,PARTFUN1:5; end; assume f = EMF(C) & g = EMF(C); hence thesis; end; theorem f = max(g,h) iff g c= f & h c= f & for h1 st g c= h1 & h c= h1 holds f c= h1 proof hereby assume A1: f = max(g,h); hence g c= f & h c= f by Th16; let h1; assume A2: g c= h1 & h c= h1; thus f c= h1 proof let x be Element of C; g.x <= h1.x & h.x <= h1.x by A2; then max(g.x,h.x) <= h1.x by XXREAL_0:28; hence thesis by A1,Def4; end; end; assume that A3: g c= f & h c= f and A4: for h1 st g c= h1 & h c= h1 holds f c= h1; g c= max(g,h) & h c= max(g,h) by Th16; then A5: f c= max(g,h) by A4; max(g,h) c= f by A3,Th18; hence thesis by A5,Lm1; end; theorem f = min(g,h) iff f c= g & f c= h & for h1 st h1 c= g & h1 c= h holds h1 c= f proof hereby assume A1: f = min(g,h); hence f c= g & f c= h by Th16; let h1; assume A2: h1 c= g & h1 c= h; thus h1 c= f proof let x be Element of C; h1.x <= g.x & h1.x <= h.x by A2; then min(g.x,h.x) >= h1.x by XXREAL_0:20; hence thesis by A1,Def3; end; end; assume that A3: f c= g & f c= h and A4: for h1 st h1 c= g & h1 c= h holds h1 c= f; min(g,h) c= g & min(g,h) c= h by Th16; then A5: min(g,h) c= f by A4; f c= min(g,h) by A3,Th23; hence thesis by A5,Lm1; end; theorem f c= max(g,h) & min(f,h) = EMF(C) implies f c= g proof assume that A1: f c= max(g,h) and A2: min(f,h) = EMF(C); let x be Element of C; min(f,max(g,h)) = f by A1,Th26; then f = max(min(f,g),min(f,h)) by Th9 .= min(f,g) by A2,Th17; then f.x = min(f.x,g.x) by Def3; hence thesis by XXREAL_0:def 9; end; Lm2: f c= g implies 1_minus g c= 1_minus f proof assume A1: f c= g; let x be Element of C; f.x <= g.x by A1; then 1-(g.x) <= 1-(f.x) by XREAL_1:10; then (1_minus(g)).x <= 1-(f.x) by Def5; hence thesis by Def5; end; theorem Th35: f c= g iff 1_minus g c= 1_minus f proof 1_minus 1_minus f = f & 1_minus 1_minus g = g; hence thesis by Lm2; end; theorem f c= 1_minus g implies g c= 1_minus f proof 1_minus 1_minus f = f; hence thesis by Th35; end; theorem 1_minus max(f,g) c= 1_minus f by Th16,Th35; theorem 1_minus f c= 1_minus min(f,g) by Th16,Th35; theorem Th39: 1_minus(EMF(C)) = UMF(C) & 1_minus(UMF(C)) = EMF(C) proof A1: for x being Element of C st x in C holds (1_minus(EMF(C))).x = (UMF(C)). x proof let x be Element of C; (1_minus(EMF(C))).x = 1 - (EMF(C)).x by Def5 .= 1 - 0 by FUNCT_3:def 3 .= 1; hence thesis by FUNCT_3:def 3; end; C = dom 1_minus(EMF(C)) & C = dom UMF(C) by FUNCT_2:def 1; hence 1_minus(EMF(C)) = UMF(C) by A1,PARTFUN1:5; A2: for x being Element of C st x in C holds (1_minus(UMF(C))).x = (EMF(C)). x proof let x be Element of C; (1_minus(UMF(C))).x = 1 - (UMF(C)).x by Def5 .= 1 - 1 by FUNCT_3:def 3 .= 0; hence thesis by FUNCT_3:def 3; end; C = dom 1_minus(UMF(C)) & C = dom EMF(C) by FUNCT_2:def 1; hence thesis by A2,PARTFUN1:5; end; :: Exclusive Sum, Absolute Difference definition let C be non empty set; let h,g be Membership_Func of C; func h \+\ g -> Membership_Func of C equals max(min(h,1_minus(g)),min( 1_minus(h),g)); coherence; commutativity; end; theorem f \+\ EMF(C) = f proof thus f \+\ EMF(C) = max(min(f,UMF(C)),min(1_minus(f),EMF(C))) by Th39 .= max(f,min(1_minus(f),EMF(C))) by Th17 .= max(f,EMF(C)) by Th17 .= f by Th17; end; theorem f \+\ UMF(C) = 1_minus f proof thus f \+\ UMF(C) = max(min(f,EMF(C)),min(1_minus(f),UMF(C))) by Th39 .= max(EMF(C),min(1_minus(f),UMF(C))) by Th17 .= min(1_minus(f),UMF(C)) by Th17 .= 1_minus f by Th17; end; theorem min(min(max(f,g),max(g,h)),max(h,f)) = max(max(min(f,g),min(g,h)),min( h,f)) proof thus min(min(max(f,g),max(g,h)),max(h,f)) = max(min(min(max(f,g),max(g,h)),h ),min(min(max(f,g),max(g,h)),f)) by Th9 .=max(min(max(f,g),min(max(g,h),h)),min(min(max(f,g),max(g,h)),f)) by Th7 .=max(min(max(f,g),min(max(h,g),h)),min(min(max(f,g),f),max(g,h))) by Th7 .=max(min(max(f,g),h),min(min(max(f,g),f),max(g,h))) by Th8 .=max(min(max(f,g),h),min(f,max(g,h))) by Th8 .=max(min(h,max(f,g)),max(min(f,g),min(f,h) )) by Th9 .=max(max(min(f,g),min(f,h)),max(min(h,f),min(h,g))) by Th9 .=max(max(max(min(f,g),min(f,h)),min(f,h)),min(h,g)) by Th7 .=max(max(min(f,g),max(min(f,h),min(f,h))),min(h,g)) by Th7 .=max(max(min(f,g),min(g,h)),min(h,f)) by Th7; end; theorem max(min(f,g),min(1_minus f, 1_minus g)) c= 1_minus (f \+\ g) proof set f1 = 1_minus f, g1 = 1_minus g; let x be Element of C; 1_minus (f \+\ g) = min( 1_minus min(f,g1) , 1_minus min(f1,g)) by Th10 .= min( max(f1,1_minus g1),1_minus min(f1,g)) by Th10 .= min( max(f1,g),max(1_minus f1,g1)) by Th10 .= max(min(max(f1,g),f),min(max(f1,g),g1)) by Th9 .= max( max(min(f,f1),min(f,g)) ,min(max(f1,g),g1)) by Th9 .= max( max(min(f,f1),min(f,g)) , max(min(g1,f1),min(g1,g))) by Th9 .= max( max(max(min(f,g),min(f,f1)),min(g1,f1)) , min(g1,g)) by Th7 .= max( max(max(min(g1,f1),min(f,g)),min(f,f1)) , min(g1,g)) by Th7 .= max( max(min(g1,f1),min(f,g)), max(min(f,f1) , min(g1,g))) by Th7; then (1_minus (f \+\ g)).x = max(max(min(f,g),min(f1,g1)).x,max(min(f,f1),min (g1,g)).x) by Def4; hence thesis by XXREAL_0:25; end; theorem max(f \+\ g, min(f,g)) c= max(f,g) proof set f1 = 1_minus f, g1 = 1_minus g; let x be Element of C; max(f \+\ g, min(f,g)) = max(min(f,g1),max(min(f1,g),min(f,g))) by Th7 .= max(min(f,g1),min(max(min(f1,g),f),max(g,min(f1,g)))) by Th9 .= max(min(f,g1),min(max(min(f1,g),f),g)) by Th8 .= min(max(min(f,g1),max(f,min(f1,g))),max(min(f,g1),g)) by Th9 .= min(max(max(f,min(f,g1)),min(f1,g)) ,max(min(f,g1),g)) by Th7 .= min(max(f,min(f1,g)) ,max(min(f,g1),g)) by Th8 .= min( min(max(f,f1),max(f,g)) ,max(g,min(f,g1))) by Th9 .= min( min(max(f,f1),max(f,g)) , min(max(g,f),max(g,g1)) ) by Th9 .= min(min( min(max(f,f1),max(f,g)),max(g,f) ),max(g,g1) ) by Th7 .= min(min( max(f,f1),min(max(f,g),max(f,g)) ),max(g,g1) ) by Th7 .= min(max(f,g),min(max(f,f1),max(g,g1))) by Th7; then max(f \+\ g, min(f,g)).x = min(max(f,g).x,min(max(f,f1),max(g,g1)).x) by Def3 ; hence thesis by XXREAL_0:17; end; theorem f \+\ f = min(f, 1_minus f); definition let C be non empty set; let h,g be Membership_Func of C; func ab_difMF(h,g) -> Membership_Func of C means for c being Element of C holds it.c = |.h.c - g.c.|; existence proof defpred P[object,object] means \$2 = |.h.\$1 - g.\$1.|; A1: for x,y1,y2 being object st x in C & P[x,y1] & P[x,y2] holds y1=y2; A2: for x,y being object st x in C & P[x,y] holds y in REAL by XREAL_0:def 1; consider IT being PartFunc of C,REAL such that A3: (for x being object holds x in dom IT iff x in C & ex y being object st P[x,y]) & for x being object st x in dom IT holds P[x,IT.x] from PARTFUN1:sch 2(A2,A1); for x being object st x in C holds x in dom IT proof let x be object; |.h.x - g.x.| is set by TARSKI:1; hence thesis by A3; end; then C c= dom IT by TARSKI:def 3; then A5: dom IT = C by XBOOLE_0:def 10; then A6: for c being Element of C holds IT.c = |.h.c - g.c.| by A3; A7: rng g c= [.0,1.] by RELAT_1:def 19; A8: rng h c= [.0,1.] by RELAT_1:def 19; for y being object st y in rng IT holds y in [.0,1.] proof reconsider A=[.0,jj.] as non empty closed_interval Subset of REAL by MEASURE5:14; let y be object; assume y in rng IT; then consider x being Element of C such that A9: x in dom IT and A10: y = IT.x by PARTFUN1:3; 0 <= |.h.x - g.x.| by COMPLEX1:46; then A11: 0 <= IT.x by A3,A9; A12: A = [. lower_bound A, upper_bound A .] by INTEGRA1:4; then A13: 0=lower_bound A by INTEGRA1:5; A14: x in C; then x in dom h by FUNCT_2:def 1; then A15: h.x in rng h by FUNCT_1:def 3; x in dom g by A14,FUNCT_2:def 1; then A16: g.x in rng g by FUNCT_1:def 3; then 0 <= g.x by A7,A13,INTEGRA2:1; then A17: 1-0 >= 1-g.x by XREAL_1:10; A18: 1=upper_bound A by A12,INTEGRA1:5; then g.x <= 1 by A7,A16,INTEGRA2:1; then A19: -g.x >= -1 by XREAL_1:24; 0 <= h.x by A8,A13,A15,INTEGRA2:1; then 0 - g.x <= h.x - g.x by XREAL_1:9; then A20: -1 <= h.x - g.x by A19,XXREAL_0:2; h.x <= 1 by A8,A18,A15,INTEGRA2:1; then h.x - g.x <= 1 - g.x by XREAL_1:9; then h.x - g.x <= 1 by A17,XXREAL_0:2; then |.h.x - g.x.| <= 1 by A20,ABSVALUE:5; then IT.x <= 1 by A3,A9; hence thesis by A10,A13,A18,A11,INTEGRA2:1; end; then A21: rng IT c= [.0,1.] by TARSKI:def 3; IT is total by A5,PARTFUN1:def 2; then IT is Membership_Func of C by A21,RELAT_1:def 19; hence thesis by A6; end; uniqueness proof let F,G be Membership_Func of C; assume that A22: for c being Element of C holds F.c = |.h.c - g.c.| and A23: for c being Element of C holds G.c = |.h.c - g.c.|; A24: for c being Element of C st c in C holds F.c = G.c proof let c be Element of C; F.c = |.h.c - g.c.| by A22; hence thesis by A23; end; C = dom F & C = dom G by FUNCT_2:def 1; hence thesis by A24,PARTFUN1:5; end; end;