The Mizar abstract of FUZZY

Journal of Formalized Mathematics
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;
The abstract of the Mizar article:

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