:: FUZZY_1 semantic presentation
begin
registration
let x, y be set ;
clusterK146(x,y) -> [.0,1.] -valued ;
coherence
chi (x,y) is [.0,1.] -valued
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; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;
registration
let C be non empty set ;
cluster non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued for Element of K6(K7(C,REAL));
existence
ex b1 being Function of C,REAL st b1 is [.0,1.] -valued
proof
take chi (C,C) ; ::_thesis: chi (C,C) is [.0,1.] -valued
thus rng (chi (C,C)) c= [.0,1.] by RELAT_1:def_19; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;
definition
let C be non empty set ;
mode Membership_Func of C is [.0,1.] -valued Function of C,REAL;
end;
theorem :: FUZZY_1:1
for C being non empty set holds chi (C,C) is Membership_Func of C ;
registration
let X be non empty set ;
cluster[.0,1.] -valued Function-like V30(X, REAL ) -> real-valued for Element of K6(K7(X,REAL));
coherence
for b1 being Membership_Func of X holds b1 is real-valued ;
end;
definition
let f, g be real-valued Function;
predf is_less_than g means :Def1: :: FUZZY_1:def 1
( dom f c= dom g & ( for x being set st x in dom f holds
f . x <= g . x ) );
reflexivity
for f being real-valued Function holds
( dom f c= dom f & ( for x being set st x in dom f holds
f . x <= f . x ) ) ;
end;
:: deftheorem Def1 defines is_less_than FUZZY_1:def_1_:_
for f, g being real-valued Function holds
( f is_less_than g iff ( dom f c= dom g & ( for x being set st x in dom f holds
f . x <= g . x ) ) );
notation
let X be non empty set ;
let f, g be Membership_Func of X;
synonym f c= g for X is_less_than f;
end;
definition
let X be non empty set ;
let f, g be Membership_Func of X;
:: original: is_less_than
redefine predf is_less_than g means :Def2: :: FUZZY_1:def 2
for x being Element of X holds f . x <= g . x;
compatibility
( f is_less_than g iff for x being Element of X holds f . x <= g . x )
proof
thus ( f is_less_than g iff for x being Element of X holds f . x <= g . x ) ::_thesis: verum
proof
hereby ::_thesis: ( ( for x being Element of X holds f . x <= g . x ) implies f is_less_than g )
assume A1: f is_less_than g ; ::_thesis: for x being Element of X holds f . x <= g . x
thus for x being Element of X holds f . x <= g . x ::_thesis: verum
proof
let x be Element of X; ::_thesis: f . x <= g . x
dom f = X by FUNCT_2:def_1;
hence f . x <= g . x by A1, Def1; ::_thesis: verum
end;
end;
assume for x being Element of X holds f . x <= g . x ; ::_thesis: f is_less_than g
then ( dom g = X & ( for x being set st x in dom f holds
f . x <= g . x ) ) by FUNCT_2:def_1;
hence f is_less_than g by Def1; ::_thesis: verum
end;
end;
end;
:: deftheorem Def2 defines is_less_than FUZZY_1:def_2_:_
for X being non empty set
for f, g being Membership_Func of X holds
( f is_less_than g iff for x being Element of X holds f . x <= g . x );
Lm1: for C being non empty set
for f, g being Membership_Func of C st g c= & f c= holds
f = g
proof
let C be non empty set ; ::_thesis: for f, g being Membership_Func of C st g c= & f c= holds
f = g
let f, g be Membership_Func of C; ::_thesis: ( g c= & f c= implies f = g )
set A = f;
set B = g;
assume A1: ( g c= & f c= ) ; ::_thesis: f = g
A2: for c being Element of C st c in C holds
f . c = g . c
proof
let c be Element of C; ::_thesis: ( c in C implies f . c = g . c )
( f . c <= g . c & g . c <= f . c ) by A1, Def2;
hence ( c in C implies f . c = g . c ) by XXREAL_0:1; ::_thesis: verum
end;
( C = dom f & C = dom g ) by FUNCT_2:def_1;
hence f = g by A2, PARTFUN1:5; ::_thesis: verum
end;
theorem :: FUZZY_1:2
for C being non empty set
for f, g being Membership_Func of C holds
( f = g iff ( g c= & f c= ) ) by Lm1;
theorem :: FUZZY_1:3
for C being non empty set
for f being Membership_Func of C holds f c= ;
theorem :: FUZZY_1:4
for C being non empty set
for f, g, h being Membership_Func of C st g c= & h c= holds
h c= ;
begin
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: :: FUZZY_1:def 3
for c being Element of C holds it . c = min ((h . c),(g . c));
existence
ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = min ((h . c),(g . c))
proof
defpred S1[ set , set ] means $2 = min ((h . $1),(g . $1));
A1: for x, y1, y2 being set st x in C & S1[x,y1] & S1[x,y2] holds
y1 = y2 ;
A2: for x, y being set st x in C & S1[x,y] holds
y in REAL ;
consider IT being PartFunc of C,REAL such that
A3: ( ( for x being set holds
( x in dom IT iff ( x in C & ex y being set st S1[x,y] ) ) ) & ( for x being set st x in dom IT holds
S1[x,IT . x] ) ) from PARTFUN1:sch_2(A2, A1);
for x being set st x in C holds
x in dom IT
proof
let x be set ; ::_thesis: ( x in C implies x in dom IT )
A4: ex y being set st y = min ((h . x),(g . x)) ;
assume x in C ; ::_thesis: x in dom IT
hence x in dom IT by A3, A4; ::_thesis: verum
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 set st y in rng IT holds
y in [.0,1.]
proof
reconsider A = [.0,1.] as non empty closed_interval Subset of REAL by MEASURE5:14;
let y be set ; ::_thesis: ( y in rng IT implies y in [.0,1.] )
assume y in rng IT ; ::_thesis: y in [.0,1.]
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 y in [.0,1.] by A10, A13, A16, A17, INTEGRA2:1; ::_thesis: verum
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 ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = min ((h . c),(g . c)) by A6; ::_thesis: verum
end;
uniqueness
for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = min ((h . c),(g . c)) ) & ( for c being Element of C holds b2 . c = min ((h . c),(g . c)) ) holds
b1 = b2
proof
let F, G be Membership_Func of C; ::_thesis: ( ( for c being Element of C holds F . c = min ((h . c),(g . c)) ) & ( for c being Element of C holds G . c = min ((h . c),(g . c)) ) implies F = G )
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)) ; ::_thesis: F = G
A22: for c being Element of C st c in C holds
F . c = G . c
proof
let c be Element of C; ::_thesis: ( c in C implies F . c = G . c )
F . c = min ((h . c),(g . c)) by A20;
hence ( c in C implies F . c = G . c ) by A21; ::_thesis: verum
end;
( C = dom F & C = dom G ) by FUNCT_2:def_1;
hence F = G by A22, PARTFUN1:5; ::_thesis: verum
end;
idempotence
for h being Membership_Func of C
for c being Element of C holds h . c = min ((h . c),(h . c)) ;
commutativity
for b1, h, g being Membership_Func of C st ( for c being Element of C holds b1 . c = min ((h . c),(g . c)) ) holds
for c being Element of C holds b1 . c = min ((g . c),(h . c)) ;
end;
:: deftheorem Def3 defines min FUZZY_1:def_3_:_
for C being non empty set
for h, g, b4 being Membership_Func of C holds
( b4 = min (h,g) iff for c being Element of C holds b4 . c = min ((h . c),(g . c)) );
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: :: FUZZY_1:def 4
for c being Element of C holds it . c = max ((h . c),(g . c));
existence
ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = max ((h . c),(g . c))
proof
defpred S1[ set , set ] means $2 = max ((h . $1),(g . $1));
A1: for x, y1, y2 being set st x in C & S1[x,y1] & S1[x,y2] holds
y1 = y2 ;
A2: for x, y being set st x in C & S1[x,y] holds
y in REAL ;
consider IT being PartFunc of C,REAL such that
A3: ( ( for x being set holds
( x in dom IT iff ( x in C & ex y being set st S1[x,y] ) ) ) & ( for x being set st x in dom IT holds
S1[x,IT . x] ) ) from PARTFUN1:sch_2(A2, A1);
for x being set st x in C holds
x in dom IT
proof
let x be set ; ::_thesis: ( x in C implies x in dom IT )
A4: ex y being set st y = max ((h . x),(g . x)) ;
assume x in C ; ::_thesis: x in dom IT
hence x in dom IT by A3, A4; ::_thesis: verum
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 set st y in rng IT holds
y in [.0,1.]
proof
reconsider A = [.0,1.] as non empty closed_interval Subset of REAL by MEASURE5:14;
let y be set ; ::_thesis: ( y in rng IT implies y in [.0,1.] )
assume y in rng IT ; ::_thesis: y in [.0,1.]
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 y in [.0,1.] by A10, A12, A16, A15, INTEGRA2:1; ::_thesis: verum
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 ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = max ((h . c),(g . c)) by A6; ::_thesis: verum
end;
uniqueness
for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = max ((h . c),(g . c)) ) & ( for c being Element of C holds b2 . c = max ((h . c),(g . c)) ) holds
b1 = b2
proof
let F, G be Membership_Func of C; ::_thesis: ( ( for c being Element of C holds F . c = max ((h . c),(g . c)) ) & ( for c being Element of C holds G . c = max ((h . c),(g . c)) ) implies F = G )
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)) ; ::_thesis: F = G
A21: for c being Element of C st c in C holds
F . c = G . c
proof
let c be Element of C; ::_thesis: ( c in C implies F . c = G . c )
F . c = max ((h . c),(g . c)) by A19;
hence ( c in C implies F . c = G . c ) by A20; ::_thesis: verum
end;
( C = dom F & C = dom G ) by FUNCT_2:def_1;
hence F = G by A21, PARTFUN1:5; ::_thesis: verum
end;
idempotence
for h being Membership_Func of C
for c being Element of C holds h . c = max ((h . c),(h . c)) ;
commutativity
for b1, h, g being Membership_Func of C st ( for c being Element of C holds b1 . c = max ((h . c),(g . c)) ) holds
for c being Element of C holds b1 . c = max ((g . c),(h . c)) ;
end;
:: deftheorem Def4 defines max FUZZY_1:def_4_:_
for C being non empty set
for h, g, b4 being Membership_Func of C holds
( b4 = max (h,g) iff for c being Element of C holds b4 . c = max ((h . c),(g . c)) );
definition
let C be non empty set ;
let h be Membership_Func of C;
func 1_minus h -> Membership_Func of C means :Def5: :: FUZZY_1:def 5
for c being Element of C holds it . c = 1 - (h . c);
existence
ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = 1 - (h . c)
proof
deffunc H1( set ) -> Element of REAL = 1 - (h . $1);
defpred S1[ set ] means $1 in dom h;
consider IT being PartFunc of C,REAL such that
A1: ( ( for x being Element of C holds
( x in dom IT iff S1[x] ) ) & ( for x being Element of C st x in dom IT holds
IT . x = H1(x) ) ) from SEQ_1:sch_3();
for x being set st x in C holds
x in dom IT
proof
let x be set ; ::_thesis: ( x in C implies x in dom IT )
A2: dom h = C by FUNCT_2:def_1;
assume x in C ; ::_thesis: x in dom IT
hence x in dom IT by A1, A2; ::_thesis: verum
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 = 1 - (h . c) by A1;
A5: rng h c= [.0,1.] by RELAT_1:def_19;
for y being set st y in rng IT holds
y in [.0,1.]
proof
reconsider A = [.0,1.] as non empty closed_interval Subset of REAL by MEASURE5:14;
let y be set ; ::_thesis: ( y in rng IT implies y in [.0,1.] )
assume y in rng IT ; ::_thesis: y in [.0,1.]
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 1 - (h . 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 <= 1 - (h . x) by XREAL_1:48;
then 0 <= IT . x by A1, A6;
hence y in [.0,1.] by A7, A9, A12, A11, INTEGRA2:1; ::_thesis: verum
end;
then A13: rng IT c= [.0,1.] by TARSKI:def_3;
IT is total by A3, PARTFUN1:def_2;
then IT is Membership_Func of C by A13, RELAT_1:def_19;
hence ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = 1 - (h . c) by A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = 1 - (h . c) ) & ( for c being Element of C holds b2 . c = 1 - (h . c) ) holds
b1 = b2
proof
let F, G be Membership_Func of C; ::_thesis: ( ( for c being Element of C holds F . c = 1 - (h . c) ) & ( for c being Element of C holds G . c = 1 - (h . c) ) implies F = G )
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) ; ::_thesis: F = G
A16: for c being Element of C st c in C holds
F . c = G . c
proof
let c be Element of C; ::_thesis: ( c in C implies F . c = G . c )
F . c = 1 - (h . c) by A14;
hence ( c in C implies F . c = G . c ) by A15; ::_thesis: verum
end;
( C = dom F & C = dom G ) by FUNCT_2:def_1;
hence F = G by A16, PARTFUN1:5; ::_thesis: verum
end;
involutiveness
for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = 1 - (b2 . c) ) holds
for c being Element of C holds b2 . c = 1 - (b1 . c)
proof
let h1, h2 be Membership_Func of C; ::_thesis: ( ( for c being Element of C holds h1 . c = 1 - (h2 . c) ) implies for c being Element of C holds h2 . c = 1 - (h1 . c) )
assume A17: for c being Element of C holds h1 . c = 1 - (h2 . c) ; ::_thesis: for c being Element of C holds h2 . c = 1 - (h1 . c)
let c be Element of C; ::_thesis: h2 . c = 1 - (h1 . c)
thus h2 . c = 1 - (1 - (h2 . c))
.= 1 - (h1 . c) by A17 ; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines 1_minus FUZZY_1:def_5_:_
for C being non empty set
for h, b3 being Membership_Func of C holds
( b3 = 1_minus h iff for c being Element of C holds b3 . c = 1 - (h . c) );
theorem :: FUZZY_1:5
for C being non empty set
for c being Element of C
for h, g being Membership_Func of C holds
( min ((h . c),(g . c)) = (min (h,g)) . c & max ((h . c),(g . c)) = (max (h,g)) . c ) by Def3, Def4;
theorem :: FUZZY_1:6
for C being non empty set
for h, f, g being Membership_Func of C holds
( 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: :: FUZZY_1:7
for C being non empty set
for f, g, h being Membership_Func of C holds
( max ((max (f,g)),h) = max (f,(max (g,h))) & min ((min (f,g)),h) = min (f,(min (g,h))) )
proof
let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds
( max ((max (f,g)),h) = max (f,(max (g,h))) & min ((min (f,g)),h) = min (f,(min (g,h))) )
let f, g, h be Membership_Func of C; ::_thesis: ( max ((max (f,g)),h) = max (f,(max (g,h))) & min ((min (f,g)),h) = min (f,(min (g,h))) )
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; ::_thesis: ( x in C implies (max ((max (f,g)),h)) . x = (max (f,(max (g,h)))) . x )
(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 ( x in C implies (max ((max (f,g)),h)) . x = (max (f,(max (g,h)))) . x ) ; ::_thesis: verum
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; ::_thesis: ( x in C implies (min ((min (f,g)),h)) . x = (min (f,(min (g,h)))) . x )
(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 ( x in C implies (min ((min (f,g)),h)) . x = (min (f,(min (g,h)))) . x ) ; ::_thesis: verum
end;
( C = dom (max ((max (f,g)),h)) & C = dom (max (f,(max (g,h)))) ) by FUNCT_2:def_1;
hence ( max ((max (f,g)),h) = max (f,(max (g,h))) & min ((min (f,g)),h) = min (f,(min (g,h))) ) by A1, A2, A3, PARTFUN1:5; ::_thesis: verum
end;
theorem Th8: :: FUZZY_1:8
for C being non empty set
for f, g being Membership_Func of C holds
( max (f,(min (f,g))) = f & min (f,(max (f,g))) = f )
proof
let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds
( max (f,(min (f,g))) = f & min (f,(max (f,g))) = f )
let f, g be Membership_Func of C; ::_thesis: ( max (f,(min (f,g))) = f & min (f,(max (f,g))) = f )
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; ::_thesis: ( x in C implies (max (f,(min (f,g)))) . x = f . x )
(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 ( x in C implies (max (f,(min (f,g)))) . x = f . x ) ; ::_thesis: verum
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; ::_thesis: ( x in C implies (min (f,(max (f,g)))) . x = f . x )
(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 ( x in C implies (min (f,(max (f,g)))) . x = f . x ) ; ::_thesis: verum
end;
( C = dom (max (f,(min (f,g)))) & C = dom f ) by FUNCT_2:def_1;
hence ( max (f,(min (f,g))) = f & min (f,(max (f,g))) = f ) by A1, A2, A3, PARTFUN1:5; ::_thesis: verum
end;
theorem Th9: :: FUZZY_1:9
for C being non empty set
for f, g, h being Membership_Func of C holds
( 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
let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds
( min (f,(max (g,h))) = max ((min (f,g)),(min (f,h))) & max (f,(min (g,h))) = min ((max (f,g)),(max (f,h))) )
let f, g, h be Membership_Func of C; ::_thesis: ( min (f,(max (g,h))) = max ((min (f,g)),(min (f,h))) & max (f,(min (g,h))) = min ((max (f,g)),(max (f,h))) )
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; ::_thesis: ( x in C implies (min (f,(max (g,h)))) . x = (max ((min (f,g)),(min (f,h)))) . x )
(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 ( x in C implies (min (f,(max (g,h)))) . x = (max ((min (f,g)),(min (f,h)))) . x ) ; ::_thesis: verum
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; ::_thesis: ( x in C implies (max (f,(min (g,h)))) . x = (min ((max (f,g)),(max (f,h)))) . x )
(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 ( x in C implies (max (f,(min (g,h)))) . x = (min ((max (f,g)),(max (f,h)))) . x ) ; ::_thesis: verum
end;
( C = dom (min (f,(max (g,h)))) & C = dom (max ((min (f,g)),(min (f,h)))) ) by FUNCT_2:def_1;
hence ( min (f,(max (g,h))) = max ((min (f,g)),(min (f,h))) & max (f,(min (g,h))) = min ((max (f,g)),(max (f,h))) ) by A1, A2, A3, PARTFUN1:5; ::_thesis: verum
end;
theorem :: FUZZY_1:10
canceled;
theorem Th11: :: FUZZY_1:11
for C being non empty set
for f, g being Membership_Func of C holds
( 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
let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds
( 1_minus (max (f,g)) = min ((1_minus f),(1_minus g)) & 1_minus (min (f,g)) = max ((1_minus f),(1_minus g)) )
let f, g be Membership_Func of C; ::_thesis: ( 1_minus (max (f,g)) = min ((1_minus f),(1_minus g)) & 1_minus (min (f,g)) = max ((1_minus f),(1_minus g)) )
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; ::_thesis: ( x in C implies (1_minus (max (f,g))) . x = (min ((1_minus f),(1_minus g))) . x )
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)) + (abs ((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))) - (abs ((1 - (f . x)) - (1 - (g . x))))) / 2 by COMPLEX1:73
.= (((2 - (f . x)) - (g . x)) - (abs (- ((f . x) - (g . x))))) / 2
.= ((2 - ((f . x) + (g . x))) - (abs ((f . x) - (g . x)))) / 2 by COMPLEX1:52
.= 1 - ((((f . x) + (g . x)) + (abs ((f . x) - (g . x)))) / 2) ;
hence ( x in C implies (1_minus (max (f,g))) . x = (min ((1_minus f),(1_minus g))) . x ) by A3; ::_thesis: verum
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; ::_thesis: ( x in C implies (1_minus (min (f,g))) . x = (max ((1_minus f),(1_minus g))) . x )
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)) - (abs ((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))) + (abs ((1 - (f . x)) - (1 - (g . x))))) / 2 by COMPLEX1:74
.= (((2 - (f . x)) - (g . x)) + (abs (- ((f . x) - (g . x))))) / 2
.= ((2 - ((f . x) + (g . x))) + (abs ((f . x) - (g . x)))) / 2 by COMPLEX1:52
.= 1 - ((((f . x) + (g . x)) - (abs ((f . x) - (g . x)))) / 2) ;
hence ( x in C implies (1_minus (min (f,g))) . x = (max ((1_minus f),(1_minus g))) . x ) by A5; ::_thesis: verum
end;
( C = dom (1_minus (max (f,g))) & C = dom (min ((1_minus f),(1_minus g))) ) by FUNCT_2:def_1;
hence ( 1_minus (max (f,g)) = min ((1_minus f),(1_minus g)) & 1_minus (min (f,g)) = max ((1_minus f),(1_minus g)) ) by A1, A2, A4, PARTFUN1:5; ::_thesis: verum
end;
begin
theorem :: FUZZY_1:12
for C being non empty set holds chi ({},C) is Membership_Func of C ;
definition
let C be non empty set ;
func EMF C -> Membership_Func of C equals :: FUZZY_1:def 6
chi ({},C);
correctness
coherence
chi ({},C) is Membership_Func of C;
;
end;
:: deftheorem defines EMF FUZZY_1:def_6_:_
for C being non empty set holds EMF C = chi ({},C);
definition
let C be non empty set ;
func UMF C -> Membership_Func of C equals :: FUZZY_1:def 7
chi (C,C);
correctness
coherence
chi (C,C) is Membership_Func of C;
;
end;
:: deftheorem defines UMF FUZZY_1:def_7_:_
for C being non empty set holds UMF C = chi (C,C);
theorem Th13: :: FUZZY_1:13
for C being non empty set
for a, b being Element of REAL
for f being 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 C be non empty set ; ::_thesis: for a, b being Element of REAL
for f being 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 )
let a, b be Element of REAL ; ::_thesis: for f being 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 )
let f be PartFunc of C,REAL; ::_thesis: ( rng f c= [.a,b.] & a <= b implies for x being Element of C st x in dom f holds
( a <= f . x & f . x <= b ) )
assume that
A1: rng f c= [.a,b.] and
A2: a <= b ; ::_thesis: for x being Element of C st x in dom f holds
( a <= f . x & f . x <= 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; ::_thesis: ( x in dom f implies ( a <= f . x & f . x <= b ) )
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 ; ::_thesis: ( a <= f . x & f . x <= b )
then f . x in rng f by FUNCT_1:def_3;
hence ( a <= f . x & f . x <= b ) by A1, A3, INTEGRA2:1; ::_thesis: verum
end;
hence for x being Element of C st x in dom f holds
( a <= f . x & f . x <= b ) ; ::_thesis: verum
end;
theorem Th14: :: FUZZY_1:14
for C being non empty set
for f being Membership_Func of C holds f c=
proof
let C be non empty set ; ::_thesis: for f being Membership_Func of C holds f c=
let f be Membership_Func of C; ::_thesis: f c=
let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (EMF C) . x <= f . x
A1: rng f c= [.0,1.] by RELAT_1:def_19;
( dom f = C & (EMF C) . x = 0 ) by FUNCT_2:def_1, FUNCT_3:def_3;
hence (EMF C) . x <= f . x by A1, Th13; ::_thesis: verum
end;
theorem Th15: :: FUZZY_1:15
for C being non empty set
for f being Membership_Func of C holds UMF C c=
proof
let C be non empty set ; ::_thesis: for f being Membership_Func of C holds UMF C c=
let f be Membership_Func of C; ::_thesis: UMF C c=
let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: f . x <= (UMF C) . x
A1: 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 f . x <= (UMF C) . x by A1, Th13; ::_thesis: verum
end;
theorem Th16: :: FUZZY_1:16
for C being non empty set
for x being Element of C
for h being Membership_Func of C holds
( (EMF C) . x <= h . x & h . x <= (UMF C) . x )
proof
let C be non empty set ; ::_thesis: for x being Element of C
for h being Membership_Func of C holds
( (EMF C) . x <= h . x & h . x <= (UMF C) . x )
let x be Element of C; ::_thesis: for h being Membership_Func of C holds
( (EMF C) . x <= h . x & h . x <= (UMF C) . x )
let h be Membership_Func of C; ::_thesis: ( (EMF C) . x <= h . x & h . x <= (UMF C) . x )
( h c= & UMF C c= ) by Th14, Th15;
hence ( (EMF C) . x <= h . x & h . x <= (UMF C) . x ) by Def2; ::_thesis: verum
end;
theorem Th17: :: FUZZY_1:17
for C being non empty set
for f, g being Membership_Func of C holds
( f c= & max (f,g) c= )
proof
let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds
( f c= & max (f,g) c= )
let f, g be Membership_Func of C; ::_thesis: ( f c= & max (f,g) c= )
thus f c= ::_thesis: max (f,g) c=
proof
let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (min (f,g)) . x <= f . x
(min (f,g)) . x = min ((f . x),(g . x)) by Def3;
hence (min (f,g)) . x <= f . x by XXREAL_0:17; ::_thesis: verum
end;
let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: f . x <= (max (f,g)) . x
(max (f,g)) . x = max ((f . x),(g . x)) by Def4;
hence f . x <= (max (f,g)) . x by XXREAL_0:25; ::_thesis: verum
end;
theorem Th18: :: FUZZY_1:18
for C being non empty set
for f being Membership_Func of C holds
( max (f,(UMF C)) = UMF C & min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C )
proof
let C be non empty set ; ::_thesis: for f being Membership_Func of C holds
( max (f,(UMF C)) = UMF C & min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C )
let f be Membership_Func of C; ::_thesis: ( max (f,(UMF C)) = UMF C & min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C )
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; ::_thesis: ( x in C implies (min (f,(UMF C))) . x = f . x )
A3: f . x <= (UMF C) . x by Th16;
(min (f,(UMF C))) . x = min ((f . x),((UMF C) . x)) by Def3
.= f . x by A3, XXREAL_0:def_9 ;
hence ( x in C implies (min (f,(UMF C))) . x = f . x ) ; ::_thesis: verum
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; ::_thesis: ( x in C implies (min (f,(EMF C))) . x = (EMF C) . x )
A5: (EMF C) . x <= f . x by Th16;
(min (f,(EMF C))) . x = min ((f . x),((EMF C) . x)) by Def3
.= (EMF C) . x by A5, XXREAL_0:def_9 ;
hence ( x in C implies (min (f,(EMF C))) . x = (EMF C) . x ) ; ::_thesis: verum
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; ::_thesis: ( x in C implies (max (f,(EMF C))) . x = f . x )
A7: (EMF C) . x <= f . x by Th16;
(max (f,(EMF C))) . x = max ((f . x),((EMF C) . x)) by Def4
.= f . x by A7, XXREAL_0:def_10 ;
hence ( x in C implies (max (f,(EMF C))) . x = f . x ) ; ::_thesis: verum
end;
( UMF C c= & max (f,(UMF C)) c= ) by Th15, Th17;
hence max (f,(UMF C)) = UMF C by Lm1; ::_thesis: ( min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C )
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 ( min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C ) by A2, A6, A1, A8, A4, PARTFUN1:5; ::_thesis: verum
end;
theorem Th19: :: FUZZY_1:19
for C being non empty set
for f, h, g being Membership_Func of C st h c= & h c= holds
h c=
proof
let C be non empty set ; ::_thesis: for f, h, g being Membership_Func of C st h c= & h c= holds
h c=
let f, h, g be Membership_Func of C; ::_thesis: ( h c= & h c= implies h c= )
assume A1: ( h c= & h c= ) ; ::_thesis: h c=
let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (max (f,g)) . x <= h . x
A2: max ((f . x),(g . x)) = (max (f,g)) . x by Def4;
( f . x <= h . x & g . x <= h . x ) by A1, Def2;
hence (max (f,g)) . x <= h . x by A2, XXREAL_0:28; ::_thesis: verum
end;
theorem :: FUZZY_1:20
for C being non empty set
for f, g, h being Membership_Func of C st g c= holds
max (g,h) c=
proof
let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C st g c= holds
max (g,h) c=
let f, g, h be Membership_Func of C; ::_thesis: ( g c= implies max (g,h) c= )
assume A1: g c= ; ::_thesis: max (g,h) c=
let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (max (f,h)) . x <= (max (g,h)) . x
f . x <= g . x by A1, Def2;
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 (max (f,h)) . x <= (max (g,h)) . x by Def4; ::_thesis: verum
end;
theorem :: FUZZY_1:21
for C being non empty set
for f, g, h, h1 being Membership_Func of C st g c= & h1 c= holds
max (g,h1) c=
proof
let C be non empty set ; ::_thesis: for f, g, h, h1 being Membership_Func of C st g c= & h1 c= holds
max (g,h1) c=
let f, g, h, h1 be Membership_Func of C; ::_thesis: ( g c= & h1 c= implies max (g,h1) c= )
assume A1: ( g c= & h1 c= ) ; ::_thesis: max (g,h1) c=
let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (max (f,h)) . x <= (max (g,h1)) . x
( f . x <= g . x & h . x <= h1 . x ) by A1, Def2;
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 (max (f,h)) . x <= (max (g,h1)) . x by Def4; ::_thesis: verum
end;
theorem :: FUZZY_1:22
for C being non empty set
for f, g being Membership_Func of C st g c= holds
max (f,g) = g
proof
let C be non empty set ; ::_thesis: for f, g being Membership_Func of C st g c= holds
max (f,g) = g
let f, g be Membership_Func of C; ::_thesis: ( g c= implies max (f,g) = g )
assume g c= ; ::_thesis: max (f,g) = g
then A1: g c= by Th19;
max (f,g) c= by Th17;
hence max (f,g) = g by A1, Lm1; ::_thesis: verum
end;
theorem :: FUZZY_1:23
for C being non empty set
for f, g being Membership_Func of C holds max (f,g) c=
proof
let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds max (f,g) c=
let f, g be Membership_Func of C; ::_thesis: max (f,g) c=
let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (min (f,g)) . x <= (max (f,g)) . x
( min ((f . x),(g . x)) <= f . x & f . x <= max ((f . x),(g . x)) ) by XXREAL_0:17, XXREAL_0: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 (min (f,g)) . x <= (max (f,g)) . x by Def3; ::_thesis: verum
end;
theorem Th24: :: FUZZY_1:24
for C being non empty set
for h, f, g being Membership_Func of C st f c= & g c= holds
min (f,g) c=
proof
let C be non empty set ; ::_thesis: for h, f, g being Membership_Func of C st f c= & g c= holds
min (f,g) c=
let h, f, g be Membership_Func of C; ::_thesis: ( f c= & g c= implies min (f,g) c= )
assume A1: ( f c= & g c= ) ; ::_thesis: min (f,g) c=
let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: h . x <= (min (f,g)) . x
( h . x <= f . x & h . x <= g . x ) by A1, Def2;
then h . x <= min ((f . x),(g . x)) by XXREAL_0:20;
hence h . x <= (min (f,g)) . x by Def3; ::_thesis: verum
end;
theorem :: FUZZY_1:25
for C being non empty set
for f, g, h being Membership_Func of C st g c= holds
min (g,h) c=
proof
let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C st g c= holds
min (g,h) c=
let f, g, h be Membership_Func of C; ::_thesis: ( g c= implies min (g,h) c= )
assume A1: g c= ; ::_thesis: min (g,h) c=
let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (min (f,h)) . x <= (min (g,h)) . x
f . x <= g . x by A1, Def2;
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 (min (f,h)) . x <= (min (g,h)) . x by Def3; ::_thesis: verum
end;
theorem :: FUZZY_1:26
for C being non empty set
for f, g, h, h1 being Membership_Func of C st g c= & h1 c= holds
min (g,h1) c=
proof
let C be non empty set ; ::_thesis: for f, g, h, h1 being Membership_Func of C st g c= & h1 c= holds
min (g,h1) c=
let f, g, h, h1 be Membership_Func of C; ::_thesis: ( g c= & h1 c= implies min (g,h1) c= )
assume A1: ( g c= & h1 c= ) ; ::_thesis: min (g,h1) c=
let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (min (f,h)) . x <= (min (g,h1)) . x
( f . x <= g . x & h . x <= h1 . x ) by A1, Def2;
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 (min (f,h)) . x <= (min (g,h1)) . x by Def3; ::_thesis: verum
end;
theorem Th27: :: FUZZY_1:27
for C being non empty set
for f, g being Membership_Func of C st g c= holds
min (f,g) = f
proof
let C be non empty set ; ::_thesis: for f, g being Membership_Func of C st g c= holds
min (f,g) = f
let f, g be Membership_Func of C; ::_thesis: ( g c= implies min (f,g) = f )
assume A1: g c= ; ::_thesis: min (f,g) = f
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; ::_thesis: ( x in C implies (min (f,g)) . x = f . x )
f . x <= g . x by A1, Def2;
then f . x = min ((f . x),(g . x)) by XXREAL_0:def_9
.= (min (f,g)) . x by Def3 ;
hence ( x in C implies (min (f,g)) . x = f . x ) ; ::_thesis: verum
end;
( C = dom (min (f,g)) & C = dom f ) by FUNCT_2:def_1;
hence min (f,g) = f by A2, PARTFUN1:5; ::_thesis: verum
end;
theorem :: FUZZY_1:28
for C being non empty set
for f, g, h being Membership_Func of C st g c= & h c= & min (g,h) = EMF C holds
f = EMF C
proof
let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C st g c= & h c= & min (g,h) = EMF C holds
f = EMF C
let f, g, h be Membership_Func of C; ::_thesis: ( g c= & h c= & min (g,h) = EMF C implies f = EMF C )
assume that
A1: ( g c= & h c= ) and
A2: min (g,h) = EMF C ; ::_thesis: f = 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; ::_thesis: ( x in C implies f . x = (EMF C) . x )
( f . x <= g . x & f . x <= h . x ) by A1, Def2;
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 Th16;
hence ( x in C implies f . x = (EMF C) . x ) by A2, A4, XXREAL_0:1; ::_thesis: verum
end;
( C = dom f & C = dom (EMF C) ) by FUNCT_2:def_1;
hence f = EMF C by A3, PARTFUN1:5; ::_thesis: verum
end;
theorem :: FUZZY_1:29
for C being non empty set
for f, g, h being Membership_Func of C st max ((min (f,g)),(min (f,h))) = f holds
max (g,h) c=
proof
let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C st max ((min (f,g)),(min (f,h))) = f holds
max (g,h) c=
let f, g, h be Membership_Func of C; ::_thesis: ( max ((min (f,g)),(min (f,h))) = f implies max (g,h) c= )
assume A1: max ((min (f,g)),(min (f,h))) = f ; ::_thesis: max (g,h) c=
let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: f . x <= (max (g,h)) . x
(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 f . x <= (max (g,h)) . x by Def4; ::_thesis: verum
end;
theorem :: FUZZY_1:30
for C being non empty set
for f, g, h being Membership_Func of C st g c= & min (g,h) = EMF C holds
min (f,h) = EMF C
proof
let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C st g c= & min (g,h) = EMF C holds
min (f,h) = EMF C
let f, g, h be Membership_Func of C; ::_thesis: ( g c= & min (g,h) = EMF C implies min (f,h) = EMF C )
assume that
A1: g c= and
A2: min (g,h) = EMF C ; ::_thesis: min (f,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; ::_thesis: ( x in C implies (min (f,h)) . x = (EMF C) . x )
f . x <= g . x by A1, Def2;
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 Th16;
hence ( x in C implies (min (f,h)) . x = (EMF C) . x ) by A2, A4, XXREAL_0:1; ::_thesis: verum
end;
( C = dom (min (f,h)) & C = dom (EMF C) ) by FUNCT_2:def_1;
hence min (f,h) = EMF C by A3, PARTFUN1:5; ::_thesis: verum
end;
theorem :: FUZZY_1:31
for C being non empty set
for f being Membership_Func of C st EMF C c= holds
f = EMF C
proof
let C be non empty set ; ::_thesis: for f being Membership_Func of C st EMF C c= holds
f = EMF C
let f be Membership_Func of C; ::_thesis: ( EMF C c= implies f = EMF C )
f c= by Th14;
hence ( EMF C c= implies f = EMF C ) by Lm1; ::_thesis: verum
end;
theorem :: FUZZY_1:32
for C being non empty set
for f, g being Membership_Func of C holds
( max (f,g) = EMF C iff ( f = EMF C & g = EMF C ) )
proof
let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds
( max (f,g) = EMF C iff ( f = EMF C & g = EMF C ) )
let f, g be Membership_Func of C; ::_thesis: ( max (f,g) = EMF C iff ( f = EMF C & g = EMF C ) )
thus ( max (f,g) = EMF C implies ( f = EMF C & g = EMF C ) ) ::_thesis: ( f = EMF C & g = EMF C implies max (f,g) = EMF C )
proof
assume A1: max (f,g) = EMF C ; ::_thesis: ( f = EMF C & 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; ::_thesis: ( x in C implies f . x = (EMF C) . x )
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 Th16;
hence ( x in C implies f . x = (EMF C) . x ) by A3, XXREAL_0:1; ::_thesis: verum
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; ::_thesis: ( x in C implies g . x = (EMF C) . x )
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 Th16;
hence ( x in C implies g . x = (EMF C) . x ) by A5, XXREAL_0:1; ::_thesis: verum
end;
( C = dom f & C = dom (EMF C) ) by FUNCT_2:def_1;
hence f = EMF C by A2, PARTFUN1:5; ::_thesis: g = EMF C
( C = dom g & C = dom (EMF C) ) by FUNCT_2:def_1;
hence g = EMF C by A4, PARTFUN1:5; ::_thesis: verum
end;
assume ( f = EMF C & g = EMF C ) ; ::_thesis: max (f,g) = EMF C
hence max (f,g) = EMF C ; ::_thesis: verum
end;
theorem :: FUZZY_1:33
for C being non empty set
for f, g, h being Membership_Func of C holds
( f = max (g,h) iff ( f c= & f c= & ( for h1 being Membership_Func of C st h1 c= & h1 c= holds
h1 c= ) ) )
proof
let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds
( f = max (g,h) iff ( f c= & f c= & ( for h1 being Membership_Func of C st h1 c= & h1 c= holds
h1 c= ) ) )
let f, g, h be Membership_Func of C; ::_thesis: ( f = max (g,h) iff ( f c= & f c= & ( for h1 being Membership_Func of C st h1 c= & h1 c= holds
h1 c= ) ) )
hereby ::_thesis: ( f c= & f c= & ( for h1 being Membership_Func of C st h1 c= & h1 c= holds
h1 c= ) implies f = max (g,h) )
assume A1: f = max (g,h) ; ::_thesis: ( f c= & f c= & ( for h1 being Membership_Func of C st h1 c= & h1 c= holds
h1 c= ) )
hence ( f c= & f c= ) by Th17; ::_thesis: for h1 being Membership_Func of C st h1 c= & h1 c= holds
h1 c=
let h1 be Membership_Func of C; ::_thesis: ( h1 c= & h1 c= implies h1 c= )
assume A2: ( h1 c= & h1 c= ) ; ::_thesis: h1 c=
thus h1 c= ::_thesis: verum
proof
let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: f . x <= h1 . x
( g . x <= h1 . x & h . x <= h1 . x ) by A2, Def2;
then max ((g . x),(h . x)) <= h1 . x by XXREAL_0:28;
hence f . x <= h1 . x by A1, Def4; ::_thesis: verum
end;
end;
assume that
A3: ( f c= & f c= ) and
A4: for h1 being Membership_Func of C st h1 c= & h1 c= holds
h1 c= ; ::_thesis: f = max (g,h)
( max (g,h) c= & max (g,h) c= ) by Th17;
then A5: max (g,h) c= by A4;
f c= by A3, Th19;
hence f = max (g,h) by A5, Lm1; ::_thesis: verum
end;
theorem :: FUZZY_1:34
for C being non empty set
for f, g, h being Membership_Func of C holds
( f = min (g,h) iff ( g c= & h c= & ( for h1 being Membership_Func of C st g c= & h c= holds
f c= ) ) )
proof
let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds
( f = min (g,h) iff ( g c= & h c= & ( for h1 being Membership_Func of C st g c= & h c= holds
f c= ) ) )
let f, g, h be Membership_Func of C; ::_thesis: ( f = min (g,h) iff ( g c= & h c= & ( for h1 being Membership_Func of C st g c= & h c= holds
f c= ) ) )
hereby ::_thesis: ( g c= & h c= & ( for h1 being Membership_Func of C st g c= & h c= holds
f c= ) implies f = min (g,h) )
assume A1: f = min (g,h) ; ::_thesis: ( g c= & h c= & ( for h1 being Membership_Func of C st g c= & h c= holds
f c= ) )
hence ( g c= & h c= ) by Th17; ::_thesis: for h1 being Membership_Func of C st g c= & h c= holds
f c=
let h1 be Membership_Func of C; ::_thesis: ( g c= & h c= implies f c= )
assume A2: ( g c= & h c= ) ; ::_thesis: f c=
thus f c= ::_thesis: verum
proof
let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: h1 . x <= f . x
( h1 . x <= g . x & h1 . x <= h . x ) by A2, Def2;
then min ((g . x),(h . x)) >= h1 . x by XXREAL_0:20;
hence h1 . x <= f . x by A1, Def3; ::_thesis: verum
end;
end;
assume that
A3: ( g c= & h c= ) and
A4: for h1 being Membership_Func of C st g c= & h c= holds
f c= ; ::_thesis: f = min (g,h)
( g c= & h c= ) by Th17;
then A5: f c= by A4;
min (g,h) c= by A3, Th24;
hence f = min (g,h) by A5, Lm1; ::_thesis: verum
end;
theorem :: FUZZY_1:35
for C being non empty set
for f, g, h being Membership_Func of C st max (g,h) c= & min (f,h) = EMF C holds
g c=
proof
let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C st max (g,h) c= & min (f,h) = EMF C holds
g c=
let f, g, h be Membership_Func of C; ::_thesis: ( max (g,h) c= & min (f,h) = EMF C implies g c= )
assume that
A1: max (g,h) c= and
A2: min (f,h) = EMF C ; ::_thesis: g c=
let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: f . x <= g . x
min (f,(max (g,h))) = f by A1, Th27;
then f = max ((min (f,g)),(min (f,h))) by Th9
.= min (f,g) by A2, Th18 ;
then f . x = min ((f . x),(g . x)) by Def3;
hence f . x <= g . x by XXREAL_0:def_9; ::_thesis: verum
end;
Lm2: for C being non empty set
for f, g being Membership_Func of C st g c= holds
1_minus f c=
proof
let C be non empty set ; ::_thesis: for f, g being Membership_Func of C st g c= holds
1_minus f c=
let f, g be Membership_Func of C; ::_thesis: ( g c= implies 1_minus f c= )
assume A1: g c= ; ::_thesis: 1_minus f c=
let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (1_minus g) . x <= (1_minus f) . x
f . x <= g . x by A1, Def2;
then 1 - (g . x) <= 1 - (f . x) by XREAL_1:10;
then (1_minus g) . x <= 1 - (f . x) by Def5;
hence (1_minus g) . x <= (1_minus f) . x by Def5; ::_thesis: verum
end;
theorem Th36: :: FUZZY_1:36
for C being non empty set
for f, g being Membership_Func of C holds
( g c= iff 1_minus f c= )
proof
let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds
( g c= iff 1_minus f c= )
let f, g be Membership_Func of C; ::_thesis: ( g c= iff 1_minus f c= )
( 1_minus (1_minus f) = f & 1_minus (1_minus g) = g ) ;
hence ( g c= iff 1_minus f c= ) by Lm2; ::_thesis: verum
end;
theorem :: FUZZY_1:37
for C being non empty set
for f, g being Membership_Func of C st 1_minus g c= holds
1_minus f c=
proof
let C be non empty set ; ::_thesis: for f, g being Membership_Func of C st 1_minus g c= holds
1_minus f c=
let f, g be Membership_Func of C; ::_thesis: ( 1_minus g c= implies 1_minus f c= )
1_minus (1_minus f) = f ;
hence ( 1_minus g c= implies 1_minus f c= ) by Th36; ::_thesis: verum
end;
theorem :: FUZZY_1:38
for C being non empty set
for f, g being Membership_Func of C holds 1_minus f c=
proof
let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds 1_minus f c=
let f, g be Membership_Func of C; ::_thesis: 1_minus f c=
max (f,g) c= by Th17;
hence 1_minus f c= by Th36; ::_thesis: verum
end;
theorem :: FUZZY_1:39
for C being non empty set
for f, g being Membership_Func of C holds 1_minus (min (f,g)) c=
proof
let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds 1_minus (min (f,g)) c=
let f, g be Membership_Func of C; ::_thesis: 1_minus (min (f,g)) c=
f c= by Th17;
hence 1_minus (min (f,g)) c= by Th36; ::_thesis: verum
end;
theorem Th40: :: FUZZY_1:40
for C being non empty set holds
( 1_minus (EMF C) = UMF C & 1_minus (UMF C) = EMF C )
proof
let C be non empty set ; ::_thesis: ( 1_minus (EMF C) = UMF C & 1_minus (UMF C) = EMF C )
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; ::_thesis: ( x in C implies (1_minus (EMF C)) . x = (UMF C) . x )
(1_minus (EMF C)) . x = 1 - ((EMF C) . x) by Def5
.= 1 - 0 by FUNCT_3:def_3
.= 1 ;
hence ( x in C implies (1_minus (EMF C)) . x = (UMF C) . x ) by FUNCT_3:def_3; ::_thesis: verum
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; ::_thesis: 1_minus (UMF C) = EMF C
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; ::_thesis: ( x in C implies (1_minus (UMF C)) . x = (EMF C) . x )
(1_minus (UMF C)) . x = 1 - ((UMF C) . x) by Def5
.= 1 - 1 by FUNCT_3:def_3
.= 0 ;
hence ( x in C implies (1_minus (UMF C)) . x = (EMF C) . x ) by FUNCT_3:def_3; ::_thesis: verum
end;
( C = dom (1_minus (UMF C)) & C = dom (EMF C) ) by FUNCT_2:def_1;
hence 1_minus (UMF C) = EMF C by A2, PARTFUN1:5; ::_thesis: verum
end;
definition
let C be non empty set ;
let h, g be Membership_Func of C;
funch \+\ g -> Membership_Func of C equals :: FUZZY_1:def 8
max ((min (h,(1_minus g))),(min ((1_minus h),g)));
coherence
max ((min (h,(1_minus g))),(min ((1_minus h),g))) is Membership_Func of C ;
commutativity
for b1, h, g being Membership_Func of C st b1 = max ((min (h,(1_minus g))),(min ((1_minus h),g))) holds
b1 = max ((min (g,(1_minus h))),(min ((1_minus g),h))) ;
end;
:: deftheorem defines \+\ FUZZY_1:def_8_:_
for C being non empty set
for h, g being Membership_Func of C holds h \+\ g = max ((min (h,(1_minus g))),(min ((1_minus h),g)));
theorem :: FUZZY_1:41
for C being non empty set
for f being Membership_Func of C holds f \+\ (EMF C) = f
proof
let C be non empty set ; ::_thesis: for f being Membership_Func of C holds f \+\ (EMF C) = f
let f be Membership_Func of C; ::_thesis: f \+\ (EMF C) = f
thus f \+\ (EMF C) = max ((min (f,(UMF C))),(min ((1_minus f),(EMF C)))) by Th40
.= max (f,(min ((1_minus f),(EMF C)))) by Th18
.= max (f,(EMF C)) by Th18
.= f by Th18 ; ::_thesis: verum
end;
theorem :: FUZZY_1:42
for C being non empty set
for f being Membership_Func of C holds f \+\ (UMF C) = 1_minus f
proof
let C be non empty set ; ::_thesis: for f being Membership_Func of C holds f \+\ (UMF C) = 1_minus f
let f be Membership_Func of C; ::_thesis: f \+\ (UMF C) = 1_minus f
thus f \+\ (UMF C) = max ((min (f,(EMF C))),(min ((1_minus f),(UMF C)))) by Th40
.= max ((EMF C),(min ((1_minus f),(UMF C)))) by Th18
.= min ((1_minus f),(UMF C)) by Th18
.= 1_minus f by Th18 ; ::_thesis: verum
end;
theorem :: FUZZY_1:43
for C being non empty set
for f, g, h being Membership_Func of C holds min ((min ((max (f,g)),(max (g,h)))),(max (h,f))) = max ((max ((min (f,g)),(min (g,h)))),(min (h,f)))
proof
let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds min ((min ((max (f,g)),(max (g,h)))),(max (h,f))) = max ((max ((min (f,g)),(min (g,h)))),(min (h,f)))
let f, g, h be Membership_Func of C; ::_thesis: min ((min ((max (f,g)),(max (g,h)))),(max (h,f))) = max ((max ((min (f,g)),(min (g,h)))),(min (h,f)))
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 ; ::_thesis: verum
end;
theorem :: FUZZY_1:44
for C being non empty set
for f, g being Membership_Func of C holds 1_minus (f \+\ g) c=
proof
let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds 1_minus (f \+\ g) c=
let f, g be Membership_Func of C; ::_thesis: 1_minus (f \+\ g) c=
set f1 = 1_minus f;
set g1 = 1_minus g;
let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (max ((min (f,g)),(min ((1_minus f),(1_minus g))))) . x <= (1_minus (f \+\ g)) . x
1_minus (f \+\ g) = min ((1_minus (min (f,(1_minus g)))),(1_minus (min ((1_minus f),g)))) by Th11
.= min ((max ((1_minus f),(1_minus (1_minus g)))),(1_minus (min ((1_minus f),g)))) by Th11
.= min ((max ((1_minus f),g)),(max ((1_minus (1_minus f)),(1_minus g)))) by Th11
.= max ((min ((max ((1_minus f),g)),f)),(min ((max ((1_minus f),g)),(1_minus g)))) by Th9
.= max ((max ((min (f,(1_minus f))),(min (f,g)))),(min ((max ((1_minus f),g)),(1_minus g)))) by Th9
.= max ((max ((min (f,(1_minus f))),(min (f,g)))),(max ((min ((1_minus g),(1_minus f))),(min ((1_minus g),g))))) by Th9
.= max ((max ((max ((min (f,g)),(min (f,(1_minus f))))),(min ((1_minus g),(1_minus f))))),(min ((1_minus g),g))) by Th7
.= max ((max ((max ((min ((1_minus g),(1_minus f))),(min (f,g)))),(min (f,(1_minus f))))),(min ((1_minus g),g))) by Th7
.= max ((max ((min ((1_minus g),(1_minus f))),(min (f,g)))),(max ((min (f,(1_minus f))),(min ((1_minus g),g))))) by Th7 ;
then (1_minus (f \+\ g)) . x = max (((max ((min (f,g)),(min ((1_minus f),(1_minus g))))) . x),((max ((min (f,(1_minus f))),(min ((1_minus g),g)))) . x)) by Def4;
hence (max ((min (f,g)),(min ((1_minus f),(1_minus g))))) . x <= (1_minus (f \+\ g)) . x by XXREAL_0:25; ::_thesis: verum
end;
theorem :: FUZZY_1:45
for C being non empty set
for f, g being Membership_Func of C holds max (f,g) c=
proof
let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds max (f,g) c=
let f, g be Membership_Func of C; ::_thesis: max (f,g) c=
set f1 = 1_minus f;
set g1 = 1_minus g;
let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (max ((f \+\ g),(min (f,g)))) . x <= (max (f,g)) . x
max ((f \+\ g),(min (f,g))) = max ((min (f,(1_minus g))),(max ((min ((1_minus f),g)),(min (f,g))))) by Th7
.= max ((min (f,(1_minus g))),(min ((max ((min ((1_minus f),g)),f)),(max (g,(min ((1_minus f),g))))))) by Th9
.= max ((min (f,(1_minus g))),(min ((max ((min ((1_minus f),g)),f)),g))) by Th8
.= min ((max ((min (f,(1_minus g))),(max (f,(min ((1_minus f),g)))))),(max ((min (f,(1_minus g))),g))) by Th9
.= min ((max ((max (f,(min (f,(1_minus g))))),(min ((1_minus f),g)))),(max ((min (f,(1_minus g))),g))) by Th7
.= min ((max (f,(min ((1_minus f),g)))),(max ((min (f,(1_minus g))),g))) by Th8
.= min ((min ((max (f,(1_minus f))),(max (f,g)))),(max (g,(min (f,(1_minus g)))))) by Th9
.= min ((min ((max (f,(1_minus f))),(max (f,g)))),(min ((max (g,f)),(max (g,(1_minus g)))))) by Th9
.= min ((min ((min ((max (f,(1_minus f))),(max (f,g)))),(max (g,f)))),(max (g,(1_minus g)))) by Th7
.= min ((min ((max (f,(1_minus f))),(min ((max (f,g)),(max (f,g)))))),(max (g,(1_minus g)))) by Th7
.= min ((max (f,g)),(min ((max (f,(1_minus f))),(max (g,(1_minus g)))))) by Th7 ;
then (max ((f \+\ g),(min (f,g)))) . x = min (((max (f,g)) . x),((min ((max (f,(1_minus f))),(max (g,(1_minus g))))) . x)) by Def3;
hence (max ((f \+\ g),(min (f,g)))) . x <= (max (f,g)) . x by XXREAL_0:17; ::_thesis: verum
end;
theorem :: FUZZY_1:46
for C being non empty set
for f being Membership_Func of C holds 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 :: FUZZY_1:def 9
for c being Element of C holds it . c = abs ((h . c) - (g . c));
existence
ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = abs ((h . c) - (g . c))
proof
defpred S1[ set , set ] means $2 = abs ((h . $1) - (g . $1));
A1: for x, y1, y2 being set st x in C & S1[x,y1] & S1[x,y2] holds
y1 = y2 ;
A2: for x, y being set st x in C & S1[x,y] holds
y in REAL ;
consider IT being PartFunc of C,REAL such that
A3: ( ( for x being set holds
( x in dom IT iff ( x in C & ex y being set st S1[x,y] ) ) ) & ( for x being set st x in dom IT holds
S1[x,IT . x] ) ) from PARTFUN1:sch_2(A2, A1);
for x being set st x in C holds
x in dom IT
proof
let x be set ; ::_thesis: ( x in C implies x in dom IT )
A4: ex y being set st y = abs ((h . x) - (g . x)) ;
assume x in C ; ::_thesis: x in dom IT
hence x in dom IT by A3, A4; ::_thesis: verum
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 = abs ((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 set st y in rng IT holds
y in [.0,1.]
proof
reconsider A = [.0,1.] as non empty closed_interval Subset of REAL by MEASURE5:14;
let y be set ; ::_thesis: ( y in rng IT implies y in [.0,1.] )
assume y in rng IT ; ::_thesis: y in [.0,1.]
then consider x being Element of C such that
A9: x in dom IT and
A10: y = IT . x by PARTFUN1:3;
0 <= abs ((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 abs ((h . x) - (g . x)) <= 1 by A20, ABSVALUE:5;
then IT . x <= 1 by A3, A9;
hence y in [.0,1.] by A10, A13, A18, A11, INTEGRA2:1; ::_thesis: verum
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 ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = abs ((h . c) - (g . c)) by A6; ::_thesis: verum
end;
uniqueness
for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = abs ((h . c) - (g . c)) ) & ( for c being Element of C holds b2 . c = abs ((h . c) - (g . c)) ) holds
b1 = b2
proof
let F, G be Membership_Func of C; ::_thesis: ( ( for c being Element of C holds F . c = abs ((h . c) - (g . c)) ) & ( for c being Element of C holds G . c = abs ((h . c) - (g . c)) ) implies F = G )
assume that
A22: for c being Element of C holds F . c = abs ((h . c) - (g . c)) and
A23: for c being Element of C holds G . c = abs ((h . c) - (g . c)) ; ::_thesis: F = G
A24: for c being Element of C st c in C holds
F . c = G . c
proof
let c be Element of C; ::_thesis: ( c in C implies F . c = G . c )
F . c = abs ((h . c) - (g . c)) by A22;
hence ( c in C implies F . c = G . c ) by A23; ::_thesis: verum
end;
( C = dom F & C = dom G ) by FUNCT_2:def_1;
hence F = G by A24, PARTFUN1:5; ::_thesis: verum
end;
end;
:: deftheorem defines ab_difMF FUZZY_1:def_9_:_
for C being non empty set
for h, g, b4 being Membership_Func of C holds
( b4 = ab_difMF (h,g) iff for c being Element of C holds b4 . c = abs ((h . c) - (g . c)) );