:: 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-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, 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;