:: Basic Formal Properties of Triangular Norms and Conorms :: by Adam Grabowski :: :: Received June 27, 2017 :: Copyright (c) 2017-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, XXREAL_1, REAL_1, XXREAL_0, SUBSET_1, CARD_1, ARYTM_1, ARYTM_3, FUNCT_1, XBOOLE_0, RELAT_1, XREAL_0, FUNCT_7, FUZNORM1, ZFMISC_1, BINOP_1, MSAFREE2, MEMBERED; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, MEMBERED, ZFMISC_1, BINOP_1, VALUED_0, RELAT_1, XXREAL_2, XREAL_0, COMPLEX1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, REAL_1, SEQ_4, RCOMP_1, PRE_TOPC, TOPS_2, METRIC_1, DOMAIN_1, STRUCT_0, TOPMETR, TSEP_1, TMAP_1, FUZZY_1, BORSUK_1, MEASURE5; constructors REAL_1, SQUARE_1, COMPLEX1, SEQ_4, RCOMP_1, CONNSP_1, TOPS_2, TMAP_1, TOPMETR, XXREAL_2, BINOP_2, RVSUM_1, PCOMPS_1, BINOP_1, FUZZY_1, XREAL_0, INTEGRA1, MESFUNC5, EXTREAL1; registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, BORSUK_1, TOPMETR, CONNSP_1, ORDINAL1, INTEGRA1, INTEGRA2, MEASURE5, EXTREAL1, SUPINF_1, SUPINF_2; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, FUNCT_2, XXREAL_2, SUBSET_1; equalities SUBSET_1, STRUCT_0, BINOP_1, ORDINAL1, PARTFUN1; expansions TARSKI, FUNCT_2, XXREAL_2; theorems SUBSET_1, FUNCT_1, FUNCT_2, XCMPLX_1, XREAL_1, XXREAL_0, XXREAL_1, BINOP_1, ZFMISC_1, FUZZY_2; schemes BINOP_1, SCHEME1; begin :: Preliminaries registration cluster [.0,1.] -> non empty; coherence by XXREAL_1:1; end; theorem MinIn01: for a,b being Element of [.0,1.] holds min (a,b) in [.0,1.] proof let a,b be Element of [.0,1.]; min (a,b) = a or min (a,b) = b by XXREAL_0:15; hence thesis; end; theorem MaxIn01: for a,b being Element of [.0,1.] holds max (a,b) in [.0,1.] proof let a,b be Element of [.0,1.]; max (a,b) = a or max (a,b) = b by XXREAL_0:16; hence thesis; end; theorem Lemma1: for a,b being Element of [.0,1.] holds a * b in [.0,1.] proof let a,b be Element of [.0,1.]; A0: 1 >= a >= 0 & 1 >= b >= 0 by XXREAL_1:1; then 1 >= a * b by XREAL_1:160; hence thesis by XXREAL_1:1,A0; end; theorem Lemma2: for a,b being Element of [.0,1.] holds max (0, a + b - 1) in [.0,1.] proof let a,b be Element of [.0,1.]; A1: max (0, a + b - 1) >= 0 by XXREAL_0:25; a <= 1 & b <= 1 by XXREAL_1:1; then a + b <= 1 + 1 by XREAL_1:7; then A2: a + b - 1 <= 2 - 1 by XREAL_1:9; max (0, a + b - 1) = 0 or max (0, a + b - 1) = a + b - 1 by XXREAL_0:16; hence thesis by A1,XXREAL_1:1,A2; end; theorem Lemma2a: for a,b being Element of [.0,1.] holds min (a + b, 1) in [.0,1.] proof let a,b be Element of [.0,1.]; A1: min (a + b, 1) <= 1 by XXREAL_0:17; A2: a >= 0 & b >= 0 by XXREAL_1:1; min (1, a + b) = 1 or min (1, a + b) = a + b by XXREAL_0:15; hence thesis by A1,XXREAL_1:1,A2; end; theorem Lemma3: for a,b,c being Element of [.0,1.] holds max (0,max(0,a+b-1)+c-1) = max (0,a+max(0,b+c-1)-1) proof let a,b,c be Element of [.0,1.]; A1: 0 <= a & 0 <= b & 0 <= c by XXREAL_1:1; zz: c - 0 <= 1 by XXREAL_1:1; then c - 1 <= 0 by XREAL_1:12; then y2: (c-1) + (a + b -1) <= 0 + (a + b -1) by XREAL_1:6; per cases; suppose Z0: 0 <= a + b - 1 & 0 <= b+c-1; then Z1: max (0,a+b-1) = a + b -1 by XXREAL_0:def 10; max (0,b+c-1) = b + c -1 by Z0,XXREAL_0:def 10; hence thesis by Z1; end; suppose Z0: 0 > a + b - 1 & 0 <= b+c-1; then Z1: max (0,a+b-1) = 0 by XXREAL_0:def 10; Z2: max (0,b+c-1) = b + c - 1 by Z0,XXREAL_0:def 10; max (0,max(0,a+b-1)+c-1) = 0 by zz,XXREAL_0:def 10,Z1,XREAL_1:12 .= max (0,a+max(0,b+c-1)-1) by Z2,y2,Z0,XXREAL_0:def 10; hence thesis; end; suppose Z0: 0 > a + b - 1 & 0 > b + c-1; then Z3: c-1 < 0 & a - 1 < 0 by XREAL_1:9,A1,XREAL_1:31; Z1: max (0,a+b-1) = 0 by Z0,XXREAL_0:def 10; Z2: max (0,b+c-1) = 0 by Z0,XXREAL_0:def 10; max (0,max(0,a+b-1)+c-1) = 0 by Z3,XXREAL_0:def 10,Z1 .= max (0,a+max(0,b+c-1)-1) by Z2,Z3,XXREAL_0:def 10; hence thesis; end; suppose Z0: 0 <= a + b - 1 & 0 > b+c-1; ds: a - 0 <= 1 by XXREAL_1:1; then a - 1 <= 0 by XREAL_1:12; then sb: a-1+(b+c-1) <= 0 + 0 by Z0; Z1: max (0,a+b-1) = a + b -1 by Z0,XXREAL_0:def 10; max (0,max(0,a+b-1)+c-1) = 0 by sb,XXREAL_0:def 10,Z1 .= max (0,a+0-1) by XXREAL_0:def 10,XREAL_1:12,ds .= max (0,a+max(0,b+c-1)-1) by Z0,XXREAL_0:def 10; hence thesis; end; end; theorem OpIn01: for a being Element of [.0,1.] holds 1 - a in [.0,1.] proof let a be Element of [.0,1.]; 0 <= a <= 1 by XXREAL_1:1; then 1 - 1 <= 1 - a <= 1 - 0 by XREAL_1:13; hence thesis by XXREAL_1:1; end; theorem abMinab01: for a, b being Element of [.0,1.] holds a + b - a * b in [.0,1.] proof let a, b be Element of [.0,1.]; S1: 1 - b in [.0,1.] by OpIn01; then a * (1 - b) in [.0,1.] by Lemma1; then B1: a * (1 - b) >= 0 by XXREAL_1:1; a0: b >= 0 by XXREAL_1:1; S2: a <= 1 & b <= 1 by XXREAL_1:1; 0 <= 1 - b <= 1 by S1,XXREAL_1:1; then a * (1 - b) <= 1 * (1 - b) by S2,XREAL_1:64; then a * (1 - b) + b <= 1 - b + b by XREAL_1:6; hence thesis by XXREAL_1:1,a0,B1; end; theorem HamIn01: for a, b being Element of [.0,1.] holds (a * b) / (a + b - a * b) in [.0,1.] proof let a, b be Element of [.0,1.]; A1: a * b in [.0,1.] by Lemma1; a + b - a * b in [.0,1.] by abMinab01; then A2: a + b - a * b >= 0 by XXREAL_1:1; T0: a * b >= 0 by A1,XXREAL_1:1; 0 <= a & b <= 1 by XXREAL_1:1; then S1: a * b <= a by XREAL_1:153; 0 <= b & a <= 1 by XXREAL_1:1; then a * b <= b by XREAL_1:153; then a * b + a * b <= a + b by S1,XREAL_1:7; then a * b <= a + b - a * b by XREAL_1:19; then (a * b) / (a + b - a * b) <= 1 by XREAL_1:183,T0; hence thesis by T0,A2,XXREAL_1:1; end; theorem DiffMax: for a,b being Element of [.0,1.] st max (a,b) <> 1 holds a <> 1 & b <> 1 proof let a,b be Element of [.0,1.]; assume A1: max (a,b) <> 1; A2: a <= 1 & b <= 1 by XXREAL_1:1; assume a = 1 or b = 1; then per cases; suppose a = 1; hence thesis by A1,A2,XXREAL_0:def 10; end; suppose b = 1; hence thesis by A1,A2,XXREAL_0:def 10; end; end; theorem Lemacik: for x, y being Element of [.0,1.] holds x * y = x + y implies x = 0 proof let x, y be Element of [.0,1.]; assume x * y = x + y; then z1: y * (1 - x) = -x; assume x <> 0; then 0 < x <= 1 by XXREAL_1:1; then A4: -x < -0 by XREAL_1:25; 1 - x in [.0,1.] by OpIn01; then A2: 0 <= 1 - x & 1 - x <= 1 by XXREAL_1:1; y < 0 by A4,A2,z1; hence thesis by XXREAL_1:1; end; theorem MaxMin: for a,b being Element of [.0,1.] holds max (a,b) = 1 - min (1-a,1-b) proof let a,b be Element of [.0,1.]; per cases; suppose A1: a <= b; then min (1-a,1-b) = 1 - b by XXREAL_0:def 9,XREAL_1:10; hence thesis by A1,XXREAL_0:def 10; end; suppose A1: a > b; then min (1-a,1-b) = 1 - a by XXREAL_0:def 9,XREAL_1:10; hence thesis by A1,XXREAL_0:def 10; end; end; theorem LukasiDual: for a,b being Element of [.0,1.] holds min (a+b,1) = 1 - max (0,1-a+(1-b)-1) proof let a,b be Element of [.0,1.]; per cases; suppose A1: a + b <= 1; then A2: a + b - (a + b) <= 1 - (a + b) by XREAL_1:9; min (a + b, 1) = 1 - (1 - a - b) by A1,XXREAL_0:def 9 .= 1 - max (0,1-a+(1-b)-1) by A2,XXREAL_0:def 10; hence thesis; end; suppose A1: a + b > 1; then A2: a + b - (a + b) > 1 - (a + b) by XREAL_1:9; min (a+b,1) = 1 - 0 by A1,XXREAL_0:def 9 .= 1 - max (0,1-a+(1-b)-1) by A2,XXREAL_0:def 10; hence thesis; end; end; theorem HamCoIn01: for a,b being Element of [.0,1.] holds (a + b - 2 * a * b) / (1 - a * b) in [.0,1.] proof let a,b be Element of [.0,1.]; 0 <= a & b <= 1 by XXREAL_1:1; then S1: a * b <= a by XREAL_1:153; S2: 0 <= b & a <= 1 by XXREAL_1:1; then a * b <= b by XREAL_1:153; then a * b + a * b <= a + b by S1,XREAL_1:7; then S5: a * b - a * b <= a + b - a * b - a * b by XREAL_1:9,19; 1 - b in [.0,1.] by OpIn01; then 1 - b >= 0 by XXREAL_1:1; then a * (1 - b) <= 1 * (1 - b) by S2,XREAL_1:64; then a - a * b + b <= 1 - b + b by XREAL_1:6; then a + b - a * b - a * b <= 1 - a * b by XREAL_1:9; then B9: (a + b - 2 * a * b) / (1 - a * b) <= 1 by XREAL_1:183,S5; a * b in [.0,1.] by Lemma1; then a * b <= 1 by XXREAL_1:1; then 1 - a * b >= 1 - 1 by XREAL_1:10; hence thesis by XXREAL_1:1,B9,S5; end; registration let f be BinOp of [.0,1.]; let a, b be Real; cluster f.(a,b) -> real; coherence proof per cases; suppose a in [.0,1.] & b in [.0,1.]; then f.(a,b) in [.0,1.] by BINOP_1:17; hence thesis; end; suppose not a in [.0,1.] or not b in [.0,1.]; then not [a,b] in dom f by ZFMISC_1:87; hence thesis by FUNCT_1:def 2; end; end; end; theorem NormIn01: for a,b being Real, t being BinOp of [.0,1.] holds t.(a,b) in [.0,1.] proof let a,b be Real; let t be BinOp of [.0,1.]; per cases; suppose a in [.0,1.] & b in [.0,1.]; then [a,b] in [:[.0,1.], [.0,1.]:] by ZFMISC_1:87; hence thesis by FUNCT_2:5; end; suppose not a in [.0,1.] or not b in [.0,1.]; then not [a,b] in dom t by ZFMISC_1:87; then t. [a,b] = 0 by FUNCT_1:def 2; hence thesis by XXREAL_1:1; end; end; theorem CoIn01: for f being BinOp of [.0,1.], a, b being Real holds 1 - f.(1 - a, 1 - b) in [.0,1.] proof let f be BinOp of [.0,1.]; let a,b be Real; per cases; suppose a in [.0,1.] & b in [.0,1.]; then reconsider aa = a, bb = b as Element of [.0,1.]; f.(1-aa, 1-bb) in [.0,1.] by NormIn01; hence thesis by OpIn01; end; suppose not a in [.0,1.] or not b in [.0,1.]; f.(1-a,1-b) in [.0,1.] by NormIn01; hence thesis by OpIn01; end; end; theorem MES57: ::: move theorems from MESFUNC5 to XXREAL_0 for x,y,k being Real st k <= 0 holds k*min(x,y) = max(k*x,k*y) & k*max(x,y) = min(k*x,k*y) proof let x,y,k be Real; assume A1: k <= 0; hereby per cases by XXREAL_0:16; suppose max(x,y) = x; then A2: y <= x by XXREAL_0:def 10; then max(k*x,k*y) = k*y by XXREAL_0:def 10,A1,XREAL_1:65; hence k*min(x,y) = max(k*x,k*y) by A2,XXREAL_0:def 9; end; suppose max(x,y) = y; then A3: x <= y by XXREAL_0:def 10; then max(k*x,k*y) = k*x by XXREAL_0:def 10,A1,XREAL_1:65; hence k*min(x,y) = max(k*x,k*y) by A3,XXREAL_0:def 9; end; end; per cases by XXREAL_0:15; suppose min(x,y) = x; then A4: x <= y by XXREAL_0:def 9; then min(k*x,k*y) = k*y by XXREAL_0:def 9,A1,XREAL_1:65; hence thesis by A4,XXREAL_0:def 10; end; suppose min(x,y) = y; then A5: y <= x by XXREAL_0:def 9; then min(k*y,k*x) = k*x by XXREAL_0:def 9,A1,XREAL_1:65; hence thesis by A5,XXREAL_0:def 10; end; end; begin :: Basic Example of a Triangular Norm and Conorm: min and max definition let A be real-membered set; let f be BinOp of A; attr f is monotonic means :MonDef: for a,b,c,d being Element of A st a <= c & b <= d holds f.(a,b) <= f.(c,d); attr f is with-1-identity means :IdDef: for a being Element of A holds f.(a,1) = a; attr f is with-1-annihilating means for a being Element of A holds f.(a,1) = 1; attr f is with-0-identity means :ZeroDef: for a being Element of A holds f.(a,0) = a; attr f is with-0-annihilating means for a being Element of A holds f.(a,0) = 0; end; scheme ExBinOp { A() -> non empty real-membered set, F(Real, Real) -> set } : ex f being BinOp of A() st for a,b being Element of A() holds f.(a,b) = F(a,b) provided A2: for a,b being Element of A() holds F(a,b) in A() proof set A = A(); deffunc F(Element of A, Element of A) = In (F(\$1,\$2),A); ex f being Function of [:A,A:], A st for x being Element of A for y being Element of A holds f.(x,y) = F(x,y) from BINOP_1:sch 4; then consider f being BinOp of A such that A1: for x being Element of A for y being Element of A holds f.(x,y) = F(x,y); take f; let a,b be Element of A; f.(a,b) = F(a,b) by A1; hence thesis by SUBSET_1:def 8,A2; end; definition func minnorm -> BinOp of [.0,1.] means :MinDef: for a,b being Element of [.0,1.] holds it.(a,b) = min (a,b); existence proof set A = [.0,1.]; deffunc F(Element of A, Element of A) = In (min (\$1,\$2),A); ex f being Function of [:A,A:], A st for x being Element of A for y being Element of A holds f.(x,y) = F(x,y) from BINOP_1:sch 4; then consider f being BinOp of A such that A1: for x being Element of A for y being Element of A holds f.(x,y) = F(x,y); take f; let a,b be Element of [.0,1.]; A2: f.(a,b) = F(a,b) by A1; min (a,b) = a or min (a,b) = b by XXREAL_0:15; hence thesis by A2,SUBSET_1:def 8; end; uniqueness proof let f1,f2 be BinOp of [.0,1.] such that A1: for a,b being Element of [.0,1.] holds f1.(a,b) = min (a,b) and A2: for a,b being Element of [.0,1.] holds f2.(a,b) = min (a,b); A3: dom f1 = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1 .= dom f2 by FUNCT_2:def 1; for x,y being object st [x,y] in dom f1 holds f1.(x,y) = f2.(x,y) proof let x,y be object; assume [x,y] in dom f1; then reconsider xx = x, yy = y as Element of [.0,1.] by ZFMISC_1:87; f1.(xx,yy) = min (xx,yy) by A1 .= f2.(xx,yy) by A2; hence thesis; end; hence thesis by A3,BINOP_1:20; end; end; registration cluster minnorm -> commutative associative monotonic with-1-identity; coherence proof set f = minnorm; A1: for a,b being Element of [.0,1.] holds f.(a,b) = f.(b,a) proof let a,b be Element of [.0,1.]; f.(a,b) = min(a,b) by MinDef .= f.(b,a) by MinDef; hence thesis; end; AA: for a,b,c being Element of [.0,1.] holds f.(f.(a,b),c) = f.(a,f.(b,c)) proof let a,b,c be Element of [.0,1.]; a2: min (a,b) = a or min (a,b) = b by XXREAL_0:15; a3: min (b,c) = b or min (b,c) = c by XXREAL_0:15; f.(f.(a,b),c) = f.(min(a,b),c) by MinDef .= min (min(a,b),c) by MinDef,a2 .= min (a,min(b,c)) by XXREAL_0:33 .= f.(a,min(b,c)) by a3,MinDef .= f.(a,f.(b,c)) by MinDef; hence thesis; end; D1: for a,b,c,d being Element of [.0,1.] st a <= c & b <= d holds f.(a,b) <= f.(c,d) proof let a,b,c,d be Element of [.0,1.]; assume a <= c & b <= d; then min (a,b) <= min (c,d) by XXREAL_0:18; then min (a,b) <= f.(c,d) by MinDef; hence thesis by MinDef; end; for a being Element of [.0,1.] holds f.(a,1) = a proof let a be Element of [.0,1.]; T1: 1 in [.0,1.] by XXREAL_1:1; a <= 1 by XXREAL_1:1; then min (a,1) = a by XXREAL_0:def 9; hence thesis by MinDef,T1; end; hence thesis by BINOP_1:def 2,def 3,A1,AA,D1; end; end; registration cluster commutative associative monotonic with-1-identity for BinOp of [.0,1.]; existence proof take minnorm; thus thesis; end; end; definition mode t-norm is commutative associative monotonic with-1-identity BinOp of [.0,1.]; end; definition func maxnorm -> BinOp of [.0,1.] means :MaxDef: for a,b being Element of [.0,1.] holds it.(a,b) = max (a,b); existence proof set A = [.0,1.]; deffunc F(Element of A, Element of A) = In (max (\$1,\$2),A); ex f being Function of [:A,A:], A st for x being Element of A for y being Element of A holds f.(x,y) = F(x,y) from BINOP_1:sch 4; then consider f being BinOp of A such that A1: for x being Element of A for y being Element of A holds f.(x,y) = F(x,y); take f; let a,b be Element of [.0,1.]; A2: f.(a,b) = F(a,b) by A1; max (a,b) = a or max (a,b) = b by XXREAL_0:16; hence thesis by A2,SUBSET_1:def 8; end; uniqueness proof let f1,f2 be BinOp of [.0,1.] such that A1: for a,b being Element of [.0,1.] holds f1.(a,b) = max (a,b) and A2: for a,b being Element of [.0,1.] holds f2.(a,b) = max (a,b); A3: dom f1 = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1 .= dom f2 by FUNCT_2:def 1; for x,y being object st [x,y] in dom f1 holds f1.(x,y) = f2.(x,y) proof let x,y be object; assume [x,y] in dom f1; then reconsider xx = x, yy = y as Element of [.0,1.] by ZFMISC_1:87; f1.(xx,yy) = max (xx,yy) by A1 .= f2.(xx,yy) by A2; hence thesis; end; hence thesis by A3,BINOP_1:20; end; end; registration cluster maxnorm -> commutative associative monotonic with-0-identity; coherence proof set f = maxnorm; A1: for a,b being Element of [.0,1.] holds f.(a,b) = f.(b,a) proof let a,b be Element of [.0,1.]; f.(a,b) = max (a,b) by MaxDef .= f.(b,a) by MaxDef; hence thesis; end; DD: for a,b,c being Element of [.0,1.] holds f.(f.(a,b),c) = f.(a,f.(b,c)) proof let a,b,c be Element of [.0,1.]; a2: max (a,b) = a or max (a,b) = b by XXREAL_0:16; a3: max (b,c) = b or max (b,c) = c by XXREAL_0:16; f.(f.(a,b),c) = f.(max(a,b),c) by MaxDef .= max (max(a,b),c) by MaxDef,a2 .= max (a,max(b,c)) by XXREAL_0:34 .= f.(a,max(b,c)) by a3,MaxDef .= f.(a,f.(b,c)) by MaxDef; hence thesis; end; D1: for a,b,c,d being Element of [.0,1.] st a <= c & b <= d holds f.(a,b) <= f.(c,d) proof let a,b,c,d be Element of [.0,1.]; assume a <= c & b <= d; then max (a,b) <= max (c,d) by XXREAL_0:26; then max (a,b) <= f.(c,d) by MaxDef; hence thesis by MaxDef; end; for a being Element of [.0,1.] holds f.(a,0) = a proof let a be Element of [.0,1.]; T1: 0 in [.0,1.] by XXREAL_1:1; a >= 0 by XXREAL_1:1; then max(a,0) = a by XXREAL_0:def 10; hence thesis by MaxDef,T1; end; hence thesis by BINOP_1:def 2,def 3,A1,DD,D1; end; end; registration cluster commutative associative monotonic with-0-identity for BinOp of [.0,1.]; existence proof take maxnorm; thus thesis; end; end; definition mode t-conorm is commutative associative monotonic with-0-identity BinOp of [.0,1.]; end; theorem NormIs0: for t being commutative monotonic with-1-identity BinOp of [.0,1.] holds for a being Element of [.0,1.] holds t.(a,0) = 0 proof let t be commutative monotonic with-1-identity BinOp of [.0,1.]; let a be Element of [.0,1.]; T0: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1; then T3: t.(1,0) = t.(0,1) by BINOP_1:def 2 .= 0 by T0,IdDef; for a being Element of [.0,1.] holds t.(a,0) = 0 proof let a be Element of [.0,1.]; t.(a,0) in [.0,1.] by NormIn01; then T4: 0 <= t.(a,0) by XXREAL_1:1; a <= 1 by XXREAL_1:1; hence thesis by T4,T0,MonDef,T3; end; hence thesis; end; theorem ConormIs1: for t being commutative monotonic with-0-identity BinOp of [.0,1.] holds for a being Element of [.0,1.] holds t.(a,1) = 1 proof let t be commutative monotonic with-0-identity BinOp of [.0,1.]; let a be Element of [.0,1.]; T0: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1; then T3: t.(0,1) = t.(1,0) by BINOP_1:def 2 .= 1 by T0,ZeroDef; for a being Element of [.0,1.] holds t.(a,1) = 1 proof let a be Element of [.0,1.]; t.(a,1) in [.0,1.] by NormIn01; then T4: t.(a,1) <= 1 by XXREAL_1:1; 0 <= a by XXREAL_1:1; then 1 <= t.(a,1) by T0,MonDef,T3; hence thesis by XXREAL_0:1,T4; end; hence thesis; end; registration cluster -> with-0-annihilating for commutative monotonic with-1-identity BinOp of [.0,1.]; coherence by NormIs0; cluster -> with-1-annihilating for commutative monotonic with-0-identity BinOp of [.0,1.]; coherence by ConormIs1; end; begin :: Further Examples of Triangular Norms definition func prodnorm -> BinOp of [.0,1.] means :ProdDef: for a,b being Element of [.0,1.] holds it.(a,b) = a * b; existence proof set A = [.0,1.]; deffunc F(Element of A, Element of A) = In (\$1 * \$2,A); ex f being Function of [:A,A:], A st for x being Element of A for y being Element of A holds f.(x,y) = F(x,y) from BINOP_1:sch 4; then consider f being BinOp of A such that A1: for x being Element of A for y being Element of A holds f.(x,y) = F(x,y); take f; let a,b be Element of [.0,1.]; f.(a,b) = F(a,b) by A1; hence thesis by SUBSET_1:def 8,Lemma1; end; uniqueness proof let f1,f2 be BinOp of [.0,1.] such that A1: for a,b being Element of [.0,1.] holds f1.(a,b) = a * b and A2: for a,b being Element of [.0,1.] holds f2.(a,b) = a * b; A3: dom f1 = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1 .= dom f2 by FUNCT_2:def 1; for x,y being object st [x,y] in dom f1 holds f1.(x,y) = f2.(x,y) proof let x,y be object; assume [x,y] in dom f1; then reconsider xx = x, yy = y as Element of [.0,1.] by ZFMISC_1:87; f1.(xx,yy) = xx * yy by A1 .= f2.(xx,yy) by A2; hence thesis; end; hence thesis by A3,BINOP_1:20; end; end; registration cluster prodnorm -> commutative associative monotonic with-1-identity; coherence proof set f = prodnorm; A1: for a,b being Element of [.0,1.] holds f.(a,b) = f.(b,a) proof let a,b be Element of [.0,1.]; f.(a,b) = a * b by ProdDef .= f.(b,a) by ProdDef; hence thesis; end; C1: for a,b,c being Element of [.0,1.] holds f.(f.(a,b),c) = f.(a,f.(b,c)) proof let a,b,c be Element of [.0,1.]; A2: a * b in [.0,1.] by Lemma1; A3: b * c in [.0,1.] by Lemma1; f.(f.(a,b),c) = f.(a * b,c) by ProdDef .= (a * b) * c by ProdDef,A2 .= a * (b * c) .= f.(a,b * c) by A3,ProdDef .= f.(a,f.(b,c)) by ProdDef; hence thesis; end; D1: for a,b,c,d being Element of [.0,1.] st a <= c & b <= d holds f.(a,b) <= f.(c,d) proof let a,b,c,d be Element of [.0,1.]; B1: 0 <= a & 0 <= b by XXREAL_1:1; assume a <= c & b <= d; then a * b <= c * d by B1,XREAL_1:66; then a * b <= f.(c,d) by ProdDef; hence thesis by ProdDef; end; T1: 1 in [.0,1.] by XXREAL_1:1; for a being Element of [.0,1.] holds f.(a,1) = a proof let a be Element of [.0,1.]; a * 1 = a; hence thesis by ProdDef,T1; end; hence thesis by BINOP_1:def 2,def 3,A1,C1,D1; end; end; definition func probsum_conorm -> BinOp of [.0,1.] means :ProbSumDef: for a,b being Element of [.0,1.] holds it.(a,b) = a + b - a * b; existence proof set A = [.0,1.]; deffunc F(Element of A, Element of A) = In (\$1 + \$2 - \$1 * \$2,A); ex f being Function of [:A,A:], A st for x being Element of A for y being Element of A holds f.(x,y) = F(x,y) from BINOP_1:sch 4; then consider f being BinOp of A such that A1: for x being Element of A for y being Element of A holds f.(x,y) = F(x,y); take f; let a,b be Element of [.0,1.]; f.(a,b) = F(a,b) by A1; hence thesis by SUBSET_1:def 8,abMinab01; end; uniqueness proof let f1,f2 be BinOp of [.0,1.] such that A1: for a,b being Element of [.0,1.] holds f1.(a,b) = a + b - a * b and A2: for a,b being Element of [.0,1.] holds f2.(a,b) = a + b - a * b; A3: dom f1 = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1 .= dom f2 by FUNCT_2:def 1; for x,y being object st [x,y] in dom f1 holds f1.(x,y) = f2.(x,y) proof let x,y be object; assume [x,y] in dom f1; then reconsider xx = x, yy = y as Element of [.0,1.] by ZFMISC_1:87; f1.(xx,yy) = xx + yy - xx * yy by A1 .= f2.(xx,yy) by A2; hence thesis; end; hence thesis by A3,BINOP_1:20; end; end; definition func Lukasiewicz_norm -> BinOp of [.0,1.] means :LukNorm: for a,b being Element of [.0,1.] holds it.(a,b) = max (0, a + b - 1); existence proof set A = [.0,1.]; deffunc F(Element of A, Element of A) = In (max (0, \$1 + \$2 - 1),A); ex f being Function of [:A,A:], A st for x being Element of A for y being Element of A holds f.(x,y) = F(x,y) from BINOP_1:sch 4; then consider f being BinOp of A such that A1: for x being Element of A for y being Element of A holds f.(x,y) = F(x,y); take f; let a,b be Element of [.0,1.]; reconsider aa = a, bb = b as Element of A; f.(a,b) = F(aa,bb) by A1; hence thesis by SUBSET_1:def 8,Lemma2; end; uniqueness proof let f1,f2 be BinOp of [.0,1.] such that A1: for a,b being Element of [.0,1.] holds f1.(a,b) = max (0, a + b - 1) and A2: for a,b being Element of [.0,1.] holds f2.(a,b) = max (0, a + b - 1); A3: dom f1 = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1 .= dom f2 by FUNCT_2:def 1; for x,y being object st [x,y] in dom f1 holds f1.(x,y) = f2.(x,y) proof let x,y be object; assume [x,y] in dom f1; then reconsider xx = x, yy = y as Element of [.0,1.] by ZFMISC_1:87; f1.(xx,yy) = max (0, xx + yy - 1) by A1 .= f2.(xx,yy) by A2; hence thesis; end; hence thesis by A3,BINOP_1:20; end; end; registration cluster Lukasiewicz_norm -> commutative associative monotonic with-1-identity; coherence proof set f = Lukasiewicz_norm; A1: for a,b being Element of [.0,1.] holds f.(a,b) = f.(b,a) proof let a,b be Element of [.0,1.]; f.(a,b) = max (0, a + b - 1) by LukNorm .= f.(b,a) by LukNorm; hence thesis; end; C1: for a,b,c being Element of [.0,1.] holds f.(f.(a,b),c) = f.(a,f.(b,c)) proof let a,b,c be Element of [.0,1.]; set B = max(0,a + b - 1); set C = max(0,b + c - 1); G1: B in [.0,1.] by Lemma2; G2: C in [.0,1.] by Lemma2; f.(f.(a,b),c) = f.(B,c) by LukNorm .= max (0,B+c-1) by LukNorm,G1 .= max (0,a+C-1) by Lemma3 .= f.(a,C) by LukNorm,G2 .= f.(a,f.(b,c)) by LukNorm; hence thesis; end; D1: for a,b,c,d being Element of [.0,1.] st a <= c & b <= d holds f.(a,b) <= f.(c,d) proof let a,b,c,d be Element of [.0,1.]; assume a <= c & b <= d; then a + b <= c + d by XREAL_1:7; then a + b - 1 <= c + d - 1 by XREAL_1:9; then max (0, a + b - 1) <= max (0, c + d - 1) by XXREAL_0:26; then max (0, a + b - 1) <= f.(c,d) by LukNorm; hence thesis by LukNorm; end; for a being Element of [.0,1.] holds f.(a,1) = a proof let a be Element of [.0,1.]; T1: 1 in [.0,1.] by XXREAL_1:1; T2: 0 <= a by XXREAL_1:1; f.(a,1) = max (0,a+1-1) by LukNorm,T1 .= a by T2,XXREAL_0:def 10; hence thesis; end; hence thesis by BINOP_1:def 2,def 3,A1,C1,D1; end; end; definition func drastic_norm -> BinOp of [.0,1.] means :Drastic2Def: for a,b being Element of [.0,1.] holds (max (a,b) = 1 implies it.(a,b) = min (a,b)) & (max (a,b) <> 1 implies it.(a,b) = 0); existence proof set C = [.0,1.]; defpred P[set,set] means \$1 = 1 or \$2 = 1; deffunc F(Element of C,Element of C) = In(min (\$1,\$2),C); deffunc G(Element of C,Element of C) = In(0,C); ex f being Function of [:C,C:],C st for c be Element of C, d be Element of C st [c,d] in dom f holds (P[c,d] implies f. [c,d] = F(c,d)) & (not P [c,d] implies f. [c,d] = G(c,d)) from SCHEME1:sch 21; then consider f being Function of [:C,C:],C such that A1: for c be Element of C, d be Element of C st [c,d] in dom f holds (P[c,d] implies f. [c,d] = F(c,d)) & (not P [c,d] implies f. [c,d] = G(c,d)); take f; A0: dom f = [:C,C:] by FUNCT_2:def 1; let a,b be Element of C; cc: min (a,b) = a or min (a,b) = b by XXREAL_0:15; AA: [a,b] in dom f by A0,ZFMISC_1:87; (max (a,b) = 1 implies f.(a,b) = min (a,b)) & (max (a,b) <> 1 implies f.(a,b) = 0) proof thus max (a,b) = 1 implies f.(a,b) = min (a,b) proof assume max (a,b) = 1; then a = 1 or b = 1 by XXREAL_0:16; then f. [a,b] = F(a,b) by A1,AA .= min (a,b) by SUBSET_1:def 8,cc; hence thesis; end; assume B0: max (a,b) <> 1; a <> 1 & b <> 1 proof assume a = 1 or b = 1; then per cases; suppose Z1: a = 1; then b <= a by XXREAL_1:1; hence thesis by B0,XXREAL_0:def 10,Z1; end; suppose Z1: b = 1; then a <= b by XXREAL_1:1; hence thesis by B0,XXREAL_0:def 10,Z1; end; end; then f. [a,b] = G(a,b) by A1,AA .= 0 by XXREAL_1:1,SUBSET_1:def 8; hence thesis; end; hence thesis; end; uniqueness proof let f1,f2 be BinOp of [.0,1.] such that A1: for a,b being Element of [.0,1.] holds (max (a,b) = 1 implies f1.(a,b) = min (a,b)) & (max (a,b) <> 1 implies f1.(a,b) = 0) and A2: for a,b being Element of [.0,1.] holds (max (a,b) = 1 implies f2.(a,b) = min (a,b)) & (max (a,b) <> 1 implies f2.(a,b) = 0); for a,b being set st a in [.0,1.] & b in [.0,1.] holds f1.(a,b) = f2.(a,b) proof let a,b be set; assume a in [.0,1.] & b in [.0,1.]; then reconsider aa = a, bb = b as Element of [.0,1.]; per cases; suppose B0: max (aa,bb) = 1; then f1.(aa,bb) = min (aa,bb) by A1 .= f2.(aa,bb) by A2,B0; hence thesis; end; suppose B1: max (aa,bb) <> 1; then f1.(aa,bb) = 0 by A1 .= f2.(aa,bb) by A2,B1; hence thesis; end; end; hence thesis by BINOP_1:def 21; end; end; theorem DrasticDef: for a,b being Element of [.0,1.] holds (a = 1 implies drastic_norm.(a,b) = b) & (b = 1 implies drastic_norm.(a,b) = a) & (a <> 1 & b <> 1 implies drastic_norm.(a,b) = 0) proof let a,b be Element of [.0,1.]; A1: b <= 1 & a <= 1 by XXREAL_1:1; thus a = 1 implies drastic_norm.(a,b) = b proof assume B1: a = 1; then max (a,b) = 1 by A1,XXREAL_0:def 10; then drastic_norm.(a,b) = min (a,b) by Drastic2Def .= b by XXREAL_0:def 9,A1,B1; hence thesis; end; thus b = 1 implies drastic_norm.(a,b) = a proof assume B1: b = 1; then max (a,b) = 1 by A1,XXREAL_0:def 10; then drastic_norm.(a,b) = min (a,b) by Drastic2Def .= a by XXREAL_0:def 9,A1,B1; hence thesis; end; assume a <> 1 & b <> 1; then max (a,b) <> 1 by XXREAL_0:16; hence thesis by Drastic2Def; end; registration cluster drastic_norm -> commutative associative with-1-identity monotonic; coherence proof set f = drastic_norm; FF: for a,b being Element of [.0,1.] holds f.(a,b) = f.(b,a) proof let a,b be Element of [.0,1.]; per cases; suppose A1: a = 1; then f.(a,b) = b by DrasticDef; hence thesis by A1,DrasticDef; end; suppose A1: b = 1; then f.(b,a) = a by DrasticDef; hence thesis by A1,DrasticDef; end; suppose a <> 1 & b <> 1; then f.(a,b) = 0 & f.(b,a) = 0 by DrasticDef; hence thesis; end; end; TT: for a being Element of [.0,1.] holds f.(a,1) = a proof let a be Element of [.0,1.]; 1 in [.0,1.] by XXREAL_1:1; hence thesis by DrasticDef; end; D1: for a,b,c,d being Element of [.0,1.] st a <= c & b <= d holds f.(a,b) <= f.(c,d) proof let a,b,c,d be Element of [.0,1.]; B2: f.(c,d) >= 0 by XXREAL_1:1; assume S1: a <= c & b <= d; per cases; suppose S0: a = 1; c <= 1 by XXREAL_1:1; then f.(c,d) = d by DrasticDef,S0,S1,XXREAL_0:1; hence thesis by S1,DrasticDef,S0; end; suppose S0: b = 1; d <= 1 by XXREAL_1:1; then f.(c,d) = c by DrasticDef,S0,S1,XXREAL_0:1; hence thesis by S1,DrasticDef,S0; end; suppose b <> 1 & a <> 1; hence thesis by B2,DrasticDef; end; end; H1: 0 in [.0,1.] by XXREAL_1:1; BU: for a being Element of [.0,1.] holds f.(a,0) = 0 proof let a be Element of [.0,1.]; H2: 0 <= a by XXREAL_1:1; per cases; suppose max (a,0) = 1; then f.(a,0) = min (a,0) by Drastic2Def,H1 .= 0 by H2,XXREAL_0:def 9; hence thesis; end; suppose max (a,0) <> 1; hence thesis by Drastic2Def,H1; end; end; for a,b,c being Element of [.0,1.] holds f.(a,f.(b,c)) = f.(f.(a,b),c) proof let a,b,c be Element of [.0,1.]; Z4: min(a,b) in [.0,1.] by MinIn01; EE: min(b,c) in [.0,1.] by MinIn01; per cases; suppose Z1: max (a,b) = 1 & max (b,c) = 1; then K1: a = 1 or b = 1 by XXREAL_0:16; max (a,c) in [.0,1.] by MaxIn01; then U2: max (a,c) <= 1 by XXREAL_1:1; Z2: f.(b,c) = min (b,c) by Drastic2Def,Z1; UU: max (a,min(b,c)) = min (max(a,b),max(a,c)) by XXREAL_0:39 .= max (a,c) by U2,XXREAL_0:def 9,Z1; per cases; suppose HU: max (a,c) = 1; U2: max (min(a,b),c) = min (max(a,c),max(b,c)) by XXREAL_0:39 .= 1 by Z1,HU; f.(a,f.(b,c)) = f.(a,min(b,c)) by Drastic2Def,Z1 .= min (a,min(b,c)) by Drastic2Def,HU,UU,EE .= min (min(a,b),c) by XXREAL_0:33 .= f.(min(a,b),c) by U2,Drastic2Def,Z4 .= f.(f.(a,b),c) by Drastic2Def,Z1; hence thesis; end; suppose HU: max (a,c) <> 1; then a <= b by XXREAL_1:1,K1,DiffMax; then K3: min (a,b) = a by XXREAL_0:def 9; U1: f.(a,b) = min (a,b) by Drastic2Def,Z1; f.(a,f.(b,c)) = 0 by Drastic2Def,HU,UU,Z2 .= f.(f.(a,b),c) by U1,K3,HU,Drastic2Def; hence thesis; end; end; suppose Z1: max (a,b) = 1 & max (b,c) <> 1; then z1: a = 1 or b = 1 by XXREAL_0:16; max (b,c) in [.0,1.] by MaxIn01; then W1: max (b,c) <= 1 by XXREAL_1:1; za: b <> 1 proof assume b = 1; then max (b,c) >= 1 by XXREAL_0:25; hence thesis by Z1,XXREAL_0:1,W1; end; c <= 1 by XXREAL_1:1; then z3: max (a,c) = 1 by z1,za,XXREAL_0:def 10; qq: max (min(a,b),c) = min (max(a,c),max(b,c)) by XXREAL_0:39 .= max (b,c) by W1,z3,XXREAL_0:def 9; f.(b,c) = 0 by Drastic2Def,Z1; then f.(a,f.(b,c)) = 0 by BU .= f.(min(a,b),c) by qq,Z1,Drastic2Def,Z4 .= f.(f.(a,b),c) by Drastic2Def,Z1; hence thesis; end; suppose Z1: max (a,b) <> 1 & max (b,c) = 1; then z1: c = 1 or b = 1 by XXREAL_0:16; max (a,b) in [.0,1.] by MaxIn01; then w1: max (a,b) <= 1 by XXREAL_1:1; zz: b <> 1 proof assume b = 1; then max (a,b) >= 1 by XXREAL_0:25; hence thesis by Z1,w1,XXREAL_0:1; end; Z2: f.(b,c) = min (b,c) by Drastic2Def,Z1; Y1: f.(a,b) = 0 by Drastic2Def,Z1; b <= c by XXREAL_1:1,zz,z1; then f.(b,c) = b by Z2,XXREAL_0:def 9; then f.(a,f.(b,c)) = 0 by Drastic2Def,Z1 .= f.(c,0) by BU .= f.(f.(a,b),c) by Y1,FF; hence thesis; end; suppose Z1: max (a,b) <> 1 & max (b,c) <> 1; then Z2: f.(b,c) = 0 by Drastic2Def; Z3: f.(a,b) = 0 by Drastic2Def,Z1; f.(a,f.(b,c)) = 0 by BU,Z2 .= f.(c,0) by BU .= f.(f.(a,b),c) by Z3,FF; hence thesis; end; end; hence thesis by FF,TT,D1,BINOP_1:def 3,def 2; end; end; definition func nilmin_norm -> BinOp of [.0,1.] means :NilminDef: for a,b being Element of [.0,1.] holds (a + b > 1 implies it.(a,b) = min (a,b)) & (a + b <= 1 implies it.(a,b) = 0); existence proof set C = [.0,1.]; defpred P[Real,Real] means \$1 + \$2 > 1; deffunc F(Element of C,Element of C) = In(min (\$1,\$2),C); deffunc G(Element of C,Element of C) = In(0,C); ex f being Function of [:C,C:],C st for c be Element of C, d be Element of C st [c,d] in dom f holds (P[c,d] implies f. [c,d] = F(c,d)) & (not P [c,d] implies f. [c,d] = G(c,d)) from SCHEME1:sch 21; then consider f being Function of [:C,C:],C such that A1: for c be Element of C, d be Element of C st [c,d] in dom f holds (P[c,d] implies f. [c,d] = F(c,d)) & (not P [c,d] implies f. [c,d] = G(c,d)); take f; A0: dom f = [:C,C:] by FUNCT_2:def 1; let a,b be Element of C; cc: min (a,b) = a or min (a,b) = b by XXREAL_0:15; AA: [a,b] in dom f by A0,ZFMISC_1:87; (a + b > 1 implies f.(a,b) = min (a,b)) & (a + b <= 1 implies f.(a,b) = 0) proof thus a + b > 1 implies f.(a,b) = min (a,b) proof assume a + b > 1; then f. [a,b] = F(a,b) by A1,AA .= min (a,b) by SUBSET_1:def 8,cc; hence thesis; end; assume a + b <= 1; then f. [a,b] = G(a,b) by A1,AA .= 0 by XXREAL_1:1,SUBSET_1:def 8; hence thesis; end; hence thesis; end; uniqueness proof let f1,f2 be BinOp of [.0,1.] such that A1: for a,b being Element of [.0,1.] holds (a + b > 1 implies f1.(a,b) = min (a,b)) & (a + b <= 1 implies f1.(a,b) = 0) and A2: for a,b being Element of [.0,1.] holds (a + b > 1 implies f2.(a,b) = min (a,b)) & (a + b <= 1 implies f2.(a,b) = 0); for a,b being set st a in [.0,1.] & b in [.0,1.] holds f1.(a,b) = f2.(a,b) proof let a,b be set; assume a in [.0,1.] & b in [.0,1.]; then reconsider aa = a, bb = b as Element of [.0,1.]; per cases; suppose B0: aa + bb > 1; then f1.(aa,bb) = min (aa,bb) by A1 .= f2.(aa,bb) by A2,B0; hence thesis; end; suppose B1: aa + bb <= 1; then f1.(aa,bb) = 0 by A1 .= f2.(aa,bb) by A2,B1; hence thesis; end; end; hence thesis by BINOP_1:def 21; end; end; registration cluster nilmin_norm -> commutative associative with-1-identity monotonic; coherence proof set f = nilmin_norm; FF: for a,b being Element of [.0,1.] holds f.(a,b) = f.(b,a) proof let a,b be Element of [.0,1.]; per cases; suppose A1: a + b > 1; hence f.(a,b) = min (a,b) by NilminDef .= f.(b,a) by NilminDef,A1; end; suppose a + b <= 1; then f.(a,b) = 0 & f.(b,a) = 0 by NilminDef; hence thesis; end; end; U1: 1 in [.0,1.] by XXREAL_1:1; TT: for a being Element of [.0,1.] holds f.(a,1) = a proof let a be Element of [.0,1.]; U4: 0 <= a <= 1 by XXREAL_1:1; per cases; suppose a + 1 > 1; then f.(a,1) = min (a,1) by NilminDef,U1 .= a by U4,XXREAL_0:def 9; hence thesis; end; suppose U2: a + 1 <= 1; then a <= 1 - 1 by XREAL_1:19; then a = 0 by XXREAL_1:1; hence thesis by NilminDef,U2,U1; end; end; D1: for a,b,c,d being Element of [.0,1.] st a <= c & b <= d holds f.(a,b) <= f.(c,d) proof let a,b,c,d be Element of [.0,1.]; assume S1: a <= c & b <= d; per cases; suppose S0: a + b > 1; then Sa: f.(a,b) = min (a,b) by NilminDef; a + b <= c + d by S1,XREAL_1:7; then c + d > 1 by S0,XXREAL_0:2; then f.(c,d) = min (c,d) by NilminDef; hence thesis by S1,Sa,XXREAL_0:18; end; suppose a + b <= 1; then f.(a,b) = 0 by NilminDef; hence thesis by XXREAL_1:1; end; end; H1: 0 in [.0,1.] by XXREAL_1:1; BU: for a being Element of [.0,1.] holds f.(a,0) = 0 proof let a be Element of [.0,1.]; per cases; suppose a + 0 > 1; hence thesis by XXREAL_1:1; end; suppose a + 0 <= 1; hence thesis by NilminDef,H1; end; end; for a,b,c being Element of [.0,1.] holds f.(a,f.(b,c)) = f.(f.(a,b),c) proof let a,b,c be Element of [.0,1.]; EE: min (b,c) in [.0,1.] by MinIn01; U3: min (a,b) in [.0,1.] by MinIn01; per cases; suppose Z1: a + b > 1 & b + c > 1; then Z2: f.(b,c) = min (b,c) by NilminDef; per cases; suppose HU: a + c > 1; then W6: a + min (b,c) > 1 by Z1,XXREAL_0:15; W7: c + min(a,b) > 1 by HU,Z1,XXREAL_0:15; f.(a,f.(b,c)) = f.(a,min(b,c)) by Z1,NilminDef .= min (a,min(b,c)) by NilminDef,EE,W6 .= min (min(a,b),c) by XXREAL_0:33 .= f.(min(a,b),c) by NilminDef,U3,W7 .= f.(f.(a,b),c) by NilminDef,Z1; hence thesis; end; suppose HU: a + c <= 1; a + min (b,c) <= a + c by XREAL_1:6,XXREAL_0:17; then W1: a + min (b,c) <= 1 by HU,XXREAL_0:2; c + min (a,b) <= a + c by XREAL_1:6,XXREAL_0:17; then W2: c + min (a,b) <= 1 by HU,XXREAL_0:2; U1: f.(a,b) = min (a,b) by NilminDef,Z1; f.(a,f.(b,c)) = 0 by W1,NilminDef,Z2 .= f.(f.(a,b),c) by U1,W2,NilminDef; hence thesis; end; end; suppose Z1: a + b > 1 & b + c <= 1; then Z2: f.(a,b) = min (a,b) by NilminDef; per cases; suppose a + c <= 1; then G2: min (a,b) + c <= 1 by Z1,XXREAL_0:15; f.(b,c) = 0 by NilminDef,Z1; then f.(a,f.(b,c)) = 0 by BU .= f.(f.(a,b),c) by Z2,NilminDef,G2; hence thesis; end; suppose hh: a + c > 1; g4: min (a,b) + c = min (a+c, b+c) by FUZZY_2:42 .= b + c by XXREAL_0:def 9,hh,XXREAL_0:2,Z1; f.(b,c) = 0 by NilminDef,Z1; hence thesis by Z2,g4,BU; end; end; suppose Z1: a + b <= 1 & b + c > 1; then Z2: f.(b,c) = min (b,c) by NilminDef; ZZ: f.(a,b) = 0 by NilminDef,Z1; per cases; suppose a + c <= 1; then G2: min (b,c) + a <= 1 by Z1,XXREAL_0:15; f.(f.(a,b),c) = f.(0,c) by Z1,NilminDef .= f.(c,0) by FF,H1 .= 0 by BU .= f.(a,f.(b,c)) by Z2,NilminDef,G2; hence thesis; end; suppose g5: a + c > 1; g4: min (c,b) + a = min (c+a, b+a) by FUZZY_2:42 .= a + b by XXREAL_0:def 9,g5,XXREAL_0:2,Z1; f.(a,f.(b,c)) = f.(a,min(b,c)) by NilminDef,Z1 .= 0 by NilminDef,g4,Z1 .= f.(c,0) by BU .= f.(f.(a,b),c) by ZZ,FF; hence thesis; end; end; suppose Z1: a + b <= 1 & b + c <= 1; then Z2: f.(b,c) = 0 by NilminDef; Z3: f.(a,b) = 0 by NilminDef,Z1; f.(a,f.(b,c)) = 0 by BU,Z2 .= f.(c,0) by BU .= f.(f.(a,b),c) by Z3,FF; hence thesis; end; end; hence thesis by FF,TT,D1,BINOP_1:def 3,def 2; end; end; definition func Hamacher_norm -> BinOp of [.0,1.] means :HamDef: for a,b being Element of [.0,1.] holds it.(a,b) = (a * b) / (a + b - a * b); existence proof set A = [.0,1.]; deffunc F(Element of A,Element of A) = In((\$1 * \$2) / (\$1 + \$2 - \$1 * \$2),A); ex f being Function of [:A,A:], A st for x being Element of A for y being Element of A holds f.(x,y) = F(x,y) from BINOP_1:sch 4; then consider f being BinOp of A such that A1: for x being Element of A for y being Element of A holds f.(x,y) = F(x,y); reconsider ff = f as BinOp of [.0,1.]; take ff; let a,b be Element of [.0,1.]; reconsider aa = a, bb = b as Element of A; ff.(a,b) = F(aa,bb) by A1; hence thesis by SUBSET_1:def 8,HamIn01; end; uniqueness proof let f1,f2 be BinOp of [.0,1.] such that A1: for a,b being Element of [.0,1.] holds f1.(a,b) = (a * b) / (a + b - a * b) and A2: for a,b being Element of [.0,1.] holds f2.(a,b) = (a * b) / (a + b - a * b); for a,b being set st a in [.0,1.] & b in [.0,1.] holds f1.(a,b) = f2.(a,b) proof let a,b be set; assume a in [.0,1.] & b in [.0,1.]; then reconsider aa = a, bb = b as Element of [.0,1.]; f1.(aa,bb) = (aa * bb) / (aa + bb - aa * bb) by A1 .= f2.(aa,bb) by A2; hence thesis; end; hence thesis by BINOP_1:def 21; end; end; registration cluster Hamacher_norm -> commutative associative with-1-identity monotonic; coherence proof set f = Hamacher_norm; FF: for a,b being Element of [.0,1.] holds f.(a,b) = f.(b,a) proof let a,b be Element of [.0,1.]; f.(a,b) = (a * b) / (a + b - a * b) by HamDef .= f.(b,a) by HamDef; hence thesis; end; TT: for a being Element of [.0,1.] holds f.(a,1) = a proof let a be Element of [.0,1.]; 1 in [.0,1.] by XXREAL_1:1; then f.(a,1) = (a * 1) / (a + 1 - a * 1) by HamDef; hence thesis; end; D1: for a,b,c,d being Element of [.0,1.] st a <= c & b <= d holds f.(a,b) <= f.(c,d) proof let a,b,c,d be Element of [.0,1.]; JJ: 0 <= a & 0 <= b & 0 <= c & 0 <= d by XXREAL_1:1; B2: f.(c,d) >= 0 by XXREAL_1:1; assume S1: a <= c & b <= d; D1: f.(a,b) = (a * b) / (a + b - a * b) by HamDef; D2: f.(c,d) = (c * d) / (c + d - c * d) by HamDef; d2: f.(a,d) = (a * d) / (a + d - a * d) by HamDef; set A = a + b - a * b, B = c + d - c * d; per cases; suppose A = 0; hence thesis by B2,XCMPLX_1:49,D1; end; suppose DD: B = 0; reconsider ad = a + d - a * d, ab = a + b - a * b as Element of [.0,1.] by abMinab01; reconsider B as Element of [.0,1.] by abMinab01; 1 - a in [.0,1.] by OpIn01; then 1 - a >= 0 by XXREAL_1:1; then b * (1 - a) <= d * (1 - a) by S1,XREAL_1:64; then w0: b * (1 - a) + a <= d * (1 - a) + a by XREAL_1:6; 1 - d in [.0,1.] by OpIn01; then 1 - d >= 0 by XXREAL_1:1; then a * (1 - d) <= c * (1 - d) by S1,XREAL_1:64; then WC: a * (1 - d) + d <= c * (1 - d) + d by XREAL_1:6; then de: ab = 0 by XXREAL_1:1,DD,w0; dg: ad >= 0 by XXREAL_1:1; hf: ad = 0 by DD,WC,XXREAL_1:1; df: f.(a,d) - f.(a,b) = (a * d) / ad - 0 by XCMPLX_1:49,de,D1,d2 .= (a * d) / ad; WA: f.(a,b) <= f.(a,d) - 0 by XREAL_1:11,df,dg,JJ; f.(c,d) - f.(a,d) = (c * d) / B - 0 by XCMPLX_1:49,hf,d2,D2 .= 0 by XCMPLX_1:49,DD; hence thesis by WA; end; suppose A <> 0 & B <> 0; then D8: f.(c,d) - f.(a,b) = (A * (c * d) - B * (a * b)) / (A * B) by XCMPLX_1:130,D1,D2 .= ((a * c) * (d - b) + (b * d) * (c - a)) / (A * B); A in [.0,1.] & B in [.0,1.] by abMinab01; then d6: A >= 0 & B >= 0 by XXREAL_1:1; b <= d - 0 by S1; then D3: d - b >= 0 by XREAL_1:11; a <= c - 0 by S1; then c - a >= 0 by XREAL_1:11; then f.(c,d) - f.(a,b) + f.(a,b) >= 0 + f.(a,b) by XREAL_1:6,d6,D8,JJ,D3; hence thesis; end; end; H1: 0 in [.0,1.] by XXREAL_1:1; BU: for a being Element of [.0,1.] holds f.(a,0) = 0 proof let a be Element of [.0,1.]; f.(a,0) = (a * 0) / (a + 0 - a * 0) by HamDef,H1; hence thesis; end; for a,b,c being Element of [.0,1.] holds f.(a,f.(b,c)) = f.(f.(a,b),c) proof let a,b,c be Element of [.0,1.]; J1: f.(a,b) = (a * b) / (a + b - a * b) by HamDef; J2: f.(b,c) = (b * c) / (b + c - b * c) by HamDef; reconsider bc = (b * c) / (b + c - b * c) as Element of [.0,1.] by HamIn01; set ab = (a * b) / (a + b - a * b); set bb = b + c - b * c; set AB = a + b - a * b; per cases; suppose Z1: a <> 0 & b <> 0 & c <> 0; then P1: a * b <> 0 by XCMPLX_1:6; j3: ab in [.0,1.] by HamIn01; per cases; suppose ab = 0; then AB = 0 by XCMPLX_1:50,P1; hence thesis by Z1,Lemacik; end; suppose T1: bc = 0; b * c <> 0 by Z1,XCMPLX_1:6; then b + c - b * c = 0 by T1,XCMPLX_1:50; hence thesis by Z1,Lemacik; end; suppose ab <> 0 & bc <> 0; then f1: AB <> 0 & bb <> 0 by XCMPLX_1:49; WA: (a * bc) * (ab + c - ab * c) = ((a * (b * c)) / bb) * (c + (((a * b) / AB) - ((a * b) / AB) * c)) by XCMPLX_1:74 .= ((a * (b * c)) / bb) * (c * AB / AB + ((a * b) / AB) * (1 - c)) by XCMPLX_1:89,f1 .= ((a * (b * c)) / bb) * (c * AB / AB + (((a * b) * (1-c)) / AB)) by XCMPLX_1:74 .= ((a * (b * c)) / bb) * ((c * AB + ((a * b) * (1-c))) / AB) by XCMPLX_1:62 .= ((a * (b * c)) * ((c * AB + ((a * b) * (1-c))))) / (AB * bb) by XCMPLX_1:76 .= ((a*b*c)/AB) * (((a * bb) + ((b*c)*(1-a)))/bb) by XCMPLX_1:76 .= ((a*b*c)/AB) * (a * bb / bb+ (((b*c)*(1-a))/bb)) by XCMPLX_1:62 .= ((a*b*c)/AB) * (a * bb / bb + ((b*c)/bb) * (1 - a)) by XCMPLX_1:74 .= (((a*b)/AB) * c) * (a * bb / bb + ((b*c)/bb) * (1 - a)) by XCMPLX_1:74 .= (((a*b)/AB) * c) * (a + ((b*c)/bb) * (1 - a)) by XCMPLX_1:89,f1 .= (ab * c) * (a + bc - a * bc); per cases; suppose that f2: a + bc - a * bc <> 0 and f3: ab + c - ab * c <> 0; f.(a,f.(b,c)) = (a * bc) / (a + bc - a * bc) by HamDef,J2 .= (ab * c) / (ab + c - ab * c) by WA,XCMPLX_1:94,f2,f3 .= f.(f.(a,b),c) by J1,HamDef; hence thesis; end; suppose a + bc - a * bc = 0; hence thesis by Z1,Lemacik; end; suppose ab + c - ab * c = 0; hence thesis by Z1,Lemacik,j3; end; end; end; suppose Z1: a <> 0 & b <> 0 & c = 0; then f.(a,f.(b,c)) = f.(a,0) by BU .= 0 by BU .= f.(f.(a,b),c) by BU,Z1; hence thesis; end; suppose Z1: a = 0 & b <> 0; f.(a,f.(b,c)) = f.(f.(b,c),a) by FF .= 0 by BU,Z1 .= f.(c,0) by BU .= f.(0,c) by FF,H1 .= f.(f.(b,a),c) by BU,Z1 .= f.(f.(a,b),c) by FF; hence thesis; end; suppose Z1: a <> 0 & b = 0; then z1: f.(a,b) = 0 by BU; f.(b,c) = f.(c,b) by FF .= 0 by Z1,BU; then f.(a,f.(b,c)) = 0 by BU .= f.(c,0) by BU .= f.(f.(a,b),c) by FF,z1; hence thesis; end; suppose Z1: a = 0 & b = 0; then Z2: f.(a,b) = (0 * 0) / (0 + 0 - 0 * 0) by HamDef .= 0; f.(b,c) = (b * c) / (b + c - b * c) by HamDef; hence thesis by Z2,Z1; end; end; hence thesis by FF,TT,D1,BINOP_1:def 3,def 2; end; end; begin :: Basic Triangular Conorms definition func drastic_conorm -> BinOp of [.0,1.] means :Drastic2CDef: for a,b being Element of [.0,1.] holds (min (a,b) = 0 implies it.(a,b) = max (a,b)) & (min (a,b) <> 0 implies it.(a,b) = 1); existence proof set C = [.0,1.]; defpred P[set,set] means \$1 = 0 or \$2 = 0; deffunc F(Element of C,Element of C) = In(max (\$1,\$2),C); deffunc G(Element of C,Element of C) = In(1,C); ex f being Function of [:C,C:],C st for c be Element of C, d be Element of C st [c,d] in dom f holds (P[c,d] implies f. [c,d] = F(c,d)) & (not P [c,d] implies f. [c,d] = G(c,d)) from SCHEME1:sch 21; then consider f being Function of [:C,C:],C such that A1: for c be Element of C, d be Element of C st [c,d] in dom f holds (P[c,d] implies f. [c,d] = F(c,d)) & (not P [c,d] implies f. [c,d] = G(c,d)); take f; A0: dom f = [:C,C:] by FUNCT_2:def 1; let a,b be Element of C; cc: max (a,b) = a or max (a,b) = b by XXREAL_0:16; AA: [a,b] in dom f by A0,ZFMISC_1:87; (min (a,b) = 0 implies f.(a,b) = max (a,b)) & (min (a,b) <> 0 implies f.(a,b) = 1) proof thus min (a,b) = 0 implies f.(a,b) = max (a,b) proof assume min (a,b) = 0; then a = 0 or b = 0 by XXREAL_0:15; then f. [a,b] = F(a,b) by A1,AA .= max (a,b) by SUBSET_1:def 8,cc; hence thesis; end; assume B0: min (a,b) <> 0; a <> 0 & b <> 0 proof assume a = 0 or b = 0; then per cases; suppose Z1: a = 0; then b >= a by XXREAL_1:1; hence thesis by B0,XXREAL_0:def 9,Z1; end; suppose Z1: b = 0; then a >= b by XXREAL_1:1; hence thesis by B0,XXREAL_0:def 9,Z1; end; end; then f. [a,b] = G(a,b) by A1,AA .= 1 by XXREAL_1:1,SUBSET_1:def 8; hence thesis; end; hence thesis; end; uniqueness proof let f1,f2 be BinOp of [.0,1.] such that A1: for a,b being Element of [.0,1.] holds (min (a,b) = 0 implies f1.(a,b) = max (a,b)) & (min (a,b) <> 0 implies f1.(a,b) = 1) and A2: for a,b being Element of [.0,1.] holds (min (a,b) = 0 implies f2.(a,b) = max (a,b)) & (min (a,b) <> 0 implies f2.(a,b) = 1); for a,b being set st a in [.0,1.] & b in [.0,1.] holds f1.(a,b) = f2.(a,b) proof let a,b be set; assume a in [.0,1.] & b in [.0,1.]; then reconsider aa = a, bb = b as Element of [.0,1.]; per cases; suppose B0: min (aa,bb) = 0; then f1.(aa,bb) = max (aa,bb) by A1 .= f2.(aa,bb) by A2,B0; hence thesis; end; suppose B1: min (aa,bb) <> 0; then f1.(aa,bb) = 1 by A1 .= f2.(aa,bb) by A2,B1; hence thesis; end; end; hence thesis by BINOP_1:def 21; end; end; begin :: Translating between Triangular Norms and Conorms definition let t be BinOp of [.0,1.]; func conorm t -> BinOp of [.0,1.] means :CoDef: for a,b being Element of [.0,1.] holds it.(a,b) = 1 - t.(1 - a,1 - b); existence proof reconsider A = [.0,1.] as non empty real-membered set; deffunc F(Element of A, Element of A) = In (1- t.(1-\$1,1-\$2),A); ex f being Function of [:A,A:], A st for x being Element of A for y being Element of A holds f.(x,y) = F(x,y) from BINOP_1:sch 4; then consider f being BinOp of A such that A1: for x being Element of A for y being Element of A holds f.(x,y) = F(x,y); reconsider ff = f as BinOp of [.0,1.]; take ff; let a,b be Element of [.0,1.]; reconsider aa = a, bb = b as Element of A; ff.(a,b) = F(aa,bb) by A1; hence thesis by SUBSET_1:def 8,CoIn01; end; uniqueness proof let f1,f2 be BinOp of [.0,1.] such that A1: for a,b being Element of [.0,1.] holds f1.(a,b) = 1-t.(1-a,1-b) and A2: for a,b being Element of [.0,1.] holds f2.(a,b) = 1-t.(1-a,1-b); A3: dom f1 = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1 .= dom f2 by FUNCT_2:def 1; for x,y being object st [x,y] in dom f1 holds f1.(x,y) = f2.(x,y) proof let x,y be object; assume [x,y] in dom f1; then reconsider xx = x, yy = y as Element of [.0,1.] by ZFMISC_1:87; f1.(xx,yy) = 1-t.(1-xx,1-yy) by A1 .= f2.(xx,yy) by A2; hence thesis; end; hence thesis by A3,BINOP_1:20; end; end; registration let t be t-norm; cluster conorm t -> monotonic commutative associative with-0-identity; coherence proof set f = conorm t; A1: for a,b being Element of [.0,1.] holds f.(a,b) = f.(b,a) proof let a,b be Element of [.0,1.]; A2: 1 - a in [.0,1.] & 1 - b in [.0,1.] by OpIn01; f.(a,b) = 1-t.(1-a,1-b) by CoDef .= 1-t.(1-b,1-a) by A2,BINOP_1:def 2 .= f.(b,a) by CoDef; hence thesis; end; C1: for a,b,c being Element of [.0,1.] holds f.(f.(a,b),c) = f.(a,f.(b,c)) proof let a,b,c be Element of [.0,1.]; A2: 1-a in [.0,1.] & 1-b in [.0,1.] & 1-c in [.0,1.] by OpIn01; set A = 1-t.(1-a,1-b); H1: A in [.0,1.] by CoIn01; set C = 1-t.(1-b,1-c); H2: C in [.0,1.] by CoIn01; f.(f.(a,b),c) = f.(1-t.(1-a,1-b),c) by CoDef .= 1-t.(1-A,1-c) by CoDef,H1 .= 1-t.(1-a,1-C) by BINOP_1:def 3,A2 .= f.(a,C) by CoDef,H2 .= f.(a,f.(b,c)) by CoDef; hence thesis; end; D1: for a,b,c,d being Element of [.0,1.] st a <= c & b <= d holds f.(a,b) <= f.(c,d) proof let a,b,c,d be Element of [.0,1.]; A2: 1-a in [.0,1.] & 1-b in [.0,1.] & 1-c in [.0,1.] & 1-d in [.0,1.] by OpIn01; assume a <= c & b <= d; then 1 - c <= 1 - a & 1 - d <= 1 - b by XREAL_1:10; then t.(1-a,1-b) >= t.(1-c,1-d) by A2,MonDef; then 1-t.(1-a,1-b) <= 1-t.(1-c,1-d) by XREAL_1:10; then f.(a,b) <= 1-t.(1-c,1-d) by CoDef; hence thesis by CoDef; end; for a being Element of [.0,1.] holds f.(a,0) = a proof let a be Element of [.0,1.]; T1: 0 in [.0,1.] by XXREAL_1:1; 1-a in [.0,1.] by OpIn01; then t.(1-a,1) = 1 - a by IdDef; then 1-t.(1-a,1-0) = a; hence thesis by CoDef,T1; end; hence thesis by A1,BINOP_1:def 2,def 3,D1,C1; end; end; theorem maxnorm = conorm minnorm proof for a,b being Element of [.0,1.] holds maxnorm.(a,b) = 1 - minnorm.(1 - a, 1 - b) proof let a,b be Element of [.0,1.]; A1: 1 - a in [.0,1.] & 1 - b in [.0,1.] by OpIn01; set e1 = -1; A2: - max(e1 * -a, e1 * -b) = - (e1 * min (-a,-b)) by MES57 .= min (-a,-b); A3: min (1 +- a, 1 +- b) = 1 + min (-a, -b) by FUZZY_2:42 .= 1 - max(a, b) by A2; maxnorm.(a,b) = 1 - min(1 - a, 1 - b) by A3,MaxDef .= 1 - minnorm.(1 - a, 1 - b) by A1,MinDef; hence thesis; end; hence thesis by CoDef; end; theorem for t being BinOp of [.0,1.] holds conorm conorm t = t proof let t be BinOp of [.0,1.]; set tt = conorm conorm t; for a,b being Element of [.0,1.] holds t.(a,b) = tt.(a,b) proof let a, b be Element of [.0,1.]; A1: 1 - a in [.0,1.] & 1 - b in [.0,1.] by OpIn01; tt.(a,b) = 1 - (conorm t).(1-a,1-b) by CoDef .= 1 - (1 - t.(1-(1-a),1-(1-b))) by CoDef,A1; hence thesis; end; hence thesis by BINOP_1:2; end; :::theorem ::: obvious ::: for t being t-norm holds conorm t is t-conorm; begin :: The Ordering of Triangular Norms (and Conorms) definition let f1, f2 be BinOp of [.0,1.]; pred f1 <= f2 means for a,b being Element of [.0,1.] holds f1.(a,b) <= f2.(a,b); end; theorem for t being t-norm holds drastic_norm <= t proof let t be t-norm; set f1 = drastic_norm; for a,b being Element of [.0,1.] holds f1.(a,b) <= t.(a,b) proof let a,b be Element of [.0,1.]; per cases; suppose A2: a = 1; reconsider aa = 1, bb = b as Element of [.0,1.] by XXREAL_1:1; t.(aa,bb) = t.(bb,aa) by BINOP_1:def 2 .= b by IdDef; hence thesis by DrasticDef,A2; end; suppose A2: b = 1; reconsider aa = a, bb = 1 as Element of [.0,1.] by XXREAL_1:1; f1.(aa,bb) = aa by DrasticDef; hence thesis by A2,IdDef; end; suppose A2: a <> 1 & b <> 1; reconsider aa = a, bb = b as Element of [.0,1.]; f1.(aa,bb) = 0 by DrasticDef,A2; hence thesis by XXREAL_1:1; end; end; hence thesis; end; theorem for t being t-norm holds t <= minnorm proof let t be t-norm; set f1 = minnorm; for a,b being Element of [.0,1.] holds t.(a,b) <= f1.(a,b) proof let a,b be Element of [.0,1.]; reconsider aa = a, bb = b as Element of [.0,1.]; A1: f1.(a,b) = min (aa,bb) by MinDef; reconsider cc = 1 as Element of [.0,1.] by XXREAL_1:1; aa <= 1 by XXREAL_1:1; then t.(aa,bb) <= t.(cc,bb) by MonDef; then t.(aa,bb) <= t.(bb,cc) by BINOP_1:def 2; then A3: t.(aa,bb) <= bb by IdDef; bb <= 1 by XXREAL_1:1; then t.(aa,bb) <= t.(aa,cc) by MonDef; then t.(aa,bb) <= aa by IdDef; hence thesis by A1,XXREAL_0:20,A3; end; hence thesis; end; theorem for t1, t2 being t-norm st t1 <= t2 holds conorm t2 <= conorm t1 proof let t1, t2 be t-norm; set c1 = conorm t1, c2 = conorm t2; assume A1: t1 <= t2; for a,b being Element of [.0,1.] holds c2.(a,b) <= c1.(a,b) proof let a,b be Element of [.0,1.]; 1-a in [.0,1.] & 1-b in [.0,1.] by OpIn01; then 1 - t2.(1-a,1-b) <= 1 - t1.(1-a,1-b) by A1,XREAL_1:10; then 1 - t2.(1-a,1-b) <= c1.(a,b) by CoDef; hence thesis by CoDef; end; hence thesis; end; begin :: The Rest of Triangular Conorms definition func Hamacher_conorm -> BinOp of [.0,1.] means :HamCoDef: for a,b being Element of [.0,1.] holds (a = b = 1 implies it.(a,b) = 1) & (a <> 1 or b <> 1 implies it.(a,b) = (a + b - 2 * a * b) / (1 - a * b)); existence proof set C = [.0,1.]; deffunc F(Element of C, Element of C) = In ((\$1 + \$2 - 2 * \$1 * \$2) / (1 - \$1 * \$2),C); defpred P[set,set] means \$1 = 1 & \$2 = 1; deffunc G(Element of C,Element of C) = In(1,C); ex f being Function of [:C,C:],C st for c be Element of C, d be Element of C st [c,d] in dom f holds (P[c,d] implies f. [c,d] = G(c,d)) & (not P [c,d] implies f. [c,d] = F(c,d)) from SCHEME1:sch 21; then consider f being Function of [:C,C:],C such that A1: for c be Element of C, d be Element of C st [c,d] in dom f holds (P[c,d] implies f. [c,d] = G(c,d)) & (not P [c,d] implies f. [c,d] = F(c,d)); take f; A0: dom f = [:C,C:] by FUNCT_2:def 1; let a,b be Element of C; AA: [a,b] in dom f by A0,ZFMISC_1:87; (a = b = 1 implies f.(a,b) = 1) & (a <> 1 or b <> 1 implies f.(a,b) = (a + b - 2 * a * b) / (1 - a * b)) proof thus a = b = 1 implies f.(a,b) = 1 proof assume a = b = 1; then f. [a,b] = G(a,b) by A1,AA .= 1 by SUBSET_1:def 8,XXREAL_1:1; hence thesis; end; assume a <> 1 or b <> 1; then f. [a,b] = F(a,b) by A1,AA .= (a + b - 2 * a * b) / (1 - a * b) by SUBSET_1:def 8,HamCoIn01; hence thesis; end; hence thesis; end; uniqueness proof let f1,f2 be BinOp of [.0,1.] such that A1: for a,b being Element of [.0,1.] holds (a = b = 1 implies f1.(a,b) = 1) & (a <> 1 or b <> 1 implies f1.(a,b) = (a + b - 2 * a * b) / (1 - a * b)) and A2: for a,b being Element of [.0,1.] holds (a = b = 1 implies f2.(a,b) = 1) & (a <> 1 or b <> 1 implies f2.(a,b) = (a + b - 2 * a * b) / (1 - a * b)); for a,b being set st a in [.0,1.] & b in [.0,1.] holds f1.(a,b) = f2.(a,b) proof let a,b be set; assume a in [.0,1.] & b in [.0,1.]; then reconsider aa = a, bb = b as Element of [.0,1.]; per cases; suppose B0: aa = bb = 1; then f1.(aa,bb) = 1 by A1 .= f2.(aa,bb) by A2,B0; hence thesis; end; suppose B1: aa <> 1 or bb <> 1; then f1.(aa,bb) = (aa + bb - 2 * aa * bb) / (1 - aa * bb) by A1 .= f2.(aa,bb) by A2,B1; hence thesis; end; end; hence thesis by BINOP_1:def 21; end; end; theorem CoHam: conorm Hamacher_norm = Hamacher_conorm proof set dn = conorm Hamacher_norm; set dc = Hamacher_conorm; for a,b being Element of [.0,1.] holds dc.(a,b) = 1 - (Hamacher_norm).(1-a,1-b) proof let a,b be Element of [.0,1.]; AB: 0 in [.0,1.] by XXREAL_1:1; A3: 1 - a in [.0,1.] & 1 - b in [.0,1.] by OpIn01; WE: 0 <= a <= 1 & 0 <= b <= 1 by XXREAL_1:1; per cases; suppose Aa: a <> 1 or b <> 1; then AA: 1 - a * b <> 0 by WE,XREAL_1:150; dc.(a,b) = (a + b - 2 * a * b) / (1 - a * b) by HamCoDef,Aa .= ((1 * ((1 - a) + (1 - b) - (1 - a) * (1 - b))) - ((1 - a) * (1 - b))) / ((1 - a) + (1 - b) - (1 - a) * (1 - b)) .= 1 - ((1 - a) * (1 - b)) / ((1 - a) + (1 - b) - (1 - a) * (1 - b)) by XCMPLX_1:127,AA .= 1 - (Hamacher_norm).(1-a,1-b) by HamDef,A3; hence thesis; end; suppose T1: a = b = 1; then Hamacher_norm.(1-a,1-b) = (0 * 0) / (0 + 0 - 0 * 0) by HamDef,AB .= 0; hence thesis by T1,HamCoDef; end; end; hence thesis by CoDef; end; registration cluster Hamacher_conorm -> commutative associative with-0-identity monotonic; coherence by CoHam; end; theorem conorm drastic_norm = drastic_conorm proof set dn = conorm drastic_norm; set dc = drastic_conorm; for a,b being Element of [.0,1.] holds dc.(a,b) = 1 - (drastic_norm).(1-a,1-b) proof let a,b be Element of [.0,1.]; A3: 1 - a in [.0,1.] & 1 - b in [.0,1.] by OpIn01; then we: 1 - a <= 1 & 1 - b <= 1 by XXREAL_1:1; WE: 0 <= a & 0 <= b by XXREAL_1:1; per cases; suppose A0: a = 0 & b = 0; then A1: min (a,b) = 0; A2: max (1-a,1-b) = 1 by A0; dc.(a,b) = max (a,b) by Drastic2CDef,A1 .= 1 - min (1-a,1-b) by A0 .= 1 - (drastic_norm).(1-a,1-b) by Drastic2Def,A2,A3; hence thesis; end; suppose BB: a <> 0 & b <> 0; then B0: min (a,b) <> 0 by XXREAL_0:15; 1 - a <> 1 & 1 - b <> 1 by BB; then B1: max (1-a,1-b) <> 1 by XXREAL_0:16; dc.(a,b) = 1 - 0 by Drastic2CDef,B0 .= 1 - (drastic_norm).(1-a,1-b) by Drastic2Def,B1,A3; hence thesis; end; suppose BB: b <> 0 & a = 0; then B0: min (a,b) = 0 by WE,XXREAL_0:def 9; B1: min (1-a,1-b) = 1 - b by we,XXREAL_0:def 9,BB; B8: max (1-a,1-b) = 1 by XXREAL_0:def 10,we,BB; dc.(a,b) = max (a,b) by Drastic2CDef,B0 .= 1 - min (1-a,1-b) by B1,BB,XXREAL_0:def 10,WE .= 1 - (drastic_norm).(1-a,1-b) by Drastic2Def,A3,B8; hence thesis; end; suppose BB: a <> 0 & b = 0; then B0: min (a,b) = 0 by WE,XXREAL_0:def 9; B1: min (1-a,1-b) = 1 - a by we,XXREAL_0:def 9,BB; B8: max (1-a,1-b) = 1 by XXREAL_0:def 10,we,BB; dc.(a,b) = max (a,b) by Drastic2CDef,B0 .= 1 - min (1-a,1-b) by B1,BB,XXREAL_0:def 10,WE .= 1 - (drastic_norm).(1-a,1-b) by Drastic2Def,A3,B8; hence thesis; end; end; hence thesis by CoDef; end; theorem ConormProd: conorm prodnorm = probsum_conorm proof set dn = conorm prodnorm; set dc = probsum_conorm; for a,b being Element of [.0,1.] holds dc.(a,b) = 1 - (prodnorm).(1-a,1-b) proof let a,b be Element of [.0,1.]; A3: 1 - a in [.0,1.] & 1 - b in [.0,1.] by OpIn01; dc.(a,b) = a + b - a*b by ProbSumDef .= 1 - (1-a) * (1-b) .= 1 - (prodnorm).(1-a,1-b) by ProdDef,A3; hence thesis; end; hence thesis by CoDef; end; registration cluster probsum_conorm -> commutative associative with-0-identity monotonic; coherence by ConormProd; end; definition func nilmax_conorm -> BinOp of [.0,1.] means :NilmaxDef: for a,b being Element of [.0,1.] holds (a + b < 1 implies it.(a,b) = max (a,b)) & (a + b >= 1 implies it.(a,b) = 1); existence proof set C = [.0,1.]; defpred P[Real,Real] means \$1 + \$2 < 1; deffunc F(Element of C,Element of C) = In(max (\$1,\$2),C); deffunc G(Element of C,Element of C) = In(1,C); ex f being Function of [:C,C:],C st for c be Element of C, d be Element of C st [c,d] in dom f holds (P[c,d] implies f. [c,d] = F(c,d)) & (not P [c,d] implies f. [c,d] = G(c,d)) from SCHEME1:sch 21; then consider f being Function of [:C,C:],C such that A1: for c be Element of C, d be Element of C st [c,d] in dom f holds (P[c,d] implies f. [c,d] = F(c,d)) & (not P [c,d] implies f. [c,d] = G(c,d)); take f; A0: dom f = [:C,C:] by FUNCT_2:def 1; let a,b be Element of C; cc: max (a,b) = a or max (a,b) = b by XXREAL_0:16; AA: [a,b] in dom f by A0,ZFMISC_1:87; (a + b < 1 implies f.(a,b) = max (a,b)) & (a + b >= 1 implies f.(a,b) = 1) proof thus a + b < 1 implies f.(a,b) = max (a,b) proof assume a + b < 1; then f. [a,b] = F(a,b) by A1,AA .= max (a,b) by SUBSET_1:def 8,cc; hence thesis; end; assume a + b >= 1; then f. [a,b] = G(a,b) by A1,AA .= 1 by XXREAL_1:1,SUBSET_1:def 8; hence thesis; end; hence thesis; end; uniqueness proof let f1,f2 be BinOp of [.0,1.] such that A1: for a,b being Element of [.0,1.] holds (a + b < 1 implies f1.(a,b) = max (a,b)) & (a + b >= 1 implies f1.(a,b) = 1) and A2: for a,b being Element of [.0,1.] holds (a + b < 1 implies f2.(a,b) = max (a,b)) & (a + b >= 1 implies f2.(a,b) = 1); for a,b being set st a in [.0,1.] & b in [.0,1.] holds f1.(a,b) = f2.(a,b) proof let a,b be set; assume a in [.0,1.] & b in [.0,1.]; then reconsider aa = a, bb = b as Element of [.0,1.]; per cases; suppose B0: aa + bb < 1; then f1.(aa,bb) = max (aa,bb) by A1 .= f2.(aa,bb) by A2,B0; hence thesis; end; suppose B1: aa + bb >= 1; then f1.(aa,bb) = 1 by A1 .= f2.(aa,bb) by A2,B1; hence thesis; end; end; hence thesis by BINOP_1:def 21; end; end; theorem ConormNilmin: conorm nilmin_norm = nilmax_conorm proof set dn = conorm nilmin_norm; set dc = nilmax_conorm; for a,b being Element of [.0,1.] holds dc.(a,b) = 1 - (nilmin_norm).(1-a,1-b) proof let a,b be Element of [.0,1.]; A3: 1 - a in [.0,1.] & 1 - b in [.0,1.] by OpIn01; per cases; suppose W0: a + b < 1; then 2 - (a + b) > 2 - 1 by XREAL_1:10; then W1: 1 - a + (1 - b) > 1; dc.(a,b) = max (a,b) by NilmaxDef,W0 .= 1 - min (1-a,1-b) by MaxMin .= 1 - (nilmin_norm).(1-a,1-b) by NilminDef,A3,W1; hence thesis; end; suppose W0: a + b >= 1; then 2 - (a + b) <= 2 - 1 by XREAL_1:10; then W1: 1 - a + (1 - b) <= 1; dc.(a,b) = 1 - 0 by NilmaxDef,W0 .= 1 - (nilmin_norm).(1-a,1-b) by NilminDef,A3,W1; hence thesis; end; end; hence thesis by CoDef; end; registration cluster nilmax_conorm -> commutative associative with-0-identity monotonic; coherence by ConormNilmin; end; definition func BoundedSum_conorm -> BinOp of [.0,1.] means :LukConorm: for a,b being Element of [.0,1.] holds it.(a,b) = min (a + b,1); existence proof reconsider A = [.0,1.] as non empty real-membered set; deffunc F(Element of A, Element of A) = In (min (\$1 + \$2,1),A); ex f being Function of [:A,A:], A st for x being Element of A for y being Element of A holds f.(x,y) = F(x,y) from BINOP_1:sch 4; then consider f being BinOp of A such that A1: for x being Element of A for y being Element of A holds f.(x,y) = F(x,y); reconsider ff = f as BinOp of [.0,1.]; take ff; let a,b be Element of [.0,1.]; reconsider aa = a, bb = b as Element of A; ff.(a,b) = F(aa,bb) by A1; hence thesis by SUBSET_1:def 8,Lemma2a; end; uniqueness proof let f1,f2 be BinOp of [.0,1.] such that A1: for a,b being Element of [.0,1.] holds f1.(a,b) = min (a + b, 1) and A2: for a,b being Element of [.0,1.] holds f2.(a,b) = min (a + b, 1); A3: dom f1 = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1 .= dom f2 by FUNCT_2:def 1; for x,y being object st [x,y] in dom f1 holds f1.(x,y) = f2.(x,y) proof let x,y be object; assume [x,y] in dom f1; then reconsider xx = x, yy = y as Element of [.0,1.] by ZFMISC_1:87; f1.(xx,yy) = min (xx + yy, 1) by A1 .= f2.(xx,yy) by A2; hence thesis; end; hence thesis by A3,BINOP_1:20; end; end; theorem ConormLukasiewicz: conorm Lukasiewicz_norm = BoundedSum_conorm proof set dn = conorm Lukasiewicz_norm; set dc = BoundedSum_conorm; for a,b being Element of [.0,1.] holds dc.(a,b) = 1 - (Lukasiewicz_norm).(1-a,1-b) proof let a,b be Element of [.0,1.]; A3: 1 - a in [.0,1.] & 1 - b in [.0,1.] by OpIn01; dc.(a,b) = min (a+b,1) by LukConorm .= 1 - max (0,1-a+(1-b)-1) by LukasiDual .= 1 - (Lukasiewicz_norm).(1-a,1-b) by LukNorm,A3; hence thesis; end; hence thesis by CoDef; end; registration cluster BoundedSum_conorm -> commutative associative with-0-identity monotonic; coherence by ConormLukasiewicz; end; theorem for t being t-conorm holds maxnorm <= t proof let t be t-conorm; set f1 = maxnorm; for a,b being Element of [.0,1.] holds f1.(a,b) <= t.(a,b) proof let a,b be Element of [.0,1.]; reconsider aa = a, bb = b as Element of [.0,1.]; A1: f1.(a,b) = max (aa,bb) by MaxDef; reconsider cc = 0 as Element of [.0,1.] by XXREAL_1:1; aa >= 0 by XXREAL_1:1; then t.(aa,bb) >= t.(cc,bb) by MonDef; then t.(aa,bb) >= t.(bb,cc) by BINOP_1:def 2; then A3: t.(aa,bb) >= bb by ZeroDef; bb >= 0 by XXREAL_1:1; then t.(aa,bb) >= t.(aa,cc) by MonDef; then t.(aa,bb) >= aa by ZeroDef; hence thesis by A1,XXREAL_0:28,A3; end; hence thesis; end; theorem for t being t-conorm holds t <= drastic_conorm proof let t be t-conorm; set f1 = drastic_conorm; for a,b being Element of [.0,1.] holds f1.(a,b) >= t.(a,b) proof let a,b be Element of [.0,1.]; per cases by XXREAL_0:15; suppose A2: a = 0; then reconsider aa = 0, bb = b as Element of [.0,1.]; aa <= bb by XXREAL_1:1; then min (aa,bb) = 0 by XXREAL_0:def 9; then A3: f1.(aa,bb) = max(aa,bb) by Drastic2CDef; t.(aa,bb) = t.(bb,aa) by BINOP_1:def 2 .= b by ZeroDef; hence thesis by A2,A3,XXREAL_0:25; end; suppose A2: b = 0; then reconsider aa = a, bb = 0 as Element of [.0,1.]; aa >= bb by XXREAL_1:1; then min (aa,bb) = 0 by XXREAL_0:def 9; then A3: f1.(aa,bb) = max(aa,bb) by Drastic2CDef; t.(aa,bb) = a by ZeroDef; hence thesis by A2,A3,XXREAL_0:25; end; suppose aa: min (a,b) <> 0; reconsider aa = a, bb = b as Element of [.0,1.]; f1.(aa,bb) = 1 by Drastic2CDef,aa; hence thesis by XXREAL_1:1; end; end; hence thesis; end;