:: Basic Properties of Fuzzy Set Operation and Membership Function
::  by Takashi Mitsuishi , Katsumi Wasaki and Yasunari Shidama
::
:: Received May 22, 2000
:: Copyright (c) 2000-2021 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, FUZZY_1, CARD_1, XXREAL_0, FUNCT_1,
      TARSKI, ARYTM_1, RELAT_1, PARTFUN1, XXREAL_1, SEQ_4, MEMBER_1, ARYTM_3,
      REAL_1, FUNCT_2, ZFMISC_1, FUNCT_3, FUZZY_2, MEASURE5;
 notations TARSKI, XBOOLE_0, ORDINAL1, SUBSET_1, ZFMISC_1, NUMBERS, XXREAL_0,
      XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3,
      INTEGRA1, RCOMP_1, SEQ_4, FUZZY_1, MEASURE5;
 constructors REAL_1, SQUARE_1, RFUNCT_1, INTEGRA1, FUZZY_1, SEQ_4, RELSET_1;
 registrations RELSET_1, NUMBERS, MEMBERED, XBOOLE_0, SUBSET_1, VALUED_0,
      MEASURE5, XREAL_0;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin :: Basic Properties of Membership Function and Difference Set

reserve x,y,y1,y2 for set;
reserve C for non empty set;
reserve c for Element of C;
reserve f,h,g,h1 for Membership_Func of C;

theorem :: FUZZY_2:1
  for x be Element of C,h be Membership_Func of C holds 0 <= h.x & h.x <= 1;

theorem :: FUZZY_2:2
  f c= h implies max(f,min(g,h)) = min(max(f,g),h);

definition
  let C be non empty set;
  let f,g be Membership_Func of C;
  func f\g -> Membership_Func of C equals
:: FUZZY_2:def 1
  min(f,1_minus g);
end;

theorem :: FUZZY_2:3
  1_minus (f\g) = max(1_minus f,g);

theorem :: FUZZY_2:4
  f c= g implies f\h c= g\h;

theorem :: FUZZY_2:5
  f c= g implies h\g c= h\f;

theorem :: FUZZY_2:6
  f c= g & h c= h1 implies f\h1 c= g\h;

theorem :: FUZZY_2:7
  f\EMF(C) = f;

theorem :: FUZZY_2:8
  f\g c= f\min(f,g);

theorem :: FUZZY_2:9
  max(min(f,g),f\g) c= f;

theorem :: FUZZY_2:10
  max(f,g\f) c= max(f,g);

theorem :: FUZZY_2:11
  f\(g\h) = max(f\g,min(f,h));

theorem :: FUZZY_2:12
  min(f,g) c= f\(f\g);

theorem :: FUZZY_2:13
  f\g c= max(f,g)\g;

theorem :: FUZZY_2:14
  f\max(g,h) = min(f\g,f\h);

theorem :: FUZZY_2:15
  f\min(g,h) = max(f\g,f\h);

theorem :: FUZZY_2:16
  (f\g)\h = f\max(g,h);

theorem :: FUZZY_2:17
  f \+\ g c= max(f,g)\min(f,g);

theorem :: FUZZY_2:18
  f\g c= h & g\f c= h implies f \+\ g c= h;

theorem :: FUZZY_2:19
  min(f,g\h) c= min(f,g)\min(f,h);

theorem :: FUZZY_2:20
  f \+\ g c= max(f,g)\min(f,g);

theorem :: FUZZY_2:21
  max(min(f,g),1_minus max(f,g)) c= 1_minus (f \+\ g);

theorem :: FUZZY_2:22
  (f \+\ g)\h = max(f\max(g,h),g\max(f,h));

theorem :: FUZZY_2:23
  max(f\ max(g,h),min(min(f,g),h)) c= f\(g \+\ h);

theorem :: FUZZY_2:24
  f c= g implies max(f,g\f) c= g;

theorem :: FUZZY_2:25
  max(f \+\ g,min(f,g)) c= max(f,g);

theorem :: FUZZY_2:26
  f\g = EMF(C) implies f c= g;

theorem :: FUZZY_2:27
  min(f,g) = EMF(C) implies f\g = f;

begin

definition
  let C be non empty set;
  let h,g be Membership_Func of C;
  func h*g -> Membership_Func of C means
:: FUZZY_2:def 2

  for c being Element of C holds it.c = (h.c)*(g.c);
  commutativity;
end;

definition
  let C be non empty set;
  let h,g be Membership_Func of C;
  func h ++ g -> Membership_Func of C means
:: FUZZY_2:def 3

  for c being Element of C holds it.c = h.c + g.c -(h.c)*(g.c);
  commutativity;
end;

theorem :: FUZZY_2:28
  f*f c= f & f c= f ++ f;

theorem :: FUZZY_2:29
  (f*g)*h = f*(g*h);

theorem :: FUZZY_2:30
  (f ++ g) ++ h = f ++ (g ++ h);

theorem :: FUZZY_2:31
  f*(f ++ g) c= f & f c= f ++ (f*g);

theorem :: FUZZY_2:32
  f*(g ++ h) c= (f*g) ++ (f*h);

theorem :: FUZZY_2:33
  (f ++ g)*(f ++ h) c= f ++ (g*h);

theorem :: FUZZY_2:34
  1_minus (f*g) = (1_minus f) ++ (1_minus g);

theorem :: FUZZY_2:35
  1_minus(f ++ g) = (1_minus f)*(1_minus g);

theorem :: FUZZY_2:36
  f ++ g = 1_minus((1_minus f)*(1_minus g));

theorem :: FUZZY_2:37
  f*(EMF(C)) = EMF(C) & f*(UMF(C)) = f;

theorem :: FUZZY_2:38
  f ++ EMF(C) = f & f ++ UMF(C) = UMF(C);

theorem :: FUZZY_2:39
  f*g c= min(f,g);

theorem :: FUZZY_2:40
  max(f,g) c= f ++ g;

theorem :: FUZZY_2:41
  for a,b,c be Real st 0 <= c holds c*max(a,b) = max(c*a,c*b) & c*min(a,
  b) = min(c*a,c*b);

theorem :: FUZZY_2:42
  for a,b,c be Real holds  c + max(a,b) = max(c+a,c+b) & c + min(a,b) =
  min(c+a,c+b);

theorem :: FUZZY_2:43
  f*max(g,h) = max(f*g,f*h);

theorem :: FUZZY_2:44
  f*min(g,h) = min(f*g,f*h);

theorem :: FUZZY_2:45
  f ++ max(g,h) = max((f ++ g),(f ++ h));

theorem :: FUZZY_2:46
  f ++ min(g,h) = min((f ++ g),(f ++ h));

theorem :: FUZZY_2:47
  max(f,g)*max(f,h) c= max(f,(g*h));

theorem :: FUZZY_2:48
  min(f,g)*min(f,h) c= min(f,(g*h));

theorem :: FUZZY_2:49
  for c be Element of C,f,g be Membership_Func of C holds (f ++ g)
  .c = 1 - ((1 - f.c)*(1 - g.c));

theorem :: FUZZY_2:50
  max(f,g ++ h) c= max(f,g) ++ max(f,h);

theorem :: FUZZY_2:51
  min(f,g ++ h) c= min(f,g) ++ min(f,h);

begin :: Addenda, moved from FUZZY_3

reserve C1,C2 for non empty set;

registration
  let C be non empty set;
  cluster -> quasi_total for Membership_Func of C;
end;

definition
  let C1,C2 be non empty set;
  mode RMembership_Func of C1,C2 is Membership_Func of [:C1,C2:];
end;

reserve f,g for RMembership_Func of C1,C2;

definition
  let C1,C2 be non empty set;
  func Zmf(C1,C2) -> RMembership_Func of C1,C2 equals
:: FUZZY_2:def 4
  chi({},[:C1,C2:]);
  func Umf(C1,C2) -> RMembership_Func of C1,C2 equals
:: FUZZY_2:def 5
  chi([:C1,C2:],[:C1,C2:]);
end;

theorem :: FUZZY_2:52
  for x be Element of [:C1,C2:],h be RMembership_Func of C1,C2 holds (
  Zmf(C1,C2)).x <= h.x & h.x <= (Umf(C1,C2)).x;

theorem :: FUZZY_2:53
  max(f,Umf(C1,C2)) = Umf(C1,C2) & min(f,Umf(C1,C2)) = f & max(f,Zmf(C1,
  C2)) = f & min(f,Zmf(C1,C2)) = Zmf(C1,C2);

theorem :: FUZZY_2:54
  1_minus(Zmf(C1,C2)) = Umf(C1,C2) & 1_minus(Umf(C1,C2)) = Zmf(C1,C2);

theorem :: FUZZY_2:55
  f\g = Zmf(C1,C2) implies f c= g;

theorem :: FUZZY_2:56
  min(f,g) = Zmf(C1,C2) implies f\g = f;