:: Formal Introduction to Fuzzy Implications :: by Adam Grabowski :: :: Received September 3, 2017 :: Copyright (c) 2017-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XXREAL_1, REAL_1, XXREAL_0, 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;