:: Basic Properties of Fuzzy Set Operation and Membership Function
:: by Takashi Mitsuishi , Katsumi Wasaki and Yasunari Shidama
::
:: Received May 22, 2000
:: Copyright (c) 2000-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, XBOOLE_0, SUBSET_1, FUZZY_1, CARD_1, XXREAL_0, FUNCT_1,
TARSKI, ARYTM_1, RELAT_1, PARTFUN1, XXREAL_1, SEQ_4, MEMBER_1, ARYTM_3,
REAL_1, FUNCT_2, ZFMISC_1, FUNCT_3, FUZZY_2, MEASURE5;
notations TARSKI, XBOOLE_0, ORDINAL1, SUBSET_1, ZFMISC_1, NUMBERS, XXREAL_0,
XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3,
INTEGRA1, RCOMP_1, SEQ_4, FUZZY_1, MEASURE5;
constructors REAL_1, SQUARE_1, RFUNCT_1, INTEGRA1, FUZZY_1, SEQ_4, RELSET_1;
registrations RELSET_1, NUMBERS, MEMBERED, XBOOLE_0, SUBSET_1, VALUED_0,
MEASURE5, XREAL_0;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions FUZZY_1;
equalities FUZZY_1;
expansions FUZZY_1;
theorems TARSKI, FUNCT_1, PARTFUN1, INTEGRA1, INTEGRA2, FUZZY_1, XBOOLE_0,
XREAL_1, XXREAL_0, FUNCT_3, FUNCT_2, RELAT_1, MEASURE5, XREAL_0;
schemes PARTFUN1;
begin :: Basic Properties of Membership Function and Difference Set
reserve x,y,y1,y2 for set;
reserve C for non empty set;
reserve c for Element of C;
reserve f,h,g,h1 for Membership_Func of C;
theorem Th1:
for x be Element of C,h be Membership_Func of C holds 0 <= h.x & h.x <= 1
proof
let x be Element of C,h be Membership_Func of C;
(EMF C).x = 0 by FUNCT_3:def 3;
hence 0 <= h.x by FUZZY_1:16;
(UMF C).x = 1 by FUNCT_3:def 3;
hence thesis by FUZZY_1:16;
end;
theorem
f c= h implies max(f,min(g,h)) = min(max(f,g),h)
proof
assume
A1: f c= h;
thus max(f,min(g,h)) = min(max(f,g),max(f,h)) by FUZZY_1:9
.= min(max(f,g),h) by A1,FUZZY_1:22;
end;
definition
let C be non empty set;
let f,g be Membership_Func of C;
func f\g -> Membership_Func of C equals
min(f,1_minus g);
correctness;
end;
theorem
1_minus (f\g) = max(1_minus f,g)
proof
thus 1_minus (f\g) = max(1_minus f,1_minus(1_minus g)) by FUZZY_1:11
.= max(1_minus f,g);
end;
theorem Th4:
f c= g implies f\h c= g\h
proof
assume
A1: f.c <= g.c;
let c;
f.c <= g.c by A1;
then min(f.c,(1_minus h).c) <= min(g.c,(1_minus h).c) by XXREAL_0:18;
then (f\h).c <= min(g.c,(1_minus h).c) by FUZZY_1:5;
hence thesis by FUZZY_1:5;
end;
theorem
f c= g implies h\g c= h\f
proof
assume
A1: f.c <= g.c;
let c;
f.c <= g.c by A1;
then 1 - f.c >= 1 - g.c by XREAL_1:10;
then (1_minus g).c <= 1- f.c by FUZZY_1:def 5;
then (1_minus g).c <= (1_minus f).c by FUZZY_1:def 5;
then min((1_minus g).c,h.c) <= min((1_minus f).c,h.c) by XXREAL_0:18;
then (h\g).c <= min((1_minus f).c,h.c) by FUZZY_1:5;
hence thesis by FUZZY_1:5;
end;
theorem
f c= g & h c= h1 implies f\h1 c= g\h
proof
assume that
A1: f.c <= g.c and
A2: h.c <= h1.c;
let c;
h.c <= h1.c by A2;
then
A3: 1-h.c >= 1-h1.c by XREAL_1:10;
f.c <= g.c by A1;
then min(f.c,1-h1.c) <= min(g.c,1- h.c) by A3,XXREAL_0:18;
then min(f.c,(1_minus h1).c) <= min(g.c,1- h.c) by FUZZY_1:def 5;
then min(f.c,(1_minus h1).c) <= min(g.c,(1_minus h).c) by FUZZY_1:def 5;
then min(f,1_minus h1).c <= min(g.c,(1_minus h).c) by FUZZY_1:5;
hence thesis by FUZZY_1:5;
end;
theorem
f\EMF(C) = f
proof
thus f\EMF(C) = min(f,UMF(C)) by FUZZY_1:40
.= f by FUZZY_1:18;
end;
theorem
f\g c= f\min(f,g)
proof
f\min(f,g) = min(f,max(1_minus f,1_minus g)) by FUZZY_1:11
.=max(min(f,1_minus f),f\g) by FUZZY_1:9;
hence thesis by FUZZY_1:17;
end;
theorem
max(min(f,g),f\g) c= f
proof
A1: f\g c= f by FUZZY_1:17;
min(f,g) c= f by FUZZY_1:17;
hence thesis by A1,FUZZY_1:19;
end;
theorem
max(f,g\f) c= max(f,g)
proof
max(f,g\f) = min(max(f,g),max(f,1_minus f)) by FUZZY_1:9;
hence thesis by FUZZY_1:17;
end;
theorem
f\(g\h) = max(f\g,min(f,h))
proof
f\(g\h) = min(f,max(1_minus g,1_minus(1_minus h))) by FUZZY_1:11
.= max(min(f,1_minus g),min(f,h)) by FUZZY_1:9;
hence thesis;
end;
theorem
min(f,g) c= f\(f\g)
proof
f\(f\g) = min(f,max(1_minus f,1_minus(1_minus g))) by FUZZY_1:11
.= max(min(f,1_minus f),min(f,g)) by FUZZY_1:9;
hence thesis by FUZZY_1:17;
end;
theorem
f\g c= max(f,g)\g by Th4,FUZZY_1:17;
theorem
f\max(g,h) = min(f\g,f\h)
proof
thus f\max(g,h) = min(min(f,f),min(1_minus g,1_minus h)) by FUZZY_1:11
.= min(f,min(f,min(1_minus g,1_minus h))) by FUZZY_1:7
.= min(f,min(min(f,1_minus g),1_minus h)) by FUZZY_1:7
.= min(f\g,f\h) by FUZZY_1:7;
end;
theorem
f\min(g,h) = max(f\g,f\h)
proof
thus f\min(g,h) = min(f,max(1_minus g,1_minus h)) by FUZZY_1:11
.= max(f\g,f\h) by FUZZY_1:9;
end;
theorem
(f\g)\h = f\max(g,h)
proof
thus (f\g)\h = min(f,min(1_minus g,1_minus h)) by FUZZY_1:7
.= f\max(g,h) by FUZZY_1:11;
end;
theorem
f \+\ g c= max(f,g)\min(f,g)
proof
let c;
(max(f,g)\min(f,g)).c = min(max(f,g),max(1_minus(f),1_minus(g))).c by
FUZZY_1:11
.= max(min(max(f,g),1_minus f),min(max(f,g),1_minus g)).c by FUZZY_1:9
.= max(max(min(1_minus f,f),min(1_minus f,g)),min(1_minus g,max(f,g))).c
by FUZZY_1:9
.= max(max(min(1_minus f,f),min(1_minus f,g)) ,max(min(1_minus g,f),min(
1_minus g,g))).c by FUZZY_1:9
.= max(max(max(min(1_minus f,f),min(1_minus f,g)),min(1_minus g,f)), min
(1_minus g,g)).c by FUZZY_1:7
.= max(max(min(1_minus f,f),max(min(1_minus f,g),min(1_minus g,f))), min
(1_minus g,g)).c by FUZZY_1:7
.= max(max(min(1_minus f,g),min(1_minus g,f)), max(min(1_minus f,f),min(
1_minus g,g))).c by FUZZY_1:7
.= max((f \+\ g).c, max(min(1_minus f,f),min(1_minus g,g)).c) by FUZZY_1:5;
hence thesis by XXREAL_0:25;
end;
theorem
f\g c= h & g\f c= h implies f \+\ g c= h
proof
assume that
A1: (f\g).c <= h.c and
A2: (g\f).c <= h.c;
let c;
A3: min(g,1_minus f).c <= h.c by A2;
min(f,1_minus g).c <= h.c by A1;
then max(min(f,1_minus g).c,min(g,1_minus f).c) <= max(h.c,h.c) by A3,
XXREAL_0:26;
hence thesis by FUZZY_1:5;
end;
theorem
min(f,g\h) c= min(f,g)\min(f,h)
proof
let c;
(1_minus h).c <= max((1_minus f).c,(1_minus h).c) by XXREAL_0:25;
then min(min(f,g).c,(1_minus h).c) <= min(min(f,g).c,max((1_minus f).c,(
1_minus h).c)) by XXREAL_0:18;
then
min(min(f,g).c,(1_minus h).c) <= min(min(f,g).c,max(1_minus f,1_minus h)
.c) by FUZZY_1:5;
then
A1: min(min(f,g).c,(1_minus h).c) <= min(min(f,g),max(1_minus f,1_minus h)).
c by FUZZY_1:5;
min(f,g\h).c = min(min(f,g),1_minus h).c by FUZZY_1:7
.= min(min(f,g).c,(1_minus h).c) by FUZZY_1:5;
hence thesis by A1,FUZZY_1:11;
end;
theorem Th20:
f \+\ g c= max(f,g)\min(f,g)
proof
let c;
(max(f,g)\min(f,g)).c = min(max(f,g),max(1_minus f,1_minus g)).c by
FUZZY_1:11
.= max(min(max(f,g),1_minus f),min(max(f,g),1_minus g)).c by FUZZY_1:9
.= max(max(min(1_minus f,f),min(1_minus f,g)),min(1_minus g,max(f,g))).c
by FUZZY_1:9
.= max(max(min(1_minus f,f),min(1_minus f,g)), max(min(1_minus g,f),min(
1_minus g,g))).c by FUZZY_1:9
.= max(max(max(min(1_minus f,f),min(1_minus f,g)),min(1_minus g,g)) ,min
(1_minus g,f)).c by FUZZY_1:7
.= max(max(max(min(1_minus f,f),min(1_minus g,g)),min(1_minus f,g)) ,min
(1_minus g,f)).c by FUZZY_1:7
.= max(max(min(1_minus f,f),min(1_minus g,g)),max(min(1_minus f,g) ,min(
1_minus g,f))).c by FUZZY_1:7
.= max(max(min(1_minus f,f),min(1_minus g,g)).c, (f \+\ g).c) by FUZZY_1:5;
hence thesis by XXREAL_0:25;
end;
theorem Th21:
max(min(f,g),1_minus max(f,g)) c= 1_minus (f \+\ g)
proof
f \+\ g c= max(f,g)\min(f,g) by Th20;
then 1_minus (max(f,g)\min(f,g)) c= 1_minus (f \+\ g) by FUZZY_1:36;
then
max(1_minus max(f,g),1_minus(1_minus min(f,g))) c= 1_minus (f \+\ g) by
FUZZY_1:11;
hence thesis;
end;
theorem
(f \+\ g)\h = max(f\max(g,h),g\max(f,h))
proof
set f1 = 1_minus f, g1 = 1_minus g, h1 = 1_minus h;
max(min(f,g1),min(f1,g))\h = max(min(h1,min(f,g1)),min(h1,min(f1,g))) by
FUZZY_1:9
.= max(min(min(h1,g1),f),min(h1,min(f1,g))) by FUZZY_1:7
.= max(min(min(h1,g1),f),min(min(h1,f1),g)) by FUZZY_1:7
.= max(min(f,1_minus max(h,g)),min(g,min(h1,f1))) by FUZZY_1:11
.= max(f\max(h,g),g\max(f,h)) by FUZZY_1:11;
hence thesis;
end;
theorem
max(f\ max(g,h),min(min(f,g),h)) c= f\(g \+\ h)
proof
max(f\ max(g,h),min(min(f,g),h)) = max(min(f,1_minus max(g,h)),min(f,min
(g,h))) by FUZZY_1:7
.= min(f,max(1_minus max(g,h),min(g,h))) by FUZZY_1:9;
hence thesis by Th21,FUZZY_1:25;
end;
theorem
f c= g implies max(f,g\f) c= g
proof
assume
A1: f.c <= g.c;
let c;
A2: f.c <= g.c by A1;
max(f,g\f).c = min(max(f,g),max(f,1_minus f)).c by FUZZY_1:9
.= min(max(f,g).c,max(f,1_minus f).c) by FUZZY_1:5
.= min(max(f.c,g.c),max(f,1_minus f).c) by FUZZY_1:5
.= min(g.c,max(f,1_minus f).c) by A2,XXREAL_0:def 10;
hence thesis by XXREAL_0:17;
end;
theorem
max(f \+\ g,min(f,g)) c= max(f,g)
proof
set f1 = 1_minus f, g1 = 1_minus g;
let c;
max(f \+\ g,min(f,g)) = max(min(f,g1),max(min(f1,g),min(f,g))) by FUZZY_1:7
.= max(min(f,g1),min(max(min(f1,g),f),max(min(f1,g),g))) by FUZZY_1:9
.= max(min(f,g1),min(max(min(f1,g),f),g)) by FUZZY_1:8
.= min(max(min(f,g1),max(min(f1,g),f)),max(min(f,g1),g)) by FUZZY_1:9;
then
max(f \+\ g,min(f,g)).c = min(max(min(f,g1),max(min(f1,g),f)).c,max(min(
f,g1),g).c) by FUZZY_1:5;
then
A1: max(f \+\ g, min(f,g)).c <= max(min(f,g1),g).c by XXREAL_0:17;
max(min(f,g1),g).c = min(max(g,f),max(g,g1)).c by FUZZY_1:9
.= min(max(f,g).c,max(g,g1).c) by FUZZY_1:5;
then max(min(f,g1),g).c <= max(f,g).c by XXREAL_0:17;
hence thesis by A1,XXREAL_0:2;
end;
theorem Th26:
f\g = EMF(C) implies f c= g
proof
assume
A1: f\g = EMF(C);
let c;
A2: min(f.c,(1_minus g).c) = (EMF(C)).c by A1,FUZZY_1:5;
per cases by A2,XXREAL_0:15;
suppose
f.c = (EMF(C)).c;
hence thesis by FUZZY_1:16;
end;
suppose
A3: (1_minus g).c = (EMF(C)).c;
g.c = (1_minus (1_minus g)).c .= 1 - (1_minus g).c by FUZZY_1:def 5
.= (1_minus EMF(C)).c by A3,FUZZY_1:def 5
.= (UMF(C)).c by FUZZY_1:40;
hence thesis by FUZZY_1:16;
end;
end;
theorem Th27:
min(f,g) = EMF(C) implies f\g = f
proof
A1: C = dom f by FUNCT_2:def 1;
assume
A2: min(f,g) = EMF(C);
A3: for x being Element of C st x in C holds min(f,1_minus g).x = f.x
proof
let x be Element of C;
A4: (EMF C).x = min(f.x,g.x) by A2,FUZZY_1:5;
per cases by A4,XXREAL_0:15;
suppose
A5: f.x = (EMF(C)).x;
min(f,1_minus g).x = min(f.x,(1_minus g).x) by FUZZY_1:5
.= min(1_minus g,EMF(C)).x by A5,FUZZY_1:5
.= (EMF(C)).x by FUZZY_1:18;
hence thesis by A5;
end;
suppose
A6: g.x = (EMF(C)).x;
min(f,1_minus g).x = min(f.x,(1_minus g).x) by FUZZY_1:5
.= min(f.x,1 - (EMF(C)).x) by A6,FUZZY_1:def 5
.= min(f.x,(1_minus EMF(C)).x) by FUZZY_1:def 5
.= min(f.x,(UMF(C)).x) by FUZZY_1:40
.= min(f,UMF(C)).x by FUZZY_1:5;
hence thesis by FUZZY_1:18;
end;
end;
C = dom min(f,1_minus g) by FUNCT_2:def 1;
hence thesis by A1,A3,PARTFUN1:5;
end;
begin :: Algebraic Product and Algebraic Sum
reconsider jj=1 as Real;
definition
let C be non empty set;
let h,g be Membership_Func of C;
func h*g -> Membership_Func of C means
:Def2:
for c being Element of C holds it.c = (h.c)*(g.c);
existence
proof
defpred P[object,object] means $2 = (h.$1)*(g.$1);
A1: for x,y1,y2 being object st x in C & P[x,y1] & P[x,y2] holds y1=y2;
A2: for x,y being object st x in C & P[x,y] holds y in REAL by XREAL_0:def 1;
consider IT being PartFunc of C,REAL such that
A3: (for x being object holds x in dom IT iff x in C &
ex y being object st P[x,y]) &
for x being object st x
in dom IT holds P[x,IT.x] from PARTFUN1:sch 2(A2,A1);
for x being object st x in C holds x in dom IT
proof
let x be object;
A4: ex y st y = (h.x)*(g.x);
assume x in C;
hence thesis by A3,A4;
end;
then C c= dom IT by TARSKI:def 3;
then
A5: dom IT = C by XBOOLE_0:def 10;
then
A6: for c being Element of C holds IT.c = (h.c)*(g.c) by A3;
A7: rng g c= [.0,1.] by RELAT_1:def 19;
A8: rng h c= [.0,1.] by RELAT_1:def 19;
for y being object st y in rng IT holds y in [.0,1.]
proof
reconsider A=[.0,jj.] as
non empty closed_interval Subset of REAL by MEASURE5:14;
let y be object;
assume y in rng IT;
then consider x being Element of C such that
A9: x in dom IT and
A10: y = IT.x by PARTFUN1:3;
A11: A = [. lower_bound A, upper_bound A .] by INTEGRA1:4;
then
A12: 0=lower_bound A by INTEGRA1:5;
A13: x in C;
then x in dom h by FUNCT_2:def 1;
then
A14: h.x in rng h by FUNCT_1:def 3;
then
A15: 0 <= h.x by A8,A12,INTEGRA2:1;
A16: 1=upper_bound A by A11,INTEGRA1:5;
x in dom g by A13,FUNCT_2:def 1;
then
A17: g.x in rng g by FUNCT_1:def 3;
then
A18: g.x <= 1 by A7,A16,INTEGRA2:1;
0 <= g.x by A7,A12,A17,INTEGRA2:1;
then 0 <= (h.x)*(g.x) by A15,XREAL_1:127;
then
A19: 0 <= IT.x by A3,A9;
h.x <= 1 by A8,A16,A14,INTEGRA2:1;
then (h.x)*(g.x) <= 1 by A15,A18,XREAL_1:160;
then IT.x <= 1 by A3,A9;
hence thesis by A10,A12,A16,A19,INTEGRA2:1;
end;
then rng IT c= [.0,1.] by TARSKI:def 3;
then IT is Membership_Func of C by A5,FUNCT_2:def 1,RELAT_1:def 19;
hence thesis by A6;
end;
uniqueness
proof
let F,G be Membership_Func of C;
assume that
A20: for c being Element of C holds F.c = (h.c)*(g.c) and
A21: for c being Element of C holds G.c = (h.c)*(g.c);
A22: for c being Element of C st c in C holds F.c = G.c
proof
let c be Element of C;
F.c = (h.c)*(g.c) by A20;
hence thesis by A21;
end;
A23: C = dom G by FUNCT_2:def 1;
C = dom F by FUNCT_2:def 1;
hence thesis by A23,A22,PARTFUN1:5;
end;
commutativity;
end;
definition
let C be non empty set;
let h,g be Membership_Func of C;
func h ++ g -> Membership_Func of C means
:Def3:
for c being Element of C holds it.c = h.c + g.c -(h.c)*(g.c);
existence
proof
defpred P[object,object] means $2 = h.$1 + g.$1 -(h.$1)*(g.$1);
A1: for x,y1,y2 being object st x in C & P[x,y1] & P[x,y2] holds y1=y2;
A2: for x,y being object st x in C & P[x,y] holds y in REAL by XREAL_0:def 1;
consider IT being PartFunc of C,REAL such that
A3: (for x being object holds x in dom IT iff x in C &
ex y being object st P[x,y]) &
for x being object st x
in dom IT holds P[x,IT.x] from PARTFUN1:sch 2(A2,A1);
for x being object st x in C holds x in dom IT
proof
let x be object;
A4: ex y st y = h.x + g.x -(h.x)*(g.x);
assume x in C;
hence thesis by A3,A4;
end;
then C c= dom IT by TARSKI:def 3;
then
A5: dom IT = C by XBOOLE_0:def 10;
then
A6: for c being Element of C holds IT.c = h.c + g.c -(h.c)*(g.c) by A3;
for y being object st y in rng IT holds y in [.0,1.]
proof
reconsider A=[.0,jj.] as
non empty closed_interval Subset of REAL by MEASURE5:14;
let y be object;
assume y in rng IT;
then consider x being Element of C such that
A7: x in dom IT and
A8: y = IT.x by PARTFUN1:3;
0 <= (1_minus h).x by Th1;
then
A9: 0 <= 1-h.x by FUZZY_1:def 5;
(1_minus g).x <= 1 by Th1;
then
A10: 1-g.x <= 1 by FUZZY_1:def 5;
(1_minus h).x <= 1 by Th1;
then 1-h.x <= 1 by FUZZY_1:def 5;
then (1-h.x)*(1-g.x) <= 1 by A9,A10,XREAL_1:160;
then 1 - (1-h.x)*(1-g.x) >= 1 - 1 by XREAL_1:10;
then 0 <= h.x + g.x -(h.x)*(g.x);
then
A11: 0 <= IT.x by A3,A7;
A12: A = [. lower_bound A, upper_bound A .] by INTEGRA1:4;
then
A13: 1=upper_bound A by INTEGRA1:5;
0 <= (1_minus g).x by Th1;
then 0 <= 1- g.x by FUZZY_1:def 5;
then 0 <= (1-h.x)*(1-g.x) by A9,XREAL_1:127;
then 1-0 >= 1 -(1-h.x)*(1-g.x) by XREAL_1:10;
then h.x + g.x -(h.x)*(g.x) <= 1;
then
A14: IT.x <= 1 by A3,A7;
0=lower_bound A by A12,INTEGRA1:5;
hence thesis by A8,A13,A11,A14,INTEGRA2:1;
end;
then rng IT c= [.0,1.] by TARSKI:def 3;
then IT is Membership_Func of C by A5,FUNCT_2:def 1,RELAT_1:def 19;
hence thesis by A6;
end;
uniqueness
proof
let F,G be Membership_Func of C;
assume that
A15: for c being Element of C holds F.c = h.c + g.c -(h.c)*(g.c) and
A16: for c being Element of C holds G.c = h.c + g.c -(h.c)*(g.c);
A17: for c being Element of C st c in C holds F.c = G.c
proof
let c be Element of C;
F.c = h.c + g.c -(h.c)*(g.c) by A15;
hence thesis by A16;
end;
A18: C = dom G by FUNCT_2:def 1;
C = dom F by FUNCT_2:def 1;
hence thesis by A18,A17,PARTFUN1:5;
end;
commutativity;
end;
theorem Th28:
f*f c= f & f c= f ++ f
proof
thus f*f c= f
proof
let c;
A1: 0 <= f.c by Th1;
f.c <= 1 by Th1;
then (f.c)*(f.c) <= 1*(f.c) by A1,XREAL_1:64;
hence thesis by Def2;
end;
let c;
A2: 0 <= f.c by Th1;
0 <= (1_minus f).c by Th1;
then 0*(f.c) <= (f.c)*((1_minus f).c) by A2,XREAL_1:64;
then 0 <= (f.c)*(1 - f.c) by FUZZY_1:def 5;
then 0 + f.c <= f.c - (f.c)*(f.c) + f.c by XREAL_1:6;
then f.c <= f.c + f.c - (f.c)*(f.c);
hence thesis by Def3;
end;
theorem Th29:
(f*g)*h = f*(g*h)
proof
A1: C = dom (f*(g*h)) by FUNCT_2:def 1;
A2: for c being Element of C st c in C holds ((f*g)*h).c = (f*(g*h)).c
proof
let c;
((f*g)*h).c = ((f*g).c)*(h.c) by Def2
.= ((f.c)*(g.c))*(h.c) by Def2
.= (f.c)*((g.c)*(h.c))
.= (f.c)*((g*h).c) by Def2;
hence thesis by Def2;
end;
C = dom ((f*g)*h) by FUNCT_2:def 1;
hence thesis by A1,A2,PARTFUN1:5;
end;
theorem
(f ++ g) ++ h = f ++ (g ++ h)
proof
A1: C = dom(f ++ (g ++ h)) by FUNCT_2:def 1;
A2: for c being Element of C st c in C holds ((f ++ g) ++ h).c = (f ++ (g ++
h)).c
proof
let c;
set x = f.c, y = g.c, z = h.c;
A3: (f ++ (g ++ h)).c = x + (g ++ h).c -x*((g ++ h).c) by Def3
.= x + (y + z -y*z) -x*((g ++ h).c) by Def3
.= x + (y + z) -y*z -x*(y + z -y*z) by Def3
.= -y*z -x*y - x*z +x*y*z + (x + y + z);
((f ++ g) ++ h).c = (f ++ g).c + h.c - ((f ++ g).c)*(h.c) by Def3
.= f.c + g.c -(f.c)*(g.c) + h.c - ((f ++ g).c)*(h.c) by Def3
.= (-x*y + (x + y)) + z - (x + y -x*y)*z by Def3
.= -x*y - x*z - y*z +x*y*z + (x + y + z);
hence thesis by A3;
end;
C = dom((f ++ g) ++ h) by FUNCT_2:def 1;
hence thesis by A1,A2,PARTFUN1:5;
end;
theorem
f*(f ++ g) c= f & f c= f ++ (f*g)
proof
thus f*(f ++ g) c= f
proof
let c;
A1: (f ++ g).c <= 1 by Th1;
0 <= f.c by Th1;
then ((f ++ g).c)*(f.c) <= 1*(f.c) by A1,XREAL_1:64;
hence thesis by Def2;
end;
let c;
A2: (1_minus f).c >= 0 by Th1;
(f*g).c >= 0 by Th1;
then 0*((f*g).c) <= ((1_minus f).c)*((f*g).c) by A2,XREAL_1:64;
then 0 <= (1 - f.c)*((f*g).c) by FUZZY_1:def 5;
then 0+f.c <= (f*g).c - (f.c)*((f*g).c) + f.c by XREAL_1:6;
then f.c <= f.c + (f*g).c - (f.c)*((f*g).c);
hence thesis by Def3;
end;
theorem
f*(g ++ h) c= (f*g) ++ (f*h)
proof
let c;
set x = f.c, y = g.c, z = h.c;
f*f c= f by Th28;
then
A1: (f*f).c <= f.c;
(g*h).c >= 0 by Th1;
then ((f*f).c)*((g*h).c) <= (f.c)*((g*h).c) by A1,XREAL_1:64;
then
((f*g).c + (f*h).c ) - ((f*f).c)*((g*h).c) >= ((f*g).c + (f*h).c) - (f.c
)*((g*h).c) by XREAL_1:10;
then
((f*g).c + (f*h).c ) - ((f*f)*(g*h)).c >= ((f*g).c + (f*h).c) - (f.c)*((
g*h).c) by Def2;
then
((f*g).c + (f*h).c ) - ((f*f)*(g*h)).c >= (x*y + (f*h).c) - (f.c)*((g*h)
.c) by Def2;
then ((f*g).c + (f*h).c ) - ((f*f)*(g*h)).c >= x*y+x*z - (f.c)*((g*h).c) by
Def2;
then (f*g).c + (f*h).c - ((f* (f*(g*h)))).c >= x*y+x*z - (f.c)*((g*h).c) by
Th29;
then (f*g).c + (f*h).c - ((f*((g*f)*h))).c >= (y + z - (g*h).c)*x by Th29;
then (f*g).c + (f*h).c - (((f*g)*(f*h))).c >= (y + z - (g*h).c)*x by Th29;
then (f*g).c + (f*h).c - (((f*g)*(f*h))).c >= x*(y + z - y*z) by Def2;
then (f*g).c + (f*h).c - ((f*g).c)*((f*h).c) >= x*(y + z - y*z) by Def2;
then ((f*g) ++(f*h)).c >= x*(y + z - y*z) by Def3;
then ((f*g) ++(f*h)).c >= x*((g ++ h).c) by Def3;
hence thesis by Def2;
end;
theorem
(f ++ g)*(f ++ h) c= f ++ (g*h)
proof
let c;
set x = f.c, y = g.c, z = h.c;
f*f c= f by Th28;
then (f*f).c <= f.c;
then x*x <= x by Def2;
then
A1: x*x - x <= 0 by XREAL_1:47;
0<=(1_minus (g++h)).c by Th1;
then
A2: ((1_minus (g++h)).c)*(-x+ x*x) <= 0*(-x+ x*x) by A1,XREAL_1:65;
((f ++ g)*(f ++ h)).c - (f ++ (g*h)).c = ((f ++ g).c)*((f ++ h).c) - (f
++ (g*h)).c by Def2
.= (x + y - x*y)*((f ++ h).c) - (f ++ (g*h)).c by Def3
.= (x + y - x*y)*(x + z - x*z) - (f ++ (g*h)).c by Def3
.= (x + y - x*y)*(x + z - x*z) - (x + (g*h).c - x*((g*h).c)) by Def3
.= (x + y - x*y)*(x + z - x*z) - (x + y*z - x*((g*h).c)) by Def2
.= (x - x*y + y)*(x + z - x*z) - (x + y*z - (y*z)*x) by Def2
.= x*(y +z -y*z -1)+( - y+y*z -z +1)*(x*x)
.= x*((g++h).c -1)+( - (y+z-y*z) +1)*(x*x) by Def3
.= x*(-(-(g++h).c +1))+( - (g++h).c +1)*(x*x) by Def3
.= (1-(g++h).c)*(-x+ x*x)
.=((1_minus (g++h)).c)*(-x+ x*x) by FUZZY_1:def 5;
hence thesis by A2,XREAL_1:50;
end;
theorem
1_minus (f*g) = (1_minus f) ++ (1_minus g)
proof
A1: C = dom ((1_minus f) ++ (1_minus g)) by FUNCT_2:def 1;
A2: for c being Element of C st c in C holds (1_minus (f*g)).c = ((1_minus f
) ++ (1_minus g)).c
proof
let c;
((1_minus f) ++ (1_minus g)).c = (1_minus f).c + (1_minus g).c - ((
1_minus f).c)*((1_minus g).c) by Def3
.= 1 - f.c + (1_minus g).c - ((1_minus f).c)*((1_minus g).c) by
FUZZY_1:def 5
.= 1 - f.c + (1- g.c) - ((1_minus f).c)*((1_minus g).c) by FUZZY_1:def 5
.= 1 - f.c + (1- g.c) - (1 - f.c)*((1_minus g).c) by FUZZY_1:def 5
.= 1 - f.c + (1- g.c) - (1 - f.c)*(1- g.c) by FUZZY_1:def 5
.= g.c- g.c + 1 - f.c*g.c
.= 1 - (f*g).c by Def2;
hence thesis by FUZZY_1:def 5;
end;
C = dom 1_minus (f*g) by FUNCT_2:def 1;
hence thesis by A1,A2,PARTFUN1:5;
end;
theorem
1_minus(f ++ g) = (1_minus f)*(1_minus g)
proof
A1: C = dom ((1_minus f)*(1_minus g)) by FUNCT_2:def 1;
A2: for c being Element of C st c in C holds (1_minus(f ++ g)).c = ((1_minus
f)*(1_minus g)).c
proof
let c;
((1_minus f)*(1_minus g)).c = ((1_minus f).c)*((1_minus g).c) by Def2
.= (1 - f.c)*((1_minus g).c) by FUZZY_1:def 5
.= (1 - f.c)*(1- g.c) by FUZZY_1:def 5
.= 1 - (f.c+ g.c - f.c*g.c)
.= 1 - (f ++ g).c by Def3;
hence thesis by FUZZY_1:def 5;
end;
C = dom 1_minus(f ++ g) by FUNCT_2:def 1;
hence thesis by A1,A2,PARTFUN1:5;
end;
theorem Th36:
f ++ g = 1_minus((1_minus f)*(1_minus g))
proof
A1: C = dom 1_minus((1_minus f)*(1_minus g)) by FUNCT_2:def 1;
A2: for c being Element of C st c in C holds (f ++ g).c = (1_minus((1_minus
f)*(1_minus g))).c
proof
let c;
(1_minus((1_minus f)*(1_minus g))).c = 1 - ((1_minus f)*(1_minus g)).c
by FUZZY_1:def 5
.= 1 - ((1_minus f).c)*((1_minus g).c) by Def2
.= 1 - (1 - f.c)*((1_minus g).c) by FUZZY_1:def 5
.= 1 - (1 - f.c)*(1 - g.c) by FUZZY_1:def 5
.= f.c + g.c - f.c*g.c;
hence thesis by Def3;
end;
C = dom (f ++ g) by FUNCT_2:def 1;
hence thesis by A1,A2,PARTFUN1:5;
end;
theorem
f*(EMF(C)) = EMF(C) & f*(UMF(C)) = f
proof
A1: C = dom (f*EMF(C)) by FUNCT_2:def 1;
A2: C = dom f by FUNCT_2:def 1;
A3: for c being Element of C st c in C holds (f*(UMF(C))).c = f.c
proof
let c;
(f*(UMF(C))).c = (f.c)*((UMF(C)).c) by Def2
.= (f.c)*1 by FUNCT_3:def 3;
hence thesis;
end;
A4: for c being Element of C st c in C holds (f*(EMF C)).c = (EMF C).c
proof
let c;
(f*EMF(C)).c = (f.c)*((EMF C).c) by Def2
.= (f.c)*0 by FUNCT_3:def 3;
hence thesis by FUNCT_3:def 3;
end;
A5: C = dom (f*UMF C) by FUNCT_2:def 1;
C = dom EMF(C) by FUNCT_2:def 1;
hence thesis by A1,A4,A2,A5,A3,PARTFUN1:5;
end;
theorem
f ++ EMF(C) = f & f ++ UMF(C) = UMF(C)
proof
A1: C = dom (f ++ EMF(C)) by FUNCT_2:def 1;
A2: C = dom UMF(C) by FUNCT_2:def 1;
A3: for c being Element of C st c in C holds (f ++ UMF(C)).c = (UMF(C)).c
proof
let c;
(f ++ UMF(C)).c = f.c + (UMF(C)).c - (f.c)*((UMF(C)).c) by Def3
.= (UMF(C)).c+f.c - (f.c)*1 by FUNCT_3:def 3
.= (UMF(C)).c + (f.c - f.c);
hence thesis;
end;
A4: for c being Element of C st c in C holds (f ++ EMF(C)).c = f.c
proof
let c;
(f ++ EMF(C)).c = f.c + (EMF(C)).c - (f.c)*((EMF(C)).c) by Def3
.= f.c + 0 - (f.c)*((EMF(C)).c) by FUNCT_3:def 3
.= f.c - (f.c)*0 by FUNCT_3:def 3;
hence thesis;
end;
A5: C = dom (f ++ UMF(C)) by FUNCT_2:def 1;
C = dom f by FUNCT_2:def 1;
hence thesis by A1,A4,A2,A5,A3,PARTFUN1:5;
end;
theorem
f*g c= min(f,g)
proof
let c;
A1: min(f,g).c = min(f.c,g.c) by FUZZY_1:5;
per cases by A1,XXREAL_0:15;
suppose
A2: min(f,g).c = f.c;
A3: f.c >= 0 by Th1;
g.c <= 1 by Th1;
then (g.c)*(f.c) <= 1*(f.c) by A3,XREAL_1:64;
hence thesis by A2,Def2;
end;
suppose
A4: min(f,g).c = g.c;
A5: g.c >= 0 by Th1;
f.c <= 1 by Th1;
then (f.c)*(g.c) <= 1*(g.c) by A5,XREAL_1:64;
hence thesis by A4,Def2;
end;
end;
theorem
max(f,g) c= f ++ g
proof
let c;
A1: max(f,g).c = max(f.c,g.c) by FUZZY_1:5;
per cases by A1,XXREAL_0:16;
suppose
A2: max(f,g).c = f.c;
A3: (1_minus f).c >= 0 by Th1;
g.c >= 0 by Th1;
then 0*(g.c) <= (g.c)*((1_minus f).c) by A3,XREAL_1:64;
then 0 <= (g.c)*(1 - f.c) by FUZZY_1:def 5;
then 0 + f.c <= g.c - (f.c)*(g.c) + f.c by XREAL_1:6;
then f.c <= f.c + g.c - (f.c)*(g.c);
hence thesis by A2,Def3;
end;
suppose
A4: max(f,g).c = g.c;
A5: (1_minus g).c >= 0 by Th1;
f.c >= 0 by Th1;
then 0*(f.c) <= (f.c)*((1_minus g).c) by A5,XREAL_1:64;
then 0 <= (f.c)*(1 - g.c) by FUZZY_1:def 5;
then 0 + g.c <= f.c - (f.c)*(g.c) + g.c by XREAL_1:6;
then g.c <= f.c + g.c - (f.c)*(g.c);
hence thesis by A4,Def3;
end;
end;
Lm1: for a,b,c be Real st 0 <= c holds c*min(a,b) = min(c*a,c*b)
proof
let a,b,c be Real;
assume
A1: 0 <= c;
per cases by XXREAL_0:15;
suppose
A2: min(a,b) = a;
then a <= b by XXREAL_0:def 9;
then a*c <= b*c by A1,XREAL_1:64;
hence thesis by A2,XXREAL_0:def 9;
end;
suppose
A3: min(a,b) = b;
then a >= b by XXREAL_0:def 9;
then a*c >= b*c by A1,XREAL_1:64;
hence thesis by A3,XXREAL_0:def 9;
end;
end;
Lm2: for a,b,c be Real st 0 <= c holds c*max(a,b) = max(c*a,c*b)
proof
let a,b,c be Real;
assume
A1: 0 <= c;
per cases by XXREAL_0:16;
suppose
A2: max(a,b) = b;
then a <= b by XXREAL_0:def 10;
then a*c <= c*b by A1,XREAL_1:64;
hence thesis by A2,XXREAL_0:def 10;
end;
suppose
A3: max(a,b) = a;
then a >= b by XXREAL_0:def 10;
then a*c >= b*c by A1,XREAL_1:64;
hence thesis by A3,XXREAL_0:def 10;
end;
end;
theorem
for a,b,c be Real st 0 <= c holds c*max(a,b) = max(c*a,c*b) & c*min(a,
b) = min(c*a,c*b) by Lm1,Lm2;
theorem
for a,b,c be Real holds c + max(a,b) = max(c+a,c+b) & c + min(a,b) =
min(c+a,c+b)
proof
let a,b,c be Real;
A1: c + min(a,b) = min(c+a,c+b)
proof
per cases by XXREAL_0:15;
suppose
A2: min(a,b) = a;
then a <= b by XXREAL_0:def 9;
then a+c <= c+b by XREAL_1:6;
hence thesis by A2,XXREAL_0:def 9;
end;
suppose
A3: min(a,b) = b;
then a >= b by XXREAL_0:def 9;
then a+c >= b+c by XREAL_1:6;
hence thesis by A3,XXREAL_0:def 9;
end;
end;
c + max(a,b) = max(c+a,c+b)
proof
per cases by XXREAL_0:16;
suppose
A4: max(a,b) = b;
then a <= b by XXREAL_0:def 10;
then c+a <= c+b by XREAL_1:6;
hence thesis by A4,XXREAL_0:def 10;
end;
suppose
A5: max(a,b) = a;
then a >= b by XXREAL_0:def 10;
then a+c >= b+c by XREAL_1:6;
hence thesis by A5,XXREAL_0:def 10;
end;
end;
hence thesis by A1;
end;
theorem
f*max(g,h) = max(f*g,f*h)
proof
A1: C = dom max(f*g,f*h) by FUNCT_2:def 1;
A2: for c being Element of C st c in C holds (f*max(g,h)).c = max(f*g,f*h).c
proof
let c;
(f*max(g,h)).c = (f.c)*(max(g,h).c) by Def2
.= (f.c)*max(g.c,h.c) by FUZZY_1:5
.= max((f.c)*g.c,(f.c)*(h.c)) by Lm2,Th1
.= max((f*g).c,(f.c)*(h.c)) by Def2
.= max((f*g).c,(f*h).c) by Def2;
hence thesis by FUZZY_1:5;
end;
C = dom (f*max(g,h)) by FUNCT_2:def 1;
hence thesis by A1,A2,PARTFUN1:5;
end;
theorem
f*min(g,h) = min(f*g,f*h)
proof
A1: C = dom min(f*g,f*h) by FUNCT_2:def 1;
A2: for c being Element of C st c in C holds (f*min(g,h)).c = min(f*g,f*h).c
proof
let c;
(f*min(g,h)).c = (f.c)*(min(g,h).c) by Def2
.= (f.c)*min(g.c,h.c) by FUZZY_1:5
.= min((f.c)*g.c,(f.c)*(h.c)) by Lm1,Th1
.= min((f*g).c,(f.c)*(h.c)) by Def2
.= min((f*g).c,(f*h).c) by Def2;
hence thesis by FUZZY_1:5;
end;
C = dom (f*min(g,h)) by FUNCT_2:def 1;
hence thesis by A1,A2,PARTFUN1:5;
end;
theorem
f ++ max(g,h) = max((f ++ g),(f ++ h))
proof
A1: C = dom max((f ++ g),(f ++ h)) by FUNCT_2:def 1;
A2: for c being Element of C st c in C holds (f ++ max(g,h)).c = (max((f ++
g),(f ++ h))).c
proof
let c;
A3: (f ++ max(g,h)).c = f.c + max(g,h).c - (f.c)*(max(g,h).c) by Def3
.= f.c + max(g.c,h.c) - (f.c)*(max(g,h).c) by FUZZY_1:5;
per cases by XXREAL_0:16;
suppose
A4: max(g.c,h.c) = g.c;
A5: (1_minus f).c >= 0 by Th1;
g.c >= h.c by A4,XXREAL_0:def 10;
then (g.c)*((1_minus f).c) >= (h.c)*((1_minus f).c) by A5,XREAL_1:64;
then (g.c)*(1- f.c) >= (h.c)*((1_minus f).c) by FUZZY_1:def 5;
then (g.c)*(1- f.c) >= (h.c)*(1- f.c) by FUZZY_1:def 5;
then (g.c)*1- (g.c)*f.c + f.c >= (h.c)*(1- f.c) + f.c by XREAL_1:6;
then
A6: f.c + g.c - (f.c)*g.c = max((f.c + g.c - (f.c)*g.c),(f.c + h.c - (f
.c)*(h.c))) by XXREAL_0:def 10
.= max((f ++ g).c,(f.c + h.c - (f.c)*(h.c))) by Def3
.= max((f ++ g).c,(f ++ h).c) by Def3;
(f ++ max(g,h)).c = f.c + g.c - (f.c)*g.c by A3,A4,FUZZY_1:5;
hence thesis by A6,FUZZY_1:5;
end;
suppose
A7: max(g.c,h.c) = h.c;
A8: (1_minus f).c >= 0 by Th1;
h.c >= g.c by A7,XXREAL_0:def 10;
then (h.c)*((1_minus f).c) >= (g.c)*((1_minus f).c) by A8,XREAL_1:64;
then (h.c)*(1- f.c) >= (g.c)*((1_minus f).c) by FUZZY_1:def 5;
then (h.c)*(1- f.c) >= (g.c)*(1- f.c) by FUZZY_1:def 5;
then (h.c)*1- (h.c)*f.c + f.c >= (g.c)*(1- f.c) + f.c by XREAL_1:6;
then
A9: f.c + h.c - (f.c)*h.c = max((f.c + g.c - (f.c)*g.c),(f.c + h.c - (f
.c)*(h.c))) by XXREAL_0:def 10
.= max((f ++ g).c,(f.c + h.c - (f.c)*(h.c))) by Def3
.= max((f ++ g).c,(f ++ h).c) by Def3;
(f ++ max(g,h)).c = f.c + h.c - (f.c)*h.c by A3,A7,FUZZY_1:5;
hence thesis by A9,FUZZY_1:5;
end;
end;
C = dom (f ++ max(g,h)) by FUNCT_2:def 1;
hence thesis by A1,A2,PARTFUN1:5;
end;
theorem
f ++ min(g,h) = min((f ++ g),(f ++ h))
proof
A1: C = dom min((f ++ g),(f ++ h)) by FUNCT_2:def 1;
A2: for c being Element of C st c in C holds (f ++ min(g,h)).c = (min((f ++
g),(f ++ h))).c
proof
let c;
A3: (f ++ min(g,h)).c = f.c + min(g,h).c - (f.c)*(min(g,h).c) by Def3
.= f.c + min(g.c,h.c) - (f.c)*(min(g,h).c) by FUZZY_1:5;
now
per cases by XXREAL_0:15;
suppose
A4: min(g.c,h.c) = g.c;
A5: (1_minus f).c >= 0 by Th1;
g.c <= h.c by A4,XXREAL_0:def 9;
then (g.c)*((1_minus f).c) <= (h.c)*((1_minus f).c) by A5,XREAL_1:64;
then (g.c)*(1- f.c) <= (h.c)*((1_minus f).c) by FUZZY_1:def 5;
then (g.c)*(1- f.c) <= (h.c)*(1- f.c) by FUZZY_1:def 5;
then (g.c)*1- (g.c)*f.c + f.c <= (h.c)*(1- f.c) + f.c by XREAL_1:6;
then
A6: f.c + g.c - (f.c)*g.c = min((f.c + g.c - (f.c)*g.c),(f.c + h.c -
(f.c)*(h.c))) by XXREAL_0:def 9
.= min((f ++ g).c,(f.c + h.c - (f.c)*(h.c))) by Def3
.= min((f ++ g).c,(f ++ h).c) by Def3;
(f ++ min(g,h)).c = f.c + g.c - (f.c)*g.c by A3,A4,FUZZY_1:5;
hence thesis by A6,FUZZY_1:5;
end;
suppose
A7: min(g.c,h.c) = h.c;
A8: (1_minus f).c >= 0 by Th1;
h.c <= g.c by A7,XXREAL_0:def 9;
then (h.c)*((1_minus f).c) <= (g.c)*((1_minus f).c) by A8,XREAL_1:64;
then (h.c)*(1- f.c) <= (g.c)*((1_minus f).c) by FUZZY_1:def 5;
then (h.c)*(1- f.c) <= (g.c)*(1- f.c) by FUZZY_1:def 5;
then (h.c)*1- (h.c)*f.c + f.c <= (g.c)*(1- f.c) + f.c by XREAL_1:6;
then
A9: f.c + h.c - (f.c)*h.c = min((f.c + g.c - (f.c)*g.c),(f.c + h.c -
(f.c)*(h.c))) by XXREAL_0:def 9
.= min((f ++ g).c,(f.c + h.c - (f.c)*(h.c))) by Def3
.= min((f ++ g).c,(f ++ h).c) by Def3;
(f ++ min(g,h)).c = f.c + h.c - (f.c)*h.c by A3,A7,FUZZY_1:5;
hence thesis by A9,FUZZY_1:5;
end;
end;
hence thesis;
end;
C = dom (f ++ min(g,h)) by FUNCT_2:def 1;
hence thesis by A1,A2,PARTFUN1:5;
end;
theorem
max(f,g)*max(f,h) c= max(f,(g*h))
proof
let c;
A1: max(f.c,g.c)*max(f.c,h.c) <= max(f,(g*h)).c
proof
per cases by XXREAL_0:16;
suppose
A2: max(f.c,g.c) = f.c;
max(f.c,g.c)*max(f.c,h.c) <= max(f,(g*h)).c
proof
per cases by XXREAL_0:16;
suppose
A3: max(f.c,h.c) = f.c;
max(f,(g*h)).c = max(f.c,(g*h).c) by FUZZY_1:5;
then
A4: max(f,(g*h)).c >= f.c by XXREAL_0:25;
f*f c= f by Th28;
then (f*f).c <= f.c;
then (f*f).c <= max(f,(g*h)).c by A4,XXREAL_0:2;
hence thesis by A2,A3,Def2;
end;
suppose
A5: max(f.c,h.c) = h.c;
A6: 1 >= h.c by Th1;
f.c <= max(f.c,(g*h).c) by XXREAL_0:25;
then
A7: f.c <= max(f,(g*h)).c by FUZZY_1:5;
f.c >= 0 by Th1;
then (f.c)*(h.c) <= (f.c)*1 by A6,XREAL_1:64;
hence thesis by A2,A5,A7,XXREAL_0:2;
end;
end;
hence thesis;
end;
suppose
A8: max(f.c,g.c) = g.c;
max(f.c,g.c)*max(f.c,h.c) <= max(f,(g*h)).c
proof
per cases by XXREAL_0:16;
suppose
A9: max(f.c,h.c) = f.c;
A10: 1 >= g.c by Th1;
f.c <= max(f.c,(g*h).c) by XXREAL_0:25;
then
A11: f.c <= max(f,(g*h)).c by FUZZY_1:5;
f.c >= 0 by Th1;
then (f.c)*(g.c) <= (f.c)*1 by A10,XREAL_1:64;
hence thesis by A8,A9,A11,XXREAL_0:2;
end;
suppose
A12: max(f.c,h.c) = h.c;
max(f,(g*h)).c = max(f.c,(g*h).c) by FUZZY_1:5;
then max(f,(g*h)).c >= (g*h).c by XXREAL_0:25;
hence thesis by A8,A12,Def2;
end;
end;
hence thesis;
end;
end;
(max(f,g)*max(f,h)).c = (max(f,g).c)*(max(f,h).c) by Def2
.= max(f.c,g.c)*(max(f,h).c) by FUZZY_1:5
.= max(f.c,g.c)*max(f.c,h.c) by FUZZY_1:5;
hence thesis by A1;
end;
theorem
min(f,g)*min(f,h) c= min(f,(g*h))
proof
let c;
A1: min(f.c,g.c)*min(f.c,h.c) <= min(f,(g*h)).c
proof
now
per cases by XXREAL_0:15;
suppose
A2: min(f.c,g.c) = f.c;
min(f.c,g.c)*min(f.c,h.c) <= min(f,(g*h)).c
proof
per cases by XXREAL_0:15;
suppose
A3: min(f.c,h.c) = f.c;
A4: 0 <= g.c by Th1;
f.c <= h.c by A3,XXREAL_0:def 9;
then
A5: (g.c)*(f.c) <= (h.c)*(g.c) by A4,XREAL_1:64;
A6: 0 <= f.c by Th1;
f*f c= f by Th28;
then
A7: (f*f).c <= f.c;
f.c <= g.c by A2,XXREAL_0:def 9;
then (f.c)*(f.c) <= (g.c)*(f.c) by A6,XREAL_1:64;
then (f.c)*(f.c) <= (g.c)*(h.c) by A5,XXREAL_0:2;
then min((f*f).c,(f.c)*(f.c)) <= min(f.c,(g.c)*(h.c)) by A7,
XXREAL_0:18;
then min((f.c)*(f.c),(f.c)*(f.c)) <= min(f.c,(g.c)*(h.c)) by Def2;
then (f.c)*(f.c) <= min(f.c,(g*h).c) by Def2;
hence thesis by A2,A3,FUZZY_1:5;
end;
suppose
A8: min(f.c,h.c) = h.c;
A9: 1 >= h.c by Th1;
A10: h.c >= 0 by Th1;
f.c <= g.c by A2,XXREAL_0:def 9;
then
A11: (f.c)*(h.c) <= (g.c)*(h.c) by A10,XREAL_1:64;
f.c >= 0 by Th1;
then (f.c)*(h.c) <= (f.c)*1 by A9,XREAL_1:64;
then (f.c)*(h.c) <= min((f.c),(g.c)*(h.c)) by A11,XXREAL_0:20;
then (f.c)*(h.c) <= min(f.c,(g*h).c) by Def2;
hence thesis by A2,A8,FUZZY_1:5;
end;
end;
hence thesis;
end;
suppose
A12: min(f.c,g.c) = g.c;
min(f.c,g.c)*min(f.c,h.c) <= min(f,(g*h)).c
proof
per cases by XXREAL_0:15;
suppose
A13: min(f.c,h.c) = f.c;
A14: g.c >= 0 by Th1;
f.c <= h.c by A13,XXREAL_0:def 9;
then
A15: (f.c)*(g.c) <= (h.c)*(g.c) by A14,XREAL_1:64;
A16: 1 >= g.c by Th1;
f.c >= 0 by Th1;
then (g.c)*(f.c) <= (f.c)*1 by A16,XREAL_1:64;
then (f.c)*(g.c) <= min((f.c),(h.c)*(g.c)) by A15,XXREAL_0:20;
then (f.c)*(g.c) <= min(f.c,(g*h).c) by Def2;
hence thesis by A12,A13,FUZZY_1:5;
end;
suppose
A17: min(f.c,h.c) = h.c;
A18: g.c <= f.c by A12,XXREAL_0:def 9;
f.c >= 0 by Th1;
then
A19: (g.c)*(f.c) <= (f.c)*(f.c) by A18,XREAL_1:64;
f*f c= f by Th28;
then (f*f).c <= f.c;
then
A20: (f.c)*(f.c) <= f.c by Def2;
A21: h.c <= f.c by A17,XXREAL_0:def 9;
g.c >= 0 by Th1;
then (h.c)*(g.c) <= (f.c)*(g.c) by A21,XREAL_1:64;
then (h.c)*(g.c) <= (f.c)*(f.c) by A19,XXREAL_0:2;
then (h.c)*(g.c) <= f.c by A20,XXREAL_0:2;
then (h.c)*(g.c) <= min(f.c,(h.c)*(g.c)) by XXREAL_0:20;
then (g.c)*(h.c) <= min(f.c,(g*h).c) by Def2;
hence thesis by A12,A17,FUZZY_1:5;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
(min(f,g)*min(f,h)).c = (min(f,g).c)*(min(f,h).c) by Def2
.= min(f.c,g.c)*(min(f,h).c) by FUZZY_1:5
.= min(f.c,g.c)*min(f.c,h.c) by FUZZY_1:5;
hence thesis by A1;
end;
theorem Th49:
for c be Element of C,f,g be Membership_Func of C holds (f ++ g)
.c = 1 - ((1 - f.c)*(1 - g.c))
proof
let c;
let g,h be Membership_Func of C;
(g ++ h).c = (1_minus((1_minus g)*(1_minus h))).c by Th36
.= 1-((1_minus g)*(1_minus h)).c by FUZZY_1:def 5
.= 1-((1_minus g).c)*((1_minus h).c) by Def2
.= 1-((1-g.c)*((1_minus h).c)) by FUZZY_1:def 5;
hence thesis by FUZZY_1:def 5;
end;
theorem
max(f,g ++ h) c= max(f,g) ++ max(f,h)
proof
let c;
A1: (max(f,g) ++ max(f,h)).c = max(f,g).c + max(f,h).c - (max(f,g).c)*(max(f
,h).c) by Def3
.= max(f.c,g.c) + max(f,h).c - (max(f,g).c)*(max(f,h).c) by FUZZY_1:5
.= max(f.c,g.c) + max(f.c,h.c) - (max(f,g).c)*(max(f,h).c) by FUZZY_1:5
.= max(f.c,g.c) + max(f.c,h.c) - (max(f.c,g.c))*(max(f,h).c) by FUZZY_1:5
.= max(f.c,g.c) + max(f.c,h.c) - (max(f.c,g.c))*(max(f.c,h.c)) by FUZZY_1:5
;
A2: max(f.c,1 - ((1 - g.c)*(1 - h.c))) <= max(f.c,g.c) + max(f.c,h.c) - (max
(f.c,g.c))*(max(f.c,h.c))
proof
per cases by XXREAL_0:16;
suppose
A3: max(f.c,g.c) = f.c & max(f.c,h.c) = f.c;
(1_minus g).c >= 0 by Th1;
then
A4: 1-g.c >= 0 by FUZZY_1:def 5;
h.c <= f.c by A3,XXREAL_0:def 10;
then 1 - h.c >= 1 - f.c by XREAL_1:10;
then
A5: (1 - g.c)*(1 - f.c) <= (1 - g.c)*(1 - h.c) by A4,XREAL_1:64;
(1_minus f).c >= 0 by Th1;
then
A6: 1-f.c >= 0 by FUZZY_1:def 5;
f c= f++f by Th28;
then (f ++ f).c >= f.c;
then
A7: f.c + f.c - (f.c)*(f.c) >= f.c by Def3;
g.c <= f.c by A3,XXREAL_0:def 10;
then 1 - g.c >= 1 - f.c by XREAL_1:10;
then (1 - f.c)*(1 - f.c) <= (1 - g.c)*(1 - f.c) by A6,XREAL_1:64;
then (1 - f.c)*(1 - f.c) <= (1 - g.c)*(1 - h.c) by A5,XXREAL_0:2;
then 1 - (1 - f.c)*(1 - f.c) >= 1 - (1 - g.c)*(1 - h.c) by XREAL_1:10;
hence thesis by A3,A7,XXREAL_0:28;
end;
suppose
A8: max(f.c,g.c) = f.c & max(f.c,h.c) = h.c;
(1_minus f).c >= 0 by Th1;
then
A9: 1 - f.c >= 0 by FUZZY_1:def 5;
h.c >= 0 by Th1;
then 0*(h.c) <= (h.c)*(1-f.c) by A9,XREAL_1:64;
then
A10: 0 + f.c <= (h.c)*(1-f.c) + f.c by XREAL_1:6;
(1_minus h).c >= 0 by Th1;
then
A11: 1 - h.c >= 0 by FUZZY_1:def 5;
g.c <= f.c by A8,XXREAL_0:def 10;
then 1 - f.c <= 1 - g.c by XREAL_1:10;
then (1 - f.c)*(1 -h.c) <= (1 - g.c)*(1 -h.c) by A11,XREAL_1:64;
then 1-(1 - f.c)*(1 -h.c) >= 1-(1 - g.c)*(1 -h.c) by XREAL_1:10;
hence thesis by A8,A10,XXREAL_0:28;
end;
suppose
A12: max(f.c,g.c) = g.c & max(f.c,h.c) = f.c;
(1_minus f).c >= 0 by Th1;
then
A13: 1 - f.c >= 0 by FUZZY_1:def 5;
g.c >= 0 by Th1;
then 0*(g.c) <= (g.c)*(1-f.c) by A13,XREAL_1:64;
then
A14: 0 + f.c <= (g.c)*(1-f.c) + f.c by XREAL_1:6;
(1_minus g).c >= 0 by Th1;
then
A15: 1 - g.c >= 0 by FUZZY_1:def 5;
h.c <= f.c by A12,XXREAL_0:def 10;
then 1 - f.c <= 1 - h.c by XREAL_1:10;
then (1 - f.c)*(1 -g.c) <= (1 - h.c)*(1 -g.c) by A15,XREAL_1:64;
then 1-(1 - f.c)*(1 -g.c) >= 1-(1 - h.c)*(1 - g.c) by XREAL_1:10;
hence thesis by A12,A14,XXREAL_0:28;
end;
suppose
A16: max(f.c,g.c) = g.c & max(f.c,h.c) = h.c;
(1_minus g).c >= 0 by Th1;
then
A17: 1-g.c >= 0 by FUZZY_1:def 5;
h.c >= f.c by A16,XXREAL_0:def 10;
then 1 - h.c <= 1 - f.c by XREAL_1:10;
then
A18: (1 - g.c)*(1 - f.c) >= (1 - g.c)*(1 - h.c) by A17,XREAL_1:64;
(1_minus f).c >= 0 by Th1;
then
A19: 1-f.c >= 0 by FUZZY_1:def 5;
g.c >= f.c by A16,XXREAL_0:def 10;
then 1 - g.c <= 1 - f.c by XREAL_1:10;
then (1 - f.c)*(1 - f.c) >= (1 - g.c)*(1 - f.c) by A19,XREAL_1:64;
then (1 - f.c)*(1 - f.c) >= (1 - g.c)*(1 - h.c) by A18,XXREAL_0:2;
then 1 - ((1 - f.c)*(1 - f.c)) <= 1 - (1 - g.c)*(1 - h.c) by XREAL_1:10;
then
A20: (f ++ f).c <= 1 - (1 - g.c)*(1 - h.c) by Th49;
f c= f++f by Th28;
then (f ++ f).c >= f.c;
then f.c <= 1 - (1 - g.c)*(1 - h.c) by A20,XXREAL_0:2;
hence thesis by A16,XXREAL_0:28;
end;
end;
max(f,g ++ h).c = max(f.c,(g ++ h).c) by FUZZY_1:5
.= max(f.c,1 - ((1 - g.c)*(1 - h.c))) by Th49;
hence thesis by A1,A2;
end;
theorem
min(f,g ++ h) c= min(f,g) ++ min(f,h)
proof
let c;
A1: (min(f,g) ++ min(f,h)).c = min(f,g).c + min(f,h).c - (min(f,g).c)*(min(f
,h).c) by Def3
.= min(f.c,g.c) + min(f,h).c - (min(f,g).c)*(min(f,h).c) by FUZZY_1:5
.= min(f.c,g.c) + min(f.c,h.c) - (min(f,g).c)*(min(f,h).c) by FUZZY_1:5
.= min(f.c,g.c) + min(f.c,h.c) - (min(f.c,g.c))*(min(f,h).c) by FUZZY_1:5
.= min(f.c,g.c) + min(f.c,h.c) - (min(f.c,g.c))*(min(f.c,h.c)) by FUZZY_1:5
;
A2: min(f.c,1 - ((1 - g.c)*(1 - h.c))) <= min(f.c,g.c) + min(f.c,h.c) - (min
(f.c,g.c))*(min(f.c,h.c))
proof
now
per cases by XXREAL_0:15;
suppose
A3: min(f.c,g.c) = f.c & min(f.c,h.c) = f.c;
f c= f ++ f by Th28;
then
A4: (f ++ f).c >= f.c;
min(f.c,1 - ((1 - g.c)*(1 - h.c))) <= f.c by XXREAL_0:17;
then min(f.c,1 - ((1 - g.c)*(1 - h.c))) <= (f ++ f).c by A4,XXREAL_0:2;
hence thesis by A3,Def3;
end;
suppose
A5: min(f.c,g.c) = f.c & min(f.c,h.c) = h.c;
(1_minus f).c >= 0 by Th1;
then
A6: 1 - f.c >= 0 by FUZZY_1:def 5;
h.c >= 0 by Th1;
then 0*(h.c) <= (h.c)*(1-f.c) by A6,XREAL_1:64;
then
A7: 0 + f.c <= (h.c)*(1-f.c) + f.c by XREAL_1:6;
min(f.c,1 - ((1 - g.c)*(1 - h.c))) <= f.c by XXREAL_0:17;
hence thesis by A5,A7,XXREAL_0:2;
end;
suppose
A8: min(f.c,g.c) = g.c & min(f.c,h.c) = f.c;
(1_minus f).c >= 0 by Th1;
then
A9: 1 - f.c >= 0 by FUZZY_1:def 5;
g.c >= 0 by Th1;
then 0*(g.c) <= (g.c)*(1-f.c) by A9,XREAL_1:64;
then
A10: 0 + f.c <= (g.c)*(1-f.c) + f.c by XREAL_1:6;
min(f.c,1 - ((1 - g.c)*(1 - h.c))) <= f.c by XXREAL_0:17;
hence thesis by A8,A10,XXREAL_0:2;
end;
suppose
min(f.c,g.c) = g.c & min(f.c,h.c) = h.c;
hence thesis by XXREAL_0:17;
end;
end;
hence thesis;
end;
min(f,g ++ h).c = min(f.c,(g ++ h).c) by FUZZY_1:5
.= min(f.c,1 - ((1 - g.c)*(1 - h.c))) by Th49;
hence thesis by A1,A2;
end;
begin :: Addenda, moved from FUZZY_3
reserve C1,C2 for non empty set;
registration
let C be non empty set;
cluster -> quasi_total for Membership_Func of C;
coherence;
end;
definition
let C1,C2 be non empty set;
mode RMembership_Func of C1,C2 is Membership_Func of [:C1,C2:];
end;
reserve f,g for RMembership_Func of C1,C2;
definition
let C1,C2 be non empty set;
func Zmf(C1,C2) -> RMembership_Func of C1,C2 equals
chi({},[:C1,C2:]);
correctness by FUZZY_1:12;
func Umf(C1,C2) -> RMembership_Func of C1,C2 equals
chi([:C1,C2:],[:C1,C2:]);
correctness by FUZZY_1:1;
end;
theorem
for x be Element of [:C1,C2:],h be RMembership_Func of C1,C2 holds (
Zmf(C1,C2)).x <= h.x & h.x <= (Umf(C1,C2)).x
proof
A1: Umf(C1,C2) = UMF [:C1,C2:];
Zmf(C1,C2) = EMF [:C1,C2:];
hence thesis by A1,FUZZY_1:16;
end;
theorem
max(f,Umf(C1,C2)) = Umf(C1,C2) & min(f,Umf(C1,C2)) = f & max(f,Zmf(C1,
C2)) = f & min(f,Zmf(C1,C2)) = Zmf(C1,C2)
proof
A1: Umf(C1,C2) = UMF [:C1,C2:];
Zmf(C1,C2) = EMF [:C1,C2:];
hence thesis by A1,FUZZY_1:18;
end;
theorem
1_minus(Zmf(C1,C2)) = Umf(C1,C2) & 1_minus(Umf(C1,C2)) = Zmf(C1,C2)
proof
A1: Umf(C1,C2) = UMF [:C1,C2:];
Zmf(C1,C2) = EMF [:C1,C2:];
hence thesis by A1,FUZZY_1:40;
end;
theorem
f\g = Zmf(C1,C2) implies f c= g
proof
Zmf(C1,C2) = EMF [:C1,C2:];
hence thesis by Th26;
end;
theorem
min(f,g) = Zmf(C1,C2) implies f\g = f
proof
Zmf(C1,C2) = EMF [:C1,C2:];
hence thesis by Th27;
end;