The abstract of the Mizar article:

The Concept of Fuzzy Relation and Basic Properties of its Operation

by

Takashi Mitsuishi,

Katsumi Wasaki, and

Yasunari Shidama

Received September 15, 2000

MML identifier: FUZZY_3

[ Mizar article, MML identifier index ]

environ

 vocabulary RELAT_1, FUNCT_3, FUNCT_1, SQUARE_1, FUZZY_1, BOOLE, FUZZY_3,
      FUNCT_2;
 notation XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, RELSET_1, FUNCT_2, RFUNCT_1,
      FUZZY_1;
 constructors SEQ_1, RFUNCT_1, FUZZY_2, RCOMP_1, XCMPLX_0, MEMBERED;
 clusters SUBSET_1, MEMBERED;


begin

 reserve C1,C2 for non empty set;

definition let C be non empty set;
 cluster -> quasi_total 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;

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

 reserve f,g for RMembership_Func of C1,C2;

begin :: Empty Fuzzy Set and Universal Fuzzy Set

definition let C1,C2 be non empty set;
  mode Zero_Relation of C1,C2 is Empty_FuzzySet of [:C1,C2:];
  mode Universe_Relation of C1,C2 is Universal_FuzzySet of [:C1,C2:];
end;

 reserve X for Universe_Relation of C1,C2;
 reserve O for Zero_Relation of C1,C2;

definition
  let C1,C2 be non empty set;
  func Zmf(C1,C2) -> RMembership_Func of C1,C2 equals
:: FUZZY_3:def 1
  chi({},[:C1,C2:]);

  func Umf(C1,C2) -> RMembership_Func of C1,C2 equals
:: FUZZY_3:def 2
  chi([:C1,C2:],[:C1,C2:]);
end;

canceled 44;

theorem :: FUZZY_3:45
Zmf(C1,C2) = EMF [:C1,C2:];

theorem :: FUZZY_3:46
Umf(C1,C2) = UMF [:C1,C2:];

theorem :: FUZZY_3:47
  O is FuzzyRelation of C1,C2,Zmf(C1,C2);

theorem :: FUZZY_3:48
  X is FuzzyRelation of C1,C2,Umf(C1,C2);

canceled 3;

theorem :: FUZZY_3: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_3: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);

canceled 7;

theorem :: FUZZY_3:61
  1_minus(Zmf(C1,C2)) = Umf(C1,C2) & 1_minus(Umf(C1,C2)) = Zmf(C1,C2);

canceled 59;

theorem :: FUZZY_3:121
  min(f,1_minus g) = Zmf(C1,C2) implies
for c being Element of [:C1,C2:] holds f.c <= g.c;

canceled;

theorem :: FUZZY_3:123
  min(f,g) = Zmf(C1,C2) implies min(f,1_minus g) = f;