The abstract of the Mizar article:

Transitive Closure of Fuzzy Relations

by

Takashi Mitsuishi, and

Grzegorz Bancerek

Received November 23, 2003

MML identifier: LFUZZY_1

[ Mizar article, MML identifier index ]

environ

 vocabulary LFUZZY_0, ARYTM, RELAT_2, LATTICES, RCOMP_1, FUNCT_1, RELAT_1,
      QC_LANG1, FUZZY_3, SEQ_1, FUZZY_1, GROUP_1, LATTICE2, LATTICE3, WAYBEL_0,
      SQUARE_1, BOOLE, SEQ_4, BHSP_3, ORDINAL2, FUNCT_2, PARTFUN1, FUNCT_4,
      CARD_3, WAYBEL_1, FUNCOP_1, FUZZY_4, FUNCT_3, LFUZZY_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, ORDINAL1,
      ORDINAL2, NUMBERS, XCMPLX_0, DOMAIN_1, PARTFUN1, CARD_3, RELAT_2,
      FUNCT_3, RFUNCT_1, SUBSET_1, XREAL_0, NAT_1, SQUARE_1, SEQ_1, SEQ_4,
      RCOMP_1, RELSET_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1,
      WAYBEL_1, WAYBEL_3, FUZZY_1, FUZZY_3, FUZZY_4, PRE_CIRC, LFUZZY_0;
 constructors NAT_1, WAYBEL_2, PSCOMP_1, WAYBEL_3, FUZZY_4, DOMAIN_1, ORDERS_3,
      PRE_CIRC, FUZZY_3, MONOID_0, LFUZZY_0, RFUNCT_1, REAL_1;
 clusters SUBSET_1, LATTICE3, RELSET_1, STRUCT_0, MONOID_0, SEQ_1, NAT_1,
      ORDINAL2, WAYBEL_2, WAYBEL10, WAYBEL17, LFUZZY_0, INT_1, MEMBERED,
      BINARITH;
 requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;


begin :: Inclusion of fuzzy relations

 reserve X, Y, Z for non empty set;

definition
  let X be non empty set;
  cluster -> real-yielding Membership_Func of X;
end;

definition
  let f,g be real-yielding Function;
  pred f is_less_than g means
:: LFUZZY_1:def 1
   dom f c= dom g &
   for x being set st x in dom f holds f.x <= g.x;
end;

definition
 let X be non empty set;
 let f,g be Membership_Func of X;
 redefine pred f is_less_than g means
:: LFUZZY_1:def 2
  for x being Element of X holds f.x <= g.x;
  synonym f c= g;
end;

definition
 let X,Y be non empty set;
 let f,g be RMembership_Func of X,Y;
 redefine pred f is_less_than g means
:: LFUZZY_1:def 3
  for x being Element of X, y being Element of Y holds f. [x,y] <= g. [x,y];
end;

theorem :: LFUZZY_1:1
  for R,S being Membership_Func of X
   st for x being Element of X holds R.x = S.x
   holds R = S;

theorem :: LFUZZY_1:2
for R,S being RMembership_Func of X,Y
 st for x being Element of X, y being Element of Y holds R. [x,y] = S. [x,y]
 holds R = S;

theorem :: LFUZZY_1:3
  for R,S being Membership_Func of X holds
  R = S iff R c= S & S c= R;

theorem :: LFUZZY_1:4
  for R being Membership_Func of X holds
  R c= R;

theorem :: LFUZZY_1:5
  for R,S,T being Membership_Func of X holds
  R c= S & S c= T implies R c= T;

theorem :: LFUZZY_1:6
  for X,Y,Z being non empty set,
  R,S being RMembership_Func of X,Y, T,U being RMembership_Func of Y,Z
  holds R c= S & T c= U implies R(#)T c= S(#)U;

definition
  let X be non empty set;
  let f,g be Membership_Func of X;
  redefine func min(f,g);
  commutativity;
  redefine func max(f,g);
  commutativity;
end;

theorem :: LFUZZY_1:7
 for f,g being Membership_Func of X holds min(f,g) c= f;

theorem :: LFUZZY_1:8
 for f,g being Membership_Func of X holds f c= max(f,g);

begin :: Properties of fuzzy relations

definition
  let X be non empty set;
  let R be RMembership_Func of X,X;
  attr R is reflexive means
:: LFUZZY_1:def 4
   Imf(X,X) c= R;
end;

definition
 let X be non empty set;
 let R be RMembership_Func of X,X;
 redefine attr R is reflexive means
:: LFUZZY_1:def 5
  for x being Element of X holds R. [x,x] = 1;
end;

definition
 let X be non empty set;
 let R be RMembership_Func of X,X;
 attr R is symmetric means
:: LFUZZY_1:def 6
  converse R = R;
end;

definition
 let X be non empty set;
 let R be RMembership_Func of X,X;
 redefine attr R is symmetric means
:: LFUZZY_1:def 7
  for x,y being Element of X holds R. [x,y] = R. [y,x];
end;

definition
 let X be non empty set;
 let R be RMembership_Func of X,X;
 attr R is transitive means
:: LFUZZY_1:def 8
  R (#) R c= R;
end;

definition
 let X be non empty set;
 let R be RMembership_Func of X,X;
 redefine attr R is transitive means
:: LFUZZY_1:def 9
  for x,y,z being Element of X holds R. [x,y] "/\" R. [y,z] <<= R. [x,z];
end;

definition
  let X be non empty set;
  let R be RMembership_Func of X,X;
  attr R is antisymmetric means
:: LFUZZY_1:def 10
   for x,y being Element of X holds
     R. [x,y] <> 0 & R. [y,x] <> 0 implies x = y;
end;

definition
 let X be non empty set;
 let R be RMembership_Func of X,X;
 redefine attr R is antisymmetric means
:: LFUZZY_1:def 11
 for x,y being Element of X holds
   R. [x,y] <> 0 & x <> y implies R. [y,x] = 0;
end;

definition
 let X;
 cluster Imf(X,X) -> symmetric transitive reflexive antisymmetric;
end;

definition
 let X;
 cluster reflexive transitive symmetric antisymmetric RMembership_Func of X,X;
end;

theorem :: LFUZZY_1:9
for R,S being RMembership_Func of X,X holds
R is symmetric & S is symmetric implies converse min(R,S) = min(R,S);

theorem :: LFUZZY_1:10
for R,S being RMembership_Func of X,X holds
R is symmetric & S is symmetric implies converse max(R,S) = max(R,S);

definition
  let X;
  let R,S be symmetric RMembership_Func of X,X;
  cluster min(R,S) -> symmetric;
  cluster max(R,S) -> symmetric;
end;

theorem :: LFUZZY_1:11
for R,S being RMembership_Func of X,X holds
R is transitive & S is transitive implies min(R,S) (#) min(R,S) c= min(R,S);

definition
 let X;
 let R,S be transitive RMembership_Func of X,X;
 cluster min(R,S) -> transitive;
end;

definition let A be set, X be non empty set;
redefine func chi(A,X) -> Membership_Func of X;
end;

theorem :: LFUZZY_1:12
for r being Relation of X st r is_reflexive_in X
holds chi(r,[:X,X:]) is reflexive;

theorem :: LFUZZY_1:13
for r being Relation of X st r is antisymmetric
holds chi(r,[:X,X:]) is antisymmetric;

theorem :: LFUZZY_1:14
for r being Relation of X st r is symmetric
holds chi(r,[:X,X:]) is symmetric;

theorem :: LFUZZY_1:15
for r being Relation of X st r is transitive
holds chi(r,[:X,X:]) is transitive;

theorem :: LFUZZY_1:16
  Zmf(X,X) is symmetric antisymmetric transitive;

theorem :: LFUZZY_1:17
Umf(X,X) is symmetric transitive reflexive;

theorem :: LFUZZY_1:18
for R being RMembership_Func of X,X holds max(R,converse R) is symmetric;

theorem :: LFUZZY_1:19
for R being RMembership_Func of X,X holds min(R,converse R) is symmetric;

theorem :: LFUZZY_1:20
for R being RMembership_Func of X,X
for R' being RMembership_Func of X,X
 st R' is symmetric & R c= R'
 holds max(R, converse R) c= R';

theorem :: LFUZZY_1:21
for R being RMembership_Func of X,X
for R' being RMembership_Func of X,X
 st R' is symmetric & R' c= R
 holds R' c= min(R, converse R);

begin :: Transitive closure of a fuzzy relation

definition
  let X be non empty set;
  let R be RMembership_Func of X,X;
  let n be natural number;
   func n iter R -> RMembership_Func of X,X means
:: LFUZZY_1:def 12
   ex F being Function of NAT,Funcs([:X,X:],[. 0,1 .]) st
   it = F.n & F.0 = Imf(X,X) &
   for k being natural number ex Q being RMembership_Func of X,X st
   F.k = Q & F.(k + 1) = Q (#) R;
end;

reserve X for non empty set;
reserve R for RMembership_Func of X,X;

theorem :: LFUZZY_1:22
  Imf(X,X) (#) R = R;

theorem :: LFUZZY_1:23
  R (#) Imf(X,X) = R;

theorem :: LFUZZY_1:24
  0 iter R = Imf(X,X);

theorem :: LFUZZY_1:25
  1 iter R = R;

theorem :: LFUZZY_1:26
  for n being natural number holds (n+1) iter R = (n iter R) (#) R;

theorem :: LFUZZY_1:27
  for m,n being natural number holds (m+n) iter R = (m iter R) (#) (n iter R);

theorem :: LFUZZY_1:28
  for m,n being natural number holds (m*n) iter R = m iter (n iter R);

definition
  let X be non empty set;
  let R be RMembership_Func of X,X;
  func TrCl R -> RMembership_Func of X,X equals
:: LFUZZY_1:def 13
  "\/"({n iter R where n is Nat : n > 0},FuzzyLattice [:X,X:]);
end;

theorem :: LFUZZY_1:29
  for x,y being Element of X holds
    (TrCl R). [x,y]
    = "\/"(pi({n iter R where n is Nat : n > 0}, [x,y]), RealPoset [. 0,1 .]);

theorem :: LFUZZY_1:30
  R c= TrCl R;

theorem :: LFUZZY_1:31
  for n being natural number st n > 0 holds n iter R c= TrCl R;

theorem :: LFUZZY_1:32
  for Q being Subset of FuzzyLattice X,
  x being Element of X holds
  ("\/"(Q,FuzzyLattice X)). x = "\/"(pi(Q, x), RealPoset [. 0,1 .]);

theorem :: LFUZZY_1:33
  for R being complete Heyting LATTICE,
  X being Subset of R,
  y be Element of R holds
  y "/\" "\/"(X,R) = "\/"({y "/\" x where x is Element of R: x in X},R);

theorem :: LFUZZY_1:34
  for R being RMembership_Func of X,X,
  Q being Subset of FuzzyLattice [:X,X:] holds
  R (#) @("\/"(Q,FuzzyLattice [:X,X:]))
  = "\/"({R (#) @r where r is Element of FuzzyLattice [:X,X:]:r in Q},
  FuzzyLattice [:X,X:]);

theorem :: LFUZZY_1:35
  for R being RMembership_Func of X,X,
  Q being Subset of FuzzyLattice [:X,X:] holds
  @("\/"(Q,FuzzyLattice [:X,X:])) (#) R
  = "\/"({@r (#) R  where r is Element of FuzzyLattice [:X,X:]:r in Q},
  FuzzyLattice [:X,X:]);

theorem :: LFUZZY_1:36
  for R being RMembership_Func of X,X holds
  (TrCl R)(#)(TrCl R)
  = "\/"({(i iter R) (#) (j iter R)
       where i is Nat, j is Nat:i > 0 & j > 0},FuzzyLattice [:X,X:]);

definition
  let X be non empty set;
  let R be RMembership_Func of X,X;
  cluster TrCl R -> transitive;
end;

theorem :: LFUZZY_1:37
  for R being RMembership_Func of X,X, n being natural number
  st R is transitive & n > 0 holds n iter R c= R;

theorem :: LFUZZY_1:38
  for R being RMembership_Func of X,X st R is transitive holds
  R = TrCl R;

theorem :: LFUZZY_1:39
  for R,S being RMembership_Func of X,X, n being natural number st R c= S holds
  n iter R c= n iter S;

theorem :: LFUZZY_1:40
  for R,S being RMembership_Func of X,X st S is transitive & R c= S holds
  TrCl R c= S;