:: Formal Introduction to Fuzzy Implications
:: by Adam Grabowski
::
:: Received September 3, 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, FUZIMPL1, SUBSET_1, CARD_1,
ARYTM_1, ARYTM_3, POWER, FUNCT_1, RELAT_1, FUNCT_7, ZFMISC_1, BINOP_1;
notations TARSKI, SUBSET_1, ORDINAL1, XCMPLX_0, XXREAL_0, ZFMISC_1, BINOP_1,
XREAL_0, POWER, FUNCT_1, RELSET_1, FUNCT_2, RCOMP_1, FUZNORM1;
constructors REAL_1, SEQ_4, TOPMETR, PREPOWER, POWER, FUZNORM1;
registrations XBOOLE_0, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, ORDINAL1,
FUZNORM1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities BINOP_1;
theorems SUBSET_1, FUNCT_2, POWER, XREAL_1, XXREAL_0, XXREAL_1, BINOP_1,
ZFMISC_1, HOLDER_1, FUZNORM1;
schemes BINOP_1, SCHEME1;
begin :: Preliminaries
theorem MaxMinIn01:
for a,b being Element of [.0,1.] holds
max (b, min (1-a,1-b)) in [.0,1.]
proof
let a,b be Element of [.0,1.];
a1: 1 - a in [.0,1.] & 1 - b in [.0,1.] by FUZNORM1:7;
max (b, min (1-a,1-b)) = b or
max (b, min (1-a,1-b)) = min (1-a,1-b) by XXREAL_0:16;
hence thesis by a1,FUZNORM1:1;
end;
theorem LukaIn01:
for a,b being Element of [.0,1.] holds
min (1,1-a+b) in [.0,1.]
proof
let a,b be Element of [.0,1.];
A1: min (1, 1-a+b) <= 1 by XXREAL_0:17;
1 - a in [.0,1.] by FUZNORM1:7; then
1 - a >= 0 & b >= 0 by XXREAL_1:1; then
min (1, 1-a+b) >= 0 by XXREAL_0:20;
hence thesis by A1,XXREAL_1:1;
end;
theorem ReichenbachIn01:
for a,b being Element of [.0,1.] holds
1 - a + a * b in [.0,1.]
proof
let a,b be Element of [.0,1.];
1 - a in [.0,1.] by FUZNORM1:7; then
A0: 1 - a >= 0 by XXREAL_1:1;
a * b in [.0,1.] by FUZNORM1:3; then
a1: a * b >= 0 by XXREAL_1:1;
b <= 1 by XXREAL_1:1; then
a2: b - 1 <= 1 - 1 by XREAL_1:9;
a >= 0 by XXREAL_1:1; then
a * (b - 1) <= 0 by a2; then
1 + (a * b - a) <= 1 + 0 by XREAL_1:7;
hence thesis by a1,A0,XXREAL_1:1;
end;
theorem Max1In01:
for a,b being Element of [.0,1.] holds
max(1-a,b) in [.0,1.]
proof
let a,b be Element of [.0,1.];
max (1-a,b) = 1 - a or max (1-a,b) = b by XXREAL_0:16;
hence thesis by FUZNORM1:7;
end;
theorem PowerIn01:
for a,b being Element of [.0,1.] st a > 0 or b > 0 holds
b to_power a in [.0,1.]
proof
let a,b be Element of [.0,1.];
YY: b <= 1 & b >= 0 by XXREAL_1:1;
XX: a >= 0 by XXREAL_1:1;
assume a > 0 or b > 0; then
per cases;
suppose
S1: a > 0 & b <> 0 & b <> 1; then
B1: a > 0 & b > 0 by XXREAL_1:1;
ZZ: b < 1 by S1,XXREAL_0:1,YY;
b to_power a < b to_power 0 by POWER:40,B1,ZZ; then
A1: b to_power a <= 1 by POWER:24;
b to_power a > 0 by B1,POWER:34;
hence thesis by A1,XXREAL_1:1;
end;
suppose
S1: a > 0 & b <> 0 & b = 1; then
A1: b to_power a <= 1 by POWER:26;
b to_power a > 0 by S1,POWER:34;
hence thesis by A1,XXREAL_1:1;
end;
suppose
B1: a > 0 & b = 0; then
A1: b to_power a <= 1 by POWER:def 2;
b to_power a >= 0 by POWER:def 2,B1;
hence thesis by A1,XXREAL_1:1;
end;
suppose B1: b > 0 & b <> 1;
b <= 1 by XXREAL_1:1; then
b to_power a <= 1 to_power a by XX,B1,HOLDER_1:3; then
A1: b to_power a <= 1 by POWER:26;
b to_power a > 0 by B1,POWER:34;
hence thesis by A1,XXREAL_1:1;
end;
suppose B1: b > 0 & b = 1; then
A1: b to_power a <= 1 by POWER:26;
b to_power a > 0 by B1,POWER:34;
hence thesis by A1,XXREAL_1:1;
end;
end;
theorem QuoIn01:
for a,b being Element of [.0,1.] st a > b holds
b / a in [.0,1.]
proof
let a,b be Element of [.0,1.];
assume
A0: a > b;
A2: 0 <= a <= 1 & 0 <= b <= 1 by XXREAL_1:1; then
b / a <= 1 by XREAL_1:185,A0;
hence thesis by A2,XXREAL_1:1;
end;
begin :: Basic Attributes Defining Fuzzy Implications
definition let f be BinOp of [.0,1.];
attr f is decreasing_on_1st means :DefDecr:
for x1,x2,y being Element of [.0,1.] st
x1 <= x2 holds f.(x1,y) >= f.(x2,y);
attr f is increasing_on_2nd means :DefIncr:
for x,y1,y2 being Element of [.0,1.] st
y1 <= y2 holds f.(x,y1) <= f.(x,y2);
attr f is 00-dominant means :Def00:
f.(0,0) = 1;
attr f is 11-dominant means :Def11:
f.(1,1) = 1;
attr f is 10-weak means :Def10:
f.(1,0) = 0;
attr f is 01-dominant means
f.(0,1) = 1;
end;
:: Classical Implication
definition let f be BinOp of [.0,1.];
attr f is with_properties_of_fuzzy_implication means
f is decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
attr f is with_properties_of_classical_implication means
f is 00-dominant 01-dominant 11-dominant 10-weak;
end;
begin :: Examples Showing Independence of Axioms
definition
func I_{-1} -> BinOp of [.0,1.] means :I1Def:
for x,y being Element of [.0,1.] holds
it.(x,y) = max (1-x,min(x,y));
existence
proof
set A = [.0,1.];
deffunc F(Element of A, Element of A) = In (max (1-$1,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;
max (1-a,min(a,b)) = 1 - a or
max (1-a,min(a,b)) = min (a,b) by XXREAL_0:16;
hence thesis by A2,SUBSET_1:def 8,FUZNORM1:7,FUZNORM1:1;
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 (1-a,min(a,b)) and
A2: for a,b being Element of [.0,1.] holds f2.(a,b) = max (1-a,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) = max(1-xx,min(xx,yy)) by A1
.= f2.(xx,yy) by A2;
hence thesis;
end;
hence thesis by A3,BINOP_1:20;
end;
end;
registration
cluster I_{-1} -> :::non decreasing_on_1st
increasing_on_2nd 00-dominant 11-dominant 10-weak;
coherence
proof
set f = I_{-1};
b2: for x,y1,y2 being Element of [.0,1.] st
y1 <= y2 holds f.(x,y1) <= f.(x,y2)
proof
let x,y1,y2 be Element of [.0,1.];
assume y1 <= y2; then
y1: min (x,y1) <= min (x,y2) by XXREAL_0:18;
f.(x,y1) = max (1-x,min(x,y1)) & f.(x,y2) = max (1-x,min(x,y2))
by I1Def;
hence thesis by y1,XXREAL_0:26;
end;
S: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1; then
T1: f.(0,0) = max (1-0,min(0,0)) by I1Def
.= 1 by XXREAL_0:def 10;
T2: f.(1,0) = max (1-1,min(1,0)) by S,I1Def
.= max (0,0) by XXREAL_0:def 9 .= 0;
f.(1,1) = max (1-1,min(1,1)) by S,I1Def
.= 1 by XXREAL_0:def 10;
hence thesis by b2,T1,T2;
end;
end;
definition
func I_{-2} -> BinOp of [.0,1.] means :I2Def:
for x,y being Element of [.0,1.] holds
it.(x,y) = max (y, min (1-x,1-y));
existence
proof
set A = [.0,1.];
deffunc F(Element of A, Element of A) = In (max ($2,min (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);
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,MaxMinIn01;
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 (b, min (1-a,1-b)) and
A2: for a,b being Element of [.0,1.] holds
f2.(a,b) = max (b, min (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) = max (yy, min (1-xx,1-yy)) by A1
.= f2.(xx,yy) by A2;
hence thesis;
end;
hence thesis by A3,BINOP_1:20;
end;
end;
registration
cluster I_{-2} -> decreasing_on_1st :::non increasing_on_2nd
00-dominant 11-dominant 10-weak;
coherence
proof
set f = I_{-2};
b1: for x1,x2,y being Element of [.0,1.] st
x1 <= x2 holds f.(x1,y) >= f.(x2,y)
proof
let x1,x2,y be Element of [.0,1.];
assume Z1: x1 <= x2;
Z2: f.(x1,y) = max (y,min(1-x1,1-y)) & f.(x2,y) = max (y,min(1-x2,1-y))
by I2Def;
1-x1 >= 1-x2 by Z1,XREAL_1:13; then
min(1-x1,1-y) >= min(1-x2,1-y) by XXREAL_0:18;
hence thesis by Z2,XXREAL_0:26;
end;
S: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1; then
T1: f.(0,0) = max (0,min(1-0,1-0)) by I2Def
.= 1 by XXREAL_0:def 10;
T2: f.(1,0) = max (0,min(1-1,1-0)) by S,I2Def
.= max (0,0) by XXREAL_0:def 9 .= 0;
f.(1,1) = max (1,min(1-1,1-1)) by S,I2Def
.= 1 by XXREAL_0:def 10;
hence thesis by b1,T1,T2;
end;
end;
definition
func I_{-3} -> BinOp of [.0,1.] means :I3Def:
for x,y being Element of [.0,1.] holds
(y < 1 implies it.(x,y) = 0) &
(y = 1 implies it.(x,y) = 1);
existence
proof
set C = [.0,1.];
defpred P[Real,Real] means $2 < 1;
deffunc F(Element of C,Element of C) = In(0,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;
AA: [a,b] in dom f by A0,ZFMISC_1:87;
(b < 1 implies f.(a,b) = 0) &
(b = 1 implies f.(a,b) = 1)
proof
thus b < 1 implies f.(a,b) = 0
proof
assume b < 1; then
f. [a,b] = F(a,b) by A1,AA
.= 0 by SUBSET_1:def 8,XXREAL_1:1;
hence thesis;
end;
assume 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
(b < 1 implies f1.(a,b) = 0) &
(b = 1 implies f1.(a,b) = 1) and
A2: for a,b being Element of [.0,1.] holds
(b < 1 implies f2.(a,b) = 0) &
(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.];
bb <= 1 by XXREAL_1:1; then
per cases by XXREAL_0:1;
suppose
B0: bb < 1; then
f1.(aa,bb) = 0 by A1 .= f2.(aa,bb) by A2,B0;
hence thesis;
end;
suppose
B1: 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;
registration
cluster I_{-3} -> decreasing_on_1st increasing_on_2nd
non 00-dominant 11-dominant 10-weak;
coherence
proof
set f = I_{-3};
b1: for x1,x2,y being Element of [.0,1.] st
x1 <= x2 holds f.(x1,y) >= f.(x2,y)
proof
let x1,x2,y be Element of [.0,1.];
SS: y <= 1 by XXREAL_1:1;
assume x1 <= x2;
per cases;
suppose y = 1; then
f.(x1,y) = 1 & f.(x2,y) = 1 by I3Def;
hence thesis;
end;
suppose y <> 1; then
y < 1 by SS,XXREAL_0:1; then
f.(x1,y) = 0 & f.(x2,y) = 0 by I3Def;
hence thesis;
end;
end;
b2: for x,y1,y2 being Element of [.0,1.] st
y1 <= y2 holds f.(x,y1) <= f.(x,y2)
proof
let x,y1,y2 be Element of [.0,1.];
assume YY: y1 <= y2;
per cases;
suppose Y0: y1 = 1;
y2 >= 1 & y2 <= 1 by XXREAL_1:1,Y0,YY; then
y2 = 1 by XXREAL_0:1; then
f.(x,y2) = 1 by I3Def;
hence thesis by XXREAL_1:1;
end;
suppose Za: y1 <> 1 & y2 = 1;
y1 <= 1 by XXREAL_1:1; then
y1 < 1 by Za,XXREAL_0:1; then
f.(x,y1) = 0 by I3Def;
hence thesis by Za,I3Def;
end;
suppose Za: y1 <> 1 & y2 <> 1;
y1 <= 1 & y2 <= 1 by XXREAL_1:1; then
y1 < 1 & y2 < 1 by Za,XXREAL_0:1; then
f.(x,y1) = 0 & f.(x,y2) = 0 by I3Def;
hence thesis;
end;
end;
0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
hence thesis by b1,b2,I3Def;
end;
end;
definition
func I_{-4} -> BinOp of [.0,1.] means :I4Def:
for x,y being Element of [.0,1.] holds
(x = 0 implies it.(x,y) = 1) &
(x > 0 implies it.(x,y) = 0);
existence
proof
set C = [.0,1.];
defpred P[Real,Real] means $1 > 0;
deffunc F(Element of C,Element of C) = In(0,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;
AA: [a,b] in dom f by A0,ZFMISC_1:87;
(a > 0 implies f.(a,b) = 0) &
(a = 0 implies f.(a,b) = 1)
proof
thus a > 0 implies f.(a,b) = 0
proof
assume a > 0; then
f. [a,b] = F(a,b) by A1,AA
.= 0 by SUBSET_1:def 8,XXREAL_1:1;
hence thesis;
end;
assume a = 0; 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 = 0 implies f1.(a,b) = 1) &
(a > 0 implies f1.(a,b) = 0) and
A2: for a,b being Element of [.0,1.] holds
(a = 0 implies f2.(a,b) = 1) &
(a > 0 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 by XXREAL_1:1;
suppose
B0: aa > 0; then
f1.(aa,bb) = 0 by A1 .= f2.(aa,bb) by A2,B0;
hence thesis;
end;
suppose
B1: aa = 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;
registration
cluster I_{-4} -> decreasing_on_1st increasing_on_2nd
00-dominant non 11-dominant 10-weak;
coherence
proof
set f = I_{-4};
b1: for x1,x2,y being Element of [.0,1.] st
x1 <= x2 holds f.(x1,y) >= f.(x2,y)
proof
let x1,x2,y be Element of [.0,1.];
assume Z1: x1 <= x2;
per cases;
suppose Z0: x2 = 0; then
x1 = 0 by Z1,XXREAL_1:1;
hence thesis by Z0;
end;
suppose x2 <> 0 & x1 <> 0; then
x1 > 0 & x2 > 0 by XXREAL_1:1; then
f.(x2,y) = 0 by I4Def;
hence thesis by XXREAL_1:1;
end;
suppose Z1: x2 <> 0 & x1 = 0;
x2 >= 0 by XXREAL_1:1; then
f.(x2,y) = 0 by I4Def,Z1;
hence thesis by Z1,I4Def;
end;
end;
b2: for x,y1,y2 being Element of [.0,1.] st
y1 <= y2 holds f.(x,y1) <= f.(x,y2)
proof
let x,y1,y2 be Element of [.0,1.];
SS: x >= 0 by XXREAL_1:1;
assume y1 <= y2;
per cases;
suppose x = 0; then
f.(x,y1) = 1 & f.(x,y2) = 1 by I4Def;
hence thesis;
end;
suppose x <> 0; then
f.(x,y1) = 0 & f.(x,y2) = 0 by I4Def,SS;
hence thesis;
end;
end;
0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
hence thesis by b1,b2,I4Def;
end;
end;
definition
func I_{-5} -> BinOp of [.0,1.] means :I5Def:
for x,y being Element of [.0,1.] holds
it.(x,y) = 1;
existence
proof
set A = [.0,1.];
deffunc F(Element of A, Element of A) = In (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.];
f.(a,b) = F(a,b) by A1;
hence thesis by SUBSET_1:def 8,XXREAL_1:1;
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 and
A2: for a,b being Element of [.0,1.] holds f2.(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) = 1 by A1
.= f2.(xx,yy) by A2;
hence thesis;
end;
hence thesis by A3,BINOP_1:20;
end;
end;
registration
cluster I_{-5} -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant non 10-weak;
coherence
proof
set f = I_{-5};
b1: for x1,x2,y being Element of [.0,1.] st
x1 <= x2 holds f.(x1,y) >= f.(x2,y)
proof
let x1,x2,y be Element of [.0,1.];
assume x1 <= x2;
f.(x1,y) = 1 & f.(x2,y) = 1 by I5Def;
hence thesis;
end;
b2: for x,y1,y2 being Element of [.0,1.] st
y1 <= y2 holds f.(x,y1) <= f.(x,y2)
proof
let x,y1,y2 be Element of [.0,1.];
assume y1 <= y2;
f.(x,y1) = 1 & f.(x,y2) = 1 by I5Def;
hence thesis;
end;
0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
hence thesis by b1,b2,I5Def;
end;
end;
begin :: Catalogue of Fuzzy Implications
definition
func Lukasiewicz_implication -> BinOp of [.0,1.] means :Luk:
for x,y being Element of [.0,1.] holds
it.(x,y) = min (1,1-x+y);
existence
proof
set A = [.0,1.];
deffunc F(Element of A, Element of A) = In (min (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);
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,LukaIn01;
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 (1,1-a+b) and
A2: for a,b being Element of [.0,1.] holds f2.(a,b) = min (1,1-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 (1,1-xx+yy) by A1
.= f2.(xx,yy) by A2;
hence thesis;
end;
hence thesis by A3,BINOP_1:20;
end;
end;
registration
cluster Lukasiewicz_implication ->
decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak;
coherence
proof
set f = Lukasiewicz_implication;
A1: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
b1: for x1,x2,y being Element of [.0,1.] st
x1 <= x2 holds f.(x1,y) >= f.(x2,y)
proof
let x1,x2,y be Element of [.0,1.];
assume
U1: x1 <= x2;
U2: f.(x1,y) = min (1,1-x1+y) by Luk;
U3: f.(x2,y) = min (1,1-x2+y) by Luk;
1 - x1 >= 1 - x2 by U1,XREAL_1:13; then
1 - x1 + y >= 1 - x2 + y by XREAL_1:7;
hence thesis by U2,U3,XXREAL_0:18;
end;
b3: for x,y1,y2 being Element of [.0,1.] st
y1 <= y2 holds f.(x,y1) <= f.(x,y2)
proof
let x,y1,y2 be Element of [.0,1.];
assume y1 <= y2; then
1 - x + y1 <= 1 - x + y2 by XREAL_1:7; then
U1: min(1,1 - x + y2) >= min(1,1 - x + y1) by XXREAL_0:18;
f.(x,y1) = min (1,1-x+y1) by Luk;
hence f.(x,y1) <= f.(x,y2) by U1,Luk;
end;
bb: min (1,1-1+0) = 0 by XXREAL_0:def 9;
min (1,1-0+0) = 1;
hence thesis by b1,b3,A1,Luk,bb;
end;
end;
registration
cluster with_properties_of_fuzzy_implication for BinOp of [.0,1.];
existence
proof
take Lukasiewicz_implication;
thus thesis;
end;
end;
registration
cluster with_properties_of_fuzzy_implication ->
decreasing_on_1st increasing_on_2nd 00-dominant
11-dominant 10-weak for BinOp of [.0,1.];
coherence;
cluster decreasing_on_1st increasing_on_2nd 00-dominant 01-dominant
11-dominant 10-weak -> with_properties_of_fuzzy_implication
for BinOp of [.0,1.];
coherence;
cluster with_properties_of_classical_implication ->
00-dominant 01-dominant 11-dominant 10-weak for BinOp of [.0,1.];
coherence;
cluster 00-dominant 01-dominant 11-dominant 10-weak ->
with_properties_of_classical_implication for BinOp of [.0,1.];
coherence;
cluster with_properties_of_fuzzy_implication ->
with_properties_of_classical_implication for BinOp of [.0,1.];
coherence
proof
let f be BinOp of [.0,1.];
assume A1: f is with_properties_of_fuzzy_implication;
f.(0,1) = 1
proof
B1: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
B2: f is increasing_on_2nd 00-dominant by A1; then
B3: f.(0,0) <= f.(0,1) by B1;
reconsider e0 = 0, e1 = 1 as Element of [.0,1.] by XXREAL_1:1;
f.(e0,e1) <= 1 by XXREAL_1:1;
hence thesis by B2,B3,XXREAL_0:1;
end; then
f is 01-dominant;
hence thesis by A1;
end;
end;
definition
mode Fuzzy_Implication is decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak BinOp of [.0,1.];
end;
definition
func FI -> set equals
the set of all f where f is Fuzzy_Implication;
coherence;
end;
definition
func Goedel_implication -> BinOp of [.0,1.] means :Goedel:
for x,y being Element of [.0,1.] holds
(x <= y implies it.(x,y) = 1) &
(x > y implies it.(x,y) = y);
existence
proof
set C = [.0,1.];
defpred P[Real,Real] means $1 <= $2;
deffunc F(Element of C,Element of C) = In(1,C);
deffunc G(Element of C,Element of C) = In($2,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;
AA: [a,b] in dom f by A0,ZFMISC_1:87;
(a <= b implies f.(a,b) = 1) &
(a > b implies f.(a,b) = b)
proof
thus a <= b implies f.(a,b) = 1
proof
assume a <= b; then
f. [a,b] = F(a,b) by A1,AA
.= 1 by SUBSET_1:def 8,XXREAL_1:1;
hence thesis;
end;
assume a > b; then
f. [a,b] = G(a,b) by A1,AA
.= b by 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 implies f1.(a,b) = 1) &
(a > b implies f1.(a,b) = b) and
A2: for a,b being Element of [.0,1.] holds
(a <= b implies f2.(a,b) = 1) &
(a > b implies f2.(a,b) = 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; then
f1.(aa,bb) = 1 by A1 .= f2.(aa,bb) by A2,B0;
hence thesis;
end;
suppose
B1: aa > bb; then
f1.(aa,bb) = bb by A1 .= f2.(aa,bb) by A2,B1;
hence thesis;
end;
end;
hence thesis by BINOP_1:def 21;
end;
end;
registration
cluster Goedel_implication -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
coherence
proof
set f = Goedel_implication;
a0: for x1,x2,y being Element of [.0,1.] st
x1 <= x2 holds f.(x1,y) >= f.(x2,y)
proof
let x1,x2,y be Element of [.0,1.];
assume Z0: x1 <= x2;
per cases;
suppose S1: x2 <= y; then
S2: f.(x2,y) = 1 by Goedel;
x1 <= y by S1,Z0,XXREAL_0:2;
hence f.(x1,y) >= f.(x2,y) by S2,Goedel;
end;
suppose x2 > y & x1 > y; then
f.(x2,y) = y & f.(x1,y) = y by Goedel;
hence f.(x1,y) >= f.(x2,y);
end;
suppose x2 > y & x1 <= y; then
f.(x2,y) = y & f.(x1,y) = 1 by Goedel;
hence f.(x1,y) >= f.(x2,y) by XXREAL_1:1;
end;
end;
aa: for x,y1,y2 being Element of [.0,1.] st
y1 <= y2 holds f.(x,y1) <= f.(x,y2)
proof
let x,y1,y2 be Element of [.0,1.];
assume Z2: y1 <= y2;
per cases;
suppose Z1: x <= y1; then
Z3: f.(x,y1) = 1 by Goedel;
x <= y2 by XXREAL_0:2,Z1,Z2;
hence thesis by Z3, Goedel;
end;
suppose x > y1 & x <= y2; then
f.(x,y1) = y1 & f.(x,y2) = 1 by Goedel;
hence thesis by XXREAL_1:1;
end;
suppose x > y1 & x > y2; then
f.(x,y1) = y1 & f.(x,y2) = y2 by Goedel;
hence thesis by Z2;
end;
end;
0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
hence thesis by a0,aa,Goedel;
end;
end;
definition
func Reichenbach_implication -> BinOp of [.0,1.] means :Reichen:
for x,y being Element of [.0,1.] holds
it.(x,y) = 1 - x + x * y;
existence
proof
set A = [.0,1.];
deffunc F(Element of A, Element of A) = In (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);
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,ReichenbachIn01;
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 - a + a * b and
A2: for a,b being Element of [.0,1.] holds f2.(a,b) = 1 - a + 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) = 1-xx+xx*yy by A1
.= f2.(xx,yy) by A2;
hence thesis;
end;
hence thesis by A3,BINOP_1:20;
end;
end;
registration
cluster Reichenbach_implication -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
coherence
proof
set f = Reichenbach_implication;
a0: for x1,x2,y being Element of [.0,1.] st
x1 <= x2 holds f.(x1,y) >= f.(x2,y)
proof
let x1,x2,y be Element of [.0,1.];
0 <= y <= 1 by XXREAL_1:1; then
-1 <= -y by XREAL_1:24; then
zs: 1+-1 <= 1+-y by XREAL_1:7;
assume x1 <= x2; then
-x2 <= -x1 by XREAL_1:24; then
(-x2) * (1 - y) <= (-x1) * (1 - y) by zs,XREAL_1:64; then
1 + (- x2) * (1 - y) <= 1 + (- x1) * (1 - y) by XREAL_1:7; then
1 - x2 + x2 * y <= 1 - x1 + x1 * y; then
f.(x2,y) <= 1 - x1 + x1 * y by Reichen;
hence thesis by Reichen;
end;
aa: for x,y1,y2 being Element of [.0,1.] st
y1 <= y2 holds f.(x,y1) <= f.(x,y2)
proof
let x,y1,y2 be Element of [.0,1.];
P1: x >= 0 by XXREAL_1:1;
assume y1 <= y2; then
x * y1 <= x * y2 by XREAL_1:64,P1; then
1 - x + x * y1 <= 1 - x + x * y2 by XREAL_1:7; then
f.(x,y1) <= 1 - x + x * y2 by Reichen;
hence thesis by Reichen;
end;
AA: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1; then
A1: f.(0,0) = 1 - 0 + 0 * 0 by Reichen .= 1;
A2: f.(1,1) = 1 - 1 + 1 * 1 by AA,Reichen .= 1;
f.(1,0) = 1 - 1 + 1 * 0 by AA,Reichen;
hence thesis by A1,A2,a0,aa;
end;
end;
definition
func Kleene-Dienes_implication -> BinOp of [.0,1.] means :Kleene:
for x,y being Element of [.0,1.] holds
it.(x,y) = max (1 - x, y);
existence
proof
set A = [.0,1.];
deffunc F(Element of A, Element of A) = In (max (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);
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,Max1In01;
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 (1-a,b) and
A2: for a,b being Element of [.0,1.] holds f2.(a,b) = max (1-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 (1-xx,yy) by A1
.= f2.(xx,yy) by A2;
hence thesis;
end;
hence thesis by A3,BINOP_1:20;
end;
end;
registration
cluster Kleene-Dienes_implication -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
coherence
proof
set f = Kleene-Dienes_implication;
a0: for x1,x2,y being Element of [.0,1.] st
x1 <= x2 holds f.(x1,y) >= f.(x2,y)
proof
let x1,x2,y be Element of [.0,1.];
assume x1 <= x2; then
-x2 <= -x1 by XREAL_1:24; then
1 + (- x2) <= 1 + (- x1) by XREAL_1:7; then
max (1-x2,y) <= max (1-x1,y) by XXREAL_0:26; then
f.(x2,y) <= max (1-x1,y) by Kleene;
hence thesis by Kleene;
end;
aa: for x,y1,y2 being Element of [.0,1.] st
y1 <= y2 holds f.(x,y1) <= f.(x,y2)
proof
let x,y1,y2 be Element of [.0,1.];
assume y1 <= y2; then
max(1-x,y1) <= max(1-x,y2) by XXREAL_0:26; then
max(1-x,y1) <= f.(x,y2) by Kleene;
hence thesis by Kleene;
end;
AA: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1; then
A1: f.(0,0) = max(1-0,0) by Kleene .= 1 by XXREAL_0:def 10;
A2: f.(1,1) = max (1-1,1) by AA,Kleene .= 1 by XXREAL_0:def 10;
f.(1,0) = max(1-1,0) by AA,Kleene .= 0;
hence thesis by A1,A2,a0,aa;
end;
end;
definition
func Goguen_implication -> BinOp of [.0,1.] means :Goguen:
for x,y being Element of [.0,1.] holds
(x <= y implies it.(x,y) = 1) &
(x > y implies it.(x,y) = y / x);
existence
proof
set C = [.0,1.];
defpred P[Real,Real] means $1 <= $2;
deffunc F(Element of C,Element of C) = In(1,C);
deffunc G(Element of C,Element of C) = In($2/$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;
AA: [a,b] in dom f by A0,ZFMISC_1:87;
(a <= b implies f.(a,b) = 1) &
(a > b implies f.(a,b) = b/a)
proof
thus a <= b implies f.(a,b) = 1
proof
assume a <= b; then
f. [a,b] = F(a,b) by A1,AA
.= 1 by SUBSET_1:def 8,XXREAL_1:1;
hence thesis;
end;
assume X0: a > b; then
f. [a,b] = G(a,b) by A1,AA
.= b / a by SUBSET_1:def 8,X0,QuoIn01;
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 implies f1.(a,b) = 1) &
(a > b implies f1.(a,b) = b/a) and
A2: for a,b being Element of [.0,1.] holds
(a <= b implies f2.(a,b) = 1) &
(a > b implies f2.(a,b) = b/a);
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; then
f1.(aa,bb) = 1 by A1 .= f2.(aa,bb) by A2,B0;
hence thesis;
end;
suppose
B1: aa > bb; then
f1.(aa,bb) = bb/aa by A1 .= f2.(aa,bb) by A2,B1;
hence thesis;
end;
end;
hence thesis by BINOP_1:def 21;
end;
end;
registration
cluster Goguen_implication -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
coherence
proof
set f = Goguen_implication;
a0: for x1,x2,y being Element of [.0,1.] st
x1 <= x2 holds f.(x1,y) >= f.(x2,y)
proof
let x1,x2,y be Element of [.0,1.];
assume Z0: x1 <= x2;
per cases;
suppose U1: x2 <= y; then
x1 <= y by Z0,XXREAL_0:2; then
f.(x1,y) = 1 & f.(x2,y) = 1 by Goguen,U1;
hence thesis;
end;
suppose x2 > y; then
U2: f.(x2,y) = y / x2 by Goguen;
per cases;
suppose U5: x1 > y; then
U3: f.(x1,y) = y / x1 by Goguen;
y >= 0 by XXREAL_1:1;
hence thesis by U2,U3,Z0,XREAL_1:118,U5;
end;
suppose x1 <= y; then
f.(x1,y) = 1 by Goguen;
hence thesis by XXREAL_1:1;
end;
end;
end;
aa: for x,y1,y2 being Element of [.0,1.] st
y1 <= y2 holds f.(x,y1) <= f.(x,y2)
proof
let x,y1,y2 be Element of [.0,1.];
P1: x >= 0 by XXREAL_1:1;
assume Z2: y1 <= y2;
per cases;
suppose P2: x <= y1; then
x <= y2 by Z2,XXREAL_0:2; then
f.(x,y1) = 1 & f.(x,y2) = 1 by Goguen,P2;
hence thesis;
end;
suppose x > y1; then
P4: f.(x,y1) = y1 / x by Goguen;
per cases;
suppose x <= y2; then
f.(x,y2) = 1 by Goguen;
hence thesis by XXREAL_1:1;
end;
suppose x > y2; then
f.(x,y2) = y2 / x by Goguen;
hence thesis by P4,Z2,XREAL_1:72,P1;
end;
end;
end;
AA: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
f.(1,0) = 0 / 1 by AA,Goguen
.= 0;
hence thesis by a0,aa,AA,Goguen;
end;
end;
definition
func Rescher_implication -> BinOp of [.0,1.] means :Rescher:
for x,y being Element of [.0,1.] holds
(x <= y implies it.(x,y) = 1) &
(x > y implies it.(x,y) = 0);
existence
proof
set C = [.0,1.];
defpred P[Real,Real] means $1 <= $2;
deffunc F(Element of C,Element of C) = In(1,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;
AA: [a,b] in dom f by A0,ZFMISC_1:87;
(a <= b implies f.(a,b) = 1) &
(a > b implies f.(a,b) = 0)
proof
thus a <= b implies f.(a,b) = 1
proof
assume a <= b; then
f. [a,b] = F(a,b) by A1,AA
.= 1 by SUBSET_1:def 8,XXREAL_1:1;
hence thesis;
end;
assume a > b; 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 implies f1.(a,b) = 1) &
(a > b implies f1.(a,b) = 0) and
A2: for a,b being Element of [.0,1.] holds
(a <= b implies f2.(a,b) = 1) &
(a > b 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; then
f1.(aa,bb) = 1 by A1 .= f2.(aa,bb) by A2,B0;
hence thesis;
end;
suppose
B1: aa > bb; 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 Rescher_implication -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
coherence
proof
set f = Rescher_implication;
b0: for x1,x2,y being Element of [.0,1.] st
x1 <= x2 holds f.(x1,y) >= f.(x2,y)
proof
let x1,x2,y be Element of [.0,1.];
assume Z0: x1 <= x2;
per cases;
suppose U1: x2 <= y; then
x1 <= y by Z0,XXREAL_0:2; then
f.(x1,y) = 1 & f.(x2,y) = 1 by Rescher,U1;
hence thesis;
end;
suppose x2 > y; then
U2: f.(x2,y) = 0 by Rescher;
thus thesis by U2,Rescher;
end;
end;
ia: for x,y1,y2 being Element of [.0,1.] st
y1 <= y2 holds f.(x,y1) <= f.(x,y2)
proof
let x,y1,y2 be Element of [.0,1.];
assume Z2: y1 <= y2;
per cases;
suppose P2: x <= y1; then
x <= y2 by Z2,XXREAL_0:2; then
f.(x,y1) = 1 & f.(x,y2) = 1 by Rescher,P2;
hence thesis;
end;
suppose x > y1; then
f.(x,y1) = 0 by Rescher;
hence thesis by Rescher;
end;
end;
0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
hence thesis by b0,ia,Rescher;
end;
end;
definition
func Yager_implication -> BinOp of [.0,1.] means :Yager:
for x,y being Element of [.0,1.] holds
(x = y = 0 implies it.(x,y) = 1) &
(x > 0 or y > 0 implies it.(x,y) = y to_power x);
existence
proof
set C = [.0,1.];
defpred P[Real,Real] means $1 = $2 = 0;
deffunc F(Element of C,Element of C) = In(1,C);
deffunc G(Element of C,Element of C) = In($2 to_power $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;
AA: [a,b] in dom f by A0,ZFMISC_1:87;
(a = b = 0 implies f.(a,b) = 1) &
(a > 0 or b > 0 implies f.(a,b) = b to_power a)
proof
thus a = b = 0 implies f.(a,b) = 1
proof
assume a = b = 0; then
f. [a,b] = F(a,b) by A1,AA
.= 1 by SUBSET_1:def 8,XXREAL_1:1;
hence thesis;
end;
assume
X0: a > 0 or b > 0; then
X1: b to_power a in C by PowerIn01;
not P[a,b] by X0; then
f. [a,b] = G(a,b) by A1,AA
.= b to_power a by SUBSET_1:def 8,X1;
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 = 0 implies f1.(a,b) = 1) &
(a > 0 or b > 0 implies f1.(a,b) = b to_power a) and
A2: for a,b being Element of [.0,1.] holds
(a = b = 0 implies f2.(a,b) = 1) &
(a > 0 or b > 0 implies f2.(a,b) = b to_power a);
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.];
aa > 0 or aa = 0 by XXREAL_1:1; then
per cases by XXREAL_1:1;
suppose
B0: aa = bb = 0; then
f1.(aa,bb) = 1 by A1 .= f2.(aa,bb) by A2,B0;
hence thesis;
end;
suppose
B1: aa > 0 or bb > 0; then
f1.(aa,bb) = bb to_power aa by A1 .= f2.(aa,bb) by A2,B1;
hence thesis;
end;
end;
hence thesis by BINOP_1:def 21;
end;
end;
registration
cluster Yager_implication -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
coherence
proof
set f = Yager_implication;
ai: for x1,x2,y being Element of [.0,1.] st
x1 <= x2 holds f.(x1,y) >= f.(x2,y)
proof
let x1,x2,y be Element of [.0,1.];
JI: 0 <= x1 & 0 <= x2 by XXREAL_1:1;
ZZ: 0 <= y <= 1 by XXREAL_1:1;
assume Z0: x1 <= x2;
per cases;
suppose x2 = 0 & y = 0;
hence thesis by JI,Z0;
end;
suppose x2 <> 0 & x1 = 0 & y = 0; then
f.(x1,y) = 1 by Yager;
hence thesis by XXREAL_1:1;
end;
suppose U6: x2 <> 0 & x1 <> 0 & y = 0; then
u6: x1 > 0 & x2 > 0 by XXREAL_1:1;
u2: f.(x1,y) = y to_power x1 by Yager,U6,JI
.= 0 by u6,U6,POWER:def 2;
f.(x2,y) = y to_power x2 by Yager,U6,JI
.= 0 by JI,U6,POWER:def 2;
hence thesis by u2;
end;
suppose za: y <> 0; then
u2: f.(x1,y) = y to_power x1 by ZZ,Yager;
U2: f.(x2,y) = y to_power x2 by Yager,za,ZZ;
per cases;
suppose zz: x1 <> x2 & y <> 1;
0 < y < 1 & x1 < x2 by zz,za,ZZ,Z0,XXREAL_0:1;
hence thesis by U2,u2,POWER:40;
end;
suppose zz: x1 <> x2 & y = 1;
1 >= 1 to_power x2 by POWER:26;
hence thesis by U2,u2,zz,POWER:26;
end;
suppose x1 = x2;
hence thesis;
end;
end;
end;
b0: for x,y1,y2 being Element of [.0,1.] st
y1 <= y2 holds f.(x,y1) <= f.(x,y2)
proof
let x,y1,y2 be Element of [.0,1.];
assume Z2: y1 <= y2;
per cases;
suppose P2: x = 0 & y2 = 0;
0 <= y1 by XXREAL_1:1;
hence thesis by P2,Z2;
end;
suppose P8: x <> 0;
su: x >= 0 & y2 >= 0 by XXREAL_1:1; then
P4: f.(x,y2) = y2 to_power x by Yager,P8;
per cases;
suppose y1 = 0 & x = 0;
hence thesis by P8;
end;
suppose y1 = 0 & x <> 0; then
p4: f.(x,y1) = y1 to_power x by Yager,su;
y1 >= 0 by XXREAL_1:1;
hence thesis by p4,P4,HOLDER_1:3,Z2,su;
end;
suppose sy: y1 <> 0;
y1 >= 0 by XXREAL_1:1; then
p4: f.(x,y1) = y1 to_power x by Yager,sy;
y1 >= 0 by XXREAL_1:1;
hence thesis by p4,P4,HOLDER_1:3,Z2,su;
end;
end;
suppose P8: y2 <> 0;
su: x >= 0 & y2 >= 0 by XXREAL_1:1; then
P4: f.(x,y2) = y2 to_power x by Yager,P8;
per cases;
suppose pg: y1 = 0 & x = 0; then
f.(x,y1) = 1 by Yager;
hence thesis by P4,POWER:24,pg;
end;
suppose y1 = 0 & x <> 0; then
p4: f.(x,y1) = y1 to_power x by Yager,su;
y1 >= 0 by XXREAL_1:1;
hence thesis by p4,P4,HOLDER_1:3,Z2,su;
end;
suppose sy: y1 <> 0;
y1 >= 0 by XXREAL_1:1; then
p4: f.(x,y1) = y1 to_power x by Yager,sy;
y1 >= 0 by XXREAL_1:1;
hence thesis by p4,P4,HOLDER_1:3,Z2,su;
end;
end;
end;
AA: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
A2: f.(1,1) = 1 to_power 1 by AA,Yager .= 1 by POWER:26;
f.(1,0) = 0 to_power 1 by AA,Yager
.= 0 by POWER:def 2;
hence thesis by AA,A2,ai,b0,Yager;
end;
end;
definition
func Weber_implication -> BinOp of [.0,1.] means :Weber:
for x,y being Element of [.0,1.] holds
(x < 1 implies it.(x,y) = 1) &
(x = 1 implies it.(x,y) = y);
existence
proof
set C = [.0,1.];
defpred P[Real,Real] means $1 < 1;
deffunc F(Element of C,Element of C) = In(1,C);
deffunc G(Element of C,Element of C) = In($2,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;
AA: [a,b] in dom f by A0,ZFMISC_1:87;
(a < 1 implies f.(a,b) = 1) &
(a = 1 implies f.(a,b) = b)
proof
thus a < 1 implies f.(a,b) = 1
proof
assume a < 1; then
f. [a,b] = F(a,b) by A1,AA
.= 1 by SUBSET_1:def 8,XXREAL_1:1;
hence thesis;
end;
assume X0: a = 1;
f. [a,b] = G(a,b) by A1,AA,X0
.= b by 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 < 1 implies f1.(a,b) = 1) &
(a = 1 implies f1.(a,b) = b) and
A2: for a,b being Element of [.0,1.] holds
(a < 1 implies f2.(a,b) = 1) &
(a = 1 implies f2.(a,b) = 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.];
aa <= 1 by XXREAL_1:1; then
per cases by XXREAL_0:1;
suppose
B0: aa < 1; then
f1.(aa,bb) = 1 by A1 .= f2.(aa,bb) by A2,B0;
hence thesis;
end;
suppose
B1: aa = 1; then
f1.(aa,bb) = bb by A1 .= f2.(aa,bb) by A2,B1;
hence thesis;
end;
end;
hence thesis by BINOP_1:def 21;
end;
end;
registration
cluster Weber_implication -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
coherence
proof
set f = Weber_implication;
a0: for x1,x2,y being Element of [.0,1.] st
x1 <= x2 holds f.(x1,y) >= f.(x2,y)
proof
let x1,x2,y be Element of [.0,1.];
assume Z0: x1 <= x2;
per cases;
suppose U1: x2 < 1; then
x1 < 1 by Z0,XXREAL_0:2; then
f.(x1,y) = 1 & f.(x2,y) = 1 by Weber,U1;
hence thesis;
end;
suppose U6: x2 >= 1;
x2 <= 1 by XXREAL_1:1; then
u2: x2 = 1 by XXREAL_0:1,U6;
per cases;
suppose x1 > y & x1 < 1; then
f.(x1,y) = 1 by Weber;
hence thesis by XXREAL_1:1;
end;
suppose U5: x1 > y & x1 >= 1;
x1 <= 1 by XXREAL_1:1;
hence thesis by u2,U5,XXREAL_0:1;
end;
suppose x1 <= y & x1 < 1; then
f.(x1,y) = 1 by Weber;
hence thesis by XXREAL_1:1;
end;
suppose IO: x1 <= y & x1 >= 1;
x1 <= 1 by XXREAL_1:1;
hence thesis by u2,IO,XXREAL_0:1;
end;
end;
end;
b0: for x,y1,y2 being Element of [.0,1.] st
y1 <= y2 holds f.(x,y1) <= f.(x,y2)
proof
let x,y1,y2 be Element of [.0,1.];
P1: x >= 0 & x <= 1 by XXREAL_1:1;
assume Z2: y1 <= y2;
per cases;
suppose x < 1; then
f.(x,y1) = 1 & f.(x,y2) = 1 by Weber;
hence thesis;
end;
suppose x >= 1; then
SS: x = 1 by XXREAL_0:1,P1; then
f.(x,y1) = y1 by Weber;
hence thesis by Z2,Weber,SS;
end;
end;
0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
hence thesis by a0,b0,Weber;
end;
end;
definition
func Fodor_implication -> BinOp of [.0,1.] means :Fodor:
for x,y being Element of [.0,1.] holds
(x <= y implies it.(x,y) = 1) &
(x > y implies it.(x,y) = max(1-x,y));
existence
proof
set C = [.0,1.];
defpred P[Real,Real] means $1 <= $2;
deffunc F(Element of C,Element of C) = In(1,C);
deffunc G(Element of C,Element of C) = In(max(1-$1,$2),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;
AA: [a,b] in dom f by A0,ZFMISC_1:87;
(a <= b implies f.(a,b) = 1) &
(a > b implies f.(a,b) = max(1-a,b))
proof
thus a <= b implies f.(a,b) = 1
proof
assume a <= b; then
f. [a,b] = F(a,b) by A1,AA
.= 1 by SUBSET_1:def 8,XXREAL_1:1;
hence thesis;
end;
assume a > b; then
f. [a,b] = G(a,b) by A1,AA
.= max (1-a,b) by SUBSET_1:def 8,Max1In01;
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 implies f1.(a,b) = 1) &
(a > b implies f1.(a,b) = max(1-a,b)) and
A2: for a,b being Element of [.0,1.] holds
(a <= b implies f2.(a,b) = 1) &
(a > b implies f2.(a,b) = max(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; then
f1.(aa,bb) = 1 by A1 .= f2.(aa,bb) by A2,B0;
hence thesis;
end;
suppose
B1: aa > bb; then
f1.(aa,bb) = max(1-aa,bb) by A1 .= f2.(aa,bb) by A2,B1;
hence thesis;
end;
end;
hence thesis by BINOP_1:def 21;
end;
end;
registration
cluster Fodor_implication -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
coherence
proof
set f = Fodor_implication;
a0: for x1,x2,y being Element of [.0,1.] st
x1 <= x2 holds f.(x1,y) >= f.(x2,y)
proof
let x1,x2,y be Element of [.0,1.];
assume Z0: x1 <= x2;
per cases;
suppose U1: x2 <= y; then
x1 <= y by Z0,XXREAL_0:2; then
f.(x1,y) = 1 & f.(x2,y) = 1 by Fodor,U1;
hence thesis;
end;
suppose x2 > y; then
U2: f.(x2,y) = max (1-x2,y) by Fodor;
per cases;
suppose x1 > y; then
U3: f.(x1,y) = max (1-x1,y) by Fodor;
-x1 >= -x2 by Z0,XREAL_1:24; then
1 +- x1 >= 1 +- x2 by XREAL_1:7;
hence thesis by U2,XXREAL_0:26,U3;
end;
suppose x1 <= y; then
f.(x1,y) = 1 by Fodor;
hence thesis by XXREAL_1:1;
end;
end;
end;
b0: for x,y1,y2 being Element of [.0,1.] st
y1 <= y2 holds f.(x,y1) <= f.(x,y2)
proof
let x,y1,y2 be Element of [.0,1.];
assume Z2: y1 <= y2;
per cases;
suppose P2: x <= y1; then
x <= y2 by Z2,XXREAL_0:2; then
f.(x,y1) = 1 & f.(x,y2) = 1 by Fodor,P2;
hence thesis;
end;
suppose x > y1; then
P4: f.(x,y1) = max (1-x,y1) by Fodor;
per cases;
suppose x <= y2; then
f.(x,y2) = 1 by Fodor;
hence thesis by XXREAL_1:1;
end;
suppose x > y2; then
f.(x,y2) = max (1-x,y2) by Fodor;
hence thesis by P4,Z2,XXREAL_0:26;
end;
end;
end;
AA: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1; then
f.(1,0) = max (1-1,0) by Fodor
.= 0;
hence thesis by a0,b0,AA,Fodor;
end;
end;
begin :: Boundary Fuzzy Implications
definition
func I_{0} -> BinOp of [.0,1.] means :I0Impl:
for x,y being Element of [.0,1.] holds
(x = 0 or y = 1 implies it.(x,y) = 1) &
(x > 0 & y < 1 implies it.(x,y) = 0);
existence
proof
set C = [.0,1.];
defpred P[Real,Real] means $1 = 0 or $2 = 1;
deffunc F(Element of C,Element of C) = In(1,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;
AA: [a,b] in dom f by A0,ZFMISC_1:87;
(a = 0 or b = 1 implies f.(a,b) = 1) &
(a > 0 & b < 1 implies f.(a,b) = 0)
proof
thus a = 0 or b = 1 implies f.(a,b) = 1
proof
assume a = 0 or b = 1; then
f. [a,b] = F(a,b) by A1,AA
.= 1 by SUBSET_1:def 8,XXREAL_1:1;
hence thesis;
end;
assume X0: a > 0 & b < 1;
f. [a,b] = G(a,b) by A1,AA,X0
.= 0 by SUBSET_1:def 8,XXREAL_1:1;
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 = 0 or b = 1 implies f1.(a,b) = 1) &
(a > 0 & b < 1 implies f1.(a,b) = 0) and
A2: for a,b being Element of [.0,1.] holds
(a = 0 or b = 1 implies f2.(a,b) = 1) &
(a > 0 & 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.];
ST: 0 <= bb <= 1 by XXREAL_1:1;
per cases;
suppose
B0: aa = 0 or bb = 1; then
f1.(aa,bb) = 1 by A1 .= f2.(aa,bb) by A2,B0;
hence thesis;
end;
suppose
aa <> 0 & bb <> 1; then
B1: aa > 0 & bb < 1 by XXREAL_1:1,ST,XXREAL_0: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 I_{0} -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
coherence
proof
set f = I_{0};
b1: for x1,x2,y being Element of [.0,1.] st
x1 <= x2 holds f.(x1,y) >= f.(x2,y)
proof
let x1,x2,y be Element of [.0,1.];
assume W0: x1 <= x2;
per cases;
suppose x1 = 0 or y = 1; then
f.(x1,y) = 1 by I0Impl;
hence thesis by XXREAL_1:1;
end;
suppose W1: x1 <> 0 & y <> 1;
x1 >= 0 & y <= 1 by XXREAL_1:1; then
W2: x1 > 0 & y < 1 by W1,XXREAL_0:1; then
f.(x1,y) = 0 by I0Impl;
hence thesis by I0Impl,W2,W0;
end;
end;
b2: for x,y1,y2 being Element of [.0,1.] st
y1 <= y2 holds f.(x,y1) <= f.(x,y2)
proof
let x,y1,y2 be Element of [.0,1.];
assume WW: y1 <= y2;
per cases;
suppose y2 = 1 or x = 0; then
f.(x,y2) = 1 by I0Impl;
hence thesis by XXREAL_1:1;
end;
suppose Ww: y2 <> 1 & x <> 0;
wc: y2 <= 1 & x >= 0 by XXREAL_1:1; then
Wc: y2 < 1 & x > 0 by Ww,XXREAL_0:1; then
Wd: f.(x,y2) = 0 by I0Impl;
y1 < 1 by WW,Wc,XXREAL_0:2;
hence thesis by Wd,wc,I0Impl,Ww;
end;
end;
0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
hence thesis by b1,b2,I0Impl;
end;
end;
definition
func I_{1} -> BinOp of [.0,1.] means :I1Impl:
for x,y being Element of [.0,1.] holds
(x < 1 or y > 0 implies it.(x,y) = 1) &
(x = 1 & y = 0 implies it.(x,y) = 0);
existence
proof
set C = [.0,1.];
defpred P[Real,Real] means $1 < 1 or $2 > 0;
deffunc F(Element of C,Element of C) = In(1,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;
AA: [a,b] in dom f by A0,ZFMISC_1:87;
(a < 1 or b > 0 implies f.(a,b) = 1) &
(a = 1 & b = 0 implies f.(a,b) = 0)
proof
thus a < 1 or b > 0 implies f.(a,b) = 1
proof
assume a < 1 or b > 0; then
f. [a,b] = F(a,b) by A1,AA
.= 1 by SUBSET_1:def 8,XXREAL_1:1;
hence thesis;
end;
assume X0: a = 1 & b = 0;
f. [a,b] = G(a,b) by A1,AA,X0
.= 0 by SUBSET_1:def 8,XXREAL_1:1;
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 < 1 or b > 0 implies f1.(a,b) = 1) &
(a = 1 & b = 0 implies f1.(a,b) = 0) and
A2: for a,b being Element of [.0,1.] holds
(a < 1 or b > 0 implies f2.(a,b) = 1) &
(a = 1 & b = 0 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.];
SS: 0 <= aa <= 1 by XXREAL_1:1;
per cases;
suppose
B0: aa = 1 & bb = 0; then
f1.(aa,bb) = 0 by A1 .= f2.(aa,bb) by A2,B0;
hence thesis;
end;
suppose
aa <> 1 or bb <> 0; then
B1: aa < 1 or bb > 0 by SS,XXREAL_1:1,XXREAL_0: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;
registration
cluster I_{1} -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
coherence
proof
set f = I_{1};
b1: for x1,x2,y being Element of [.0,1.] st
x1 <= x2 holds f.(x1,y) >= f.(x2,y)
proof
let x1,x2,y be Element of [.0,1.];
assume A0: x1 <= x2;
per cases;
suppose x2 = 1 & y = 0; then
f.(x2,y) = 0 by I1Impl;
hence thesis by XXREAL_1:1;
end;
suppose W1: x2 <> 1;
x2 <= 1 by XXREAL_1:1; then
Y3: x2 < 1 by W1,XXREAL_0:1; then
Y2: f.(x2,y) = 1 by I1Impl;
x1 < 1 by XXREAL_0:2,A0,Y3;
hence thesis by Y2,I1Impl;
end;
suppose W2: y <> 0;
y4: y >= 0 by XXREAL_1:1;
f.(x1,y) = 1 by I1Impl,W2,y4;
hence thesis by XXREAL_1:1;
end;
end;
b2: for x,y1,y2 being Element of [.0,1.] st
y1 <= y2 holds f.(x,y1) <= f.(x,y2)
proof
let x,y1,y2 be Element of [.0,1.];
assume A0: y1 <= y2;
per cases;
suppose y1 = 0 & x = 1; then
f.(x,y1) = 0 by I1Impl;
hence thesis by XXREAL_1:1;
end;
suppose y1 <> 0; then
A2: y1 > 0 by XXREAL_1:1; then
f.(x,y1) = 1 by I1Impl;
hence thesis by I1Impl,A0,A2;
end;
suppose B1: x <> 1;
x <= 1 by XXREAL_1:1; then
A2: x < 1 by B1,XXREAL_0:1; then
f.(x,y1) = 1 by I1Impl;
hence thesis by A2,I1Impl;
end;
end;
0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
hence thesis by b1,b2,I1Impl;
end;
end;
definition let f be BinOp of [.0,1.];
attr f is satisfying_(LB) means
for y being Element of [.0,1.] holds
f.(0,y) = 1;
attr f is satisfying_(RB) means
for x being Element of [.0,1.] holds
f.(x,1) = 1;
end;
theorem LBProp:
for fi being Fuzzy_Implication,
y being Element of [.0,1.] holds
fi.(0,y) = 1
proof
let fi be Fuzzy_Implication,
y be Element of [.0,1.];
A1: fi.(0,0) = 1 by Def00;
B1: 0 in [.0,1.] by XXREAL_1:1;
reconsider z = 0 as Element of [.0,1.] by XXREAL_1:1;
0 <= y by XXREAL_1:1; then
B2: fi.(0,0) <= fi.(0,y) by DefIncr,B1;
fi.(z,y) in [.0,1.]; then
fi.(0,y) <= 1 by XXREAL_1:1;
hence thesis by XXREAL_0:1,A1,B2;
end;
theorem RBProp:
for fi being Fuzzy_Implication,
x being Element of [.0,1.] holds
fi.(x,1) = 1
proof
let fi be Fuzzy_Implication,
x be Element of [.0,1.];
A1: fi.(1,1) = 1 by Def11;
B1: 1 in [.0,1.] by XXREAL_1:1;
reconsider z = 1 as Element of [.0,1.] by XXREAL_1:1;
x <= 1 by XXREAL_1:1; then
B2: fi.(1,1) <= fi.(x,1) by DefDecr,B1;
fi.(x,z) in [.0,1.]; then
fi.(x,1) <= 1 by XXREAL_1:1;
hence thesis by XXREAL_0:1,A1,B2;
end;
registration
cluster -> satisfying_(LB) satisfying_(RB) for Fuzzy_Implication;
coherence by LBProp,RBProp;
end;
theorem
for fi being Fuzzy_Implication holds
I_{0} <= fi
proof
let fi be Fuzzy_Implication;
set f = I_{0};
for x,y being Element of [.0,1.] holds
f.(x,y) <= fi.(x,y)
proof
let x,y be Element of [.0,1.];
A0: x >= 0 & y <= 1 by XXREAL_1:1;
per cases;
suppose A1: x = 0 or y = 1; then
f.(x,y) = 1 by LBProp,RBProp;
hence thesis by LBProp,RBProp,A1;
end;
suppose x <> 0 & y <> 1; then
x > 0 & y < 1 by A0,XXREAL_0:1; then
f.(x,y) = 0 by I0Impl;
hence thesis by XXREAL_1:1;
end;
end;
hence thesis by FUZNORM1:def 16;
end;
theorem
for fi being Fuzzy_Implication holds
fi <= I_{1}
proof
let fi be Fuzzy_Implication;
set f = I_{1};
for x,y being Element of [.0,1.] holds
f.(x,y) >= fi.(x,y)
proof
let x,y be Element of [.0,1.];
a0: x <= 1 & y >= 0 by XXREAL_1:1;
per cases;
suppose
x <> 1 or y <> 0; then
x < 1 or y > 0 by a0,XXREAL_0:1; then
f.(x,y) = 1 by I1Impl;
hence thesis by XXREAL_1:1;
end;
suppose Aa: x = 1 & y = 0; then
f.(x,y) = 0 by I1Impl;
hence thesis by Aa,Def10;
end;
end;
hence thesis by FUZNORM1:def 16;
end;