:: Properties of Fuzzy Relation
:: by Noboru Endou , Takashi Mitsuishi and Keiji Ohkubo
::
:: Received June 25, 2001
:: Copyright (c) 2001-2016 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~~ RMembership_Func of C1,C2 means
: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~~~~=
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~~~~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~~~~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 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~~~~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~~~~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;
~~