:: Lattice of Fuzzy Sets :: by Takashi Mitsuishi and Grzegorz Bancerek :: :: Received August 12, 2003 :: Copyright (c) 2003-2018 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, ORDERS_2, XREAL_0, STRUCT_0, TARSKI, XXREAL_0, MEASURE5, XXREAL_1, XBOOLE_0, SUBSET_1, CARD_1, RELAT_2, LATTICE3, EQREL_1, LATTICES, XXREAL_2, YELLOW_0, REAL_1, SEQ_4, REWRITE1, TREES_2, LATTICE2, WAYBEL_0, RELAT_1, FUNCT_1, ORDINAL2, YELLOW_1, WAYBEL_3, PBOOLE, CARD_3, WAYBEL_1, NEWTON, FUNCOP_1, FUNCT_2, MONOID_0, FUZZY_1, PARTFUN1, QC_LANG1, FUZZY_2, VALUED_1, ZFMISC_1, LFUZZY_0, MEMBERED; notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, DOMAIN_1, ORDINAL1, PARTFUN1, SUBSET_1, NUMBERS, XXREAL_2, XREAL_0, MEMBERED, SEQ_4, RCOMP_1, RELSET_1, STRUCT_0, ORDERS_2, PBOOLE, MONOID_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, WAYBEL_3, FUZZY_1, FUZZY_2, FUZZY_4, MEASURE5, FUNCOP_1, XXREAL_0; constructors DOMAIN_1, SQUARE_1, LATTICE3, MONOID_0, ORDERS_3, WAYBEL_1, WAYBEL_3, INTEGRA1, FUZZY_4, SEQ_4, RELSET_1, FUZZY_1, BINOP_2; registrations SUBSET_1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, LATTICE3, YELLOW_0, MONOID_0, YELLOW_1, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL10, WAYBEL17, ORDERS_4, ORDERS_2, FUNCOP_1; requirements BOOLE, SUBSET, NUMERALS, REAL; definitions TARSKI, RELAT_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1; equalities XBOOLE_0, BINOP_1; expansions TARSKI, XBOOLE_0, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, BINOP_1; theorems ZFMISC_1, ORDERS_2, WAYBEL_1, FUNCT_1, XBOOLE_1, LATTICE3, YELLOW_0, INTEGRA1, XBOOLE_0, TARSKI, SEQ_4, JORDAN5A, FUNCT_2, YELLOW_2, WAYBEL_3, YELLOW_3, CARD_3, YELLOW_1, FUNCOP_1, FUZZY_2, FUZZY_4, FUZZY_1, PARTFUN1, MONOID_0, WAYBEL_0, XXREAL_0, XXREAL_1, XXREAL_2, RELSET_1, RELAT_1, MEASURE5, MEMBERED; schemes YELLOW_0, PBOOLE, YELLOW_3, FRAENKEL; begin :: Posets of Real Numbers definition let R be RelStr; attr R is real means : Def1: the carrier of R c= REAL & for x,y being Real st x in the carrier of R & y in the carrier of R holds [x,y] in the InternalRel of R iff x <= y; end; definition let R be RelStr; attr R is interval means : Def2: R is real & ex a,b being Real st a <= b & the carrier of R = [.a,b.]; end; registration cluster interval -> real non empty for RelStr; coherence by XXREAL_1:1; end; registration cluster empty -> real for RelStr; coherence proof let R being RelStr; assume A1: the carrier of R is empty; hence the carrier of R c= REAL; thus thesis by A1; end; end; theorem Th1: for X being real-membered set ex R being strict RelStr st the carrier of R = X & R is real proof let X be real-membered set; per cases; suppose A1: X is empty; set E = the empty strict RelStr; take E; thus thesis by A1; end; suppose X is non empty; then reconsider Y = X as non empty set; defpred X[set,set] means ex x,y being Real st $1=x & $2=y & x<=y; consider L being non empty strict RelStr such that A2: the carrier of L = Y and A3: for a,b being Element of L holds a <= b iff X[a,b] from YELLOW_0: sch 1; take L; thus the carrier of L = X by A2; thus the carrier of L c= REAL by A2,MEMBERED:3; let x,y be Real; assume x in the carrier of L & y in the carrier of L; then reconsider a = x, b = y as Element of L; a <= b iff [x,y] in the InternalRel of L by ORDERS_2:def 5; then [x,y] in the InternalRel of L iff ex x,y being Real st a=x & b= y & x<=y by A3; hence thesis; end; end; registration cluster interval strict for RelStr; existence proof set X = [. 0,1 qua Real .]; consider R being strict RelStr such that A1: the carrier of R = X & R is real by Th1; take R; thus thesis by A1; end; end; theorem Th2: for R1,R2 being real RelStr st the carrier of R1 = the carrier of R2 holds the RelStr of R1 = the RelStr of R2 proof let R1, R2 be real RelStr such that A1: the carrier of R1 = the carrier of R2; set X = the carrier of R1; the InternalRel of R1 = the InternalRel of R2 proof let a,b be object; A2: X c= REAL by Def1; hereby assume A3: [a,b] in the InternalRel of R1; then A4: a in X & b in X by ZFMISC_1:87; then reconsider a9 = a, b9 = b as Element of REAL by A2; a9 <= b9 by A3,A4,Def1; hence [a,b] in the InternalRel of R2 by A1,A4,Def1; end; assume A5: [a,b] in the InternalRel of R2; then A6: a in X & b in X by A1,ZFMISC_1:87; then reconsider a9 = a, b9 = b as Element of REAL by A2; a9 <= b9 by A1,A5,A6,Def1; hence thesis by A6,Def1; end; hence thesis by A1; end; registration let R be non empty real RelStr; cluster -> real for Element of R; coherence proof let x be Element of R; the carrier of R c= REAL by Def1; hence thesis; end; end; definition let X be real-membered set; func RealPoset X -> real strict RelStr means : Def3: the carrier of it = X; existence proof ex R being strict RelStr st the carrier of R = X & R is real by Th1; hence thesis; end; uniqueness by Th2; end; registration let X be non empty real-membered set; cluster RealPoset X -> non empty; coherence by Def3; end; notation let R be RelStr; let x,y be Element of R; synonym x <<= y for x <= y; synonym y >>= x for x <= y; antonym x ~<= y for x <= y; antonym y ~>= x for x <= y; end; theorem Th3: for R being non empty real RelStr for x,y being Element of R holds x <= y iff x <<= y proof let R be non empty real RelStr; let x,y be Element of R; [x,y] in the InternalRel of R iff x <= y by Def1; hence thesis by ORDERS_2:def 5; end; registration cluster real -> reflexive antisymmetric transitive for RelStr; coherence proof let R be RelStr such that A1: R is real; per cases; suppose R is empty; hence thesis; end; suppose R is non empty; then reconsider R9 = R as non empty real RelStr by A1; A2: R9 is antisymmetric proof let x,y be Element of R9; assume x <<= y & x >>= y; then x <= y & x >= y by Th3; hence thesis by XXREAL_0:1; end; A3: R9 is transitive proof let x,y,z be Element of R9; assume x <<= y & y <<= z; then x <= y & y <= z by Th3; then x <= z by XXREAL_0:2; hence thesis by Th3; end; R9 is reflexive by Th3; hence thesis by A2,A3; end; end; end; registration cluster -> connected for real non empty RelStr; coherence proof let R be non empty real RelStr; let x,y be Element of R; x <= y or x >= y; hence thesis by Th3; end; end; definition let R be non empty real RelStr; let x,y be Element of R; redefine func max(x,y) -> Element of R; coherence by XXREAL_0:16; end; definition let R be non empty real RelStr; let x,y be Element of R; redefine func min(x,y) -> Element of R; coherence by XXREAL_0:15; end; registration cluster -> with_suprema with_infima for real non empty RelStr; coherence; end; reserve x,y,z for Real, R for real non empty RelStr, a,b for Element of R; registration let R; let a,b be Element of R; identify a"\/"b with max(a,b); compatibility proof A1: for d being Element of R st d >>= a & d >>= b holds max(a,b) <<= d proof let d be Element of R; assume d >>= a & d >>= b; then d >= a & d >= b by Th3; then max(a,b) <= d by XXREAL_0:28; hence thesis by Th3; end; max(a,b) >= b by XXREAL_0:25; then A2: max(a,b) >>= b by Th3; max(a,b) >= a by XXREAL_0:25; then max(a,b) >>= a by Th3; hence thesis by A2,A1,YELLOW_0:22; end; identify a"/\"b with min(a,b); compatibility proof A3: for d being Element of R st d <<= a & d <<= b holds min(a,b) >>= d proof let d being Element of R; assume d <<= a & d <<= b; then d <= a & d <= b by Th3; then d <= min(a,b) by XXREAL_0:20; hence thesis by Th3; end; min(a,b) <= b by XXREAL_0:17; then A4: min(a,b) <<= b by Th3; min(a,b) <= a by XXREAL_0:17; then min(a,b) <<= a by Th3; hence thesis by A4,A3,YELLOW_0:23; end; end; theorem a"\/"b = max(a,b); theorem a"/\"b = min(a,b); theorem Th6: (ex x st x in the carrier of R & for y st y in the carrier of R holds x <= y) iff R is lower-bounded proof hereby given x such that A1: x in the carrier of R and A2: for y st y in the carrier of R holds x <= y; reconsider a = x as Element of R by A1; for b st b in the carrier of R holds a <<= b by A2,Th3; then a is_<=_than the carrier of R; hence R is lower-bounded; end; given x being Element of R such that A3: x is_<=_than the carrier of R; take x; thus x in the carrier of R; let y; assume y in the carrier of R; then reconsider b = y as Element of R; x <<= b by A3; hence thesis by Th3; end; theorem Th7: (ex x st x in the carrier of R & for y st y in the carrier of R holds x >= y) iff R is upper-bounded proof hereby given x such that A1: x in the carrier of R and A2: for y st y in the carrier of R holds x >= y; reconsider a = x as Element of R by A1; for b st b in the carrier of R holds a >>= b by A2,Th3; then a is_>=_than the carrier of R; hence R is upper-bounded; end; given x being Element of R such that A3: x is_>=_than the carrier of R; take x; thus x in the carrier of R; let y; assume y in the carrier of R; then reconsider b = y as Element of R; x >>= b by A3; hence thesis by Th3; end; registration cluster interval -> bounded for non empty RelStr; coherence proof let R being non empty RelStr; assume A1: R is real; given x,y being Real such that A2: x <= y and A3: the carrier of R = [.x,y.]; ex x st x in the carrier of R & for y st y in the carrier of R holds x <= y proof take x; thus x in the carrier of R by A2,A3,XXREAL_1:1; let z; assume z in the carrier of R; hence thesis by A3,XXREAL_1:1; end; then A4: R is lower-bounded by A1,Th6; ex x st x in the carrier of R & for y st y in the carrier of R holds x >= y proof take y; thus y in the carrier of R by A2,A3,XXREAL_1:1; let z; assume z in the carrier of R; hence thesis by A3,XXREAL_1:1; end; then R is upper-bounded by A1,Th7; hence thesis by A4; end; end; theorem Th8: for R being interval non empty RelStr, X being set holds ex_sup_of X,R proof let R being interval non empty RelStr; let X being set; consider a,b being Real such that A1: a <= b and A2: the carrier of R = [.a,b.] by Def2; reconsider a,b as Real; reconsider Y = X /\ [.a,b.] as Subset of REAL; [.a,b.] is non empty closed_interval by A1,MEASURE5:14; then A3: [.a,b.] is bounded_above by INTEGRA1:3; then A4: Y is bounded_above by XBOOLE_1:17,XXREAL_2:43; A5: X /\ [.a,b.] c= [.a,b.] by XBOOLE_1:17; ex a being Element of R st Y is_<=_than a & for b being Element of R st Y is_<=_than b holds a <<= b proof per cases; suppose A6: Y is empty; reconsider x = a as Element of R by A1,A2,XXREAL_1:1; take x; thus Y is_<=_than x by A6; let y be Element of R; x <= y by A2,XXREAL_1:1; hence thesis by Th3; end; suppose A7: Y is non empty; set c = the Element of Y; A8: c in Y by A7; reconsider c as Real; A9: a<=c by A5,A8,XXREAL_1:1; c <= upper_bound Y by A4,A7,SEQ_4:def 1; then A10: a <= upper_bound Y by A9,XXREAL_0:2; upper_bound [.a,b.] = b by A1,JORDAN5A:19; then upper_bound Y <= b by A3,A7,SEQ_4:48,XBOOLE_1:17; then reconsider x = upper_bound Y as Element of R by A2,A10,XXREAL_1:1; A11: for y being Element of R st Y is_<=_than y holds x <<= y proof let y be Element of R; assume A12: Y is_<=_than y; for z being Real st z in Y holds z <= y proof let z being Real; assume A13: z in Y; then reconsider z as Element of R by A2,XBOOLE_0:def 4; z <<= y by A12,A13; hence thesis by Th3; end; then upper_bound Y <= y by A7,SEQ_4:144; hence thesis by Th3; end; take x; for b being Element of R st b in Y holds b <<= x proof let b be Element of R; assume b in Y; then b <= upper_bound Y by A4,SEQ_4:def 1; hence thesis by Th3; end; hence thesis by A11; end; end; then ex_sup_of Y,R by YELLOW_0:15; hence thesis by A2,YELLOW_0:50; end; registration cluster -> complete for interval non empty RelStr; coherence proof let R be interval non empty RelStr; for X being Subset of R holds ex_sup_of X,R by Th8; hence thesis by YELLOW_0:53; end; end; registration cluster -> distributive for Chain; coherence proof let C be Chain; for x,y,z being Element of C holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) proof let x,y,z be Element of C; A1: x <= x; per cases by WAYBEL_0:def 29; suppose A2: x <= y & x <= z & y <= z; then A3: x "/\" (y "\/" z) = x "/\" z by YELLOW_0:24 .= x by A2,YELLOW_0:25; (x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A2,YELLOW_0:25 .= x "\/" x by A2,YELLOW_0:25 .= x by A1,YELLOW_0:24; hence thesis by A3; end; suppose A4: x <= y & x <= z & y >= z; then A5: x "/\" (y "\/" z) = x "/\" y by YELLOW_0:24 .= x by A4,YELLOW_0:25; (x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A4,YELLOW_0:25 .= x "\/" x by A4,YELLOW_0:25 .= x by A1,YELLOW_0:24; hence thesis by A5; end; suppose A6: x <= y & x >= z & y <= z; then z <= y by YELLOW_0:def 2; then A7: z = y by A6,YELLOW_0:def 3; A8: x "/\" (y "\/" z) = x "/\" z by A6,YELLOW_0:24 .= z by A6,YELLOW_0:25; (x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A6,YELLOW_0:25 .= x "\/" z by A6,YELLOW_0:25 .= x by A6,YELLOW_0:24; hence thesis by A6,A7,A8,YELLOW_0:def 3; end; suppose A9: x <= y & x >= z & y >= z; then A10: x "/\" (y "\/" z) = x "/\" y by YELLOW_0:24 .= x by A9,YELLOW_0:25; (x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A9,YELLOW_0:25 .= x "\/" z by A9,YELLOW_0:25 .= x by A9,YELLOW_0:24; hence thesis by A10; end; suppose A11: x >= y & x <= z & y <= z; then A12: x "/\" (y "\/" z) = x "/\" z by YELLOW_0:24 .= x by A11,YELLOW_0:25; (x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A11,YELLOW_0:25 .= y "\/" x by A11,YELLOW_0:25 .= x by A11,YELLOW_0:24; hence thesis by A12; end; suppose A13: x >= y & x <= z & y >= z; then z >= y by YELLOW_0:def 2; then A14: z = y by A13,YELLOW_0:def 3; A15: x "/\" (y "\/" z) = x "/\" y by A13,YELLOW_0:24 .= y by A13,YELLOW_0:25; (x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A13,YELLOW_0:25 .= y "\/" x by A13,YELLOW_0:25 .= x by A13,YELLOW_0:24; hence thesis by A13,A14,A15,YELLOW_0:def 3; end; suppose A16: x >= y & x >= z & y <= z; then A17: x "/\" (y "\/" z) = x "/\" z by YELLOW_0:24 .= z by A16,YELLOW_0:25; (x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A16,YELLOW_0:25 .= y "\/" z by A16,YELLOW_0:25 .= z by A16,YELLOW_0:24; hence thesis by A17; end; suppose A18: x >= y & x >= z & y >= z; then A19: x "/\" (y "\/" z) = x "/\" y by YELLOW_0:24 .= y by A18,YELLOW_0:25; (x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A18,YELLOW_0:25 .= y "\/" z by A18,YELLOW_0:25 .= y by A18,YELLOW_0:24; hence thesis by A19; end; end; hence thesis; end; end; registration cluster -> Heyting for interval non empty RelStr; coherence proof let R be interval non empty RelStr; thus R is LATTICE; let x be Element of R; set f = x "/\"; f is sups-preserving proof let X be Subset of R; assume ex_sup_of X,R; A1: now let b being Element of R such that A2: b is_>=_than f.:X; per cases; suppose A3: x is_>=_than X; b is_>=_than X proof let a be Element of R; assume A4: a in X; then x >>= a by A3; then x "/\" a = a by YELLOW_0:25; then A5: a = f.a by WAYBEL_1:def 18; f.a in f.:X by A4,FUNCT_2:35; hence thesis by A2,A5; end; then A6: b >>= sup X by YELLOW_0:32; x >>= sup X by A3,YELLOW_0:32; then x "/\" sup X = sup X by YELLOW_0:25; hence f.sup X <<= b by A6,WAYBEL_1:def 18; end; suppose not x is_>=_than X; then consider a being Element of R such that A7: a in X and A8: not x >>= a; A9: x <<= a by A8,WAYBEL_0:def 29; a <<= sup X by A7,YELLOW_2:22; then x <<= sup X by A9,ORDERS_2:3; then x = x "/\"sup X by YELLOW_0:25; then A10: x = f.sup X by WAYBEL_1:def 18; A11: f.a in f.:X by A7,FUNCT_2:35; x = x "/\" a by A9,YELLOW_0:25 .= f.a by WAYBEL_1:def 18; hence f.sup X <<= b by A2,A10,A11; end; end; thus ex_sup_of f.:X,R by Th8; f.sup X is_>=_than f.:X proof let a be Element of R; A12: f.sup X = x "/\" sup X & x <<= x by WAYBEL_1:def 18,YELLOW_0:def 1; assume a in f.:X; then consider y being object such that A13: y in the carrier of R and A14: y in X & a = f.y by FUNCT_2:64; reconsider y as Element of R by A13; y <<= sup X & a = x "/\" y by A14,WAYBEL_1:def 18,YELLOW_2:22; hence thesis by A12,YELLOW_3:2; end; hence thesis by A1,YELLOW_0:30; end; hence thesis by WAYBEL_1:17; end; end; registration cluster [.0,1 .] -> non empty; coherence by MEASURE5:14; end; registration cluster RealPoset [.0,1 .] -> interval; coherence by Def3; end; begin :: Product of Heyting Lattices theorem Th9: for I being non empty set for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st for i being Element of I holds J.i is sup-Semilattice holds product J is with_suprema proof let I being non empty set; let J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I such that A1: for i being Element of I holds J.i is sup-Semilattice; set IT = product J; for x,y being Element of IT ex z being Element of IT st x <= z & y <= z & for z9 being Element of IT st x <= z9 & y <= z9 holds z <= z9 proof let x,y being Element of IT; deffunc U(Element of I) = x.$1 "\/" y.$1; consider z be ManySortedSet of I such that A2: for i be Element of I holds z.i = U(i) from PBOOLE:sch 5; A3: for i being Element of I holds z.i is Element of J.i proof let i being Element of I; z.i = x.i "\/" y.i by A2; hence thesis; end; dom z = I by PARTFUN1:def 2; then reconsider z as Element of product J by A3,WAYBEL_3:27; take z; for i being Element of I holds x.i <= z.i & y.i <= z.i proof let i being Element of I; J.i is antisymmetric with_suprema RelStr & z.i = x.i "\/" y.i by A1,A2; hence thesis by YELLOW_0:22; end; hence x <= z & y <= z by WAYBEL_3:28; let z9 be Element of IT; assume that A4: x <= z9 and A5: y <= z9; for i being Element of I holds z.i <= z9.i proof let i being Element of I; A6: z9.i >= y.i & z.i = x.i "\/" y.i by A2,A5,WAYBEL_3:28; J.i is antisymmetric with_suprema RelStr & z9.i >= x.i by A1,A4, WAYBEL_3:28; hence thesis by A6,YELLOW_0:22; end; hence thesis by WAYBEL_3:28; end; hence thesis; end; theorem Th10: for I being non empty set for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st for i being Element of I holds J.i is Semilattice holds product J is with_infima proof let I being non empty set; let J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I such that A1: for i being Element of I holds J.i is Semilattice; set IT = product J; for x,y being Element of IT ex z being Element of IT st x >= z & y >= z & for z9 being Element of IT st x >= z9 & y >= z9 holds z >= z9 proof let x,y being Element of IT; deffunc U(Element of I) = x.$1 "/\" y.$1; consider z be ManySortedSet of I such that A2: for i be Element of I holds z.i = U(i) from PBOOLE:sch 5; A3: for i being Element of I holds z.i is Element of J.i proof let i being Element of I; z.i = x.i "/\" y.i by A2; hence thesis; end; dom z = I by PARTFUN1:def 2; then reconsider z as Element of product J by A3,WAYBEL_3:27; take z; for i being Element of I holds x.i >= z.i & y.i >= z.i proof let i being Element of I; J.i is antisymmetric with_infima RelStr & z.i = x.i "/\" y.i by A1,A2; hence thesis by YELLOW_0:23; end; hence x >= z & y >= z by WAYBEL_3:28; let z9 be Element of IT; assume that A4: x >= z9 and A5: y >= z9; for i being Element of I holds z.i >= z9.i proof let i being Element of I; A6: z9.i <= y.i & z.i = x.i "/\" y.i by A2,A5,WAYBEL_3:28; J.i is antisymmetric with_infima RelStr & x.i >= z9.i by A1,A4, WAYBEL_3:28; hence thesis by A6,YELLOW_0:23; end; hence thesis by WAYBEL_3:28; end; hence thesis; end; theorem Th11: for I being non empty set for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st for i being Element of I holds J.i is Semilattice for f,g being Element of product J, i being Element of I holds (f "/\" g).i = (f.i) "/\" (g.i) proof let I being non empty set; let J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I such that A1: for i being Element of I holds J.i is Semilattice; let f,g being Element of product J; let i being Element of I; A2: J.i is Semilattice by A1; for i being Element of I holds J.i is antisymmetric by A1; then A3: product J is antisymmetric with_infima by A1,Th10,WAYBEL_3:30; then g >= f "/\" g by YELLOW_0:23; then A4: g.i >= (f "/\" g).i by WAYBEL_3:28; A5: (f "/\" g).i >= (f.i) "/\" (g.i) proof deffunc U(Element of I) = f.$1 "/\" g.$1; consider z be ManySortedSet of I such that A6: for i be Element of I holds z.i = U(i) from PBOOLE:sch 5; A7: for i being Element of I holds z.i is Element of J.i proof let i being Element of I; z.i = f.i "/\" g.i by A6; hence thesis; end; dom z = I by PARTFUN1:def 2; then reconsider z as Element of product J by A7,WAYBEL_3:27; for i being Element of I holds z.i <= f.i & z.i <= g.i proof let i being Element of I; J.i is antisymmetric with_infima RelStr & z.i = f.i "/\" g.i by A1,A6; hence thesis by YELLOW_0:23; end; then z <= f & z <= g by WAYBEL_3:28; then A8: f "/\" g >= z by A3,YELLOW_0:23; for i being Element of I holds (f "/\" g).i >= f.i "/\" g.i proof let i being Element of I; f.i "/\" g.i = z.i by A6; hence thesis by A8,WAYBEL_3:28; end; hence thesis; end; f >= f "/\" g by A3,YELLOW_0:23; then f.i >= (f "/\" g).i by WAYBEL_3:28; then (f "/\" g).i <= (f.i) "/\" (g.i) by A2,A4,YELLOW_0:23; hence thesis by A2,A5,YELLOW_0:def 3; end; theorem Th12: for I being non empty set for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st for i being Element of I holds J.i is sup-Semilattice for f,g being Element of product J, i being Element of I holds (f "\/" g).i = (f.i) "\/" (g.i) proof let I being non empty set; let J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I such that A1: for i being Element of I holds J.i is sup-Semilattice; let f,g being Element of product J; let i being Element of I; A2: J.i is sup-Semilattice by A1; for i being Element of I holds J.i is antisymmetric by A1; then A3: product J is antisymmetric with_suprema by A1,Th9,WAYBEL_3:30; then g <= f "\/" g by YELLOW_0:22; then A4: g.i <= (f "\/" g).i by WAYBEL_3:28; A5: (f "\/" g).i <= (f.i) "\/" (g.i) proof deffunc U(Element of I) = f.$1 "\/" g.$1; consider z be ManySortedSet of I such that A6: for i be Element of I holds z.i = U(i) from PBOOLE:sch 5; A7: for i being Element of I holds z.i is Element of J.i proof let i being Element of I; z.i = f.i "\/" g.i by A6; hence thesis; end; dom z = I by PARTFUN1:def 2; then reconsider z as Element of product J by A7,WAYBEL_3:27; for i being Element of I holds z.i >= f.i & z.i >= g.i proof let i being Element of I; J.i is antisymmetric with_suprema RelStr & z.i = f.i "\/" g.i by A1,A6; hence thesis by YELLOW_0:22; end; then z >= f & z >= g by WAYBEL_3:28; then A8: f "\/" g <= z by A3,YELLOW_0:22; for i being Element of I holds (f "\/" g).i <= f.i "\/" g.i proof let i being Element of I; f.i "\/" g.i = z.i by A6; hence thesis by A8,WAYBEL_3:28; end; hence thesis; end; f <= f "\/" g by A3,YELLOW_0:22; then f.i <= (f "\/" g).i by WAYBEL_3:28; then (f "\/" g).i >= (f.i) "\/" (g.i) by A2,A4,YELLOW_0:22; hence thesis by A2,A5,YELLOW_0:def 3; end; theorem Th13: for I being non empty set for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st for i being Element of I holds J.i is Heyting complete LATTICE holds product J is complete Heyting proof let I be non empty set; let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I such that A1: for i being Element of I holds J.i is Heyting complete LATTICE; A2: for i being Element of I holds J.i is complete LATTICE by A1; set H = product J; reconsider H as complete LATTICE by A2,WAYBEL_3:31; H = H; hence product J is complete & product J is LATTICE; let f be Element of product J; reconsider g = f as Element of H; reconsider F = f "/\" as Function of H,H; A3: for i being Element of I holds J.i is Semilattice by A1; F is sups-preserving proof let X be Subset of H; reconsider Y = F.:X, X9 = X as Subset of product J; reconsider sX = sup X as Element of product J; assume ex_sup_of X, H; thus ex_sup_of F.:X, H by YELLOW_0:17; reconsider f1 = sup (F.:X), f2 = F.sup X as Element of product J; A4: now let x be object; assume x in dom f1; then reconsider i = x as Element of I by WAYBEL_3:27; A5: J.i is complete Heyting LATTICE by A1; then A6: ex_sup_of pi(X9,i), J.i by YELLOW_0:17; A7: ((f.i) "/\").:pi(X9,i) c= pi(Y,i) proof let b be object; assume b in ((f.i) "/\").:pi(X9,i); then consider f4 being object such that f4 in dom ((f.i) "/\") and A8: f4 in pi(X9,i) and A9: b = ((f.i) "/\").f4 by FUNCT_1:def 6; consider f5 being Function such that A10: f5 in X9 and A11: f4 = f5.i by A8,CARD_3:def 6; reconsider f5 as Element of product J by A10; (f "/\" f5) = f "/\". f5 by WAYBEL_1:def 18; then A12: (f "/\" f5) in f"/\" .: X by A10,FUNCT_2:35; ((f.i) "/\").f4 = (f.i) "/\" (f5.i) by A11,WAYBEL_1:def 18 .= (f "/\" f5).i by A3,Th11; hence thesis by A9,A12,CARD_3:def 6; end; pi(Y,i) c= ((f.i) "/\").:pi(X9,i) proof let a be object; assume a in pi(Y,i); then consider f3 being Function such that A13: f3 in Y and A14: a = f3.i by CARD_3:def 6; reconsider f3 as Element of product J by A13; consider h being object such that A15: h in dom F and A16: h in X and A17: f3=F.h by A13,FUNCT_1:def 6; reconsider h as Element of product J by A15; A18: (h.i) in pi(X9,i) by A16,CARD_3:def 6; f3.i = (f "/\" h).i by A17,WAYBEL_1:def 18 .= f.i "/\" h.i by A3,Th11 .= (f.i "/\").(h.i) by WAYBEL_1:def 18; hence thesis by A14,A18,FUNCT_2:35; end; then A19: pi(Y,i) = ((f.i) "/\").:pi(X9,i) by A7; (f.i) "/\" is lower_adjoint by A5,WAYBEL_1:def 19; then A20: (f.i) "/\" preserves_sup_of pi(X9,i) by A5,WAYBEL_0:def 33; f2 = g "/\" sup X by WAYBEL_1:def 18; then f2.i = (f.i) "/\" (sX.i) by A3,Th11 .= (f.i) "/\" sup pi(X9, i) by A2,WAYBEL_3:32 .= ((f.i) "/\").sup pi(X9,i) by WAYBEL_1:def 18 .= sup (((f.i) "/\").:pi(X9,i)) by A20,A6; hence f1.x = f2.x by A2,A19,WAYBEL_3:32; end; dom f1 = I & dom f2 = I by WAYBEL_3:27; hence thesis by A4,FUNCT_1:2; end; hence thesis by WAYBEL_1:17; end; registration let A be non empty set; let R be complete Heyting LATTICE; cluster R |^ A -> Heyting; coherence proof for i being Element of A holds (A --> R).i is complete Heyting LATTICE by FUNCOP_1:7; then product (A --> R) is complete Heyting by Th13; hence thesis by YELLOW_1:def 5; end; end; begin :: Lattice of Fuzzy Sets definition let A be non empty set; func FuzzyLattice A -> Heyting complete LATTICE equals (RealPoset [. 0,1 .]) |^ A; coherence; end; theorem Th14: for A being non empty set holds the carrier of FuzzyLattice A = Funcs(A, [. 0, 1 .]) proof let A be non empty set; thus the carrier of FuzzyLattice A = Funcs (A, the carrier of RealPoset [. 0 ,1 .]) by YELLOW_1:28 .= Funcs (A, [. 0,1 .]) by Def3; end; Lm1: for A being non empty set holds FuzzyLattice A is constituted-Functions proof let A be non empty set; for a being Element of FuzzyLattice A holds a is Function proof let a be Element of FuzzyLattice A; a in the carrier of FuzzyLattice A; then a in Funcs(A, [. 0, 1 .]) by Th14; then ex f being Function st a = f & dom f = A & rng f c= [. 0, 1 .] by FUNCT_2:def 2; hence thesis; end; hence thesis by MONOID_0:def 1; end; registration let A be non empty set; cluster FuzzyLattice A -> constituted-Functions; coherence by Lm1; end; theorem Th15: for R being complete Heyting LATTICE, X being Subset of R, y be Element of R holds "\/"(X,R) "/\" y = "\/"({x "/\" y where x is Element of R: x in X},R) proof let R be complete Heyting LATTICE, X be Subset of R, y be Element of R; set Z = {y "/\" x where x is Element of R: x in X}, W = {x "/\" y where x is Element of R: x in X}; A1: W c= Z proof let w be object; assume w in W; then ex x being Element of R st w = x "/\" y & x in X; hence thesis; end; Z c= W proof let z be object; assume z in Z; then ex x being Element of R st z = y "/\" x & x in X; hence thesis; end; then ( for z being Element of R holds z "/\" is lower_adjoint & ex_sup_of X,R )& Z = W by A1,WAYBEL_1:def 19,YELLOW_0:17; hence thesis by WAYBEL_1:63; end; Lm2: for X being non empty set for a being Element of FuzzyLattice X holds a is Membership_Func of X proof let X be non empty set; let a be Element of FuzzyLattice X; a in the carrier of FuzzyLattice X; then a in Funcs(X, [. 0,1 .]) by Th14; then A1: ex f being Function st a = f & dom f = X & rng f c= [. 0 ,1 .] by FUNCT_2:def 2; then reconsider a as PartFunc of X, [. 0,1 .] by RELSET_1:4; reconsider a as PartFunc of X, REAL by RELSET_1:7; a is Function of X,REAL by A1,FUNCT_2:def 1; hence thesis; end; definition let X be non empty set; let a be Element of FuzzyLattice X; func @a -> Membership_Func of X equals a; coherence by Lm2; end; Lm3: for X be non empty set for f be Membership_Func of X holds f is Element of FuzzyLattice X proof let X be non empty set; let f be Membership_Func of X; dom f = X & rng f c= [. 0,1 .] by FUNCT_2:def 1,RELAT_1:def 19; then f in Funcs(X, [. 0,1 .]) by FUNCT_2:def 2; hence thesis by Th14; end; definition let X be non empty set; let f be Membership_Func of X; func (X,f)@ -> Element of FuzzyLattice X equals f; coherence by Lm3; end; definition let X be non empty set; let f be Membership_Func of X; let x be Element of X; redefine func f.x -> Element of RealPoset [. 0,1 .]; coherence proof 0 <= f.x & f.x <= 1 by FUZZY_2:1; then f.x in [. 0,1 .] by XXREAL_1:1; hence thesis by Def3; end; end; definition let X,Y be non empty set; let f be RMembership_Func of X,Y; let x be Element of X, y be Element of Y; redefine func f.(x,y) -> Element of RealPoset [. 0,1 .]; coherence proof f. [x,y] is Element of RealPoset [. 0,1 .]; hence thesis; end; end; definition let X be non empty set; let f be Element of FuzzyLattice X; let x be Element of X; redefine func f.x -> Element of RealPoset [. 0,1 .]; coherence proof 0 <= @f.x by FUZZY_2:1; hence thesis; end; end; reserve C for non empty set, c for Element of C, f,g for Membership_Func of C, s,t for Element of FuzzyLattice C; theorem Th16: (for c holds f.c <= g.c) iff (C,f)@ <<= (C,g)@ proof A1: (RealPoset [. 0,1 .]) |^ C = product (C --> RealPoset [. 0,1 .]) by YELLOW_1:def 5; A2: (for c holds f.c <= g.c) implies (C,f)@ <<= (C,g)@ proof set f9 = (C,f)@, g9 = (C,g)@; reconsider f9,g9 as Element of product (C --> RealPoset [. 0,1 .]) by YELLOW_1:def 5; assume A3: for c holds f.c <= g.c; for c holds f9.c <<= g9.c proof let c be Element of C; set f1 = f.c, g1=g.c; (C --> RealPoset [. 0,1 .]).c = RealPoset [. 0,1 .] & f1 <= g1 by A3, FUNCOP_1:7; hence thesis by Th3; end; hence thesis by A1,WAYBEL_3:28; end; (C,f)@ <<= (C,g)@ implies for c holds f.c <= g.c proof reconsider ff = (C,f)@, gg = (C,g)@ as Element of product (C --> RealPoset [. 0,1 .]) by YELLOW_1:def 5; assume A4: (C,f)@ <<= (C,g)@; let c; (C --> RealPoset [. 0,1 .]).c = RealPoset [. 0,1 .] & ff.c <<= gg.c by A1 ,A4,FUNCOP_1:7,WAYBEL_3:28; hence thesis by Th3; end; hence thesis by A2; end; theorem s <<= t iff for c holds @s.c <= @t.c proof (C,@s)@ = s & (C,@t)@ = t; hence thesis by Th16; end; theorem Th18: max(f,g) = (C,f)@ "\/" (C,g)@ proof set fg = (C,f)@ "\/" (C,g)@, R = RealPoset [. 0,1 .], J = C --> R; A1: (RealPoset [. 0,1 .]) |^ C = product (C --> RealPoset [. 0,1 .]) by YELLOW_1:def 5; now let c; ( for c being Element of C holds J.c is sup-Semilattice)& J.c = RealPoset [. 0 ,1 .] by FUNCOP_1:7; hence (@fg).c = ((C,f)@.c) "\/" ((C,g)@.c) by A1,Th12 .= max(f.c, g.c); end; hence thesis by FUZZY_1:def 4; end; theorem s "\/" t = max(@s, @t) proof (C,@s)@ = s & (C,@t)@ = t; hence thesis by Th18; end; theorem Th20: min(f,g) = (C,f)@ "/\" (C,g)@ proof set fg = (C,f)@ "/\" (C,g)@, R = RealPoset [. 0,1 .], J = C --> R; A1: (RealPoset [. 0,1 .]) |^ C = product (C --> RealPoset [. 0,1 .]) by YELLOW_1:def 5; now let c; ( for c being Element of C holds J.c is Semilattice)& J.c = RealPoset [. 0,1 .] by FUNCOP_1:7; hence (@fg).c = ((C,f)@.c) "/\" ((C,g)@.c) by A1,Th11 .= min(f.c, g.c); end; hence thesis by FUZZY_1:def 3; end; theorem s "/\" t = min(@s, @t) proof (C,@s)@ = s & (C,@t)@ = t; hence thesis by Th20; end; begin :: Associativity of composition of fuzzy relations scheme SupDistributivity { L() -> complete LATTICE, X, Y() -> non empty set, F(set, set) -> Element of L(), P,Q[set]}: "\/"({ "\/"({F(x,y) where y is Element of Y( ): Q[y]}, L()) where x is Element of X(): P[x] }, L()) = "\/"({F(x,y) where x is Element of X(), y is Element of Y(): P[x] & Q[y]}, L()) proof defpred R[set] means ex x being Element of X() st P[x] & for a being set holds a in $1 iff ex y being Element of Y() st a = F(x,y) & Q[y]; A1: "\/" ({ "\/"(A,L()) where A is Subset of L(): R[A] },L()) = "\/" (union {A where A is Subset of L(): R[A]}, L()) from YELLOW_3:sch 5; A2: {F(x,y) where x is Element of X(), y is Element of Y(): P[x] & Q[y] } c= union {A where A is Subset of L(): R[A]} proof let a be object; assume a in {F(x,y) where x is Element of X(), y is Element of Y() : P[x ] & Q[y]}; then consider x being Element of X(), y being Element of Y() such that A3: a = F(x,y) and A4: P[x] and A5: Q[y]; set A1 = {F(x,y9) where y9 is Element of Y(): Q[y9]}; A1 c= the carrier of L() proof let b be object; assume b in A1; then ex y9 being Element of Y() st b = F(x,y9) & Q[y9]; hence thesis; end; then reconsider A1 as Subset of L(); R[A1] proof take x; thus P[x] by A4; let a be set; thus thesis; end; then A6: A1 in {A where A is Subset of L(): R[A]}; a in A1 by A3,A5; hence thesis by A6,TARSKI:def 4; end; A7: { "\/"({F(x,y) where y is Element of Y(): Q[y]}, L()) where x is Element of X(): P[x] } c= { "\/"(A,L()) where A is Subset of L(): R[A] } proof let a be object; assume a in { "\/"({F(x,y) where y is Element of Y(): Q[y]}, L()) where x is Element of X(): P[x] }; then consider x being Element of X() such that A8: a = "\/"({F(x,y) where y is Element of Y(): Q[y]}, L()) and A9: P[x]; ex A1 being Subset of L() st a = "\/"(A1,L()) & R[A1] proof set A2 = {F(x,y) where y is Element of Y(): Q[y]}; A2 c= the carrier of L() proof let b be object; assume b in A2; then ex y being Element of Y() st b = F(x,y) & Q[y]; hence thesis; end; then reconsider A1 = A2 as Subset of L(); R[A1] proof take x; thus P[x] by A9; thus thesis; end; hence thesis by A8; end; hence thesis; end; A10: { "\/"(A,L()) where A is Subset of L(): R[A] } c= { "\/"({F(x,y) where y is Element of Y(): Q[y]}, L()) where x is Element of X(): P[x] } proof let a be object; assume a in { "\/"(A,L()) where A is Subset of L(): R[A] }; then consider A1 being Subset of L() such that A11: a = "\/"(A1,L()) and A12: R[A1]; consider x being Element of X() such that A13: P[x] and A14: for a being set holds a in A1 iff ex y being Element of Y() st a = F(x,y) & Q[y] by A12; now let a be object; a in {F(x,y) where y is Element of Y(): Q[y]} iff ex y being Element of Y() st a = F(x,y) & Q[y]; hence a in A1 iff a in {F(x,y) where y is Element of Y(): Q[y]} by A14; end; then A1 = {F(x,y) where y is Element of Y(): Q[y]} by TARSKI:2; hence thesis by A11,A13; end; union {A where A is Subset of L(): R[A]} c= {F(x,y) where x is Element of X(), y is Element of Y(): P[x] & Q[y]} proof let a be object; assume a in union {A where A is Subset of L(): R[A]}; then consider A1 be set such that A15: a in A1 and A16: A1 in {A where A is Subset of L(): R[A]} by TARSKI:def 4; consider A2 being Subset of L() such that A17: A1 = A2 and A18: R[A2] by A16; consider x being Element of X() such that A19: P[x] and A20: for a being set holds a in A2 iff ex y being Element of Y() st a = F(x,y) & Q[y] by A18; ex y being Element of Y() st a = F(x,y) & Q[y] by A15,A17,A20; hence thesis by A19; end; then union {A where A is Subset of L(): R[A]} = {F(x,y) where x is Element of X( ), y is Element of Y(): P[x] & Q[y]} by A2; hence thesis by A1,A10,A7,XBOOLE_0:def 10; end; scheme SupDistributivity9 { L() -> complete LATTICE, X, Y() -> non empty set, F(set ,set) -> Element of L(), P,Q[set]}: "\/"({ "\/"({F(x,y) where x is Element of X (): P[x]},L()) where y is Element of Y(): Q[y] }, L()) = "\/"({F(x,y) where x is Element of X(), y is Element of Y(): P[x] & Q[y]}, L()) proof defpred R[set] means ex y being Element of Y() st Q[y] & for a being set holds a in $1 iff ex x being Element of X() st a = F(x,y) & P[x]; A1: "\/" ({ "\/"(A,L()) where A is Subset of L(): R[A] },L()) = "\/" (union {A where A is Subset of L(): R[A]}, L()) from YELLOW_3:sch 5; A2: {F(x,y) where x is Element of X(), y is Element of Y(): P[x] & Q[y] } c= union {A where A is Subset of L(): R[A]} proof let a be object; assume a in {F(x,y) where x is Element of X(), y is Element of Y() : P[x ] & Q[y]}; then consider x being Element of X(), y being Element of Y() such that A3: a = F(x,y) & P[x] and A4: Q[y]; set A1 = {F(x9,y) where x9 is Element of X(): P[x9]}; A1 c= the carrier of L() proof let b be object; assume b in A1; then ex x9 being Element of X() st b = F(x9,y) & P[x9]; hence thesis; end; then reconsider A1 as Subset of L(); R[A1] proof take y; thus Q[y] by A4; let a be set; thus thesis; end; then A5: A1 in {A where A is Subset of L(): R[A]}; a in A1 by A3; hence thesis by A5,TARSKI:def 4; end; A6: { "\/"({F(x,y) where x is Element of X(): P[x]}, L()) where y is Element of Y(): Q[y] } c= { "\/"(A,L()) where A is Subset of L(): R[A] } proof let a be object; assume a in { "\/"({F(x,y) where x is Element of X(): P[x]}, L()) where y is Element of Y(): Q[y] }; then consider y being Element of Y() such that A7: a = "\/"({F(x,y) where x is Element of X(): P[x]}, L()) and A8: Q[y]; ex A1 being Subset of L() st a = "\/"(A1,L()) & R[A1] proof set A2 = {F(x,y) where x is Element of X(): P[x]}; A2 c= the carrier of L() proof let b be object; assume b in A2; then ex x being Element of X() st b = F(x,y) & P[x]; hence thesis; end; then reconsider A1 = A2 as Subset of L(); R[A1] proof take y; thus Q[y] by A8; thus thesis; end; hence thesis by A7; end; hence thesis; end; A9: { "\/"(A,L()) where A is Subset of L(): R[A] } c= { "\/"({F(x,y) where x is Element of X(): P[x]}, L()) where y is Element of Y(): Q[y] } proof let a be object; assume a in { "\/"(A,L()) where A is Subset of L(): R[A] }; then consider A1 being Subset of L() such that A10: a = "\/"(A1,L()) and A11: R[A1]; consider y being Element of Y() such that A12: Q[y] and A13: for a being set holds a in A1 iff ex x being Element of X() st a = F(x,y) & P[x] by A11; now let a be object; a in {F(x,y) where x is Element of X(): P[x]} iff ex x being Element of X() st a = F(x,y) & P[x]; hence a in A1 iff a in {F(x,y) where x is Element of X(): P[x]} by A13; end; then A1 = {F(x,y) where x is Element of X(): P[x]} by TARSKI:2; hence thesis by A10,A12; end; union {A where A is Subset of L(): R[A]} c= {F(x,y) where x is Element of X(), y is Element of Y(): P[x] & Q[y]} proof let a be object; assume a in union {A where A is Subset of L(): R[A]}; then consider A1 be set such that A14: a in A1 and A15: A1 in {A where A is Subset of L(): R[A]} by TARSKI:def 4; consider A2 being Subset of L() such that A16: A1 = A2 and A17: R[A2] by A15; consider y being Element of Y() such that A18: Q[y] and A19: for a being set holds a in A2 iff ex x being Element of X() st a = F(x,y) & P[x] by A17; ex x being Element of X() st a = F(x,y) & P[x] by A14,A16,A19; hence thesis by A18; end; then union {A where A is Subset of L(): R[A]} = {F(x,y) where x is Element of X( ), y is Element of Y(): P[x] & Q[y]} by A2; hence thesis by A1,A9,A6,XBOOLE_0:def 10; end; scheme FraenkelF9R9{ A() -> non empty set,B() -> non empty set, F1, F2(set,set) -> set, P[set,set] } : { F1(u1,v1) where u1 is (Element of A()), v1 is Element of B() : P[u1,v1] } = { F2(u2,v2) where u2 is (Element of A()), v2 is Element of B () : P[u2,v2] } provided A1: for u being (Element of A()), v being Element of B() st P[u,v] holds F1(u,v) = F2(u,v) proof set A = { F1(u1,v1) where u1 is (Element of A()), v1 is Element of B() : P[ u1,v1] }, C = { F2(u3,v3) where u3 is (Element of A()), v3 is Element of B() : P[u3,v3] }; for a be object holds a in A iff a in C proof let a be object; hereby assume a in A; then consider u being (Element of A()), v being Element of B() such that A2: a = F1(u,v) and A3: P[u,v]; a = F2(u,v) by A1,A2,A3; hence a in C by A3; end; assume a in C; then consider u being (Element of A()), v being Element of B() such that A4: a = F2(u,v) and A5: P[u,v]; a = F1(u,v) by A1,A4,A5; hence thesis by A5; end; hence thesis by TARSKI:2; end; scheme FraenkelF699R { A() -> non empty set, B() -> non empty set, F1, F2(set,set) -> set, P[set,set], Q[set,set] } : { F1(u1,v1) where u1 is (Element of A()), v1 is Element of B() : P[u1,v1] } = { F2(u2,v2) where u2 is (Element of A()), v2 is Element of B() : Q[u2,v2] } provided A1: for u being (Element of A()), v being Element of B() holds P[u,v] iff Q[u,v] and A2: for u being (Element of A()), v being Element of B() st P[u,v] holds F1(u,v) = F2(u,v) proof set A = { F1(u1,v1) where u1 is (Element of A()), v1 is Element of B() : P[ u1,v1] }, B = { F2(u2,v2) where u2 is (Element of A()), v2 is Element of B() : Q[u2,v2] }, C = { F2(u3,v3) where u3 is (Element of A()), v3 is Element of B() : P[u3,v3] }; A3: C = B from FRAENKEL:sch 4(A1); A = C from FraenkelF9R9(A2); hence thesis by A3; end; scheme SupCommutativity { L() -> complete LATTICE, X, Y() -> non empty set, F1, F2( set,set) -> Element of L(), P,Q[set]}: "\/"({ "\/"({F1(x,y) where y is Element of Y(): Q[y]}, L()) where x is Element of X(): P[x] }, L()) = "\/"({ "\/"({F2( x9,y9) where x9 is Element of X(): P[x9]}, L()) where y9 is Element of Y(): Q[ y9] }, L()) provided A1: for x being Element of X(), y being Element of Y() st P[x] & Q[y] holds F1(x,y) = F2(x,y) proof defpred X[set,set] means P[$1] & Q[$2]; A2: for x being Element of X(), y being Element of Y() holds X[x,y] iff X[x, y]; A3: for x being Element of X(), y being Element of Y() st X[x,y] holds F1(x, y) = F2(x,y) by A1; A4: {F1(x9,y9) where x9 is Element of X(), y9 is Element of Y(): X[x9,y9]} = {F2(x,y) where x is Element of X(), y is Element of Y(): X[x,y]} from FraenkelF699R(A2,A3); A5: "\/"({ "\/"({F1(x,y) where y is Element of Y(): Q[y]}, L()) where x is Element of X(): P[x] }, L()) ="\/"({F1(x,y) where x is Element of X(), y is Element of Y(): P[x] & Q[y]}, L()) from SupDistributivity; "\/"({ "\/"({F2(x9,y9) where x9 is Element of X(): P[x9]}, L()) where y9 is Element of Y(): Q[y9] }, L()) ="\/"({F2(x9,y9) where x9 is Element of X(), y9 is Element of Y(): P[x9] & Q[y9]}, L()) from SupDistributivity9 .="\/"({F1(x9,y9) where x9 is Element of X(), y9 is Element of Y(): P[x9 ] & Q[y9]}, L()) by A4; hence thesis by A5; end; Lm4: 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, z being Element of Z holds rng min(R,S,x,z) = the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y & rng min(R,S,x,z) <> {} proof let X,Y,Z being non empty set; let R being RMembership_Func of X,Y; let S being RMembership_Func of Y,Z; let x being Element of X, z being Element of Z; set L = the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y; A1: Y = dom min(R,S,x,z) & min(R,S,x,z) is PartFunc of dom min(R,S,x,z), rng min (R,S,x,z) by FUNCT_2:def 1,RELSET_1:4; for c be object holds c in L iff c in rng min(R,S,x,z) proof let c be object; hereby assume c in L; then consider y being Element of Y such that A2: c = R.(x,y) "/\" S.(y,z); c = min(R,S,x,z).y by A2,FUZZY_4:def 2; hence c in rng min(R,S,x,z) by A1,PARTFUN1:4; end; assume c in rng min(R,S,x,z); then consider y being Element of Y such that y in dom min(R,S,x,z) and A3: c = min(R,S,x,z).y by PARTFUN1:3; c = R.(x,y) "/\" S.(y,z) by A3,FUZZY_4:def 2; hence thesis; end; hence rng min(R,S,x,z) = L by TARSKI:2; ex d be set st d in rng min(R,S,x,z) proof set y = the Element of Y; take min(R,S,x,z).y; thus thesis by A1,PARTFUN1:4; end; hence rng min(R,S,x,z) <> {}; end; theorem Th22: 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, z being Element of Z holds (R (#) S).(x,z) = "\/"((the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y), RealPoset [. 0,1 .]) proof let X,Y,Z being non empty set; let R being RMembership_Func of X,Y; let S being RMembership_Func of Y,Z; let x being Element of X, z being Element of Z; set L = the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y; [x,z] in [:X,Z:]; then A1: (R (#) S).(x,z) = upper_bound(rng(min(R,S,x,z))) by FUZZY_4:def 3; A2: for b being Element of RealPoset [. 0,1 .] st b is_>=_than L holds (R (#) S).(x,z) <<= b proof let b be Element of RealPoset [. 0,1 .]; assume A3: b is_>=_than the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y; A4: rng min(R,S,x,z) c= [. 0,1 .] by RELAT_1:def 19; A5: L = rng min(R,S,x,z) by Lm4; A6: for r being Real st r in rng min(R,S,x,z) holds r <= b proof let r be Real; assume A7: r in rng min(R,S,x,z); then reconsider r as Element of RealPoset [. 0,1 .] by A4,Def3; r <<= b by A3,A5,A7; hence thesis by Th3; end; rng min(R,S,x,z) <> {} by Lm4; then upper_bound rng min(R,S,x,z) <= b by A6,SEQ_4:144; hence thesis by A1,Th3; end; for b being Element of RealPoset [. 0,1 .] st b in L holds (R (#) S). [x ,z] >>= b proof let b be Element of RealPoset [. 0,1 .]; assume b in L; then consider y being Element of Y such that A8: b = R.(x,y) "/\" S.(y,z); reconsider b as Real; dom min(R,S,x,z) = Y & b = min(R,S,x,z).y by A8,FUNCT_2:def 1,FUZZY_4:def 2; then b <= upper_bound rng min(R,S,x,z) by FUZZY_4:1; hence thesis by A1,Th3; end; then (R (#) S). [x,z] is_>=_than L; hence thesis by A2,YELLOW_0:32; end; 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, z being Element of Z for a being Element of RealPoset [. 0,1 .] holds (R (#) S).(x,z) "/\" a = "\/"( (the set of all R.(x,y) "/\" S.(y,z) "/\" a where y is Element of Y), RealPoset [. 0,1 .]) proof let X,Y,Z being non empty set; let R being RMembership_Func of X,Y; let S being RMembership_Func of Y,Z; let x being Element of X, z being Element of Z; let a being Element of RealPoset [. 0,1 .]; A1: the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y c= the carrier of RealPoset [. 0,1 .] proof let d be object; assume d in the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y; then ex t being Element of Y st d = R.(x,t) "/\" S.(t,z); hence thesis; end; set A = {b "/\" a where b is Element of RealPoset [. 0,1 .]: b in the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y}; set B = the set of all R.(x,y) "/\" S.(y,z) "/\" a where y is Element of Y; A2: for c be object holds c in A iff c in B proof let c be object; hereby assume c in A; then consider b being Element of RealPoset [. 0,1 .] such that A3: c = b "/\" a and A4: b in the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y; ex y being Element of Y st b = R.(x,y) "/\" S.(y,z) by A4; hence c in B by A3; end; assume c in B; then consider y being Element of Y such that A5: c = R.(x,y) "/\" S.(y,z) "/\" a; R.(x,y) "/\" S.(y,z) in the set of all R.(x,y1) "/\" S.(y1,z) where y1 is Element of Y; hence thesis by A5; end; (R (#) S).(x,z) "/\" a = "\/"((the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y), RealPoset [. 0,1 .]) "/\" a by Th22 .= "\/"({b "/\" a where b is Element of RealPoset [. 0,1 .]: b in the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y}, RealPoset [. 0,1 .]) by A1,Th15; hence thesis by A2,TARSKI:2; end; 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, z being Element of Z for a being Element of RealPoset [. 0,1 .] holds a "/\" (R (#) S).(x,z) = "\/"( (the set of all a "/\" R.(x,y) "/\" S.(y,z) where y is Element of Y), RealPoset [. 0,1 .]) proof let X,Y,Z being non empty set; let R being RMembership_Func of X,Y; let S being RMembership_Func of Y,Z; let x being Element of X, z being Element of Z; let a being Element of RealPoset [. 0,1 .]; set A = the set of all a "/\" R.(x,y) "/\" S.(y,z) where y is Element of Y; set B = the set of all R.(x,y) "/\" S.(y,z) "/\" a where y is Element of Y; for b be object holds b in A iff b in B proof let b be object; hereby assume b in A; then consider y being Element of Y such that A1: b = a "/\" R.(x,y) "/\" S.(y,z); b = R.(x,y) "/\" S.(y,z) "/\" a by A1,LATTICE3:16; hence b in B; end; assume b in B; then consider y being Element of Y such that A2: b = R.(x,y) "/\" S.(y,z) "/\" a; b = a "/\" R.(x,y) "/\" S.(y,z) by A2,LATTICE3:16; hence thesis; end; then A = B by TARSKI:2; hence thesis by Lm5; end; theorem for X,Y,Z,W being non empty set for R being RMembership_Func of X,Y for S being RMembership_Func of Y,Z for T being RMembership_Func of Z,W holds ( R (#) S) (#) T = R (#) (S (#) T) proof let X,Y,Z,W be non empty set; let R be RMembership_Func of X,Y; let S be RMembership_Func of Y,Z; let T be RMembership_Func of Z,W; A1: for x,w being object st x in X & w in W holds ((R (#) S) (#) T).(x,w) = (R (#) (S (#) T)).(x,w) proof let x,w being object; assume that A2: x in X and A3: w in W; reconsider w as Element of W by A3; reconsider x as Element of X by A2; set A = the set of all "\/"((the set of all R.(x,y) "/\" S.(y,z) "/\" T.(z,w) where y is Element of Y), RealPoset [. 0,1 .]) where z is Element of Z; set B = the set of all (R (#) S).(x,z) "/\" T.(z,w) where z is Element of Z; set C = the set of all "\/"((the set of all R.(x,y) "/\" S.(y,z) "/\" T.(z,w) where z is Element of Z), RealPoset [. 0,1 .]) where y is Element of Y; set D = the set of all R.(x,y) "/\" ((S (#) T).(y,w)) where y is Element of Y; defpred X[set] means not contradiction; deffunc U(Element of Y,Element of Z) = R.(x,$1) "/\" S.($1,$2) "/\" T.($2, w); A4: for a be object holds a in A iff a in B proof let a be object; hereby assume a in A; then consider z being Element of Z such that A5: a = "\/"((the set of all R.(x,y) "/\" S.(y,z) "/\" T.(z,w) where y is Element of Y), RealPoset [. 0,1 .]); a = (R (#) S).(x,z) "/\" T.(z,w) by A5,Lm5; hence a in B; end; assume a in B; then consider z being Element of Z such that A6: a = (R (#) S).(x,z) "/\" T.(z,w); a = "\/"((the set of all R.(x,y) "/\" S.(y,z) "/\" T.(z,w) where y is Element of Y), RealPoset [. 0,1 .]) by A6,Lm5; hence thesis; end; A7: for y being Element of Y, z being Element of Z st X[y] & X[z] holds U (y,z) = U(y,z); A8: "\/"({"\/"({U(y,z) where z is Element of Z: X[z]}, RealPoset [. 0,1 .]) where y is Element of Y :X[y]}, RealPoset [. 0,1 .]) ="\/"({"\/"({U(y1,z1) where y1 is Element of Y: X[y1]}, RealPoset [. 0,1 .]) where z1 is Element of Z :X[z1]}, RealPoset [. 0,1 .]) from SupCommutativity(A7); for c be object holds c in C iff c in D proof let c be object; hereby assume c in C; then consider y being Element of Y such that A9: c = "\/"((the set of all R.(x,y) "/\" S.(y,z) "/\" T.(z,w) where z is Element of Z), RealPoset [. 0,1 .]); c = R.(x,y) "/\" (S (#) T).(y,w) by A9,Lm6; hence c in D; end; assume c in D; then consider y being Element of Y such that A10: c = R.(x,y) "/\" ((S (#) T).(y,w)); c = "\/"((the set of all R.(x,y) "/\" S.(y,z) "/\" T.(z,w) where z is Element of Z),RealPoset [. 0,1 .]) by A10,Lm6; hence thesis; end; then A11: C = D by TARSKI:2; ((R (#) S) (#) T).(x,w) = "\/"((the set of all ((R (#) S).(x,z)) "/\" T.(z,w) where z is Element of Z), RealPoset [. 0,1 .]) & (R (#) (S (#) T)).( x, w) = "\/"((the set of all R.(x,y) "/\" ((S (#) T).(y,w)) where y is Element of Y), RealPoset [. 0,1 .]) by Th22; hence thesis by A4,A11,A8,TARSKI:2; end; thus thesis by A1; end;