:: Properties of Fuzzy Relation :: by Noboru Endou , Takashi Mitsuishi and Keiji Ohkubo :: :: Received June 25, 2001 :: Copyright (c) 2001-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, FUZZY_1, RELAT_1, SUBSET_1, FUNCT_1, XXREAL_2, XXREAL_0, XXREAL_1, CARD_1, TARSKI, ARYTM_3, ARYTM_1, FUZZY_2, ZFMISC_1, PARTFUN1, VALUED_1, SEQ_4, FUZZY_4, MEASURE5, REAL_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, FUNCT_1, BINOP_1, RELAT_1, RELSET_1, PARTFUN1, XXREAL_2, FUNCT_4, INTEGRA1, RCOMP_1, MEASURE6, FUZZY_1, FUZZY_2, SEQ_4, MEASURE5; constructors FUNCT_4, REAL_1, SQUARE_1, RFUNCT_1, MEASURE6, INTEGRA1, FUZZY_2, XXREAL_2, SEQ_4, RELSET_1, RELAT_1, FUZZY_1, BINOP_2, RVSUM_1, BINOP_1, NUMBERS; registrations XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, INTEGRA1, RELAT_1, VALUED_0, RELSET_1, MEASURE5, BINOP_2, ORDINAL1; requirements NUMERALS, REAL, SUBSET, BOOLE; begin :: Basic properties of the membership function reserve c,c1,c2,x,y,z,z1,z2 for set; reserve C1,C2,C3 for non empty set; registration let C1 be non empty set; let F be Membership_Func of C1; cluster rng F -> non empty; end; theorem :: FUZZY_4:1 for F be Membership_Func of C1 holds rng F is real-bounded & (for x st x in dom F holds F.x <= upper_bound rng F) & for x st x in dom F holds F.x >= lower_bound rng F; theorem :: FUZZY_4:2 for F,G be Membership_Func of C1 holds (for x st x in C1 holds F.x <= G.x) implies upper_bound rng F <= upper_bound rng G; theorem :: FUZZY_4:3 for f be RMembership_Func of C1,C2, c be set holds 0 <= f.c & f.c <= 1; theorem :: FUZZY_4:4 for f be RMembership_Func of C1,C2, x,y holds 0 <= f.(x,y) & f.(x,y) <= 1; begin :: Definition and properties of converse fuzzy relation notation let C1,C2 be non empty set; let h be RMembership_Func of C2,C1; synonym converse h for ~h; end; definition let C1,C2 be non empty set; let h be RMembership_Func of C2,C1; redefine func converse h -> RMembership_Func of C1,C2 means :: FUZZY_4:def 1 for x,y being object st [x,y] in [:C1,C2:] holds it.(x,y) = h.(y,x); end; theorem :: FUZZY_4:5 for f be RMembership_Func of C1,C2 holds converse converse f = f; theorem :: FUZZY_4:6 for f be RMembership_Func of C1,C2 holds 1_minus(converse f) = converse(1_minus f); theorem :: FUZZY_4:7 for f,g be RMembership_Func of C1,C2 holds converse max(f,g) = max(converse f,converse g); theorem :: FUZZY_4:8 for f,g be RMembership_Func of C1,C2 holds converse min(f,g) = min(converse f,converse g); theorem :: FUZZY_4:9 for f,g be RMembership_Func of C1,C2, x,y st x in C1 & y in C2 holds f. [x,y] <= g. [x,y] implies (converse f). [y,x] <= (converse g). [y,x]; theorem :: FUZZY_4:10 for f,g be RMembership_Func of C1,C2 holds f c= g implies converse f c= converse g; theorem :: FUZZY_4:11 for f,g be RMembership_Func of C1,C2 holds converse(f\g) = (converse f )\(converse g); theorem :: FUZZY_4:12 for f,g be RMembership_Func of C1,C2 holds converse (f \+\ g) = ( converse f) \+\ (converse g); begin :: Definition and properties of the composition definition let C1,C2,C3 be non empty set; let h be RMembership_Func of C1,C2; let g be RMembership_Func of C2,C3; let x,z be object; assume that x in C1 and z in C3; func min(h,g,x,z) -> Membership_Func of C2 means :: FUZZY_4:def 2 for y being Element of C2 holds it.y = min(h. [x,y],g. [y,z]); end; definition let C1,C2,C3 be non empty set; let h be RMembership_Func of C1,C2; let g be RMembership_Func of C2,C3; func h(#)g -> RMembership_Func of C1,C3 means :: FUZZY_4:def 3 for x,z being object st [x,z] in [: C1,C3:] holds it.(x,z) = upper_bound(rng(min(h,g,x,z))); end; theorem :: FUZZY_4:13 for f be RMembership_Func of C1,C2, g,h be RMembership_Func of C2,C3 holds f(#)(max(g,h)) = max(f(#)g,f(#)h); theorem :: FUZZY_4:14 for f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3 holds (max(f,g))(#)h = max(f(#)h,g(#)h); theorem :: FUZZY_4:15 for f be RMembership_Func of C1,C2, g,h be RMembership_Func of C2,C3 holds f(#)(min(g,h)) c= min(f(#)g,f(#)h); theorem :: FUZZY_4:16 for f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3 holds min(f,g)(#)h c= min(f(#)h,g(#)h); theorem :: FUZZY_4:17 for f be RMembership_Func of C1,C2, g be RMembership_Func of C2,C3 holds converse(f(#)g) = (converse g)(#)(converse f); theorem :: FUZZY_4:18 for f,g be RMembership_Func of C1,C2, h,k be RMembership_Func of C2,C3, x,z be set st x in C1 & z in C3 & (for y be set st y in C2 holds f. [x,y ]<=g. [x,y] & h. [y,z]<=k. [y,z]) holds (f(#)h). [x,z] <= (g(#)k). [x,z]; theorem :: FUZZY_4:19 for f,g be RMembership_Func of C1,C2, h,k be RMembership_Func of C2,C3 st f c= g & h c= k holds f(#)h c= g(#)k; begin definition let C1,C2 be non empty set; func Imf(C1,C2) -> RMembership_Func of C1,C2 means :: FUZZY_4:def 4 for x,y being object st [x,y] in [:C1,C2:] holds (x=y implies it.(x,y) = 1) & (x<>y implies it.(x,y) = 0); end; theorem :: FUZZY_4:20 for c be Element of [:C1,C2:] holds (Zmf(C1,C2)).c = 0 & (Umf(C1,C2)). c = 1; theorem :: FUZZY_4:21 for x,y st [x,y] in [:C1,C2:] holds (Zmf(C1,C2)). [x,y] = 0 & (Umf(C1, C2)). [x,y] = 1; theorem :: FUZZY_4:22 for f be RMembership_Func of C2,C3 holds Zmf(C1,C2)(#)f = Zmf(C1 ,C3); theorem :: FUZZY_4:23 for f be RMembership_Func of C1,C2 holds f(#)Zmf(C2,C3) = Zmf(C1 ,C3); theorem :: FUZZY_4:24 for f be RMembership_Func of C1,C1 holds f(#)Zmf(C1,C1) = Zmf(C1,C1) (#)f; begin :: Addenda :: missing, 2006.12.03, AT theorem :: FUZZY_4:25 for X,Y being non empty set for x being Element of X, y being Element of Y holds (x = y implies Imf(X,Y).(x,y) = 1) & (x <> y implies Imf(X,Y).(x,y) = 0); theorem :: FUZZY_4:26 for X,Y being non empty set for x being Element of X, y being Element of Y for f being RMembership_Func of X,Y holds (converse f).(y,x) = f.(x,y);