The abstract of the Mizar article:

Properties of Fuzzy Relation

by

Noboru Endou,

Takashi Mitsuishi, and

Keiji Ohkubo

Received June 25, 2001

MML identifier: FUZZY_4

[ Mizar article, MML identifier index ]

environ

 vocabulary FUZZY_1, RELAT_1, FUNCT_1, LATTICES, ORDINAL2, RCOMP_1, INTEGRA1,
      SEQ_2, ARYTM_1, FUZZY_3, FUNCT_3, BOOLE, PARTFUN1, SUBSET_1, SQUARE_1,
      SEQ_1, FUZZY_4, ARYTM;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XREAL_0, SQUARE_1, RELSET_1, PARTFUN1, SEQ_1, SEQ_4, RFUNCT_1, INTEGRA1,
      RCOMP_1, PSCOMP_1, FUZZY_1, FUZZY_2, FUZZY_3;
 constructors SQUARE_1, INTEGRA2, RFUNCT_1, REAL_1, PSCOMP_1, FUZZY_2, FUZZY_3;
 clusters XREAL_0, RELSET_1, SUBSET_1, INTEGRA1, MEMBERED;
 requirements NUMERALS, REAL, SUBSET, BOOLE;


begin :: Basic properties of the membership function

 reserve a,c,c1,c2,x,y,z,z1,z2 for set;
 reserve C1,C2,C3 for non empty set;


definition
let C1 be non empty set;
let F be Membership_Func of C1;
cluster rng F -> non empty;
end;

theorem :: FUZZY_4:1
for F be Membership_Func of C1 holds
(rng F is bounded) & (for x st x in dom F holds F.x <= sup rng F) &
(for x st x in dom F holds F.x >= inf rng F);

theorem :: FUZZY_4:2
  for F,G be Membership_Func of C1 holds
(for x st x in C1 holds F.x <= G.x) implies sup rng F <= sup rng G;

theorem :: FUZZY_4:3
for f be RMembership_Func of C1,C2, c be Element of [:C1,C2:] holds
0 <= f.c & f.c <= 1;

theorem :: FUZZY_4:4
  for f be RMembership_Func of C1,C2, x,y st [x,y] in [:C1,C2:] holds
0 <= f. [x,y] & f. [x,y] <= 1;

begin
:: Definition and properties of converse fuzzy relation

definition
let C1,C2 be non empty set;
let h be RMembership_Func of C2,C1;
func converse h -> RMembership_Func of C1,C2 means
:: FUZZY_4:def 1
for x,y st [x,y] in [:C1,C2:] holds it. [x,y] = h. [y,x];
end;

definition
let C1,C2 be non empty set;
let f be RMembership_Func of C2,C1;
let R be FuzzyRelation of C2,C1,f;
func R" -> FuzzyRelation of C1,C2,(converse f) equals
:: FUZZY_4:def 2
   [:[:C1,C2:],(converse f).:[:C1,C2:]:];
end;

theorem :: FUZZY_4:5
for f be RMembership_Func of C1,C2 holds
converse converse f = f;

theorem :: FUZZY_4:6
  for f be RMembership_Func of C1,C2, R be FuzzyRelation of C1,C2,f holds
(R")" = R;

theorem :: FUZZY_4:7
for f be RMembership_Func of C1,C2 holds
1_minus(converse f) = converse(1_minus f);

theorem :: FUZZY_4:8
  for f be RMembership_Func of C1,C2, R be FuzzyRelation of C1,C2,f holds
(R")` = (R`)";

theorem :: FUZZY_4:9
for f,g be RMembership_Func of C1,C2 holds
converse max(f,g) = max(converse f,converse g);

theorem :: FUZZY_4:10
  for f,g be RMembership_Func of C1,C2,
R be FuzzyRelation of C1,C2,f, S be FuzzyRelation of C1,C2,g holds
(R \/ S)" = R" \/ S";

theorem :: FUZZY_4:11
for f,g be RMembership_Func of C1,C2 holds
converse min(f,g) = min(converse f,converse g);

theorem :: FUZZY_4:12
  for f,g be RMembership_Func of C1,C2,
R be FuzzyRelation of C1,C2,f, S be FuzzyRelation of C1,C2,g holds
(R /\ S)" = R" /\ S";

theorem :: FUZZY_4:13
for f,g be RMembership_Func of C1,C2,
x,y st x in C1 & y in C2 holds f. [x,y] <= g. [x,y]
implies (converse f). [y,x] <= (converse g). [y,x];

theorem :: FUZZY_4:14
  for f,g be RMembership_Func of C1,C2,
R be FuzzyRelation of C1,C2,f, S be FuzzyRelation of C1,C2,g holds
R c= S implies R" c= S";

theorem :: FUZZY_4:15
for f,g be RMembership_Func of C1,C2 holds
converse(min(f,1_minus g)) = min(converse f,1_minus(converse g));

theorem :: FUZZY_4:16
  for f,g be RMembership_Func of C1,C2,
R be FuzzyRelation of C1,C2,f, S be FuzzyRelation of C1,C2,g holds
(R \ S)" = R" \ S";

theorem :: FUZZY_4:17
for f,g be RMembership_Func of C1,C2 holds
converse max(min(f,1_minus g),min(1_minus f,g))
=max( min(converse f,1_minus(converse g)),
      min(1_minus(converse f),converse g) );

theorem :: FUZZY_4:18
  for f,g be RMembership_Func of C1,C2,
R be FuzzyRelation of C1,C2,f, S be FuzzyRelation of C1,C2,g holds
(R \+\ S)" = R" \+\ S";

begin
:: Definition and properties of the composition

definition
let C1,C2,C3 be non empty set;
let h be RMembership_Func of C1,C2;
let g be RMembership_Func of C2,C3;
let x,z be set;
assume x in C1 & z in C3;
func min(h,g,x,z) -> Membership_Func of C2 means
:: FUZZY_4:def 3
for y being Element of C2 holds it.y = min(h. [x,y],g. [y,z]);
end;

definition
let C1,C2,C3 be non empty set;
let h be RMembership_Func of C1,C2;
let g be RMembership_Func of C2,C3;
func h(#)g -> RMembership_Func of C1,C3 means
:: FUZZY_4:def 4
for x,z st [x,z] in [:C1,C3:] holds it. [x,z] = sup(rng(min(h,g,x,z)));
end;

definition
let C1,C2,C3 be non empty set;
let f be RMembership_Func of C1,C2;
let g be RMembership_Func of C2,C3;
let R be FuzzyRelation of C1,C2,f;
let S be FuzzyRelation of C2,C3,g;
func R(#)S -> FuzzyRelation of C1,C3,(f(#)g) equals
:: FUZZY_4:def 5
   [:[:C1,C3:],(f(#)g).:[:C1,C3:]:];
end;

theorem :: FUZZY_4:19
for f   be RMembership_Func of C1,C2,
    g,h be RMembership_Func of C2,C3 holds
f(#)(max(g,h)) = max(f(#)g,f(#)h);

theorem :: FUZZY_4:20
  for f be RMembership_Func of C1,C2, g,h be RMembership_Func of C2,C3,
R be FuzzyRelation of C1,C2,f, S be FuzzyRelation of C2,C3,g,
T be FuzzyRelation of C2,C3,h holds
R(#)(S \/ T) = (R (#) S) \/ (R (#) T);

theorem :: FUZZY_4:21
for f,g be RMembership_Func of C1,C2,
    h   be RMembership_Func of C2,C3 holds
(max(f,g))(#)h = max(f(#)h,g(#)h);

theorem :: FUZZY_4:22
  for f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3,
R be FuzzyRelation of C1,C2,f, S be FuzzyRelation of C1,C2,g,
T be FuzzyRelation of C2,C3,h holds
(R \/ S)(#)T = (R (#) T) \/ (S (#) T);

theorem :: FUZZY_4:23
for f   be RMembership_Func of C1,C2,
    g,h be RMembership_Func of C2,C3,
    x,z be set st x in C1 & z in C3 holds
(f(#)(min(g,h))). [x,z] <= min(f(#)g,f(#)h). [x,z];

theorem :: FUZZY_4:24
  for f be RMembership_Func of C1,C2, g,h be RMembership_Func of C2,C3,
R be FuzzyRelation of C1,C2,f, S be FuzzyRelation of C2,C3,g,
T be FuzzyRelation of C2,C3,h holds
R(#)(S /\ T) c= (R(#)S) /\ (R(#)T);

theorem :: FUZZY_4:25
for f,g be RMembership_Func of C1,C2,
    h   be RMembership_Func of C2,C3,
    x,z be set st x in C1 & z in C3 holds
(min(f,g)(#)h). [x,z] <= min(f(#)h,g(#)h). [x,z];

theorem :: FUZZY_4:26
  for f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3,
R be FuzzyRelation of C1,C2,f, S be FuzzyRelation of C1,C2,g,
T be FuzzyRelation of C2,C3,h holds
(R /\ S)(#)T c= (R(#)T) /\ (S(#)T);

theorem :: FUZZY_4:27
for f be RMembership_Func of C1,C2, g be RMembership_Func of C2,C3 holds
converse(f(#)g) = (converse g)(#)(converse f);

theorem :: FUZZY_4:28
  for f be RMembership_Func of C1,C2, g be RMembership_Func of C2,C3,
R be FuzzyRelation of C1,C2,f, S be FuzzyRelation of C2,C3,g holds
(R(#)S)" = (S")(#)(R");

theorem :: FUZZY_4:29
for f,g be RMembership_Func of C1,C2,
    h,k be RMembership_Func of C2,C3, x,z be set st
x in C1 & z in C3 &
(for y be set st y in C2 holds f. [x,y]<=g. [x,y] & h. [y,z]<=k. [y,z]) holds
(f(#)h). [x,z] <= (g(#)k). [x,z];

theorem :: FUZZY_4:30
  for f,g be RMembership_Func of C1,C2, h,k be RMembership_Func of C2,C3,
R be FuzzyRelation of C1,C2,f, S be FuzzyRelation of C1,C2,g,
T be FuzzyRelation of C2,C3,h, W be FuzzyRelation of C2,C3,k holds
R c= S & T c= W implies R(#)T c= S(#)W;

begin
:: Definition of identity relation
:: and properties of universe relation and zero relation

definition
let C1,C2 be non empty set;
func Imf(C1,C2) -> RMembership_Func of C1,C2 means
:: FUZZY_4:def 6
  for x,y st [x,y] in [:C1,C2:]
holds (x=y implies it. [x,y] = 1) & (not x=y implies it. [x,y] = 0);
end;

theorem :: FUZZY_4:31
for c be Element of [:C1,C2:] holds
(Zmf(C1,C2)).c = 0 & (Umf(C1,C2)).c = 1;

theorem :: FUZZY_4:32
  for x,y st [x,y] in [:C1,C2:] holds
(Zmf(C1,C2)). [x,y] = 0 & (Umf(C1,C2)). [x,y] = 1;

theorem :: FUZZY_4:33
  for f be RMembership_Func of C2,C3,
    O1 be Zero_Relation of C1,C2,
    O2 be Zero_Relation of C1,C3,
    R be FuzzyRelation of C2,C3,f holds
O1(#)R = O2;

theorem :: FUZZY_4:34
for f be RMembership_Func of C1,C2 holds
f(#)Zmf(C2,C3) = Zmf(C1,C3);

theorem :: FUZZY_4:35
  for f be RMembership_Func of C1,C2,
O1 be Zero_Relation of C2,C3,
O2 be Zero_Relation of C1,C3,
R be FuzzyRelation of C1,C2,f holds
R(#)O1 = O2;

theorem :: FUZZY_4:36
for f be RMembership_Func of C1,C1 holds
f(#)Zmf(C1,C1) = Zmf(C1,C1)(#)f;

theorem :: FUZZY_4:37
  for f be RMembership_Func of C1,C1,
O be Zero_Relation of C1,C1,
R be FuzzyRelation of C1,C1,f holds
R(#)O = O(#)R;