:: Basic Formal Properties of Triangular Norms and Conorms
:: by Adam Grabowski
::
:: Received June 27, 2017
:: Copyright (c) 2017-2026 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, XXREAL_0, XREAL_0, MEMBERED, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities BINOP_1, ORDINAL1;
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;