:: 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; 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; end; registration let C; cluster [.0,1.]-valued for Function of C,REAL; end; definition let C; mode Membership_Func of C is [.0,1.]-valued Function of C,REAL; end; theorem :: FUZZY_1:1 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; end; definition let f,g be real-valued Function; pred f is_less_than g means :: FUZZY_1:def 1 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 :: FUZZY_1:def 2 for x being Element of X holds f .x <= g.x; end; theorem :: FUZZY_1:2 f = g iff f c= g & g c= f; theorem :: FUZZY_1:3 f c= f; theorem :: FUZZY_1:4 f c= g & g c= h implies g c= h; begin definition let C be non empty set; let h,g be Membership_Func of C; func min(h,g) -> Membership_Func of C means :: FUZZY_1:def 3 for c being Element of C holds it.c = min(h.c,g.c); 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 :: FUZZY_1:def 4 for c being Element of C holds it.c = max(h.c,g.c); 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 :: FUZZY_1:def 5 for c being Element of C holds it.c = 1-h.c; involutiveness; end; theorem :: FUZZY_1:5 min(h.c,g.c) = min(h,g).c & max(h.c,g.c) = max(h,g).c; theorem :: FUZZY_1:6 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 :: FUZZY_1:7 max(max(f,g),h) = max(f,max(g,h)) & min(min(f,g),h) = min(f,min(g ,h)); theorem :: FUZZY_1:8 max(f,min(f,g)) = f & min(f,max(f,g)) = f; theorem :: FUZZY_1:9 min(f,max(g,h)) = max(min(f,g),min(f,h)) & max(f,min(g,h)) = min (max(f,g),max(f,h)); ::\$CT theorem :: FUZZY_1:11 1_minus(max(f,g)) = min(1_minus(f),1_minus(g)) & 1_minus(min(f,g )) = max(1_minus(f),1_minus(g)); begin :: Empty Fuzzy Set and Universal Fuzzy Set theorem :: FUZZY_1:12 chi({},C) is Membership_Func of C; definition let C be non empty set; func EMF(C) -> Membership_Func of C equals :: FUZZY_1:def 6 chi({},C); end; definition let C be non empty set; func UMF(C) -> Membership_Func of C equals :: FUZZY_1:def 7 chi(C,C); end; theorem :: FUZZY_1:13 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; theorem :: FUZZY_1:14 EMF(C) c= f; theorem :: FUZZY_1:15 f c= UMF(C); theorem :: FUZZY_1:16 for x be Element of C,h be Membership_Func of C holds (EMF(C)).x <= h.x & h.x <= (UMF(C)).x; theorem :: FUZZY_1:17 min(f,g) c= f & f c= max(f,g); theorem :: FUZZY_1:18 max(f,UMF(C)) = UMF(C) & min(f,UMF(C)) = f & max(f,EMF(C)) = f & min(f,EMF(C)) = EMF(C); theorem :: FUZZY_1:19 f c= h & g c= h implies max(f,g) c= h; theorem :: FUZZY_1:20 f c= g implies max(f,h) c= max(g,h); theorem :: FUZZY_1:21 f c= g & h c= h1 implies max(f,h) c= max(g,h1); theorem :: FUZZY_1:22 f c= g implies max(f,g) = g; theorem :: FUZZY_1:23 min(f,g) c= max(f,g); theorem :: FUZZY_1:24 h c= f & h c= g implies h c= min(f,g); theorem :: FUZZY_1:25 f c= g implies min(f,h) c= min(g,h); theorem :: FUZZY_1:26 f c= g & h c= h1 implies min(f,h) c= min(g,h1); theorem :: FUZZY_1:27 f c= g implies min(f,g) = f; theorem :: FUZZY_1:28 f c= g & f c= h & min(g,h) = EMF(C) implies f = EMF(C); theorem :: FUZZY_1:29 max(min(f,g),min(f,h)) = f implies f c= max(g,h); theorem :: FUZZY_1:30 f c= g & min(g,h) = EMF(C) implies min(f,h) = EMF(C); theorem :: FUZZY_1:31 f c= EMF(C) implies f = EMF(C); theorem :: FUZZY_1:32 max(f,g) = EMF(C) iff f = EMF(C) & g = EMF(C); theorem :: FUZZY_1:33 f = max(g,h) iff g c= f & h c= f & for h1 st g c= h1 & h c= h1 holds f c= h1; theorem :: FUZZY_1:34 f = min(g,h) iff f c= g & f c= h & for h1 st h1 c= g & h1 c= h holds h1 c= f; theorem :: FUZZY_1:35 f c= max(g,h) & min(f,h) = EMF(C) implies f c= g; theorem :: FUZZY_1:36 f c= g iff 1_minus g c= 1_minus f; theorem :: FUZZY_1:37 f c= 1_minus g implies g c= 1_minus f; theorem :: FUZZY_1:38 1_minus max(f,g) c= 1_minus f; theorem :: FUZZY_1:39 1_minus f c= 1_minus min(f,g); theorem :: FUZZY_1:40 1_minus(EMF(C)) = UMF(C) & 1_minus(UMF(C)) = EMF(C); :: 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 :: FUZZY_1:def 8 max(min(h,1_minus(g)),min( 1_minus(h),g)); commutativity; end; theorem :: FUZZY_1:41 f \+\ EMF(C) = f; theorem :: FUZZY_1:42 f \+\ UMF(C) = 1_minus f; theorem :: FUZZY_1:43 min(min(max(f,g),max(g,h)),max(h,f)) = max(max(min(f,g),min(g,h)),min( h,f)); theorem :: FUZZY_1:44 max(min(f,g),min(1_minus f, 1_minus g)) c= 1_minus (f \+\ g); theorem :: FUZZY_1:45 max(f \+\ g, min(f,g)) c= max(f,g); theorem :: FUZZY_1:46 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 :: FUZZY_1:def 9 for c being Element of C holds it.c = |.h.c - g.c.|; end;