:: Concept of Fuzzy Set and Membership Function and Basic
:: Properties of Fuzzy Set Operation
:: by Takashi Mitsuishi , Noboru Endou and Yasunari Shidama
::
:: Received May 18, 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, FUNCT_3, XXREAL_1, CARD_1, RELAT_1,
TARSKI, FUNCT_1, VALUED_0, LATTICE3, XXREAL_0, PARTFUN1, SEQ_4, ARYTM_1,
ARYTM_3, COMPLEX1, FUZZY_1, MEASURE5, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0,
COMPLEX1, XREAL_0, RELAT_1, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2,
VALUED_0, SEQ_4, RFUNCT_1, MEASURE5, INTEGRA1, RCOMP_1;
constructors REAL_1, SQUARE_1, COMPLEX1, RFUNCT_1, INTEGRA1, SEQ_4, RELSET_1,
NUMBERS;
registrations RELSET_1, NUMBERS, XXREAL_0, MEMBERED, XBOOLE_0, VALUED_0,
RFUNCT_1, FUNCT_2, MEASURE5, XREAL_0, ORDINAL1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions RELAT_1;
theorems TARSKI, FUNCT_1, FUNCT_3, ABSVALUE, PARTFUN1, ZFMISC_1, INTEGRA1,
INTEGRA2, XBOOLE_0, XBOOLE_1, COMPLEX1, XREAL_1, XXREAL_0, XXREAL_1,
FUNCT_2, RELAT_1, MEASURE5, XREAL_0;
schemes SEQ_1, PARTFUN1;
begin
reserve x,y,y1,y2 for set;
reserve C for non empty set;
reserve c for Element of C;
:: Definition of Membership Function and Fuzzy Set
registration
let x,y;
cluster chi(x,y) -> [.0,1.]-valued;
coherence
proof
1 in [.0,1.] & 0 in [.0,1.] by XXREAL_1:1;
then rng chi(x,y) c= {0,1} & {0,1} c= [.0,1.] by FUNCT_3:39,ZFMISC_1:32;
hence rng chi(x,y) c= [.0,1.] by XBOOLE_1:1;
end;
end;
registration
let C;
cluster [.0,1.]-valued for Function of C,REAL;
existence
proof
take chi(C,C);
thus rng chi(C,C) c= [.0,1.] by RELAT_1:def 19;
end;
end;
definition
let C;
mode Membership_Func of C is [.0,1.]-valued Function of C,REAL;
end;
theorem
chi(C,C) is Membership_Func of C;
reserve f,h,g,h1 for Membership_Func of C;
registration
let X be non empty set;
cluster -> real-valued for Membership_Func of X;
coherence;
end;
definition
let f,g be real-valued Function;
pred f is_less_than g means
dom f c= dom g & for x being set st x in dom f holds f.x <= g.x;
reflexivity;
end;
notation
let X be non empty set;
let f,g be Membership_Func of X;
synonym f c= g for f is_less_than g;
end;
definition
let X be non empty set;
let f,g be Membership_Func of X;
redefine pred f is_less_than g means :: redefines is_less_than (FUZZY_1, definition)
:Def2:
for x being Element of X holds f .x <= g.x;
compatibility
proof
thus f is_less_than g iff for x being Element of X holds f.x <= g.x
proof
hereby
assume
A1: f is_less_than g;
thus for x being Element of X holds f.x <= g.x
proof
let x be Element of X;
dom f = X by FUNCT_2:def 1;
hence thesis by A1;
end;
end;
assume for x being Element of X holds f.x <= g.x;
then dom g = X & for x being set st x in dom f holds f.x <= g.x
by FUNCT_2:def 1;
hence thesis;
end;
end;
end;
Lm1: f c= g & g c= f implies f = g
proof
set A = f, B = g;
assume
A1: A c= B & B c= A;
A2: for c being Element of C st c in C holds f.c = g.c
proof
let c be Element of C;
f.c <= g.c & g.c <= f.c by A1;
hence thesis by XXREAL_0:1;
end;
C = dom f & C = dom g by FUNCT_2:def 1;
hence thesis by A2,PARTFUN1:5;
end;
theorem
f = g iff f c= g & g c= f by Lm1;
theorem
f c= f;
theorem
f c= g & g c= h implies g c= h;
begin
:: Intersection,Union and Complement
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
definition
let C be non empty set;
let h,g be Membership_Func of C;
func min(h,g) -> Membership_Func of C means
:Def3:
for c being Element of C holds it.c = min(h.c,g.c);
existence
proof
defpred P[object,object] means $2 = min(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;
min(h.x,g.x) is set by TARSKI:1;
hence thesis by A3;
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 = min(h.c,g.c) by A3;
A7: rng h c= [.0,1.] by RELAT_1:def 19;
A8: rng g 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: h.x >= min(h.x,g.x) by XXREAL_0:17;
A12: A = [. lower_bound A, upper_bound A .] by INTEGRA1:4;
then
A13: 0=lower_bound A by INTEGRA1:5;
A14: x in C;
then x in dom h by FUNCT_2:def 1;
then
A15: h.x in rng h by FUNCT_1:def 3;
A16: 1=upper_bound A by A12,INTEGRA1:5;
then h.x <= 1 by A7,A15,INTEGRA2:1;
then min(h.x,g.x) <= 1 by A11,XXREAL_0:2;
then
A17: IT.x <= 1 by A3,A9;
x in dom g by A14,FUNCT_2:def 1;
then g.x in rng g by FUNCT_1:def 3;
then
A18: 0 <= g.x by A8,A13,INTEGRA2:1;
0 <= h.x by A7,A13,A15,INTEGRA2:1;
then 0 <= min(h.x,g.x) by A18,XXREAL_0:20;
then 0 <= IT.x by A3,A9;
hence thesis by A10,A13,A16,A17,INTEGRA2:1;
end;
then
A19: rng IT c= [.0,1.] by TARSKI:def 3;
IT is total by A5,PARTFUN1:def 2;
then IT is Membership_Func of C by A19,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 = min(h.c,g.c) and
A21: for c being Element of C holds G.c = min(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 = min(h.c,g.c) by A20;
hence thesis by A21;
end;
C = dom F & C = dom G by FUNCT_2:def 1;
hence thesis by A22,PARTFUN1:5;
end;
idempotence;
commutativity;
end;
definition
let C be non empty set;
let h,g be Membership_Func of C;
func max(h,g) -> Membership_Func of C means
:Def4:
for c being Element of C holds it.c = max(h.c,g.c);
existence
proof
defpred P[object,object] means $2 = max(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;
max(h.x,g.x) is set by TARSKI:1;
hence thesis by A3;
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 = max(h.c,g.c) by A3;
A7: rng h c= [.0,1.] by RELAT_1:def 19;
A8: rng g 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 0 <= h.x by A7,A12,INTEGRA2:1;
then 0 <= max(h.x,g.x) by XXREAL_0:30;
then
A15: 0 <= IT.x by A3,A9;
A16: 1=upper_bound A by A11,INTEGRA1:5;
x in dom g by A13,FUNCT_2:def 1;
then g.x in rng g by FUNCT_1:def 3;
then
A17: g.x <= 1 by A8,A16,INTEGRA2:1;
h.x <= 1 by A7,A16,A14,INTEGRA2:1;
then max(h.x,g.x) <= 1 by A17,XXREAL_0:28;
then IT.x <= 1 by A3,A9;
hence thesis by A10,A12,A16,A15,INTEGRA2:1;
end;
then
A18: rng IT c= [.0,1.] by TARSKI:def 3;
IT is total by A5,PARTFUN1:def 2;
then IT is Membership_Func of C by A18,RELAT_1:def 19;
hence thesis by A6;
end;
uniqueness
proof
let F,G be Membership_Func of C;
assume that
A19: for c being Element of C holds F.c = max(h.c,g.c) and
A20: for c being Element of C holds G.c = max(h.c,g.c);
A21: for c being Element of C st c in C holds F.c = G.c
proof
let c be Element of C;
F.c = max(h.c,g.c) by A19;
hence thesis by A20;
end;
C = dom F & C = dom G by FUNCT_2:def 1;
hence thesis by A21,PARTFUN1:5;
end;
idempotence;
commutativity;
end;
definition
let C be non empty set;
let h be Membership_Func of C;
func 1_minus h -> Membership_Func of C means
:Def5:
for c being Element of C holds it.c = 1-h.c;
existence
proof
deffunc F(set) = In(1 - h.$1,REAL);
defpred P[set] means $1 in dom h;
consider IT being PartFunc of C,REAL such that
A1: (for x be Element of C holds x in dom IT iff P[x]) & for x be
Element of C st x in dom IT holds IT.x = F(x) from SEQ_1:sch 3;
for x being object st x in C holds x in dom IT
proof
let x be object;
A2: dom h = C by FUNCT_2:def 1;
assume x in C;
hence thesis by A1,A2;
end;
then C c= dom IT by TARSKI:def 3;
then
A3: dom IT = C by XBOOLE_0:def 10;
then
A4: for c being Element of C holds IT.c = F(c) by A1;
A5: 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
A6: x in dom IT and
A7: y = IT.x by PARTFUN1:3;
A8: A = [. lower_bound A, upper_bound A .] by INTEGRA1:4;
then
A9: 0=lower_bound A by INTEGRA1:5;
x in C;
then x in dom h by FUNCT_2:def 1;
then
A10: h.x in rng h by FUNCT_1:def 3;
then 0 <= h.x by A5,A9,INTEGRA2:1;
then 0+1 <= 1+h.x by XREAL_1:6;
then F(x) <= 1 by XREAL_1:20;
then
A11: IT.x <= 1 by A1,A6;
A12: 1=upper_bound A by A8,INTEGRA1:5;
then h.x <= 1 by A5,A10,INTEGRA2:1;
then 0 <= F(x) by XREAL_1:48;
then 0 <= IT.x by A1,A6;
hence thesis by A7,A9,A12,A11,INTEGRA2:1;
end;
then
A13: rng IT c= [.0,1.] by TARSKI:def 3;
IT is total by A3,PARTFUN1:def 2;
then reconsider IT as Membership_Func of C by A13,RELAT_1:def 19;
take IT;
let c be Element of C;
IT.c = F(c) by A4;
hence thesis;
end;
uniqueness
proof
let F,G be Membership_Func of C;
assume that
A14: for c being Element of C holds F.c = 1-h.c and
A15: for c being Element of C holds G.c = 1-h.c;
A16: for c being Element of C st c in C holds F.c = G.c
proof
let c be Element of C;
F.c = 1-h.c by A14;
hence thesis by A15;
end;
C = dom F & C = dom G by FUNCT_2:def 1;
hence thesis by A16,PARTFUN1:5;
end;
involutiveness
proof
let h1,h2 be Membership_Func of C;
assume
A17: for c being Element of C holds h1.c = 1-h2.c;
let c be Element of C;
thus h2.c = 1-(1-h2.c) .= 1-h1.c by A17;
end;
end;
theorem
min(h.c,g.c) = min(h,g).c & max(h.c,g.c) = max(h,g).c by Def3,Def4;
theorem
max(h,h) = h & min(h,h) = h & max(h,h) = min(h,h) & min(f,g) = min(g,f
) & max(f,g) = max(g,f);
theorem Th7:
max(max(f,g),h) = max(f,max(g,h)) & min(min(f,g),h) = min(f,min(g ,h))
proof
A1: C = dom min(min(f,g),h) & C = dom min(f,min(g,h)) by FUNCT_2:def 1;
A2: for x being Element of C st x in C holds max(max(f,g),h).x = max(f,max(g
,h)).x
proof
let x be Element of C;
max(max(f,g),h).x = max(max(f,g).x,h.x) by Def4
.= max(max(f.x,g.x),h.x) by Def4
.= max(f.x,max(g.x,h.x)) by XXREAL_0:34
.= max(f.x,max(g,h).x) by Def4
.= max(f,max(g,h)).x by Def4;
hence thesis;
end;
A3: for x being Element of C st x in C holds min(min(f,g),h).x = min(f,min(g
,h)).x
proof
let x be Element of C;
min(min(f,g),h).x = min(min(f,g).x,h.x) by Def3
.= min(min(f.x,g.x),h.x) by Def3
.= min(f.x,min(g.x,h.x)) by XXREAL_0:33
.= min(f.x,min(g,h).x) by Def3
.= min(f,min(g,h)).x by Def3;
hence thesis;
end;
C = dom max(max(f,g),h) & C = dom max(f,max(g,h)) by FUNCT_2:def 1;
hence thesis by A1,A2,A3,PARTFUN1:5;
end;
theorem Th8:
max(f,min(f,g)) = f & min(f,max(f,g)) = f
proof
A1: C = dom min(f,max(f,g)) by FUNCT_2:def 1;
A2: for x being Element of C st x in C holds max(f,min(f,g)).x = f.x
proof
let x be Element of C;
max(f,min(f,g)).x = max(f.x,min(f,g).x) by Def4
.= max(f.x,min(f.x,g.x)) by Def3
.= f.x by XXREAL_0:36;
hence thesis;
end;
A3: for x being Element of C st x in C holds min(f,max(f,g)).x = f.x
proof
let x be Element of C;
min(f,max(f,g)).x = min(f.x,max(f,g).x) by Def3
.= min(f.x,max(f.x,g.x)) by Def4
.= f.x by XXREAL_0:35;
hence thesis;
end;
C = dom max(f,min(f,g)) & C = dom f by FUNCT_2:def 1;
hence thesis by A1,A2,A3,PARTFUN1:5;
end;
theorem Th9:
min(f,max(g,h)) = max(min(f,g),min(f,h)) & max(f,min(g,h)) = min
(max(f,g),max(f,h))
proof
A1: C = dom max(f,min(g,h)) & C = dom min(max(f,g),max(f,h)) by FUNCT_2:def 1;
A2: for x being Element of C st x in C holds min(f,max(g,h)).x = max(min(f,g
),min(f,h)).x
proof
let x be Element of C;
min(f,max(g,h)).x = min(f.x,max(g,h).x) by Def3
.= min(f.x,max(g.x,h.x)) by Def4
.= max(min(f.x,g.x),min(f.x,h.x)) by XXREAL_0:38
.= max(min(f,g).x,min(f.x,h.x)) by Def3
.= max(min(f,g).x,min(f,h).x) by Def3
.= max(min(f,g),min(f,h)).x by Def4;
hence thesis;
end;
A3: for x being Element of C st x in C holds max(f,min(g,h)).x = min(max(f,g
),max(f,h)).x
proof
let x be Element of C;
max(f,min(g,h)).x = max(f.x,min(g,h).x) by Def4
.= max(f.x,min(g.x,h.x)) by Def3
.= min(max(f.x,g.x),max(f.x,h.x)) by XXREAL_0:39
.= min(max(f,g).x,max(f.x,h.x)) by Def4
.= min(max(f,g).x,max(f,h).x) by Def4
.= min(max(f,g),max(f,h)).x by Def3;
hence thesis;
end;
C = dom min(f,max(g,h)) & C = dom max(min(f,g),min(f,h)) by FUNCT_2:def 1;
hence thesis by A1,A2,A3,PARTFUN1:5;
end;
::$CT
theorem Th10:
1_minus(max(f,g)) = min(1_minus(f),1_minus(g)) & 1_minus(min(f,g
)) = max(1_minus(f),1_minus(g))
proof
A1: C = dom 1_minus(min(f,g)) & C = dom max(1_minus(f),1_minus(g)) by
FUNCT_2:def 1;
A2: for x being Element of C st x in C holds (1_minus(max(f,g))).x = min(
1_minus(f),1_minus(g)).x
proof
let x be Element of C;
A3: (1_minus(max(f,g))).x =1 - max(f,g).x by Def5
.=1 - max(f.x,g.x) by Def4
.=1 - (f.x + g.x + |.f.x - g.x.|)/2 by COMPLEX1:74;
min(1_minus(f),1_minus(g)).x =min((1_minus(f)).x,(1_minus(g)).x) by Def3
.=min((1 - f.x),(1_minus(g)).x) by Def5
.=min((1 - f.x),(1- g.x)) by Def5
.=((1-f.x) + (1-g.x) - |.(1-f.x) - (1-g.x).|)/2 by COMPLEX1:73
.=(2-f.x -g.x- |.-(f.x-g.x).|)/2
.=(2-(f.x + g.x) - |.f.x-g.x.|)/2 by COMPLEX1:52
.=1 - ((f.x + g.x) + |.f.x-g.x.|)/2;
hence thesis by A3;
end;
A4: for x being Element of C st x in C holds (1_minus(min(f,g))).x = max(
1_minus(f),1_minus(g)).x
proof
let x be Element of C;
A5: (1_minus(min(f,g))).x =1 - min(f,g).x by Def5
.=1 - min(f.x,g.x) by Def3
.=1 - (f.x + g.x - |.f.x-g.x.|)/2 by COMPLEX1:73;
max(1_minus(f),1_minus(g)).x =max((1_minus(f)).x,(1_minus(g)).x) by Def4
.=max((1 - f.x),(1_minus(g)).x) by Def5
.=max((1 - f.x),(1- g.x)) by Def5
.=((1-f.x) + (1-g.x) + |.(1-f.x) - (1-g.x).|)/2 by COMPLEX1:74
.=(2-f.x -g.x + |.-(f.x-g.x).|)/2
.=(2-(f.x + g.x) + |.f.x-g.x.|)/2 by COMPLEX1:52
.=1 - ((f.x + g.x) - |.f.x-g.x.|)/2;
hence thesis by A5;
end;
C = dom 1_minus(max(f,g)) & C = dom min(1_minus(f),1_minus(g)) by
FUNCT_2:def 1;
hence thesis by A1,A2,A4,PARTFUN1:5;
end;
begin
:: Empty Fuzzy Set and Universal Fuzzy Set
theorem
chi({},C) is Membership_Func of C;
definition
let C be non empty set;
func EMF(C) -> Membership_Func of C equals
chi({},C);
correctness;
end;
definition
let C be non empty set;
func UMF(C) -> Membership_Func of C equals
chi(C,C);
correctness;
end;
theorem Th12:
for a,b be Element of REAL, f be PartFunc of C,REAL st rng f c=
[.a,b.] & a <= b holds for x being Element of C st x in dom f holds a <= f.x &
f.x <= b
proof
let a,b be Element of REAL;
let f be PartFunc of C,REAL;
assume that
A1: rng f c= [.a,b.] and
A2: a <= b;
for x being Element of C st x in dom f holds a <= f.x & f.x <= b
proof
reconsider A=[.a,b.] as
non empty closed_interval Subset of REAL by A2,MEASURE5:14;
let x be Element of C;
A = [. lower_bound A, upper_bound A .] by INTEGRA1:4;
then
A3: a=lower_bound A & b=upper_bound A by INTEGRA1:5;
assume x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis by A1,A3,INTEGRA2:1;
end;
hence thesis;
end;
theorem Th13:
EMF(C) c= f
proof
let x be Element of C;
A1: rng f c= [.0,jj.] by RELAT_1:def 19;
dom f = C & (EMF(C)).x = 0 by FUNCT_2:def 1,FUNCT_3:def 3;
hence thesis by A1,Th12;
end;
theorem Th14:
f c= UMF(C)
proof
let x be Element of C;
A1: 0 in REAL by XREAL_0:def 1;
A2: rng f c= [.0,1.] by RELAT_1:def 19;
dom f = C & (UMF(C)).x = 1 by FUNCT_2:def 1,FUNCT_3:def 3;
hence thesis by A2,Th12,A1;
end;
theorem Th15:
for x be Element of C,h be Membership_Func of C holds (EMF(C)).x
<= h.x & h.x <= (UMF(C)).x by Th13,Th14,Def2;
theorem Th16:
min(f,g) c= f & f c= max(f,g)
proof
thus min(f,g) c= f
proof
let x be Element of C;
min(f,g).x = min(f.x,g.x) by Def3;
hence thesis by XXREAL_0:17;
end;
let x be Element of C;
max(f,g).x = max(f.x,g.x) by Def4;
hence thesis by XXREAL_0:25;
end;
theorem Th17:
max(f,UMF(C)) = UMF(C) & min(f,UMF(C)) = f & max(f,EMF(C)) = f &
min(f,EMF(C)) = EMF(C)
proof
A1: C = dom max(f,EMF(C)) & C = dom min(f,EMF(C)) by FUNCT_2:def 1;
A2: for x being Element of C st x in C holds min(f,UMF(C)).x = f.x
proof
let x be Element of C;
A3: f.x <= (UMF(C)).x by Th15;
min(f,UMF(C)).x = min(f.x,(UMF(C)).x) by Def3
.=f.x by A3,XXREAL_0:def 9;
hence thesis;
end;
A4: for x being Element of C st x in C holds min(f,EMF(C)).x = (EMF(C)).x
proof
let x be Element of C;
A5: (EMF(C)).x <= f.x by Th15;
min(f,EMF(C)).x = min(f.x,(EMF(C)).x) by Def3
.=(EMF(C)).x by A5,XXREAL_0:def 9;
hence thesis;
end;
A6: for x being Element of C st x in C holds max(f,EMF(C)).x = f.x
proof
let x be Element of C;
A7: (EMF(C)).x <= f.x by Th15;
max(f,EMF(C)).x = max(f.x,(EMF(C)).x) by Def4
.=f.x by A7,XXREAL_0:def 10;
hence thesis;
end;
max(f,UMF(C)) c= UMF(C) & UMF(C) c= max(f,UMF(C)) by Th14,Th16;
hence max(f,UMF(C)) = UMF(C) by Lm1;
A8: C = dom EMF(C) by FUNCT_2:def 1;
C = dom min(f,UMF(C)) & C = dom f by FUNCT_2:def 1;
hence thesis by A2,A6,A1,A8,A4,PARTFUN1:5;
end;
theorem Th18:
f c= h & g c= h implies max(f,g) c= h
proof
assume
A1: f c= h & g c= h;
let x be Element of C;
A2: max(f.x,g.x) = max(f,g).x by Def4;
f.x <= h.x & g.x <= h.x by A1;
hence thesis by A2,XXREAL_0:28;
end;
theorem
f c= g implies max(f,h) c= max(g,h)
proof
assume
A1: f c= g;
let x be Element of C;
f.x <= g.x by A1;
then max(f.x,h.x) <= max(g.x,h.x) by XXREAL_0:26;
then max(f.x,h.x) <= max(g,h).x by Def4;
hence thesis by Def4;
end;
theorem
f c= g & h c= h1 implies max(f,h) c= max(g,h1)
proof
assume
A1: f c= g & h c= h1;
let x be Element of C;
f.x <= g.x & h.x <= h1.x by A1;
then max(f.x,h.x) <= max(g.x,h1.x) by XXREAL_0:26;
then max(f,h).x <= max(g.x,h1.x) by Def4;
hence thesis by Def4;
end;
theorem
f c= g implies max(f,g) = g
proof
assume f c= g;
then
A1: max(f,g) c= g by Th18;
g c= max(f,g) by Th16;
hence thesis by A1,Lm1;
end;
theorem
min(f,g) c= max(f,g)
proof
let x be Element of C;
min(f.x,g.x) <= f.x & f.x <= max(f.x,g.x) by XXREAL_0:17,25;
then min(f.x,g.x) <= max(f.x,g.x) by XXREAL_0:2;
then min(f.x,g.x) <= max(f,g).x by Def4;
hence thesis by Def3;
end;
theorem Th23:
h c= f & h c= g implies h c= min(f,g)
proof
assume
A1: h c= f & h c= g;
let x be Element of C;
h.x <= f.x & h.x <= g.x by A1;
then h.x <= min(f.x,g.x) by XXREAL_0:20;
hence thesis by Def3;
end;
theorem
f c= g implies min(f,h) c= min(g,h)
proof
assume
A1: f c= g;
let x be Element of C;
f.x <= g.x by A1;
then min(f.x,h.x) <= min(g.x,h.x) by XXREAL_0:18;
then min(f,h).x <= min(g.x,h.x) by Def3;
hence thesis by Def3;
end;
theorem
f c= g & h c= h1 implies min(f,h) c= min(g,h1)
proof
assume
A1: f c= g & h c= h1;
let x be Element of C;
f.x <= g.x & h.x <= h1.x by A1;
then min(f.x,h.x) <= min(g.x,h1.x) by XXREAL_0:18;
then min(f,h).x <= min(g.x,h1.x) by Def3;
hence thesis by Def3;
end;
theorem Th26:
f c= g implies min(f,g) = f
proof
assume
A1: f c= g;
A2: for x being Element of C st x in C holds min(f,g).x = f.x
proof
let x be Element of C;
f.x <= g.x by A1;
then f.x = min(f.x,g.x) by XXREAL_0:def 9
.= min(f,g).x by Def3;
hence thesis;
end;
C = dom min(f,g) & C = dom f by FUNCT_2:def 1;
hence thesis by A2,PARTFUN1:5;
end;
theorem
f c= g & f c= h & min(g,h) = EMF(C) implies f = EMF(C)
proof
assume that
A1: f c= g & f c= h and
A2: min(g,h)= EMF(C);
A3: for x being Element of C st x in C holds f.x = (EMF(C)).x
proof
let x be Element of C;
f.x <= g.x & f.x <= h.x by A1;
then f.x <= min(g.x,h.x) by XXREAL_0:20;
then
A4: f.x <= min(g,h).x by Def3;
(EMF(C)).x <= f.x by Th15;
hence thesis by A2,A4,XXREAL_0:1;
end;
C = dom f & C = dom EMF(C) by FUNCT_2:def 1;
hence thesis by A3,PARTFUN1:5;
end;
theorem
max(min(f,g),min(f,h)) = f implies f c= max(g,h)
proof
assume
A1: max(min(f,g),min(f,h)) = f;
let x be Element of C;
max(min(f,g),min(f,h)).x = max(min(f,g).x,min(f,h).x) by Def4
.=max(min(f,g).x,min(f.x,h.x)) by Def3
.=max(min(f.x,g.x),min(f.x,h.x)) by Def3
.=min(f.x,max(g.x,h.x)) by XXREAL_0:38;
then f.x <= max(g.x,h.x) by A1,XXREAL_0:def 9;
hence thesis by Def4;
end;
theorem
f c= g & min(g,h) = EMF(C) implies min(f,h) = EMF(C)
proof
assume that
A1: f c= g and
A2: min(g,h) = EMF(C);
A3: for x being Element of C st x in C holds min(f,h).x = (EMF(C)).x
proof
let x be Element of C;
f.x <= g.x by A1;
then min(f.x,h.x) <= min(g.x,h.x) by XXREAL_0:18;
then min(f.x,h.x) <= min(g,h).x by Def3;
then
A4: min(f,h).x <= min(g,h).x by Def3;
(EMF(C)).x <= min(f,h).x by Th15;
hence thesis by A2,A4,XXREAL_0:1;
end;
C = dom min(f,h) & C = dom EMF(C) by FUNCT_2:def 1;
hence thesis by A3,PARTFUN1:5;
end;
theorem
f c= EMF(C) implies f = EMF(C)
proof
EMF(C) c= f by Th13;
hence thesis by Lm1;
end;
theorem
max(f,g) = EMF(C) iff f = EMF(C) & g = EMF(C)
proof
thus max(f,g) = EMF(C) implies f = EMF(C) & g = EMF(C)
proof
assume
A1: max(f,g) = EMF(C);
A2: for x being Element of C st x in C holds f.x = (EMF(C)).x
proof
let x be Element of C;
max(f.x,g.x) =(EMF(C)).x by A1,Def4;
then
A3: f.x <= (EMF(C)).x by XXREAL_0:25;
(EMF(C)).x <= f.x by Th15;
hence thesis by A3,XXREAL_0:1;
end;
A4: for x being Element of C st x in C holds g.x = (EMF(C)).x
proof
let x be Element of C;
max(f.x,g.x) =(EMF(C)).x by A1,Def4;
then
A5: g.x <= (EMF(C)).x by XXREAL_0:25;
(EMF(C)).x <= g.x by Th15;
hence thesis by A5,XXREAL_0:1;
end;
C = dom f & C = dom EMF(C) by FUNCT_2:def 1;
hence f = EMF(C) by A2,PARTFUN1:5;
C = dom g & C = dom EMF(C) by FUNCT_2:def 1;
hence g = EMF(C) by A4,PARTFUN1:5;
end;
assume f = EMF(C) & g = EMF(C);
hence thesis;
end;
theorem
f = max(g,h) iff g c= f & h c= f & for h1 st g c= h1 & h c= h1 holds f c= h1
proof
hereby
assume
A1: f = max(g,h);
hence g c= f & h c= f by Th16;
let h1;
assume
A2: g c= h1 & h c= h1;
thus f c= h1
proof
let x be Element of C;
g.x <= h1.x & h.x <= h1.x by A2;
then max(g.x,h.x) <= h1.x by XXREAL_0:28;
hence thesis by A1,Def4;
end;
end;
assume that
A3: g c= f & h c= f and
A4: for h1 st g c= h1 & h c= h1 holds f c= h1;
g c= max(g,h) & h c= max(g,h) by Th16;
then
A5: f c= max(g,h) by A4;
max(g,h) c= f by A3,Th18;
hence thesis by A5,Lm1;
end;
theorem
f = min(g,h) iff f c= g & f c= h & for h1 st h1 c= g & h1 c= h holds h1 c= f
proof
hereby
assume
A1: f = min(g,h);
hence f c= g & f c= h by Th16;
let h1;
assume
A2: h1 c= g & h1 c= h;
thus h1 c= f
proof
let x be Element of C;
h1.x <= g.x & h1.x <= h.x by A2;
then min(g.x,h.x) >= h1.x by XXREAL_0:20;
hence thesis by A1,Def3;
end;
end;
assume that
A3: f c= g & f c= h and
A4: for h1 st h1 c= g & h1 c= h holds h1 c= f;
min(g,h) c= g & min(g,h) c= h by Th16;
then
A5: min(g,h) c= f by A4;
f c= min(g,h) by A3,Th23;
hence thesis by A5,Lm1;
end;
theorem
f c= max(g,h) & min(f,h) = EMF(C) implies f c= g
proof
assume that
A1: f c= max(g,h) and
A2: min(f,h) = EMF(C);
let x be Element of C;
min(f,max(g,h)) = f by A1,Th26;
then f = max(min(f,g),min(f,h)) by Th9
.= min(f,g) by A2,Th17;
then f.x = min(f.x,g.x) by Def3;
hence thesis by XXREAL_0:def 9;
end;
Lm2: f c= g implies 1_minus g c= 1_minus f
proof
assume
A1: f c= g;
let x be Element of C;
f.x <= g.x by A1;
then 1-(g.x) <= 1-(f.x) by XREAL_1:10;
then (1_minus(g)).x <= 1-(f.x) by Def5;
hence thesis by Def5;
end;
theorem Th35:
f c= g iff 1_minus g c= 1_minus f
proof
1_minus 1_minus f = f & 1_minus 1_minus g = g;
hence thesis by Lm2;
end;
theorem
f c= 1_minus g implies g c= 1_minus f
proof
1_minus 1_minus f = f;
hence thesis by Th35;
end;
theorem
1_minus max(f,g) c= 1_minus f by Th16,Th35;
theorem
1_minus f c= 1_minus min(f,g) by Th16,Th35;
theorem Th39:
1_minus(EMF(C)) = UMF(C) & 1_minus(UMF(C)) = EMF(C)
proof
A1: for x being Element of C st x in C holds (1_minus(EMF(C))).x = (UMF(C)). x
proof
let x be Element of C;
(1_minus(EMF(C))).x = 1 - (EMF(C)).x by Def5
.= 1 - 0 by FUNCT_3:def 3
.= 1;
hence thesis by FUNCT_3:def 3;
end;
C = dom 1_minus(EMF(C)) & C = dom UMF(C) by FUNCT_2:def 1;
hence 1_minus(EMF(C)) = UMF(C) by A1,PARTFUN1:5;
A2: for x being Element of C st x in C holds (1_minus(UMF(C))).x = (EMF(C)). x
proof
let x be Element of C;
(1_minus(UMF(C))).x = 1 - (UMF(C)).x by Def5
.= 1 - 1 by FUNCT_3:def 3
.= 0;
hence thesis by FUNCT_3:def 3;
end;
C = dom 1_minus(UMF(C)) & C = dom EMF(C) by FUNCT_2:def 1;
hence thesis by A2,PARTFUN1:5;
end;
:: Exclusive Sum, Absolute Difference
definition
let C be non empty set;
let h,g be Membership_Func of C;
func h \+\ g -> Membership_Func of C equals
max(min(h,1_minus(g)),min(
1_minus(h),g));
coherence;
commutativity;
end;
theorem
f \+\ EMF(C) = f
proof
thus f \+\ EMF(C) = max(min(f,UMF(C)),min(1_minus(f),EMF(C))) by Th39
.= max(f,min(1_minus(f),EMF(C))) by Th17
.= max(f,EMF(C)) by Th17
.= f by Th17;
end;
theorem
f \+\ UMF(C) = 1_minus f
proof
thus f \+\ UMF(C) = max(min(f,EMF(C)),min(1_minus(f),UMF(C))) by Th39
.= max(EMF(C),min(1_minus(f),UMF(C))) by Th17
.= min(1_minus(f),UMF(C)) by Th17
.= 1_minus f by Th17;
end;
theorem
min(min(max(f,g),max(g,h)),max(h,f)) = max(max(min(f,g),min(g,h)),min( h,f))
proof
thus min(min(max(f,g),max(g,h)),max(h,f)) = max(min(min(max(f,g),max(g,h)),h
),min(min(max(f,g),max(g,h)),f)) by Th9
.=max(min(max(f,g),min(max(g,h),h)),min(min(max(f,g),max(g,h)),f)) by Th7
.=max(min(max(f,g),min(max(h,g),h)),min(min(max(f,g),f),max(g,h))) by Th7
.=max(min(max(f,g),h),min(min(max(f,g),f),max(g,h))) by Th8
.=max(min(max(f,g),h),min(f,max(g,h))) by Th8
.=max(min(h,max(f,g)),max(min(f,g),min(f,h) )) by Th9
.=max(max(min(f,g),min(f,h)),max(min(h,f),min(h,g))) by Th9
.=max(max(max(min(f,g),min(f,h)),min(f,h)),min(h,g)) by Th7
.=max(max(min(f,g),max(min(f,h),min(f,h))),min(h,g)) by Th7
.=max(max(min(f,g),min(g,h)),min(h,f)) by Th7;
end;
theorem
max(min(f,g),min(1_minus f, 1_minus g)) c= 1_minus (f \+\ g)
proof
set f1 = 1_minus f, g1 = 1_minus g;
let x be Element of C;
1_minus (f \+\ g) = min( 1_minus min(f,g1) , 1_minus min(f1,g)) by Th10
.= min( max(f1,1_minus g1),1_minus min(f1,g)) by Th10
.= min( max(f1,g),max(1_minus f1,g1)) by Th10
.= max(min(max(f1,g),f),min(max(f1,g),g1)) by Th9
.= max( max(min(f,f1),min(f,g)) ,min(max(f1,g),g1)) by Th9
.= max( max(min(f,f1),min(f,g)) , max(min(g1,f1),min(g1,g))) by Th9
.= max( max(max(min(f,g),min(f,f1)),min(g1,f1)) , min(g1,g)) by Th7
.= max( max(max(min(g1,f1),min(f,g)),min(f,f1)) , min(g1,g)) by Th7
.= max( max(min(g1,f1),min(f,g)), max(min(f,f1) , min(g1,g))) by Th7;
then
(1_minus (f \+\ g)).x = max(max(min(f,g),min(f1,g1)).x,max(min(f,f1),min
(g1,g)).x) by Def4;
hence thesis by XXREAL_0:25;
end;
theorem
max(f \+\ g, min(f,g)) c= max(f,g)
proof
set f1 = 1_minus f, g1 = 1_minus g;
let x be Element of C;
max(f \+\ g, min(f,g)) = max(min(f,g1),max(min(f1,g),min(f,g))) by Th7
.= max(min(f,g1),min(max(min(f1,g),f),max(g,min(f1,g)))) by Th9
.= max(min(f,g1),min(max(min(f1,g),f),g)) by Th8
.= min(max(min(f,g1),max(f,min(f1,g))),max(min(f,g1),g)) by Th9
.= min(max(max(f,min(f,g1)),min(f1,g)) ,max(min(f,g1),g)) by Th7
.= min(max(f,min(f1,g)) ,max(min(f,g1),g)) by Th8
.= min( min(max(f,f1),max(f,g)) ,max(g,min(f,g1))) by Th9
.= min( min(max(f,f1),max(f,g)) , min(max(g,f),max(g,g1)) ) by Th9
.= min(min( min(max(f,f1),max(f,g)),max(g,f) ),max(g,g1) ) by Th7
.= min(min( max(f,f1),min(max(f,g),max(f,g)) ),max(g,g1) ) by Th7
.= min(max(f,g),min(max(f,f1),max(g,g1))) by Th7;
then
max(f \+\ g, min(f,g)).x = min(max(f,g).x,min(max(f,f1),max(g,g1)).x) by Def3
;
hence thesis by XXREAL_0:17;
end;
theorem
f \+\ f = min(f, 1_minus f);
definition
let C be non empty set;
let h,g be Membership_Func of C;
func ab_difMF(h,g) -> Membership_Func of C means
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;
|.h.x - g.x.| is set by TARSKI:1;
hence thesis by A3;
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;
0 <= |.h.x - g.x.| by COMPLEX1:46;
then
A11: 0 <= IT.x by A3,A9;
A12: A = [. lower_bound A, upper_bound A .] by INTEGRA1:4;
then
A13: 0=lower_bound A by INTEGRA1:5;
A14: x in C;
then x in dom h by FUNCT_2:def 1;
then
A15: h.x in rng h by FUNCT_1:def 3;
x in dom g by A14,FUNCT_2:def 1;
then
A16: g.x in rng g by FUNCT_1:def 3;
then 0 <= g.x by A7,A13,INTEGRA2:1;
then
A17: 1-0 >= 1-g.x by XREAL_1:10;
A18: 1=upper_bound A by A12,INTEGRA1:5;
then g.x <= 1 by A7,A16,INTEGRA2:1;
then
A19: -g.x >= -1 by XREAL_1:24;
0 <= h.x by A8,A13,A15,INTEGRA2:1;
then 0 - g.x <= h.x - g.x by XREAL_1:9;
then
A20: -1 <= h.x - g.x by A19,XXREAL_0:2;
h.x <= 1 by A8,A18,A15,INTEGRA2:1;
then h.x - g.x <= 1 - g.x by XREAL_1:9;
then h.x - g.x <= 1 by A17,XXREAL_0:2;
then |.h.x - g.x.| <= 1 by A20,ABSVALUE:5;
then IT.x <= 1 by A3,A9;
hence thesis by A10,A13,A18,A11,INTEGRA2:1;
end;
then
A21: rng IT c= [.0,1.] by TARSKI:def 3;
IT is total by A5,PARTFUN1:def 2;
then IT is Membership_Func of C by A21,RELAT_1:def 19;
hence thesis by A6;
end;
uniqueness
proof
let F,G be Membership_Func of C;
assume that
A22: for c being Element of C holds F.c = |.h.c - g.c.| and
A23: for c being Element of C holds G.c = |.h.c - g.c.|;
A24: 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 A22;
hence thesis by A23;
end;
C = dom F & C = dom G by FUNCT_2:def 1;
hence thesis by A24,PARTFUN1:5;
end;
end;