:: Properties of Fuzzy Relation
:: by Noboru Endou , Takashi Mitsuishi and Keiji Ohkubo
::
:: Received June 25, 2001
:: Copyright (c) 2001-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, FUZZY_1, RELAT_1, SUBSET_1, FUNCT_1, XXREAL_2,
XXREAL_0, XXREAL_1, CARD_1, TARSKI, ARYTM_3, ARYTM_1, FUZZY_2, ZFMISC_1,
PARTFUN1, VALUED_1, SEQ_4, FUZZY_4, MEASURE5, REAL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, REAL_1, FUNCT_1, BINOP_1, RELAT_1, RELSET_1, PARTFUN1,
XXREAL_2, FUNCT_4, INTEGRA1, RCOMP_1, MEASURE6, FUZZY_1, FUZZY_2, SEQ_4,
MEASURE5;
constructors FUNCT_4, REAL_1, SQUARE_1, RFUNCT_1, MEASURE6, INTEGRA1, FUZZY_2,
XXREAL_2, SEQ_4, RELSET_1, RELAT_1, FUZZY_1, BINOP_2, RVSUM_1, BINOP_1,
NUMBERS;
registrations XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED,
INTEGRA1, RELAT_1, VALUED_0, RELSET_1, MEASURE5, BINOP_2, ORDINAL1;
requirements NUMERALS, REAL, SUBSET, BOOLE;
definitions TARSKI, FUZZY_1, RELAT_1;
equalities TARSKI, FUZZY_1, FUZZY_2, BINOP_1, ORDINAL1;
expansions FUZZY_1, BINOP_1, RELAT_1;
theorems FUZZY_1, FUNCT_3, PARTFUN1, FUNCT_1, INTEGRA1, INTEGRA2, ZFMISC_1,
SEQ_4, SUBSET_1, XBOOLE_0, FUZZY_2, XXREAL_0, FUNCT_4, XXREAL_2, XREAL_1,
RELSET_1, MEMBERED, FUNCT_2, RELAT_1, MEASURE5, XREAL_0, TARSKI;
schemes PARTFUN1, BINOP_1;
begin :: Basic properties of the membership function
reserve c,c1,c2,x,y,z,z1,z2 for set;
reserve C1,C2,C3 for non empty set;
registration
let C1 be non empty set;
let F be Membership_Func of C1;
cluster rng F -> non empty;
coherence
proof
dom F = C1 by FUNCT_2:def 1;
then consider y being Element of C1 such that
A1: y in dom F by SUBSET_1:4;
F.y in rng F by A1,FUNCT_1:def 3;
hence thesis;
end;
end;
reconsider jj=1 as Real;
theorem Th1:
for F be Membership_Func of C1 holds rng F is real-bounded & (for x st
x in dom F holds F.x <= upper_bound rng F) & for x st x in dom F
holds F.x >= lower_bound rng F
proof
let F be Membership_Func of C1;
A1: [.0,jj.] is non empty closed_interval Subset of REAL by MEASURE5:14;
A2: rng F c= [.0,1.] by RELAT_1:def 19;
then
A3: rng F is real-bounded by A1,XXREAL_2:45;
A4: for x st x in dom F holds F.x >= lower_bound rng F
proof
let x;
assume x in dom F;
then
A5: F.x in rng F by FUNCT_1:def 3;
rng F is bounded_below by A3,XXREAL_2:def 11;
hence thesis by A5,SEQ_4:def 2;
end;
for x st x in dom F holds F.x <= upper_bound rng F
proof
let x;
assume x in dom F;
then
A6: F.x in rng F by FUNCT_1:def 3;
rng F is bounded_above by A3,XXREAL_2:def 11;
hence thesis by A6,SEQ_4:def 1;
end;
hence thesis by A2,A1,A4,XXREAL_2:45;
end;
theorem
for F,G be Membership_Func of C1 holds (for x st x in C1 holds F.x <=
G.x) implies upper_bound rng F <= upper_bound rng G
proof
let F,G be Membership_Func of C1;
rng F is real-bounded by Th1;
then
A1: rng F is bounded_above by XXREAL_2:def 11;
assume
A2: for c st c in C1 holds F.c <= G.c;
A3: for s being Real st 0<s ex y st y in dom F &
upper_bound rng F - s <= G.y
proof
let s being Real;
assume 0<s;
then consider r being Real such that
A4: r in rng F and
A5: upper_bound rng F-s<r by A1,SEQ_4:def 1;
consider y being object such that
A6: y in dom F and
A7: r = F.y by A4,FUNCT_1:def 3;
r <= G.y by A2,A6,A7;
hence thesis by A5,A6,XXREAL_0:2;
end;
for s being Real st 0<s
holds upper_bound rng F - s <= upper_bound rng G
proof
let s being Real;
assume 0<s;
then consider y such that
A8: y in dom F and
A9: upper_bound rng F - s <= G.y by A3;
y in C1 by A8;
then y in dom G by FUNCT_2:def 1;
then G.y <= upper_bound rng G by Th1;
hence thesis by A9,XXREAL_0:2;
end;
hence thesis by XREAL_1:57;
end;
theorem Th3:
for f be RMembership_Func of C1,C2, c be set holds 0 <= f.c & f.c <= 1
proof
let f being RMembership_Func of C1,C2;
let c be set;
per cases;
suppose
c in [:C1,C2:];
then reconsider c as Element of [:C1,C2:];
A1: f.c <= (Umf(C1,C2)).c by FUZZY_2:52;
(Zmf(C1,C2)).c <= f.c by FUZZY_2:52;
hence thesis by A1,FUNCT_3:def 3;
end;
suppose
A2: not c in [:C1,C2:];
dom f = [:C1,C2:] by FUNCT_2:def 1;
hence thesis by A2,FUNCT_1:def 2;
end;
end;
theorem
for f be RMembership_Func of C1,C2, x,y holds 0 <= f.(x,y) & f.(x,y)
<= 1 by Th3;
begin
:: Definition and properties of converse fuzzy relation
notation
let C1,C2 be non empty set;
let h be RMembership_Func of C2,C1;
synonym converse h for ~h;
end;
definition
let C1,C2 be non empty set;
let h be RMembership_Func of C2,C1;
redefine func converse h -> RMembership_Func of C1,C2 means :: redefines converse (FUZZY_4, synonym) → ~ (FUNCT_4, definition)
:Def1:
for x,y being object st [x,y] in [:C1,C2:] holds it.(x,y) = h.(y,x);
coherence
proof
set IT = converse h;
A1: dom h = [:C2,C1:] by FUNCT_2:def 1;
then
A2: dom IT = [:C1,C2:] by FUNCT_4:46;
rng h c= [.0,1.] by RELAT_1:def 19;
then
A3: rng IT c= [.0,1.] by A1,FUNCT_4:47;
then rng IT c= REAL by MEMBERED:3;
then reconsider IT as PartFunc of [:C1,C2:],REAL by A2,RELSET_1:4;
IT is Membership_Func of [:C1,C2:] by A2,A3,FUNCT_2:def 1,RELAT_1:def 19;
hence thesis;
end;
compatibility
proof
let IT be RMembership_Func of C1,C2;
A4: dom h = [:C2,C1:] by FUNCT_2:def 1;
thus IT = ~h implies
for x,y being object st [x,y] in [:C1,C2:] holds IT.(x,y) = h.(y,x
)
proof
assume
A5: IT = ~h;
let x,y be object;
assume [x,y] in [:C1,C2:];
then [y,x] in dom h by A4,ZFMISC_1:88;
hence thesis by A5,FUNCT_4:def 2;
end;
A6: dom IT = [:C1,C2:] by FUNCT_2:def 1;
A7: for x being object holds x in dom IT iff
ex y,z being object st x = [z,y] & [y,z] in dom h
proof
let x be object;
thus x in dom IT implies
ex y,z being object st x = [z,y] & [y,z] in dom h
proof
assume x in dom IT;
then consider z,y being object such that
A8: z in C1 and
A9: y in C2 and
A10: x = [z,y] by ZFMISC_1:def 2;
reconsider y,z as set by TARSKI:1;
take y,z;
thus thesis by A4,A8,A9,A10,ZFMISC_1:def 2;
end;
thus thesis by A6,ZFMISC_1:88;
end;
assume for x,y being object st [x,y] in [:C1,C2:]
holds IT.(x,y) = h.(y,x);
then for y,z being object st [y,z] in dom h holds IT.(z,y) = h.(y,z)
by ZFMISC_1:88;
hence thesis by A7,FUNCT_4:def 2;
end;
end;
theorem
for f be RMembership_Func of C1,C2 holds converse converse f = f
proof
let f being RMembership_Func of C1,C2;
A1: dom f = [:C1,C2:] by FUNCT_2:def 1;
A2: for c being Element of [:C1,C2:] st c in [:C1,C2:] holds (converse
converse f).c = f.c
proof
let c being Element of [:C1,C2:];
assume c in [:C1,C2:];
consider x,y being object such that
A3: x in C1 and
A4: y in C2 and
A5: c = [x,y] by ZFMISC_1:def 2;
A6: [y,x] in [:C2,C1:] by A3,A4,ZFMISC_1:87;
(converse converse f).(x,y) = (converse f).(y,x) by A5,Def1
.= f.(x,y) by A6,Def1;
hence thesis by A5;
end;
dom(converse converse f) = [:C1,C2:] by FUNCT_2:def 1;
hence thesis by A2,A1,PARTFUN1:5;
end;
theorem Th6:
for f be RMembership_Func of C1,C2 holds 1_minus(converse f) =
converse(1_minus f)
proof
let f being RMembership_Func of C1,C2;
A1: [:C2,C1:] = dom converse(1_minus f ) by FUNCT_2:def 1;
A2: for c being Element of [:C2,C1:] st c in [:C2,C1:] holds (1_minus(
converse f)).c = (converse(1_minus f)).c
proof
let c being Element of [:C2,C1:];
assume c in [:C2,C1:];
consider y,x being object such that
A3: y in C2 and
A4: x in C1 and
A5: c = [y,x] by ZFMISC_1:def 2;
reconsider y,x as set by TARSKI:1;
A6: [x,y] in [:C1,C2:] by A3,A4,ZFMISC_1:87;
(1_minus(converse f)).(y,x) = 1-(converse f).(y,x) by A5,FUZZY_1:def 5
.= 1-f.(x,y) by A5,Def1
.= (1_minus f).(x,y) by A6,FUZZY_1:def 5
.= (converse(1_minus f)).(y,x) by A5,Def1;
hence thesis by A5;
end;
dom(1_minus(converse f)) = [:C2,C1:] by FUNCT_2:def 1;
hence thesis by A2,A1,PARTFUN1:5;
end;
theorem Th7:
for f,g be RMembership_Func of C1,C2 holds converse max(f,g) =
max(converse f,converse g)
proof
let f,g be RMembership_Func of C1,C2;
A1: dom max(converse f,converse g) = [:C2,C1:] by FUNCT_2:def 1;
A2: for c being Element of [:C2,C1:] st c in [:C2,C1:] holds (converse max(f
,g)).c = max(converse f,converse g).c
proof
let c being Element of [:C2,C1:];
assume c in [:C2,C1:];
consider y,x being object such that
A3: y in C2 and
A4: x in C1 and
A5: c = [y,x] by ZFMISC_1:def 2;
reconsider y,x as set by TARSKI:1;
A6: [x,y] in [:C1,C2:] by A3,A4,ZFMISC_1:87;
(converse max(f,g)).(y,x) = max(f,g).(x,y) by A5,Def1
.=max(f.(x,y),g.(x,y)) by A6,FUZZY_1:def 4
.=max((converse f).(y,x), g.(x,y)) by A5,Def1
.=max((converse f).(y,x),(converse g).(y,x)) by A5,Def1
.=max(converse f,converse g).(y,x) by A5,FUZZY_1:def 4;
hence thesis by A5;
end;
dom converse max(f,g) = [:C2,C1:] by FUNCT_2:def 1;
hence thesis by A1,A2,PARTFUN1:5;
end;
theorem Th8:
for f,g be RMembership_Func of C1,C2 holds converse min(f,g) =
min(converse f,converse g)
proof
let f,g be RMembership_Func of C1,C2;
A1: dom min(converse f,converse g) = [:C2,C1:] by FUNCT_2:def 1;
A2: for c being Element of [:C2,C1:] st c in [:C2,C1:] holds (converse min(f
,g)).c = min(converse f,converse g).c
proof
let c being Element of [:C2,C1:];
assume c in [:C2,C1:];
consider y,x being object such that
A3: y in C2 and
A4: x in C1 and
A5: c = [y,x] by ZFMISC_1:def 2;
reconsider y,x as set by TARSKI:1;
A6: [x,y] in [:C1,C2:] by A3,A4,ZFMISC_1:87;
(converse min(f,g)).(y,x) = min(f,g).(x,y) by A5,Def1
.=min(f.(x,y),g.(x,y)) by A6,FUZZY_1:def 3
.=min((converse f).(y,x), g.(x,y)) by A5,Def1
.=min((converse f).(y,x),(converse g).(y,x)) by A5,Def1;
hence thesis by A5,FUZZY_1:def 3;
end;
dom converse min(f,g) = [:C2,C1:] by FUNCT_2:def 1;
hence thesis by A1,A2,PARTFUN1:5;
end;
theorem Th9:
for f,g be RMembership_Func of C1,C2, x,y st x in C1 & y in C2
holds f. [x,y] <= g. [x,y]
implies (converse f). [y,x] <= (converse g). [y,x]
proof
let f,g being RMembership_Func of C1,C2, x,y;
assume that
A1: x in C1 and
A2: y in C2 and
A3: f. [x,y] <= g. [x,y];
A4: [y,x] in [:C2,C1:] by A1,A2,ZFMISC_1:87;
then
A5: g.(x,y) = (converse g).(y,x) by Def1;
f.(x,y) = (converse f).(y,x) by A4,Def1;
hence thesis by A3,A5;
end;
theorem
for f,g be RMembership_Func of C1,C2 holds f c= g implies converse f
c= converse g
proof
let f,g be RMembership_Func of C1,C2;
assume
A1: f c= g;
let c being Element of [:C2,C1:];
ex y,x being object st y in C2 & x in C1 & c = [y,x] by ZFMISC_1:def 2;
then consider x,y being set such that
A2: x in C1 and
A3: y in C2 and
A4: c = [y,x];
[x,y] in [:C1,C2:] by A2,A3,ZFMISC_1:87;
then f. [x,y] <= g. [x,y] by A1;
hence thesis by A2,A3,A4,Th9;
end;
theorem
for f,g be RMembership_Func of C1,C2 holds converse(f\g) = (converse f
)\(converse g)
proof
let f,g be RMembership_Func of C1,C2;
converse(f\g) = min(converse f,converse 1_minus g) by Th8
.= min(converse f,1_minus converse g) by Th6;
hence thesis;
end;
theorem
for f,g be RMembership_Func of C1,C2 holds converse (f \+\ g) = (
converse f) \+\ (converse g)
proof
let f,g be RMembership_Func of C1,C2;
converse (f \+\ g) = max(converse min(f,1_minus g),converse min(1_minus
f,g)) by Th7
.= max(min(converse f,converse 1_minus g), converse min(1_minus f,g)) by
Th8
.= max(min(converse f,converse 1_minus g), min(converse 1_minus f,
converse g)) by Th8
.= max(min(converse f,1_minus (converse g)), min(converse 1_minus f,
converse g)) by Th6
.= max(min(converse f,1_minus (converse g)), min(1_minus converse f,
converse g)) by Th6;
hence thesis;
end;
begin
:: Definition and properties of the composition
definition
let C1,C2,C3 be non empty set;
let h be RMembership_Func of C1,C2;
let g be RMembership_Func of C2,C3;
let x,z be object;
assume that
A1: x in C1 and
A2: z in C3;
func min(h,g,x,z) -> Membership_Func of C2 means
:Def2:
for y being Element of C2 holds it.y = min(h. [x,y],g. [y,z]);
existence
proof
defpred P[object,object] means $2 = min(h. [x,$1],g. [$1,z]);
A3: for y,c1,c2 being object st y in C2 & P[y,c1] & P[y,c2] holds c1=c2;
A4: for y,c being object st y in C2 & P[y,c] holds c in REAL by XREAL_0:def 1;
consider IT being PartFunc of C2,REAL such that
A5: (for y being object holds y in dom IT iff y in C2 &
ex c being object st P[y,c]) &
for y being object st
y in dom IT holds P[y,IT.y] from PARTFUN1:sch 2(A4,A3);
A6: dom IT = C2 & rng IT c= [.0,1.]
proof
C2 c= dom IT
proof
let y being object;
min(h. [x,y],g. [y,z]) is set by TARSKI:1;
hence thesis by A5;
end;
hence dom IT = C2 by XBOOLE_0:def 10;
reconsider A=[.0,jj.] as
non empty closed_interval Subset of REAL by MEASURE5:14;
let c being object;
A8: rng h c= [.0,1.] by RELAT_1:def 19;
assume c in rng IT;
then consider y being Element of C2 such that
A9: y in dom IT and
A10: c = IT.y by PARTFUN1:3;
A11: h. [x,y] >= min(h. [x,y],g. [y,z]) by XXREAL_0:17;
[x,y] in [:C1,C2:] by A1,ZFMISC_1:87;
then [x,y] in dom h by FUNCT_2:def 1;
then
A12: h. [x,y] in rng h by FUNCT_1:def 3;
[y,z] in [:C2,C3:] by A2,ZFMISC_1:87;
then [y,z] in dom g by FUNCT_2:def 1;
then
A13: g. [y,z] in rng g by FUNCT_1:def 3;
A14: A = [. lower_bound A, upper_bound A .] by INTEGRA1:4;
then
A15: 0=lower_bound A by INTEGRA1:5;
A16: 1=upper_bound A by A14,INTEGRA1:5;
then h. [x,y] <= 1 by A8,A12,INTEGRA2:1;
then min(h. [x,y],g. [y,z]) <= 1 by A11,XXREAL_0:2;
then
A17: IT.y <= 1 by A5,A9;
rng g c= [.0,1.] by RELAT_1:def 19;
then
A18: 0 <= g. [y,z] by A15,A13,INTEGRA2:1;
0 <= h. [x,y] by A8,A15,A12,INTEGRA2:1;
then 0 <= min(h. [x,y],g. [y,z]) by A18,XXREAL_0:20;
then 0 <= IT.y by A5,A9;
hence thesis by A10,A15,A16,A17,INTEGRA2:1;
end;
then
A19: IT is Membership_Func of C2 by FUNCT_2:def 1,RELAT_1:def 19;
for y being Element of C2 holds IT.y = min(h. [x,y],g. [y,z]) by A5,A6;
hence thesis by A19;
end;
uniqueness
proof
let F,G be Membership_Func of C2;
assume that
A20: for y being Element of C2 holds F.y = min(h. [x,y],g. [y,z]) and
A21: for y being Element of C2 holds G.y = min(h. [x,y],g. [y,z]);
A22: for y being Element of C2 st y in C2 holds F.y = G.y
proof
let y being Element of C2;
F.y = min(h. [x,y],g. [y,z]) by A20;
hence thesis by A21;
end;
A23: dom G = C2 by FUNCT_2:def 1;
dom F = C2 by FUNCT_2:def 1;
hence thesis by A23,A22,PARTFUN1:5;
end;
end;
definition
let C1,C2,C3 be non empty set;
let h be RMembership_Func of C1,C2;
let g be RMembership_Func of C2,C3;
func h(#)g -> RMembership_Func of C1,C3 means
:Def3:
for x,z being object st [x,z] in [:
C1,C3:] holds it.(x,z) = upper_bound(rng(min(h,g,x,z)));
existence
proof
defpred P[object,object,object] means
$3 = upper_bound(rng(min(h,g,$1,$2)));
A1: for x,z,c1,c2 being object
st x in C1 & z in C3 & P[x,z,c1] & P[x,z,c2] holds c1=c2;
A2: for x,z,c being object st x in C1 & z in C3 & P[x,z,c]
holds c in REAL by XREAL_0:def 1;
consider IT being PartFunc of [:C1,C3:],REAL such that
A3: (for x,z being object holds [x,z] in dom IT iff x in C1 & z in C3 &
ex c being object st P[x,z,c]) &
for x,z being object st [x,z] in dom IT holds P[x,z,IT.(x,z)]
from BINOP_1:sch 5(A2,A1);
[:C1,C3:] c= dom IT
proof
let x,z being object;
A5: upper_bound(rng(min(h,g,x,z))) is set by TARSKI:1;
assume
A6: [x,z] in [:C1,C3:];
then
A7: z in C3 by ZFMISC_1:87;
x in C1 by A6,ZFMISC_1:87;
hence thesis by A3,A5,A7;
end;
then
A8: dom IT = [:C1,C3:];
rng IT c= [.0,1.]
proof
reconsider A=[.0,jj.] as
non empty closed_interval Subset of REAL by MEASURE5:14;
let c being object;
assume c in rng IT;
then consider a being Element of [:C1,C3:] such that
a in dom IT and
A10: c = IT.a by PARTFUN1:3;
A11: A = [. lower_bound A, upper_bound A .] by INTEGRA1:4;
then
A12: 0=lower_bound A by INTEGRA1:5;
A13: 0 <= upper_bound(rng(min(h,g,x,z))) & upper_bound(rng(min(h,g,x,z))) <= 1
proof
A14: rng(min(h,g,x,z)) c= A by RELAT_1:def 19;
A is bounded_below by INTEGRA1:3;
then
A15: lower_bound A <= lower_bound(rng(min (h,g,x,z))) by A14,SEQ_4:47;
A is bounded_above by INTEGRA1:3;
then
A16: upper_bound(rng(min(h,g,x,z))) <= upper_bound A by A14,SEQ_4:48;
lower_bound(rng(min(h,g,x,z))) <= upper_bound(rng(min(h,g,x,z)))
by Th1,SEQ_4:11;
hence thesis by A11,A16,A15,INTEGRA1:5;
end;
consider x,z being object such that
x in C1 and
z in C3 and
A17: a = [x,z] by ZFMISC_1:def 2;
reconsider z,x as set by TARSKI:1;
A18: IT.(x,z) = upper_bound(rng(min(h,g,x,z))) by A3,A8,A17;
then
A19: IT.a <= 1 by A13,A17;
A20: 1=upper_bound A by A11,INTEGRA1:5;
0 <= IT.a by A13,A17,A18;
hence thesis by A10,A12,A20,A19,INTEGRA2:1;
end;
then IT is RMembership_Func of C1,C3 by A8,FUNCT_2:def 1,RELAT_1:def 19;
hence thesis by A3,A8;
end;
uniqueness
proof
let F,G be RMembership_Func of C1,C3;
assume that
A21: for x,z being object st [x,z] in [:C1,C3:]
holds F.(x,z) = upper_bound(rng(min(h,g,x,z
))) and
A22: for x,z being object st [x,z] in [:C1,C3:]
holds G.(x,z) = upper_bound(rng(min(h,g,x,z
)));
A23: for c being Element of [:C1,C3:] st c in [:C1,C3:] holds F.c = G.c
proof
let c being Element of [:C1,C3:];
consider x,z being object such that
x in C1 and
z in C3 and
A24: c = [x,z] by ZFMISC_1:def 2;
reconsider z,x as set by TARSKI:1;
A25: G.(x,z) = upper_bound(rng(min(h,g,x,z))) by A22,A24;
F.(x,z) = upper_bound(rng(min(h,g,x,z))) by A21,A24;
hence thesis by A24,A25;
end;
A26: dom G = [:C1,C3:] by FUNCT_2:def 1;
dom F = [:C1,C3:] by FUNCT_2:def 1;
hence thesis by A26,A23,PARTFUN1:5;
end;
end;
Lm1: for f be RMembership_Func of C1,C2, g,h be RMembership_Func of C2,C3, x,z
be set st x in C1 & z in C3
holds upper_bound(rng(min(f,max(g,h),x,z))) = max(upper_bound rng(
min(f,g,x,z)),upper_bound rng(min(f,h,x,z)))
proof
let f being RMembership_Func of C1,C2, g,h being RMembership_Func of C2,C3,x
,z being set;
assume that
A1: x in C1 and
A2: z in C3;
A3: for y be Element of C2 st y in C2 holds max(min(f,g,x,z),min(f,h,x,z)).y
=min(f,max(g,h),x,z).y
proof
let y being Element of C2;
assume y in C2;
A4: [y,z] in [:C2,C3:] by A2,ZFMISC_1:87;
max(min(f,g,x,z),min(f,h,x,z)).y =max(min(f,g,x,z).y,min(f,h,x,z).y)
by FUZZY_1:def 4
.=max(min(f,g,x,z).y,min(f. [x,y],h. [y,z])) by A1,A2,Def2
.=max( min(f. [x,y],g. [y,z]),min(f. [x,y],h. [y,z]) ) by A1,A2,Def2
.=min(f. [x,y],max(g. [y,z],h. [y,z])) by XXREAL_0:38
.=min(f. [x,y],max(g,h). [y,z]) by A4,FUZZY_1:def 4
.=min(f,max(g,h),x,z).y by A1,A2,Def2;
hence thesis;
end;
set F = min(f,g,x,z), G = min(f,h,x,z);
A5: dom min(f,max(g,h),x,z) = C2 by FUNCT_2:def 1;
rng max(F,G) is real-bounded by Th1;
then
A6: rng max(F,G) is bounded_above by XXREAL_2:def 11;
A7: for s being Real st 0<s
ex y st y in dom max(F,G) & upper_bound rng max(
F,G) - s < max(F,G).y
proof
let s being Real;
assume 0 < s;
then consider r being Real such that
A8: r in rng max(F,G) and
A9: upper_bound rng max(F,G) - s < r by A6,SEQ_4:def 1;
ex y being object st y in dom max(F,G) & r = max(F,G).y
by A8,FUNCT_1:def 3;
hence thesis by A9;
end;
for s being Real st 0<s
holds upper_bound rng max(F,G) - s < max(upper_bound rng
F,upper_bound rng G)
proof
let s being Real;
assume 0 < s;
then consider y such that
A10: y in dom max(F,G) and
A11: upper_bound rng max(F,G) - s < max(F,G).y by A7;
A12: max(F,G).y = max(F.y,G.y) by A10,FUZZY_1:def 4;
A13: for y st y in C2 holds F.y <= upper_bound rng F & G.y <= upper_bound rng G
proof
let y;
assume
A14: y in C2;
then y in dom G by FUNCT_2:def 1;
then
A15: G.y in rng G by FUNCT_1:def 3;
rng G is real-bounded by Th1;
then
A16: rng G is bounded_above by XXREAL_2:def 11;
rng F is real-bounded by Th1;
then
A17: rng F is bounded_above by XXREAL_2:def 11;
y in dom F by A14,FUNCT_2:def 1;
then F.y in rng F by FUNCT_1:def 3;
hence thesis by A15,A17,A16,SEQ_4:def 1;
end;
then
A18: G.y <= upper_bound rng G by A10;
F.y <= upper_bound rng F by A10,A13;
then max(F,G).y <= max(upper_bound rng F,upper_bound rng G)
by A12,A18,XXREAL_0:26;
hence thesis by A11,XXREAL_0:2;
end;
then for s being Real st 0<s
holds upper_bound rng max(F,G) - s <= max(upper_bound
rng F,upper_bound rng G);
then
A19: upper_bound rng max(F,G) <= max(upper_bound rng F, upper_bound rng G)
by XREAL_1:57;
A20: for y st y in C2 holds max(F,G).y <= upper_bound rng max(F,G)
proof
let y;
assume y in C2;
then y in dom max(F,G) by FUNCT_2:def 1;
then
A21: max(F,G).y in rng max(F,G) by FUNCT_1:def 3;
rng max(F,G) is real-bounded by Th1;
then rng max(F,G) is bounded_above by XXREAL_2:def 11;
hence thesis by A21,SEQ_4:def 1;
end;
rng G is real-bounded by Th1;
then
A22: rng G is bounded_above by XXREAL_2:def 11;
A23: for s being Real st 0<s
ex y st y in dom G & upper_bound rng G - s < G.y
proof
let s being Real;
assume 0 < s;
then consider r being Real such that
A24: r in rng G and
A25: upper_bound rng G - s < r by A22,SEQ_4:def 1;
ex y being object st y in dom G & r = G.y by A24,FUNCT_1:def 3;
hence thesis by A25;
end;
for s being Real st 0<s
holds upper_bound rng G - s <= upper_bound rng max(F,G)
proof
let s being Real;
assume 0<s;
then consider y such that
A26: y in dom G and
A27: upper_bound rng G - s < G.y by A23;
G.y <= max(F.y,G.y) by XXREAL_0:25;
then G.y <= max(F,G).y by A26,FUZZY_1:def 4;
then
A28: upper_bound rng G - s < max(F,G).y by A27,XXREAL_0:2;
max(F,G).y <= upper_bound rng max(F,G) by A20,A26;
hence thesis by A28,XXREAL_0:2;
end;
then
A29: upper_bound rng G <= upper_bound rng max(F,G) by XREAL_1:57;
rng F is real-bounded by Th1;
then
A30: rng F is bounded_above by XXREAL_2:def 11;
A31: for s being Real st 0<s
ex y st y in dom F & upper_bound rng F - s < F.y
proof
let s being Real;
assume 0 < s;
then consider r being Real such that
A32: r in rng F and
A33: upper_bound rng F - s < r by A30,SEQ_4:def 1;
ex y being object st y in dom F & r = F.y by A32,FUNCT_1:def 3;
hence thesis by A33;
end;
for s being Real st 0<s
holds upper_bound rng F - s <= upper_bound rng max(F,G)
proof
let s being Real;
assume 0<s;
then consider y such that
A34: y in dom F and
A35: upper_bound rng F - s < F.y by A31;
F.y <= max(F.y,G.y) by XXREAL_0:25;
then F.y <= max(F,G).y by A34,FUZZY_1:def 4;
then
A36: upper_bound rng F - s < max(F,G).y by A35,XXREAL_0:2;
max(F,G).y <= upper_bound rng max(F,G) by A20,A34;
hence thesis by A36,XXREAL_0:2;
end;
then upper_bound rng F <= upper_bound rng max(F,G) by XREAL_1:57;
then max(upper_bound rng F, upper_bound rng G)
<= upper_bound rng max(F,G) by A29,XXREAL_0:28;
then
A37: upper_bound rng max(F,G) = max(upper_bound rng F, upper_bound rng G)
by A19,XXREAL_0:1;
dom max(min(f,g,x,z),min(f,h,x,z)) = C2 by FUNCT_2:def 1;
hence thesis by A5,A3,A37,PARTFUN1:5;
end;
theorem
for f be RMembership_Func of C1,C2, g,h be RMembership_Func of C2,C3
holds f(#)(max(g,h)) = max(f(#)g,f(#)h)
proof
let f be RMembership_Func of C1,C2,g,h be RMembership_Func of C2,C3;
A1: dom max(f(#)g,f(#)h) = [:C1,C3:] by FUNCT_2:def 1;
A2: for c being Element of [:C1,C3:] st c in [:C1,C3:] holds (f(#)(max(g,h))
).c = max(f(#)g,f(#)h).c
proof
let c being Element of [:C1,C3:];
consider x,z being object such that
A3: x in C1 and
A4: z in C3 and
A5: c = [x,z] by ZFMISC_1:def 2;
reconsider z,x as set by TARSKI:1;
(f(#)(max(g,h))).c = (f(#)(max(g,h))).(x,z) by A5
.= upper_bound(rng(min(f,max(g,h),x,z))) by A5,Def3
.= max(upper_bound rng(min(f,g,x,z)),upper_bound rng(min(f,h,x,z)))
by A3,A4,Lm1
.= max((f(#)g).(x,z),upper_bound rng(min(f,h,x,z))) by A5,Def3
.= max((f(#)g).(x,z),(f(#)h).(x,z)) by A5,Def3
.= max(f(#)g,f(#)h).c by A5,FUZZY_1:def 4;
hence thesis;
end;
dom(f(#)(max(g,h))) = [:C1,C3:] by FUNCT_2:def 1;
hence thesis by A1,A2,PARTFUN1:5;
end;
Lm2: for f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3, x,z
be set st x in C1 & z in C3
holds upper_bound(rng(min(max(f,g),h,x,z))) = max(upper_bound rng(
min(f,h,x,z)),upper_bound rng(min(g,h,x,z)))
proof
let f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3, x,z be
set;
assume that
A1: x in C1 and
A2: z in C3;
A3: for y being Element of C2 st y in C2 holds min(max(f,g),h,x,z).y = max(
min(f,h,x,z),min(g,h,x,z)).y
proof
let y being Element of C2;
assume y in C2;
A4: [x,y] in [:C1,C2:] by A1,ZFMISC_1:87;
min(max(f,g),h,x,z).y = min(max(f,g). [x,y],h. [y,z]) by A1,A2,Def2
.= min(max(f. [x,y],g. [x,y]),h. [y,z]) by A4,FUZZY_1:def 4
.= max(min(f. [x,y],h. [y,z]),min(g. [x,y],h. [y,z])) by XXREAL_0:38
.= max(min(f. [x,y],h. [y,z]),min(g,h,x,z).y) by A1,A2,Def2
.= max(min(f,h,x,z).y,min(g,h,x,z).y) by A1,A2,Def2;
hence thesis by FUZZY_1:def 4;
end;
set F = min(f,h,x,z), G = min(g,h,x,z);
A5: dom max(min(f,h,x,z),min(g,h,x,z)) = C2 by FUNCT_2:def 1;
rng max(F,G) is real-bounded by Th1;
then
A6: rng max(F,G) is bounded_above by XXREAL_2:def 11;
A7: for y st y in dom max(F,G) holds max(F,G).y <= upper_bound rng(max(F,G))
proof
let y;
assume y in dom max(F,G);
then max(F,G).y in rng max(F,G) by FUNCT_1:def 3;
hence thesis by A6,SEQ_4:def 1;
end;
rng G is real-bounded by Th1;
then
A8: rng G is bounded_above by XXREAL_2:def 11;
A9: for y st y in dom G holds G.y <= upper_bound rng G
proof
let y;
assume y in dom G;
then G.y in rng G by FUNCT_1:def 3;
hence thesis by A8,SEQ_4:def 1;
end;
A10: for s being Real st 0<s
ex y st y in dom G & upper_bound rng G-s <= max(
F,G).y
proof
let s being Real;
assume 0<s;
then consider r being Real such that
A11: r in rng G and
A12: upper_bound rng G-s<r by A8,SEQ_4:def 1;
consider y being object such that
A13: y in dom G and
A14: r = G.y by A11,FUNCT_1:def 3;
G.y <= max(F.y,G.y) by XXREAL_0:25;
then r <= max(F,G).y by A13,A14,FUZZY_1:def 4;
hence thesis by A12,A13,XXREAL_0:2;
end;
for s being Real st 0<s
holds upper_bound rng G-s <= upper_bound rng max(F,G)
proof
let s being Real;
assume 0<s;
then consider y such that
A15: y in dom G and
A16: upper_bound rng G - s <= max(F,G).y by A10;
y in C2 by A15;
then y in dom max(F,G) by FUNCT_2:def 1;
then max(F,G).y <= upper_bound rng max(F,G) by A7;
hence thesis by A16,XXREAL_0:2;
end;
then
A17: upper_bound rng G <= upper_bound rng(max(F,G)) by XREAL_1:57;
rng F is real-bounded by Th1;
then
A18: rng F is bounded_above by XXREAL_2:def 11;
A19: for s being Real st 0<s
ex y st y in dom F & upper_bound rng F-s <= max(
F,G).y
proof
let s being Real;
assume 0<s;
then consider r being Real such that
A20: r in rng F and
A21: upper_bound rng F-s<r by A18,SEQ_4:def 1;
consider y being object such that
A22: y in dom F and
A23: r = F.y by A20,FUNCT_1:def 3;
F.y <= max(F.y,G.y) by XXREAL_0:25;
then r <= max(F,G).y by A22,A23,FUZZY_1:def 4;
hence thesis by A21,A22,XXREAL_0:2;
end;
for s being Real st 0<s
holds upper_bound rng F-s <= upper_bound rng max(F,G)
proof
let s being Real;
assume 0<s;
then consider y such that
A24: y in dom F and
A25: upper_bound rng F - s <= max(F,G).y by A19;
y in C2 by A24;
then y in dom max(F,G) by FUNCT_2:def 1;
then max(F,G).y <= upper_bound rng max(F,G) by A7;
hence thesis by A25,XXREAL_0:2;
end;
then upper_bound rng F <= upper_bound rng(max(F,G)) by XREAL_1:57;
then
A26: upper_bound rng(max(F,G)) >=
max(upper_bound rng F,upper_bound rng G) by A17,XXREAL_0:28;
A27: for y st y in dom F holds F.y <= upper_bound rng F
proof
let y;
assume y in dom F;
then F.y in rng F by FUNCT_1:def 3;
hence thesis by A18,SEQ_4:def 1;
end;
for s being Real st 0<s
holds upper_bound rng max(F,G) - s <= max(upper_bound
rng F,upper_bound rng G)
proof
let s being Real;
assume 0<s;
then consider r being Real such that
A28: r in rng max(F,G) and
A29: upper_bound rng max(F,G)-s<r by A6,SEQ_4:def 1;
consider y be object such that
A30: y in dom max(F,G) and
A31: r = max(F,G).y by A28,FUNCT_1:def 3;
A32: y in C2 by A30;
then y in dom G by FUNCT_2:def 1;
then
A33: G.y <= upper_bound rng G by A9;
y in dom F by A32,FUNCT_2:def 1;
then F.y <= upper_bound rng F by A27;
then
A34: max(F.y,G.y) <=
max(upper_bound rng F,upper_bound rng G) by A33,XXREAL_0:26;
upper_bound rng max(F,G)-s<=max(F.y,G.y) by A29,A30,A31,FUZZY_1:def 4;
hence thesis by A34,XXREAL_0:2;
end;
then
A35: upper_bound rng(max(F,G)) <=
max(upper_bound rng F,upper_bound rng G) by XREAL_1:57;
dom min(max(f,g),h,x,z) = C2 by FUNCT_2:def 1;
then min(max(f,g),h,x,z) = max(min(f,h,x,z),min(g,h,x,z)) by A5,A3,PARTFUN1:5
;
hence thesis by A35,A26,XXREAL_0:1;
end;
theorem
for f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3
holds (max(f,g))(#)h = max(f(#)h,g(#)h)
proof
let f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3;
A1: dom max(f(#)h,g(#)h) = [:C1,C3:] by FUNCT_2:def 1;
A2: for c being Element of [:C1,C3:] st c in [:C1,C3:] holds ((max(f,g))(#)h
).c = max(f(#)h,g(#)h).c
proof
let c being Element of [:C1,C3:];
consider x,z being object such that
A3: x in C1 and
A4: z in C3 and
A5: c = [x,z] by ZFMISC_1:def 2;
reconsider z,x as set by TARSKI:1;
((max(f,g))(#)h).c = ((max(f,g))(#)h).(x,z) by A5
.= upper_bound(rng(min(max(f,g),h,x,z))) by A5,Def3
.= max(upper_bound rng(min(f,h,x,z)),upper_bound rng(min(g,h,x,z)))
by A3,A4,Lm2
.= max((f(#)h).(x,z),upper_bound rng(min(g,h,x,z))) by A5,Def3
.= max((f(#)h).(x,z),(g(#)h).(x,z)) by A5,Def3
.= max(f(#)h,g(#)h).c by A5,FUZZY_1:def 4;
hence thesis;
end;
dom((max(f,g))(#)h) = [:C1,C3:] by FUNCT_2:def 1;
hence thesis by A1,A2,PARTFUN1:5;
end;
Lm3: for f be RMembership_Func of C1,C2, g,h be RMembership_Func of C2,C3, x,z
be set st x in C1 & z in C3
holds upper_bound(rng(min(f,min(g,h),x,z))) <= min(upper_bound rng(
min(f,g,x,z)),upper_bound rng(min(f,h,x,z)))
proof
let f be RMembership_Func of C1,C2, g,h be RMembership_Func of C2,C3, x,z be
set;
assume that
A1: x in C1 and
A2: z in C3;
set F = min(f,min(g,h),x,z), G = min(f,g,x,z), H = min(f,h,x,z);
rng F is real-bounded by Th1;
then
A3: rng F is bounded_above by XXREAL_2:def 11;
A4: for s being Real st 0<s
ex y st y in dom F & upper_bound rng F - s <= G.
y
proof
let s being Real;
assume 0<s;
then consider r being Real such that
A5: r in rng F and
A6: upper_bound rng F-s<r by A3,SEQ_4:def 1;
consider y being object such that
A7: y in dom F and
A8: r = F.y by A5,FUNCT_1:def 3;
A9: [y,z] in [:C2,C3:] by A2,A7,ZFMISC_1:87;
F.y = min(f. [x,y],min(g,h). [y,z]) by A1,A2,A7,Def2
.= min(f. [x,y],min(g. [y,z],h. [y,z])) by A9,FUZZY_1:def 3
.= min(min(f. [x,y],g. [y,z]),h. [y,z]) by XXREAL_0:33
.= min(G.y,h. [y,z]) by A1,A2,A7,Def2;
then r <= G.y by A8,XXREAL_0:17;
hence thesis by A6,A7,XXREAL_0:2;
end;
A10: for s being Real st 0<s
ex y st y in dom F & upper_bound rng F - s <= H.
y
proof
let s being Real;
assume 0<s;
then consider r being Real such that
A11: r in rng F and
A12: upper_bound rng F-s<r by A3,SEQ_4:def 1;
consider y being object such that
A13: y in dom F and
A14: r = F.y by A11,FUNCT_1:def 3;
A15: [y,z] in [:C2,C3:] by A2,A13,ZFMISC_1:87;
F.y = min(f. [x,y],min(g,h). [y,z]) by A1,A2,A13,Def2
.= min(f. [x,y],min(g. [y,z],h. [y,z])) by A15,FUZZY_1:def 3
.= min(min(f. [x,y],h. [y,z]),g. [y,z]) by XXREAL_0:33
.= min(H.y,g. [y,z]) by A1,A2,A13,Def2;
then r <= H.y by A14,XXREAL_0:17;
hence thesis by A12,A13,XXREAL_0:2;
end;
rng H is real-bounded by Th1;
then
A16: rng H is bounded_above by XXREAL_2:def 11;
A17: for y st y in dom H holds H.y <= upper_bound rng H
proof
let y;
assume y in dom H;
then H.y in rng H by FUNCT_1:def 3;
hence thesis by A16,SEQ_4:def 1;
end;
for s being Real st 0<s
holds upper_bound rng F - s <= upper_bound rng H
proof
let s being Real;
assume 0<s;
then consider y such that
A18: y in dom F and
A19: upper_bound rng F - s <= H.y by A10;
y in C2 by A18;
then y in dom H by FUNCT_2:def 1;
then H.y <= upper_bound rng H by A17;
hence thesis by A19,XXREAL_0:2;
end;
then
A20: upper_bound rng F <= upper_bound rng H by XREAL_1:57;
rng G is real-bounded by Th1;
then
A21: rng G is bounded_above by XXREAL_2:def 11;
A22: for y st y in dom G holds G.y <= upper_bound rng G
proof
let y;
assume y in dom G;
then G.y in rng G by FUNCT_1:def 3;
hence thesis by A21,SEQ_4:def 1;
end;
for s being Real st 0<s
holds upper_bound rng F - s <= upper_bound rng G
proof
let s being Real;
assume 0<s;
then consider y such that
A23: y in dom F and
A24: upper_bound rng F - s <= G.y by A4;
y in C2 by A23;
then y in dom G by FUNCT_2:def 1;
then G.y <= upper_bound rng G by A22;
hence thesis by A24,XXREAL_0:2;
end;
then upper_bound rng F <= upper_bound rng G by XREAL_1:57;
hence thesis by A20,XXREAL_0:20;
end;
theorem
for f be RMembership_Func of C1,C2, g,h be RMembership_Func of C2,C3
holds f(#)(min(g,h)) c= min(f(#)g,f(#)h)
proof
let f be RMembership_Func of C1,C2,g,h be RMembership_Func of C2,C3;
let c be Element of [:C1,C3:];
consider x,z being object such that
A1: x in C1 and
A2: z in C3 and
A3: c = [x,z] by ZFMISC_1:def 2;
reconsider z,x as set by TARSKI:1;
A4: (f(#)(min(g,h))).(x,z) = upper_bound(rng(min(f,min(g,h),x,z))) by A3,Def3;
min(f(#)g,f(#)h).(x,z) = min((f(#)g).(x,z),(f(#)h).(x,z)) by A3,FUZZY_1:def 3
.= min((f(#)g).(x,z),upper_bound rng(min(f,h,x,z))) by A3,Def3
.= min(upper_bound rng(min(f,g,x,z)),
upper_bound rng(min(f,h,x,z))) by A3,Def3;
hence thesis by A1,A2,A3,A4,Lm3;
end;
Lm4: for f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3, x,z
be set st x in C1 & z in C3
holds upper_bound(rng(min(min(f,g),h,x,z))) <= min(upper_bound(rng(
min(f,h,x,z))),upper_bound(rng(min(g,h,x,z))))
proof
let f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3, x,z be
set;
assume that
A1: x in C1 and
A2: z in C3;
set F = min(min(f,g),h,x,z), G = min(f,h,x,z), H = min(g,h,x,z);
rng F is real-bounded by Th1;
then
A3: rng F is bounded_above by XXREAL_2:def 11;
A4: for s being Real st 0<s
ex y st y in dom F & upper_bound rng F - s <= G.
y
proof
let s being Real;
assume 0<s;
then consider r being Real such that
A5: r in rng F and
A6: upper_bound rng F-s<r by A3,SEQ_4:def 1;
consider y being object such that
A7: y in dom F and
A8: r = F.y by A5,FUNCT_1:def 3;
A9: [x,y] in [:C1,C2:] by A1,A7,ZFMISC_1:87;
F.y = min(min(f,g). [x,y],h. [y,z]) by A1,A2,A7,Def2
.= min(min(f. [x,y],g. [x,y]),h. [y,z]) by A9,FUZZY_1:def 3
.= min(min(h. [y,z],f. [x,y]),g. [x,y]) by XXREAL_0:33
.= min(G.y,g. [x,y]) by A1,A2,A7,Def2;
then r <= G.y by A8,XXREAL_0:17;
hence thesis by A6,A7,XXREAL_0:2;
end;
A10: for s being Real st 0<s
ex y st y in dom F & upper_bound rng F - s <= H.
y
proof
let s being Real;
assume 0<s;
then consider r being Real such that
A11: r in rng F and
A12: upper_bound rng F-s<r by A3,SEQ_4:def 1;
consider y being object such that
A13: y in dom F and
A14: r = F.y by A11,FUNCT_1:def 3;
A15: [x,y] in [:C1,C2:] by A1,A13,ZFMISC_1:87;
F.y = min(min(f,g). [x,y],h. [y,z]) by A1,A2,A13,Def2
.= min(min(f. [x,y],g. [x,y]),h. [y,z]) by A15,FUZZY_1:def 3
.= min(f. [x,y],min(h. [y,z],g. [x,y])) by XXREAL_0:33
.= min(H.y,f. [x,y]) by A1,A2,A13,Def2;
then r <= H.y by A14,XXREAL_0:17;
hence thesis by A12,A13,XXREAL_0:2;
end;
rng H is real-bounded by Th1;
then
A16: rng H is bounded_above by XXREAL_2:def 11;
A17: for y st y in dom H holds H.y <= upper_bound rng H
proof
let y;
assume y in dom H;
then H.y in rng H by FUNCT_1:def 3;
hence thesis by A16,SEQ_4:def 1;
end;
for s being Real st 0<s
holds upper_bound rng F - s <= upper_bound rng H
proof
let s being Real;
assume 0<s;
then consider y such that
A18: y in dom F and
A19: upper_bound rng F - s <= H.y by A10;
y in C2 by A18;
then y in dom H by FUNCT_2:def 1;
then H.y <= upper_bound rng H by A17;
hence thesis by A19,XXREAL_0:2;
end;
then
A20: upper_bound rng F <= upper_bound rng H by XREAL_1:57;
rng G is real-bounded by Th1;
then
A21: rng G is bounded_above by XXREAL_2:def 11;
A22: for y st y in dom G holds G.y <= upper_bound rng G
proof
let y;
assume y in dom G;
then G.y in rng G by FUNCT_1:def 3;
hence thesis by A21,SEQ_4:def 1;
end;
for s being Real st 0<s
holds upper_bound rng F - s <= upper_bound rng G
proof
let s being Real;
assume 0<s;
then consider y such that
A23: y in dom F and
A24: upper_bound rng F - s <= G.y by A4;
y in C2 by A23;
then y in dom G by FUNCT_2:def 1;
then G.y <= upper_bound rng G by A22;
hence thesis by A24,XXREAL_0:2;
end;
then upper_bound rng F <= upper_bound rng G by XREAL_1:57;
hence thesis by A20,XXREAL_0:20;
end;
theorem
for f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3
holds min(f,g)(#)h c= min(f(#)h,g(#)h)
proof
let f,g be RMembership_Func of C1,C2, h be RMembership_Func of C2,C3;
let c be Element of [:C1,C3:];
consider x,z being object such that
A1: x in C1 and
A2: z in C3 and
A3: c = [x,z] by ZFMISC_1:def 2;
reconsider z,x as set by TARSKI:1;
A4: (min(f,g)(#)h).(x,z) = upper_bound(rng(min(min(f,g),h,x,z))) by A3,Def3;
min(f(#)h,g(#)h).(x,z) = min((f(#)h).(x,z),(g(#)h).(x,z)) by A3,FUZZY_1:def 3
.= min(upper_bound(rng(min(f,h,x,z))),(g(#)h).(x,z)) by A3,Def3
.= min(upper_bound(rng(min(f,h,x,z))),
upper_bound(rng(min(g,h,x,z)))) by A3,Def3;
hence thesis by A1,A2,A3,A4,Lm4;
end;
Lm5: for f be RMembership_Func of C1,C2, g be RMembership_Func of C2,C3, x,z
be set st x in C1 & z in C3
holds upper_bound rng min(converse g,converse f,z,x) = upper_bound
rng min(f,g,x,z)
proof
let f be RMembership_Func of C1,C2, g be RMembership_Func of C2,C3, x,z be
set;
assume that
A1: x in C1 and
A2: z in C3;
rng min(f,g,x,z) is real-bounded by Th1;
then
A3: rng min(f,g,x,z) is bounded_above by XXREAL_2:def 11;
for s being Real st 0<s
holds upper_bound rng min(f,g,x,z) - s <= upper_bound
rng min(converse g,converse f,z,x)
proof
let s being Real;
assume s>0;
then consider r being Real such that
A4: r in rng min(f,g,x,z) and
A5: upper_bound rng min(f,g,x,z) - s < r by A3,SEQ_4:def 1;
consider y be object such that
A6: y in dom min(f,g,x,z) and
A7: r = min(f,g,x,z).y by A4,FUNCT_1:def 3;
reconsider y as set by TARSKI:1;
A8: [z,y] in [:C3,C2:] by A2,A6,ZFMISC_1:87;
y in C2 by A6;
then y in dom min(converse g,converse f,z,x) by FUNCT_2:def 1;
then
A9: min(converse g,converse f,z,x).y <=
upper_bound rng min(converse g,converse f
,z,x) by Th1;
A10: [y,x] in [:C2,C1:] by A1,A6,ZFMISC_1:87;
r = min(f.(x,y),g.(y,z)) by A1,A2,A6,A7,Def2
.= min((converse f).(y,x),g.(y,z)) by A10,Def1
.= min((converse f).(y,x),(converse g).(z,y)) by A8,Def1
.= min(converse g,converse f,z,x).y by A1,A2,A6,Def2;
hence thesis by A5,A9,XXREAL_0:2;
end;
then
A11: upper_bound rng min(converse g,converse f,z,x) >=
upper_bound rng min(f,g,x,z) by XREAL_1:57;
rng min(converse g,converse f,z,x) is real-bounded by Th1;
then
A12: rng min(converse g,converse f,z,x) is bounded_above by XXREAL_2:def 11;
for s being Real st 0<s
holds upper_bound rng min(converse g,converse f,z
,x) - s <= upper_bound rng min(f,g,x,z)
proof
let s being Real;
assume s>0;
then consider r being Real such that
A13: r in rng min(converse g,converse f,z,x) and
A14: upper_bound rng min(converse g,converse f,z,x) - s < r by A12,SEQ_4:def 1;
consider y be object such that
A15: y in dom min(converse g,converse f,z,x) and
A16: r = min(converse g,converse f,z,x).y by A13,FUNCT_1:def 3;
A17: [z,y] in [:C3,C2:] by A2,A15,ZFMISC_1:87;
y in C2 by A15;
then y in dom min(f,g,x,z ) by FUNCT_2:def 1;
then
A18: min(f,g,x,z).y <= upper_bound rng min(f,g,x,z) by Th1;
A19: [y,x] in [:C2,C1:] by A1,A15,ZFMISC_1:87;
reconsider y as set by TARSKI:1;
r = min((converse g).(z,y),(converse f).(y,x)) by A1,A2,A15,A16,Def2
.= min(g.(y,z),(converse f).(y,x)) by A17,Def1
.= min(g.(y,z),f.(x,y)) by A19,Def1
.= min(f,g,x,z).y by A1,A2,A15,Def2;
hence thesis by A14,A18,XXREAL_0:2;
end;
then upper_bound rng min(converse g,converse f,z,x) <=
upper_bound rng min(f,g,x,z) by XREAL_1:57;
hence thesis by A11,XXREAL_0:1;
end;
theorem
for f be RMembership_Func of C1,C2, g be RMembership_Func of C2,C3
holds converse(f(#)g) = (converse g)(#)(converse f)
proof
let f be RMembership_Func of C1,C2, g be RMembership_Func of C2,C3;
A1: dom((converse g)(#)(converse f)) = [:C3,C1:] by FUNCT_2:def 1;
A2: for c being Element of [:C3,C1:] st c in [:C3,C1:] holds (converse(f(#)g
)).c = ((converse g)(#)(converse f)).c
proof
let c being Element of [:C3,C1:];
assume c in [:C3,C1:];
consider z,x be object such that
A3: z in C3 and
A4: x in C1 and
A5: c =[z,x] by ZFMISC_1:def 2;
A6: [x,z] in [:C1,C3:] by A3,A4,ZFMISC_1:87;
reconsider z,x as set by TARSKI:1;
A7: ((converse g)(#)(converse f)).(z,x) =
upper_bound rng min(converse g,converse
f,z,x) by A5,Def3;
(converse(f(#)g)).(z,x) = (f(#)g).(x,z) by A5,Def1
.= upper_bound rng min(f,g,x,z) by A6,Def3;
hence thesis by A3,A4,A5,A7,Lm5;
end;
dom converse(f(#)g) = [:C3,C1:] by FUNCT_2:def 1;
hence thesis by A1,A2,PARTFUN1:5;
end;
theorem Th18:
for f,g be RMembership_Func of C1,C2, h,k be RMembership_Func of
C2,C3, x,z be set st x in C1 & z in C3 & (for y be set st y in C2 holds f. [x,y
]<=g. [x,y] & h. [y,z]<=k. [y,z]) holds (f(#)h). [x,z] <= (g(#)k). [x,z]
proof
let f,g be RMembership_Func of C1,C2, h,k be RMembership_Func of C2,C3, x,z
be set;
assume that
A1: x in C1 and
A2: z in C3 and
A3: for y be set st y in C2 holds f. [x,y]<=g. [x,y] & h. [y,z]<=k. [y, z];
A4: [x,z] in [:C1,C3:] by A1,A2,ZFMISC_1:87;
then
A5: (g(#)k).(x,z) = upper_bound rng min(g,k,x,z) by Def3;
rng min(f,h,x,z) is real-bounded by Th1;
then
A6: rng min(f,h,x,z) is bounded_above by XXREAL_2:def 11;
A7: for s being Real st s>0
holds upper_bound (rng (min(f,h,x,z))) - s <= upper_bound
rng min(g,k,x,z)
proof
let s being Real;
assume s>0;
then consider r be Real such that
A8: r in rng min(f,h,x,z) and
A9: upper_bound rng min(f,h,x,z)-s<r by A6,SEQ_4:def 1;
consider y being object such that
A10: y in dom min(f,h,x,z) and
A11: r=min(f,h,x,z).y by A8,FUNCT_1:def 3;
A12: h. [y,z]<=k. [y,z] by A3,A10;
f. [x,y]<=g. [x,y] by A3,A10;
then min(f. [x,y],h. [y,z]) <= min(g. [x,y],k. [y,z]) by A12,XXREAL_0:18;
then
A13: min(f,h,x,z).y <= min(g. [x,y],k. [y,z]) by A1,A2,A10,Def2;
y in C2 by A10;
then
A14: y in dom min(g,k,x,z) by FUNCT_2:def 1;
min(g. [x,y],k. [y,z]) = min(g,k,x,z).y by A1,A2,A10,Def2;
then min(g. [x,y],k. [y,z]) <= upper_bound rng min(g,k,x,z) by A14,Th1;
then min(f,h,x,z).y <= upper_bound rng min(g,k,x,z) by A13,XXREAL_0:2;
hence thesis by A9,A11,XXREAL_0:2;
end;
(f(#)h).(x,z) = upper_bound (rng (min(f,h,x,z))) by A4,Def3;
hence thesis by A5,A7,XREAL_1:57;
end;
theorem
for f,g be RMembership_Func of C1,C2, h,k be RMembership_Func of C2,C3
st f c= g & h c= k holds f(#)h c= g(#)k
proof
let f,g be RMembership_Func of C1,C2, h,k being RMembership_Func of C2,C3;
assume that
A1: f c= g and
A2: h c= k;
let c be Element of [:C1,C3:];
consider x,z being object such that
A3: x in C1 and
A4: z in C3 and
A5: c = [x,z] by ZFMISC_1:def 2;
for y be set st y in C2 holds f. [x,y]<=g. [x,y] & h. [y,z]<=k. [y,z]
proof
let y be set;
assume
A6: y in C2;
then
A7: [y,z] in [:C2,C3:] by A4,ZFMISC_1:87;
[x,y] in [:C1,C2:] by A3,A6,ZFMISC_1:87;
hence thesis by A1,A2,A7;
end;
hence thesis by A3,A4,A5,Th18;
end;
begin
:: Definition of identity relation
:: and properties of universe relation and zero relation
Lm6: 1 in REAL & 0 in REAL by XREAL_0:def 1;
definition
let C1,C2 be non empty set;
func Imf(C1,C2) -> RMembership_Func of C1,C2 means
:Def4:
for x,y being object st [x,y]
in [:C1,C2:] holds (x=y implies it.(x,y) = 1) & (x<>y implies it.(x,y) = 0);
existence
proof
defpred P[object,object,object] means
($1=$2 implies $3 = 1) & (not $1=$2 implies
$3 = 0);
A1: for x,y,z1,z2 being object st x in C1 & y in C2 & P[x,y,z1] & P[x,y,z2]
holds z1=z2;
A2: for x,y,z being object st x in C1 & y in C2 & P[x,y,z]
holds z in REAL by Lm6;
consider IT being PartFunc of [:C1,C2:],REAL such that
A3: (for x,y being object holds [x,y] in dom IT iff x in C1 & y in C2 &
ex z being object st P[x,y,z]) &
for x,y being object st [x,y] in dom IT holds P[x,y,IT.(x,y)]
from BINOP_1:sch 5(A2
,A1);
[:C1,C2:] c= dom IT
proof
let x,y be object;
A4: not x=y implies ex z st (x=y implies z = 1) & (not x=y implies z = 0 );
assume
A5: [x,y] in [:C1,C2:];
then
A6: y in C2 by ZFMISC_1:87;
x in C1 by A5,ZFMISC_1:87;
hence thesis by A3,A6,A4;
end;
then
A7: dom IT = [:C1,C2:];
rng IT c= [.0,1.]
proof
let c being object;
assume c in rng IT;
then consider z being Element of [:C1,C2:] such that
A8: z in dom IT and
A9: c = IT.z by PARTFUN1:3;
consider x,y being object such that
x in C1 and
y in C2 and
A10: z = [x,y] by ZFMISC_1:def 2;
A11: 1 in [.0,1.] & 0 in [.0,1.]
proof
reconsider A=[.0,jj.] as
non empty closed_interval Subset of REAL by MEASURE5:14;
A12: A = [. lower_bound A, upper_bound A .] by INTEGRA1:4;
then
A13: 1=upper_bound A by INTEGRA1:5;
0=lower_bound A by A12,INTEGRA1:5;
hence thesis by A13,INTEGRA2:1;
end;
then
A14: x<>y implies IT.(x,y) in [.0 , 1.] by A3,A8,A10;
x=y implies IT.(x,y) in [.0,1.] by A3,A8,A10,A11;
hence thesis by A9,A10,A14;
end;
then IT is RMembership_Func of C1,C2 by A7,FUNCT_2:def 1,RELAT_1:def 19;
hence thesis by A3,A7;
end;
uniqueness
proof
let F,G be RMembership_Func of C1,C2;
assume that
A15: for x,y being object
st [x,y] in [:C1,C2:] holds (x=y implies F.(x,y) = 1) & (
x<>y implies F.(x,y) = 0) and
A16: for x,y being object
st [x,y] in [:C1,C2:] holds (x=y implies G.(x,y) = 1) & (
x<>y implies G.(x,y) = 0);
A17: for x,y being object st x in C1 & y in C2 holds F.(x,y) = G.(x,y)
proof
let x,y be object;
assume that
A18: x in C1 and
A19: y in C2;
A20: [x,y] in [:C1,C2:] by A18,A19,ZFMISC_1:87;
then
A21: not x=y implies F.(x,y) = 0 by A15;
x=y implies F.(x,y) = 1 by A15,A20;
hence thesis by A16,A20,A21;
end;
thus thesis by A17;
end;
end;
theorem
for c be Element of [:C1,C2:] holds (Zmf(C1,C2)).c = 0 & (Umf(C1,C2)).
c = 1 by FUNCT_3:def 3;
theorem
for x,y st [x,y] in [:C1,C2:] holds (Zmf(C1,C2)). [x,y] = 0 & (Umf(C1,
C2)). [x,y] = 1 by FUNCT_3:def 3;
Lm7: for f be RMembership_Func of C2,C3, x,z be set st x in C1 & z in C3 holds
upper_bound rng min(Zmf(C1,C2),f,x,z) = Zmf(C1,C3). [x,z]
proof
let f be RMembership_Func of C2,C3, x,z be set;
assume that
A1: x in C1 and
A2: z in C3;
rng min(Zmf(C1,C2),f,x,z) is real-bounded by Th1;
then
A3: rng min(Zmf(C1,C2),f,x,z) is bounded_above by XXREAL_2:def 11;
for s being Real st 0<s
holds upper_bound rng min(Zmf(C1,C2),f,x,z) - s
<= Zmf(C1,C3). [x,z]
proof
let s being Real;
assume s>0;
then consider r being Real such that
A4: r in rng min(Zmf(C1,C2),f,x,z) and
A5: upper_bound rng min(Zmf(C1,C2),f,x,z) - s < r by A3,SEQ_4:def 1;
consider y be object such that
A6: y in dom min(Zmf(C1,C2),f,x,z) and
A7: r = min(Zmf(C1,C2),f,x,z).y by A4,FUNCT_1:def 3;
A8: [x,y] in [:C1,C2:] by A1,A6,ZFMISC_1:87;
A9: [x,z] in [:C1,C3:] by A1,A2,ZFMISC_1:87;
A10: 0 <= f. [y,z] by Th3;
r = min(Zmf(C1,C2). [x,y],f. [y,z]) by A1,A2,A6,A7,Def2
.= min(0,f. [y,z]) by A8,FUNCT_3:def 3
.= 0 by A10,XXREAL_0:def 9
.= Zmf(C1,C3). [x,z] by A9,FUNCT_3:def 3;
hence thesis by A5;
end;
then
A11: upper_bound rng min(Zmf(C1,C2),f,x,z) <= Zmf(C1,C3). [x,z] by XREAL_1:57;
upper_bound rng min(Zmf(C1,C2),f,x,z) >= Zmf(C1,C3). [x,z]
proof
reconsider A=[.0,jj.] as
non empty closed_interval Subset of REAL by MEASURE5:14;
A12: A is bounded_below by INTEGRA1:3;
rng min(Zmf(C1,C2),f,x,z) c= [.0,1.] by RELAT_1:def 19;
then
A13: lower_bound A <= lower_bound rng min(Zmf(C1,C2),f,x,z) by A12,SEQ_4:47;
A = [. lower_bound A, upper_bound A .] by INTEGRA1:4;
then
A14: 0=lower_bound A by INTEGRA1:5;
A15: lower_bound rng min(Zmf(C1,C2),f,x,z) <=
upper_bound rng min(Zmf(C1,C2),f,x,z) by Th1,SEQ_4:11;
[x,z] in [:C1,C3:] by A1,A2,ZFMISC_1:87;
hence thesis by A14,A13,A15,FUNCT_3:def 3;
end;
hence thesis by A11,XXREAL_0:1;
end;
theorem Th22:
for f be RMembership_Func of C2,C3 holds Zmf(C1,C2)(#)f = Zmf(C1 ,C3)
proof
let f be RMembership_Func of C2,C3;
A1: dom(Zmf(C1,C3)) = [:C1,C3:] by FUNCT_2:def 1;
A2: for c being Element of [:C1,C3:] st c in [:C1,C3:] holds (Zmf(C1,C2)(#)f
).c = Zmf(C1,C3).c
proof
let c be Element of [:C1,C3:];
consider x,z being object such that
A3: x in C1 and
A4: z in C3 and
A5: c = [x,z] by ZFMISC_1:def 2;
reconsider z,x as set by TARSKI:1;
(Zmf(C1,C2)(#)f).c = (Zmf(C1,C2)(#)f).(x,z) by A5
.= upper_bound rng min(Zmf(C1,C2),f,x,z) by A5,Def3
.= Zmf(C1,C3).c by A3,A4,A5,Lm7;
hence thesis;
end;
dom(Zmf(C1,C2)(#)f) = [:C1,C3:] by FUNCT_2:def 1;
hence thesis by A1,A2,PARTFUN1:5;
end;
Lm8: for f be RMembership_Func of C1,C2, x,z be set st x in C1 & z in C3 holds
upper_bound rng min(f,Zmf(C2,C3),x,z) = Zmf(C1,C3). [x,z]
proof
let f be RMembership_Func of C1,C2, x,z be set;
assume that
A1: x in C1 and
A2: z in C3;
rng min(f,Zmf(C2,C3),x,z) is real-bounded by Th1;
then
A3: rng min(f,Zmf(C2,C3),x,z) is bounded_above by XXREAL_2:def 11;
for s being Real st 0<s
holds upper_bound rng min(f,Zmf(C2,C3),x,z) - s
<= Zmf(C1,C3). [x,z]
proof
let s being Real;
assume s>0;
then consider r being Real such that
A4: r in rng min(f,Zmf(C2,C3),x,z) and
A5: upper_bound rng min(f,Zmf(C2,C3),x,z) - s < r by A3,SEQ_4:def 1;
consider y be object such that
A6: y in dom min(f,Zmf(C2,C3),x,z) and
A7: r = min(f,Zmf(C2,C3),x,z).y by A4,FUNCT_1:def 3;
A8: [y,z] in [:C2,C3:] by A2,A6,ZFMISC_1:87;
A9: [x,z] in [:C1,C3:] by A1,A2,ZFMISC_1:87;
A10: 0 <= f. [x,y] by Th3;
r = min(f. [x,y],Zmf(C2,C3). [y,z]) by A1,A2,A6,A7,Def2
.= min(f. [x,y],0) by A8,FUNCT_3:def 3
.= 0 by A10,XXREAL_0:def 9
.= Zmf(C1,C3). [x,z] by A9,FUNCT_3:def 3;
hence thesis by A5;
end;
then
A11: upper_bound rng min(f,Zmf(C2,C3),x,z) <= Zmf(C1,C3). [x,z] by XREAL_1:57;
upper_bound rng min(f,Zmf(C2,C3),x,z) >= Zmf(C1,C3). [x,z]
proof
reconsider A=[.0,jj.] as
non empty closed_interval Subset of REAL by MEASURE5:14;
A12: A is bounded_below by INTEGRA1:3;
rng min(f,Zmf(C2,C3),x,z) c= [.0,1.] by RELAT_1:def 19;
then
A13: lower_bound A <= lower_bound rng min(f,Zmf(C2,C3),x,z) by A12,SEQ_4:47;
A = [. lower_bound A, upper_bound A .] by INTEGRA1:4;
then
A14: 0=lower_bound A by INTEGRA1:5;
A15: lower_bound rng min(f,Zmf(C2,C3),x,z) <=
upper_bound rng min(f,Zmf(C2,C3),x,z) by Th1,SEQ_4:11;
[x,z] in [:C1,C3:] by A1,A2,ZFMISC_1:87;
hence thesis by A14,A13,A15,FUNCT_3:def 3;
end;
hence thesis by A11,XXREAL_0:1;
end;
theorem Th23:
for f be RMembership_Func of C1,C2 holds f(#)Zmf(C2,C3) = Zmf(C1 ,C3)
proof
let f be RMembership_Func of C1,C2;
A1: dom(Zmf(C1,C3)) = [:C1,C3:] by FUNCT_2:def 1;
A2: for c being Element of [:C1,C3:] st c in [:C1,C3:] holds (f(#)Zmf(C2,C3)
).c = Zmf(C1,C3).c
proof
let c be Element of [:C1,C3:];
consider x,z being object such that
A3: x in C1 and
A4: z in C3 and
A5: c = [x,z] by ZFMISC_1:def 2;
reconsider z,x as set by TARSKI:1;
(f(#)Zmf(C2,C3)).c = (f(#)Zmf(C2,C3)).(x,z) by A5
.= upper_bound rng min(f,Zmf(C2,C3),x,z) by A5,Def3
.= Zmf(C1,C3).c by A3,A4,A5,Lm8;
hence thesis;
end;
dom(f(#)Zmf(C2,C3)) = [:C1,C3:] by FUNCT_2:def 1;
hence thesis by A1,A2,PARTFUN1:5;
end;
theorem
for f be RMembership_Func of C1,C1 holds f(#)Zmf(C1,C1) = Zmf(C1,C1) (#)f
proof
let f be RMembership_Func of C1,C1;
f(#)Zmf(C1,C1) = Zmf(C1,C1) by Th23;
hence thesis by Th22;
end;
begin :: Addenda
:: missing, 2006.12.03, AT
theorem
for X,Y being non empty set for x being Element of X, y being Element
of Y holds (x = y implies Imf(X,Y).(x,y) = 1) & (x <> y implies Imf(X,Y).(x,y)
= 0)
proof
let X,Y being non empty set;
let x being Element of X, y being Element of Y;
[x,y] in [:X,Y:] by ZFMISC_1:87;
hence thesis by Def4;
end;
theorem
for X,Y being non empty set for x being Element of X, y being Element
of Y for f being RMembership_Func of X,Y holds (converse f).(y,x) = f.(x,y)
by Def1,ZFMISC_1:87;