:: Transitive Closure of Fuzzy Relations
:: by Takashi Mitsuishi and Grzegorz Bancerek
::
:: Received November 23, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

registration
let X be non empty set ;
cluster[.0,1.] -valued Function-like quasi_total  ->  real-valued for Element of bool [:X,REAL:];
coherence
 for b1 being Membership_Func of X holds b1 is real-valued ;
end;

definition
let X, Y be non empty set ;
let f, g be RMembership_Func of X,Y;
:: original:is_less_than
redefine predf is_less_than g means :Def1: :: LFUZZY_1:def 1
 for x being Element of X
for y being Element of Y holds f . (x,y) <= g . (x,y);
compatibility
 ( f is_less_than g iff for x being Element of X
for y being Element of Y holds f . (x,y) <= g . (x,y) )
proofend;
end;

:: deftheorem Def1 defines is_less_than LFUZZY_1:def_1_:_
 for X, Y being non empty set
for f, g being RMembership_Func of X,Y holds
( f is_less_than g iff for x being Element of X
for y being Element of Y holds f . (x,y) <= g . (x,y) );

theorem Th1: :: LFUZZY_1:1
for X being non empty set
for R, S being Membership_Func of X st ( for x being Element of X holds R . x = S . x ) holds
R = S
proofend;

theorem Th2: :: LFUZZY_1:2
for X, Y being non empty set
for R, S being RMembership_Func of X,Y st ( for x being Element of X
for y being Element of Y holds R . (x,y) = S . (x,y) ) holds
R = S
proofend;

theorem Th3: :: LFUZZY_1:3
for X being non empty set
for R, S being Membership_Func of X holds
( R = S iff ( S c= &amp; R c= ) )
proofend;

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

theorem Th5: :: LFUZZY_1:5
for X being non empty set
for R, S, T being Membership_Func of X st S c= &amp; T c= holds
T c=
proofend;

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

definition
let X be non empty set ;
let f, g be Membership_Func of X;
:: original:min
redefine func min (f,g) ->  Element of bool [:X,REAL:];
commutativity
 for f, g being Membership_Func of X holds min (f,g) = min (g,f) ;
:: original:max
redefine func max (f,g) ->  Element of bool [:X,REAL:];
commutativity
 for f, g being Membership_Func of X holds max (f,g) = max (g,f) ;
end;

theorem :: LFUZZY_1:7
for X being non empty set
for f, g being Membership_Func of X holds f c=
proofend;

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

begin

definition
let X be non empty set ;
let R be RMembership_Func of X,X;
attrR is reflexive  means :Def2: :: LFUZZY_1:def 2
R c= ;
end;

:: deftheorem Def2 defines reflexive LFUZZY_1:def_2_:_
 for X being non empty set
for R being RMembership_Func of X,X holds
( R is reflexive iff R c= );

definition
let X be non empty set ;
let R be RMembership_Func of X,X;
redefine attr R is reflexive  means :Def3: :: LFUZZY_1:def 3
 for x being Element of X holds R . (x,x) = 1;
compatibility
 ( R is reflexive iff for x being Element of X holds R . (x,x) = 1 )
proofend;
end;

:: deftheorem Def3 defines reflexive LFUZZY_1:def_3_:_
 for X being non empty set
for R being RMembership_Func of X,X holds
( R is reflexive iff for x being Element of X holds R . (x,x) = 1 );

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

:: deftheorem Def4 defines symmetric LFUZZY_1:def_4_:_
 for X being non empty set
for R being RMembership_Func of X,X holds
( R is symmetric iff converse R = R );

definition
let X be non empty set ;
let R be RMembership_Func of X,X;
redefine attr R is symmetric  means :Def5: :: LFUZZY_1:def 5
 for x, y being Element of X holds R . (x,y) = R . (y,x);
compatibility
 ( R is symmetric iff for x, y being Element of X holds R . (x,y) = R . (y,x) )
proofend;
end;

:: deftheorem Def5 defines symmetric LFUZZY_1:def_5_:_
 for X being non empty set
for R being RMembership_Func of X,X holds
( R is symmetric iff for x, y being Element of X holds R . (x,y) = R . (y,x) );

definition
let X be non empty set ;
let R be RMembership_Func of X,X;
attrR is transitive  means :Def6: :: LFUZZY_1:def 6
R c= ;
end;

:: deftheorem Def6 defines transitive LFUZZY_1:def_6_:_
 for X being non empty set
for R being RMembership_Func of X,X holds
( R is transitive iff R c= );

Lm1:  for X, Y, Z being non empty set
for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds
( rng (min (R,S,x,z)) =  {  ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum  }  &amp; rng (min (R,S,x,z)) <> {} )
proofend;

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

:: deftheorem  defines transitive LFUZZY_1:def_7_:_
 for X being non empty set
for R being RMembership_Func of X,X holds
( R is transitive iff for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] );

definition
let X be non empty set ;
let R be RMembership_Func of X,X;
attrR is antisymmetric  means :Def8: :: LFUZZY_1:def 8
 for x, y being Element of X st R . (x,y) <> 0 &amp; R . (y,x) <> 0 holds
x = y;
end;

:: deftheorem Def8 defines antisymmetric LFUZZY_1:def_8_:_
 for X being non empty set
for R being RMembership_Func of X,X holds
( R is antisymmetric iff for x, y being Element of X st R . (x,y) <> 0 &amp; R . (y,x) <> 0 holds
x = y );

registration
let X be non empty set ;
cluster Imf (X,X) ->  reflexive symmetric transitive antisymmetric ;
coherence
 ( Imf (X,X) is symmetric &amp; Imf (X,X) is transitive &amp; Imf (X,X) is reflexive &amp; Imf (X,X) is antisymmetric )
proofend;
end;

registration
let X be non empty set ;
cluster non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued reflexive symmetric transitive antisymmetric for Element of bool [:[:X,X:],REAL:];
existence
 ex b1 being RMembership_Func of X,X st
( b1 is reflexive &amp; b1 is transitive &amp; b1 is symmetric &amp; b1 is antisymmetric )
proofend;
end;

theorem Th9: :: LFUZZY_1:9
for X being non empty set
for R, S being RMembership_Func of X,X st R is symmetric &amp; S is symmetric holds
converse (min (R,S)) = min (R,S)
proofend;

theorem Th10: :: LFUZZY_1:10
for X being non empty set
for R, S being RMembership_Func of X,X st R is symmetric &amp; S is symmetric holds
converse (max (R,S)) = max (R,S)
proofend;

registration
let X be non empty set ;
let R, S be symmetric RMembership_Func of X,X;
cluster min (R,S) ->  symmetric ;
coherence
 min (R,S) is symmetric
proofend;
cluster max (R,S) ->  symmetric ;
coherence
 max (R,S) is symmetric
proofend;
end;

theorem Th11: :: LFUZZY_1:11
for X being non empty set
for R, S being RMembership_Func of X,X st R is transitive &amp; S is transitive holds
min (R,S) c=
proofend;

registration
let X be non empty set ;
let R, S be transitive RMembership_Func of X,X;
cluster min (R,S) ->  transitive ;
coherence
 min (R,S) is transitive
proofend;
end;

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

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

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

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

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

theorem :: LFUZZY_1:16
for X being non empty set holds
( Zmf (X,X) is symmetric &amp; Zmf (X,X) is antisymmetric &amp; Zmf (X,X) is transitive )
proofend;

theorem :: LFUZZY_1:17
for X being non empty set holds
( Umf (X,X) is symmetric &amp; Umf (X,X) is transitive &amp; Umf (X,X) is reflexive )
proofend;

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

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

theorem :: LFUZZY_1:20
for X being non empty set
for R, R9 being RMembership_Func of X,X st R9 is symmetric &amp; R9 c= holds
R9 c=
proofend;

theorem :: LFUZZY_1:21
for X being non empty set
for R, R9 being RMembership_Func of X,X st R9 is symmetric &amp; R c= holds
min (R,(converse R)) c=
proofend;

begin

definition
let X be non empty set ;
let R be RMembership_Func of X,X;
let n be Nat;
funcn iter R ->  RMembership_Func of X,X means :Def9: :: LFUZZY_1:def 9
 ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st
( it = F . n &amp; F . 0 = Imf (X,X) &amp; ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q &amp; F . (k + 1) = Q (#) R ) ) );
existence
 ex b1 being RMembership_Func of X,X ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st
( b1 = F . n &amp; F . 0 = Imf (X,X) &amp; ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q &amp; F . (k + 1) = Q (#) R ) ) )
proofend;
uniqueness
 for b1, b2 being RMembership_Func of X,X st ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st
( b1 = F . n &amp; F . 0 = Imf (X,X) &amp; ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q &amp; F . (k + 1) = Q (#) R ) ) ) &amp; ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st
( b2 = F . n &amp; F . 0 = Imf (X,X) &amp; ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q &amp; F . (k + 1) = Q (#) R ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines iter LFUZZY_1:def_9_:_
 for X being non empty set
for R being RMembership_Func of X,X
for n being Nat
for b4 being RMembership_Func of X,X holds
( b4 = n iter R iff ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st
( b4 = F . n &amp; F . 0 = Imf (X,X) &amp; ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q &amp; F . (k + 1) = Q (#) R ) ) ) );

theorem Th22: :: LFUZZY_1:22
for X being non empty set
for R being RMembership_Func of X,X holds (Imf (X,X)) (#) R = R
proofend;

theorem Th23: :: LFUZZY_1:23
for X being non empty set
for R being RMembership_Func of X,X holds R (#) (Imf (X,X)) = R
proofend;

theorem Th24: :: LFUZZY_1:24
for X being non empty set
for R being RMembership_Func of X,X holds 0 iter R = Imf (X,X)
proofend;

theorem Th25: :: LFUZZY_1:25
for X being non empty set
for R being RMembership_Func of X,X holds 1 iter R = R
proofend;

theorem Th26: :: LFUZZY_1:26
for X being non empty set
for R being RMembership_Func of X,X
for n being Nat holds (n + 1) iter R = (n iter R) (#) R
proofend;

theorem Th27: :: LFUZZY_1:27
for X being non empty set
for R being RMembership_Func of X,X
for m, n being Nat holds (m + n) iter R = (m iter R) (#) (n iter R)
proofend;

theorem :: LFUZZY_1:28
for X being non empty set
for R being RMembership_Func of X,X
for m, n being Nat holds (m * n) iter R = m iter (n iter R)
proofend;

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 10
 "\/" ( {  (n iter R) where n is Element of NAT : n > 0  }  ,(FuzzyLattice [:X,X:]));
coherence
 "\/" ( {  (n iter R) where n is Element of NAT : n > 0  }  ,(FuzzyLattice [:X,X:])) is RMembership_Func of X,X
proofend;
end;

:: deftheorem  defines TrCl LFUZZY_1:def_10_:_
 for X being non empty set
for R being RMembership_Func of X,X holds TrCl R = "\/" ( {  (n iter R) where n is Element of NAT : n > 0  }  ,(FuzzyLattice [:X,X:]));

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

theorem Th30: :: LFUZZY_1:30
for X being non empty set
for R being RMembership_Func of X,X holds TrCl R c=
proofend;

theorem Th31: :: LFUZZY_1:31
for X being non empty set
for R being RMembership_Func of X,X
for n being Nat st n > 0 holds
TrCl R c=
proofend;

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

Lm2:  for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds  {  ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum  }  =  {  ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum  }
proofend;

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

Lm3:  for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds  {  ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum  }  =  {  ("\/" ( {  ((R . [x,y9]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y9,z])  }  ,(RealPoset [.0,1.]))) where y9 is Element of X : verum  }
proofend;

Lm4:  for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds  {  ("\/" ( {  ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z])  }  ,(RealPoset [.0,1.]))) where y is Element of X : verum  }  =  {  ("\/" ( {  ((R . [x,y9]) "/\" (r . [y9,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q  }  ,(RealPoset [.0,1.]))) where y9 is Element of X : verum  }
proofend;

Lm5:  for X, Y, Z being non empty set
for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds
( rng (min (R,S,x,z)) =  {  ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum  }  &amp; rng (min (R,S,x,z)) <> {} )
proofend;

Lm6:  for X, Y, Z being non empty set
for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds (R (#) S) . [x,z] = "\/" ( {  ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
proofend;

Lm7:  for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds  {  ("\/" ( {  ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum  }  ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q  }  =  {  ("\/" ( {  ((R . [x,y]) "/\" ((@ r9) . [y,z])) where y is Element of X : verum  }  ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q  }
proofend;

Lm8:  for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds  {  ("\/" ( {  ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum  }  ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q  }  =  {  ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q  }
proofend;

Lm9:  for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds  {  ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q  }  = pi ( {  (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q  }  ,[x,z])
proofend;

Lm10:  for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds "\/" ( {  ("\/" ( {  ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q  }  ,(RealPoset [.0,1.]))) where y is Element of X : verum  }  ,(RealPoset [.0,1.])) = "\/" ( {  ("\/" ( {  ((R . [x,y]) "/\" (r9 . [y,z])) where y is Element of X : verum  }  ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q  }  ,(RealPoset [.0,1.]))
proofend;

theorem Th34: :: LFUZZY_1:34
for X being non empty set
for R being RMembership_Func of X,X
for 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:]))
proofend;

theorem Th35: :: LFUZZY_1:35
for X being non empty set
for R being RMembership_Func of X,X
for 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:]))
proofend;

theorem Th36: :: LFUZZY_1:36
for X being non empty set
for R being RMembership_Func of X,X holds (TrCl R) (#) (TrCl R) = "\/" ( {  ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 &amp; j > 0 )  }  ,(FuzzyLattice [:X,X:]))
proofend;

registration
let X be non empty set ;
let R be RMembership_Func of X,X;
cluster TrCl R ->  transitive ;
coherence
 TrCl R is transitive
proofend;
end;

theorem Th37: :: LFUZZY_1:37
for X being non empty set
for R being RMembership_Func of X,X
for n being Nat st R is transitive &amp; n > 0 holds
R c=
proofend;

theorem Th38: :: LFUZZY_1:38
for X being non empty set
for R being RMembership_Func of X,X st R is transitive holds
R = TrCl R
proofend;

theorem Th39: :: LFUZZY_1:39
for X being non empty set
for R, S being RMembership_Func of X,X
for n being Nat st S c= holds
n iter S c=
proofend;

theorem :: LFUZZY_1:40
for X being non empty set
for R, S being RMembership_Func of X,X st S is transitive &amp; S c= holds
S c=
proofend;