:: Transitive Closure of Fuzzy Relations :: by Takashi Mitsuishi and Grzegorz Bancerek :: :: Received November 23, 2003 :: Copyright (c) 2003-2021 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;