Volume 15, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

### 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;

Back to top