:: Transitive Closure of Fuzzy Relations
:: by Takashi Mitsuishi and Grzegorz Bancerek
::
:: Received November 23, 2003
:: Copyright (c) 2003-2016 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, VALUED_0, FUZZY_1, FUZZY_2, LATTICE3,
SUBSET_1, FUNCT_1, XXREAL_0, RELAT_1, ZFMISC_1, TARSKI, VALUED_1,
RELAT_2, FUZZY_4, CARD_1, LATTICES, PARTFUN1, LFUZZY_0, EQREL_1,
XXREAL_1, SEQ_4, FUNCT_3, FUNCT_7, FUNCT_2, ARYTM_3, STRUCT_0, QC_LANG1,
CARD_3, FUNCOP_1, REWRITE1, WAYBEL_0, NEWTON, ORDINAL2, LATTICE2,
WAYBEL_1, NAT_1, LFUZZY_1, REAL_1, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, ORDINAL1,
NUMBERS, XCMPLX_0, DOMAIN_1, PARTFUN1, CARD_3, RELAT_2, BINOP_1, FUNCT_3,
RFUNCT_1, SUBSET_1, XREAL_0, NAT_1, SEQ_4, VALUED_0, RCOMP_1, RELSET_1,
STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, WAYBEL_3,
FUZZY_1, FUZZY_2, FUZZY_4, FUNCOP_1, LFUZZY_0, XXREAL_0;
constructors DOMAIN_1, SQUARE_1, RFUNCT_1, MONOID_0, WAYBEL_3, FUZZY_2,
FUZZY_4, LFUZZY_0, SEQ_4, RELSET_1, FUNCOP_1, FUZZY_1;
registrations XBOOLE_0, SUBSET_1, XREAL_0, NAT_1, MEMBERED, STRUCT_0,
LATTICE3, MONOID_0, YELLOW_1, WAYBEL10, WAYBEL17, LFUZZY_0, RELAT_1,
FUNCT_2, NUMBERS, FUZZY_1, RELSET_1, VALUED_0, ORDINAL1, CARD_1;
requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
begin :: Inclusion of fuzzy relations
reserve X, Y for non empty set;
registration
let X;
cluster -> real-valued for Membership_Func of X;
end;
definition
let X,Y;
let f,g be RMembership_Func of X,Y;
redefine pred f is_less_than g means
:: LFUZZY_1:def 1
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 2
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 3
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 4
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 5
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 6
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 7
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 8
for x,y being Element of X holds R.(x,y ) <> 0 & R.(y,x) <> 0 implies x = y;
end;
registration
let X;
cluster Imf(X,X) -> symmetric transitive reflexive antisymmetric;
end;
registration
let X;
cluster reflexive transitive symmetric antisymmetric for
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);
registration
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);
registration
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 R9 being RMembership_Func of X
,X st R9 is symmetric & R c= R9 holds max(R, converse R) c= R9;
theorem :: LFUZZY_1:21
for R being RMembership_Func of X,X for R9 being RMembership_Func of X
,X st R9 is symmetric & R9 c= R holds R9 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 Nat;
func n iter R -> RMembership_Func of X,X means
:: LFUZZY_1:def 9
ex F being sequence of Funcs([:X,X:],[. 0,1 .]) st it = F.n & F.0 = Imf(X,X)
& for k being Nat
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 Nat holds (n+1) iter R = (n iter R) (#) R;
theorem :: LFUZZY_1:27
for m,n being Nat holds (m+n) iter R = (m iter R) (#) (n iter R);
theorem :: LFUZZY_1:28
for m,n being Nat 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 10
"\/"({n iter R where n is
Element of 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 Element of NAT : n > 0}, [x,y]), RealPoset [. 0,1 .]);
theorem :: LFUZZY_1:30
R c= TrCl R;
theorem :: LFUZZY_1:31
for n being Nat 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 Element of NAT, j is Element of NAT:
i > 0 & j > 0},FuzzyLattice [:X,X:]);
registration
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 Nat 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 Nat 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;