Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users

The Concept of Fuzzy Set and Membership Function and Basic Properties of Fuzzy Set Operation

by
Takashi Mitsuishi,
Noboru Endou, and
Yasunari Shidama

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;