Volume 12, 2000

University of Bialystok

Copyright (c) 2000 Association of Mizar Users

### The abstract of the Mizar article:

### The 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
- MML identifier: FUZZY_1

- [ Mizar article, MML identifier index ]

environ vocabulary RELAT_1, FUNCT_3, RCOMP_1, PARTFUN1, FUNCT_1, SQUARE_1, INTEGRA1, ORDINAL2, ARYTM_1, BOOLE, SUBSET_1, ABSVALUE, ARYTM_3, FUZZY_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, SQUARE_1, REAL_1, ABSVALUE, RELSET_1, PARTFUN1, SEQ_1, RFUNCT_1, INTEGRA1, RCOMP_1, PSCOMP_1; constructors ABSVALUE, RFUNCT_1, REAL_1, INTEGRA1, SQUARE_1, PSCOMP_1; clusters XREAL_0, RELSET_1, INTEGRA1, MEMBERED; 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 theorem :: FUZZY_1:1 rng chi(x,y) c= [.0,1.]; definition let C; mode Membership_Func of C -> PartFunc of C,REAL means :: FUZZY_1:def 1 dom it = C & rng it c= [.0,1.]; end; theorem :: FUZZY_1:2 chi(C,C) is Membership_Func of C; reserve f,h,g,h1 for Membership_Func of C; definition let C be non empty set; let h be Membership_Func of C; mode FuzzySet of C,h-> set means :: FUZZY_1:def 2 it = [:C,h.:C:]; end; definition let C be non empty set; let h,g be Membership_Func of C; let A be FuzzySet of C,h; let B be FuzzySet of C,g; pred A=B means :: FUZZY_1:def 3 h = g; end; definition let C be non empty set; let h,g be Membership_Func of C; let A be FuzzySet of C,h; let B be FuzzySet of C,g; pred A c= B means :: FUZZY_1:def 4 for c being Element of C holds h.c <= g.c; end; reserve A for FuzzySet of C,f; reserve B for FuzzySet of C,g; reserve D for FuzzySet of C,h; reserve D1 for FuzzySet of C,h1; theorem :: FUZZY_1:3 A = B iff A c= B & B c= A; theorem :: FUZZY_1:4 A c= A; theorem :: FUZZY_1:5 A c= B & B c= D implies A c= D; begin ::::::Intersection,Union and Complement 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 5 for c being Element of C holds it.c = min(h.c,g.c); 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 6 for c being Element of C holds it.c = max(h.c,g.c); 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 7 for c being Element of C holds it.c = 1-h.c; end; definition let C be non empty set; let h,g be Membership_Func of C; let A be FuzzySet of C,h; let B be FuzzySet of C,g; func A /\ B -> FuzzySet of C,min(h,g) equals :: FUZZY_1:def 8 [:C,min(h,g).:C:]; end; definition let C be non empty set; let h,g be Membership_Func of C; let A be FuzzySet of C,h; let B be FuzzySet of C,g; func A \/ B -> FuzzySet of C,max(h,g) equals :: FUZZY_1:def 9 [:C,max(h,g).:C:]; end; definition let C be non empty set; let h be Membership_Func of C; let A be FuzzySet of C,h; func A` -> FuzzySet of C,(1_minus h) equals :: FUZZY_1:def 10 [:C,(1_minus h).:C:]; end; theorem :: FUZZY_1:6 min(h.c,g.c) = min(h,g).c & max(h.c,g.c) = max(h,g).c; theorem :: FUZZY_1:7 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); canceled; theorem :: FUZZY_1:9 A /\ A = A & A \/ A = A; theorem :: FUZZY_1:10 A /\ B = B /\ A & A \/ B = B \/ A; theorem :: FUZZY_1:11 max(max(f,g),h) = max(f,max(g,h)) & min(min(f,g),h) = min(f,min(g,h)); theorem :: FUZZY_1:12 (A \/ B) \/ D = A \/ (B \/ D); theorem :: FUZZY_1:13 (A /\ B) /\ D = A /\ (B /\ D); theorem :: FUZZY_1:14 max(f,min(f,g)) = f & min(f,max(f,g)) = f; theorem :: FUZZY_1:15 A \/ (A /\ B) = A & A /\ (A \/ B) = A; theorem :: FUZZY_1:16 min(f,max(g,h)) = max(min(f,g),min(f,h)) & max(f,min(g,h)) = min(max(f,g),max(f,h)); theorem :: FUZZY_1:17 A \/ (B /\ D) = (A \/ B) /\ (A \/ D) & A /\ (B \/ D) = (A /\ B) \/ (A /\ D); theorem :: FUZZY_1:18 1_minus(1_minus(h)) = h; theorem :: FUZZY_1:19 (A`)` = A; theorem :: FUZZY_1:20 1_minus(max(f,g)) = min(1_minus(f),1_minus(g)) & 1_minus(min(f,g)) = max(1_minus(f),1_minus(g)); theorem :: FUZZY_1:21 ::DE MORGAN:: (A \/ B)` = A` /\ B` & (A /\ B)` = A` \/ B`; begin ::::::Empty Fuzzy Set and Universal Fuzzy Set definition let C be non empty set; mode Empty_FuzzySet of C -> set means :: FUZZY_1:def 11 it = [:C,chi({},C).:C:]; mode Universal_FuzzySet of C -> set means :: FUZZY_1:def 12 it = [:C,chi(C,C).:C:]; end; reserve X for Universal_FuzzySet of C; reserve E for Empty_FuzzySet of C; canceled; theorem :: FUZZY_1:23 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 13 chi({},C); end; definition let C be non empty set; func UMF(C) -> Membership_Func of C equals :: FUZZY_1:def 14 chi(C,C); end; canceled 2; theorem :: FUZZY_1:26 E is FuzzySet of C,EMF(C); theorem :: FUZZY_1:27 X is FuzzySet of C,UMF(C); definition let C be non empty set; redefine mode Empty_FuzzySet of C -> FuzzySet of C,EMF(C); redefine mode Universal_FuzzySet of C -> FuzzySet of C,UMF(C); end; reserve X for Universal_FuzzySet of C; reserve E for Empty_FuzzySet of C; theorem :: FUZZY_1:28 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:29 E c= A; theorem :: FUZZY_1:30 A c= X; theorem :: FUZZY_1:31 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:32 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:33 A \/ X = X & A /\ X = A; theorem :: FUZZY_1:34 A \/ E = A & A /\ E = E; theorem :: FUZZY_1:35 A c= A \/ B; theorem :: FUZZY_1:36 A c= D & B c= D implies A \/ B c= D; canceled; theorem :: FUZZY_1:38 A c= B implies A \/ D c= B \/ D; theorem :: FUZZY_1:39 A c= B & D c= D1 implies A \/ D c= B \/ D1; theorem :: FUZZY_1:40 A c= B implies A \/ B = B; theorem :: FUZZY_1:41 A /\ B c= A; theorem :: FUZZY_1:42 A /\ B c= A \/ B; theorem :: FUZZY_1:43 D c= A & D c= B implies D c= A /\ B; theorem :: FUZZY_1:44 for a,b,c,d be Element of REAL st a <= b & c <= d holds min(a,c) <= min(b,d); theorem :: FUZZY_1:45 for a,b,c be Element of REAL st a <= b holds min(a,c) <= min(b,c); theorem :: FUZZY_1:46 A c= B implies A /\ D c= B /\ D; theorem :: FUZZY_1:47 A c= B & D c= D1 implies A /\ D c= B /\ D1; theorem :: FUZZY_1:48 A c= B implies A /\ B = A; theorem :: FUZZY_1:49 A c= B & A c= D & B /\ D = E implies A = E; theorem :: FUZZY_1:50 (A /\ B) \/ (A /\ D) = A implies A c= B \/ D; theorem :: FUZZY_1:51 A c= B & B /\ D = E implies A /\ D = E; theorem :: FUZZY_1:52 A c= E implies A = E; theorem :: FUZZY_1:53 A \/ B = E iff A = E & B = E; theorem :: FUZZY_1:54 A = B \/ D iff B c= A & D c= A & for h1,D1 st B c= D1 & D c= D1 holds A c= D1 ; theorem :: FUZZY_1:55 A = B /\ D iff A c= B & A c= D & for h1,D1 st D1 c= B & D1 c= D holds D1 c= A ; theorem :: FUZZY_1:56 A c= (B \/ D) & A /\ D = E implies A c= B; theorem :: FUZZY_1:57 A c= B iff B` c= A`; theorem :: FUZZY_1:58 A c= B` implies B c= A`; theorem :: FUZZY_1:59 A` c= B implies B` c= A; theorem :: FUZZY_1:60 (A \/ B)` c= A` & (A \/ B)` c= B`; theorem :: FUZZY_1:61 A` c= (A /\ B)` & B` c= (A /\ B)`; theorem :: FUZZY_1:62 1_minus(EMF(C)) = UMF(C) & 1_minus(UMF(C)) = EMF(C); theorem :: FUZZY_1:63 E` = X & X` = E; begin ::::::Exclusive Sum, Absolute Difference definition let C be non empty set; let h,g be Membership_Func of C; let A be FuzzySet of C,h; let B be FuzzySet of C,g; func A \+\ B -> FuzzySet of C,max(min(h,1_minus(g)),min(1_minus(h),g)) equals :: FUZZY_1:def 15 [:C,max(min(h,1_minus(g)),min(1_minus(h),g)).:C:]; end; canceled; theorem :: FUZZY_1:65 A \+\ B = B \+\ A; theorem :: FUZZY_1:66 A \+\ E = A & E \+\ A = A; theorem :: FUZZY_1:67 A \+\ X = A` & X \+\ A = A`; theorem :: FUZZY_1:68 (A /\ B) \/ (B /\ D) \/ (D /\ A) = (A \/ B) /\ (B \/ D) /\ (D \/ A); theorem :: FUZZY_1:69 (A /\ B) \/ (A` /\ B`) c= (A \+\ B)`; theorem :: FUZZY_1:70 (A \+\ B) \/ A /\ B c= A \/ B; theorem :: FUZZY_1:71 A \+\ A = A /\ A`; 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 16 for c being Element of C holds it.c = abs(h.c - g.c); end; definition let C be non empty set; let h,g be Membership_Func of C; let A be FuzzySet of C,h; let B be FuzzySet of C,g; func ab_dif(A,B) -> FuzzySet of C,ab_difMF(h,g) equals :: FUZZY_1:def 17 [:C,ab_difMF(h,g).:C:]; end;

Back to top