:: Lattice of Fuzzy Sets
:: by Takashi Mitsuishi and Grzegorz Bancerek
::
:: Received August 12, 2003
:: Copyright (c) 2003-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, ORDERS_2, XREAL_0, STRUCT_0, TARSKI, XXREAL_0, MEASURE5,
XXREAL_1, XBOOLE_0, SUBSET_1, CARD_1, RELAT_2, LATTICE3, EQREL_1,
LATTICES, XXREAL_2, YELLOW_0, REAL_1, SEQ_4, REWRITE1, TREES_2, LATTICE2,
WAYBEL_0, RELAT_1, FUNCT_1, ORDINAL2, YELLOW_1, WAYBEL_3, PBOOLE, CARD_3,
WAYBEL_1, NEWTON, FUNCOP_1, FUNCT_2, MONOID_0, FUZZY_1, PARTFUN1,
QC_LANG1, FUZZY_2, VALUED_1, ZFMISC_1, LFUZZY_0, MEMBERED;
notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1,
DOMAIN_1, ORDINAL1, PARTFUN1, SUBSET_1, NUMBERS, XXREAL_2, XREAL_0,
MEMBERED, SEQ_4, RCOMP_1, RELSET_1, STRUCT_0, ORDERS_2, PBOOLE, MONOID_0,
LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, WAYBEL_3, FUZZY_1,
FUZZY_2, FUZZY_4, MEASURE5, FUNCOP_1, XXREAL_0;
constructors DOMAIN_1, SQUARE_1, LATTICE3, MONOID_0, ORDERS_3, WAYBEL_1,
WAYBEL_3, INTEGRA1, FUZZY_4, SEQ_4, RELSET_1, FUZZY_1, BINOP_2;
registrations SUBSET_1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0,
LATTICE3, MONOID_0, YELLOW_1, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL10,
WAYBEL17, ORDERS_4, ORDERS_2, FUNCOP_1;
requirements BOOLE, SUBSET, NUMERALS, REAL;
definitions TARSKI, RELAT_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1;
equalities XBOOLE_0, BINOP_1;
expansions TARSKI, XBOOLE_0, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, BINOP_1;
theorems ZFMISC_1, ORDERS_2, WAYBEL_1, FUNCT_1, XBOOLE_1, LATTICE3, YELLOW_0,
INTEGRA1, XBOOLE_0, TARSKI, SEQ_4, JORDAN5A, FUNCT_2, YELLOW_2, WAYBEL_3,
YELLOW_3, CARD_3, YELLOW_1, FUNCOP_1, FUZZY_2, FUZZY_4, FUZZY_1,
PARTFUN1, MONOID_0, WAYBEL_0, XXREAL_0, XXREAL_1, XXREAL_2, RELSET_1,
RELAT_1, MEASURE5, MEMBERED;
schemes YELLOW_0, PBOOLE, YELLOW_3, FRAENKEL;
begin :: Posets of Real Numbers
definition
let R be RelStr;
attr R is real means
: Def1:
the carrier of R c= REAL & for x,y being Real
st x in the carrier of R & y in the carrier of R holds [x,y] in the
InternalRel of R iff x <= y;
end;
definition
let R be RelStr;
attr R is interval means
: Def2:
R is real & ex a,b being Real st a <= b & the carrier of R = [.a,b.];
end;
registration
cluster interval -> real non empty for RelStr;
coherence
by XXREAL_1:1;
end;
registration
cluster empty -> real for RelStr;
coherence
proof
let R being RelStr;
assume
A1: the carrier of R is empty;
hence the carrier of R c= REAL;
thus thesis by A1;
end;
end;
theorem Th1:
for X being real-membered set ex R being strict RelStr st the
carrier of R = X & R is real
proof
let X be real-membered set;
per cases;
suppose
A1: X is empty;
set E = the empty strict RelStr;
take E;
thus thesis by A1;
end;
suppose
X is non empty;
then reconsider Y = X as non empty set;
defpred X[set,set] means ex x,y being Real st $1=x & $2=y & x<=y;
consider L being non empty strict RelStr such that
A2: the carrier of L = Y and
A3: for a,b being Element of L holds a <= b iff X[a,b] from YELLOW_0:
sch 1;
take L;
thus the carrier of L = X by A2;
thus the carrier of L c= REAL by A2,MEMBERED:3;
let x,y be Real;
assume x in the carrier of L & y in the carrier of L;
then reconsider a = x, b = y as Element of L;
a <= b iff [x,y] in the InternalRel of L by ORDERS_2:def 5;
then
[x,y] in the InternalRel of L iff ex x,y being Real st a=x & b=
y & x<=y by A3;
hence thesis;
end;
end;
registration
cluster interval strict for RelStr;
existence
proof
set X = [. 0,1 qua Real .];
consider R being strict RelStr such that
A1: the carrier of R = X & R is real by Th1;
take R;
thus thesis by A1;
end;
end;
theorem Th2:
for R1,R2 being real RelStr st the carrier of R1 = the carrier of
R2 holds the RelStr of R1 = the RelStr of R2
proof
let R1, R2 be real RelStr such that
A1: the carrier of R1 = the carrier of R2;
set X = the carrier of R1;
the InternalRel of R1 = the InternalRel of R2
proof
let a,b be object;
A2: X c= REAL by Def1;
hereby
assume
A3: [a,b] in the InternalRel of R1;
then
A4: a in X & b in X by ZFMISC_1:87;
then reconsider a9 = a, b9 = b as Element of REAL by A2;
a9 <= b9 by A3,A4,Def1;
hence [a,b] in the InternalRel of R2 by A1,A4,Def1;
end;
assume
A5: [a,b] in the InternalRel of R2;
then
A6: a in X & b in X by A1,ZFMISC_1:87;
then reconsider a9 = a, b9 = b as Element of REAL by A2;
a9 <= b9 by A1,A5,A6,Def1;
hence thesis by A6,Def1;
end;
hence thesis by A1;
end;
registration
let R be non empty real RelStr;
cluster -> real for Element of R;
coherence
proof
let x be Element of R;
the carrier of R c= REAL by Def1;
hence thesis;
end;
end;
definition
let X be real-membered set;
func RealPoset X -> real strict RelStr means
: Def3:
the carrier of it = X;
existence
proof
ex R being strict RelStr st the carrier of R = X & R is real by Th1;
hence thesis;
end;
uniqueness by Th2;
end;
registration
let X be non empty real-membered set;
cluster RealPoset X -> non empty;
coherence by Def3;
end;
notation
let R be RelStr;
let x,y be Element of R;
synonym x <<= y for x <= y;
synonym y >>= x for x <= y;
antonym x ~<= y for x <= y;
antonym y ~>= x for x <= y;
end;
theorem Th3:
for R being non empty real RelStr for x,y being Element of R
holds x <= y iff x <<= y
proof
let R be non empty real RelStr;
let x,y be Element of R;
[x,y] in the InternalRel of R iff x <= y by Def1;
hence thesis by ORDERS_2:def 5;
end;
registration
cluster real -> reflexive antisymmetric transitive for RelStr;
coherence
proof
let R be RelStr such that
A1: R is real;
per cases;
suppose
R is empty;
hence thesis;
end;
suppose
R is non empty;
then reconsider R9 = R as non empty real RelStr by A1;
A2: R9 is antisymmetric
proof
let x,y be Element of R9;
assume x <<= y & x >>= y;
then x <= y & x >= y by Th3;
hence thesis by XXREAL_0:1;
end;
A3: R9 is transitive
proof
let x,y,z be Element of R9;
assume x <<= y & y <<= z;
then x <= y & y <= z by Th3;
then x <= z by XXREAL_0:2;
hence thesis by Th3;
end;
R9 is reflexive
by Th3;
hence thesis by A2,A3;
end;
end;
end;
registration
cluster -> connected for real non empty RelStr;
coherence
proof
let R be non empty real RelStr;
let x,y be Element of R;
x <= y or x >= y;
hence thesis by Th3;
end;
end;
definition
let R be non empty real RelStr;
let x,y be Element of R;
redefine func max(x,y) -> Element of R; :: redefines max (XXREAL_0, definition)
coherence by XXREAL_0:16;
end;
definition
let R be non empty real RelStr;
let x,y be Element of R;
redefine func min(x,y) -> Element of R; :: redefines min (XXREAL_0, definition)
coherence by XXREAL_0:15;
end;
registration
cluster -> with_suprema with_infima for real non empty RelStr;
coherence;
end;
reserve x,y,z for Real,
R for real non empty RelStr,
a,b for Element of R;
registration
let R;
let a,b be Element of R;
identify a"\/"b with max(a,b);
compatibility
proof
A1: for d being Element of R st d >>= a & d >>= b holds max(a,b) <<= d
proof
let d be Element of R;
assume d >>= a & d >>= b;
then d >= a & d >= b by Th3;
then max(a,b) <= d by XXREAL_0:28;
hence thesis by Th3;
end;
max(a,b) >= b by XXREAL_0:25;
then
A2: max(a,b) >>= b by Th3;
max(a,b) >= a by XXREAL_0:25;
then max(a,b) >>= a by Th3;
hence thesis by A2,A1,YELLOW_0:22;
end;
identify a"/\"b with min(a,b);
compatibility
proof
A3: for d being Element of R st d <<= a & d <<= b holds min(a,b) >>= d
proof
let d being Element of R;
assume d <<= a & d <<= b;
then d <= a & d <= b by Th3;
then d <= min(a,b) by XXREAL_0:20;
hence thesis by Th3;
end;
min(a,b) <= b by XXREAL_0:17;
then
A4: min(a,b) <<= b by Th3;
min(a,b) <= a by XXREAL_0:17;
then min(a,b) <<= a by Th3;
hence thesis by A4,A3,YELLOW_0:23;
end;
end;
theorem
a"\/"b = max(a,b);
theorem
a"/\"b = min(a,b);
theorem Th6:
(ex x st x in the carrier of R & for y st y in the carrier of R
holds x <= y) iff R is lower-bounded
proof
hereby
given x such that
A1: x in the carrier of R and
A2: for y st y in the carrier of R holds x <= y;
reconsider a = x as Element of R by A1;
for b st b in the carrier of R holds a <<= b by A2,Th3;
then a is_<=_than the carrier of R;
hence R is lower-bounded;
end;
given x being Element of R such that
A3: x is_<=_than the carrier of R;
take x;
thus x in the carrier of R;
let y;
assume y in the carrier of R;
then reconsider b = y as Element of R;
x <<= b by A3;
hence thesis by Th3;
end;
theorem Th7:
(ex x st x in the carrier of R & for y st y in the carrier of R
holds x >= y) iff R is upper-bounded
proof
hereby
given x such that
A1: x in the carrier of R and
A2: for y st y in the carrier of R holds x >= y;
reconsider a = x as Element of R by A1;
for b st b in the carrier of R holds a >>= b by A2,Th3;
then a is_>=_than the carrier of R;
hence R is upper-bounded;
end;
given x being Element of R such that
A3: x is_>=_than the carrier of R;
take x;
thus x in the carrier of R;
let y;
assume y in the carrier of R;
then reconsider b = y as Element of R;
x >>= b by A3;
hence thesis by Th3;
end;
registration
cluster interval -> bounded for non empty RelStr;
coherence
proof
let R being non empty RelStr;
assume
A1: R is real;
given x,y being Real such that
A2: x <= y and
A3: the carrier of R = [.x,y.];
ex x st x in the carrier of R & for y st y in the carrier of R holds x <= y
proof
take x;
thus x in the carrier of R by A2,A3,XXREAL_1:1;
let z;
assume z in the carrier of R;
hence thesis by A3,XXREAL_1:1;
end;
then
A4: R is lower-bounded by A1,Th6;
ex x st x in the carrier of R & for y st y in the carrier of R holds x >= y
proof
take y;
thus y in the carrier of R by A2,A3,XXREAL_1:1;
let z;
assume z in the carrier of R;
hence thesis by A3,XXREAL_1:1;
end;
then R is upper-bounded by A1,Th7;
hence thesis by A4;
end;
end;
theorem Th8:
for R being interval non empty RelStr, X being set holds ex_sup_of X,R
proof
let R being interval non empty RelStr;
let X being set;
consider a,b being Real such that
A1: a <= b and
A2: the carrier of R = [.a,b.] by Def2;
reconsider a,b as Real;
reconsider Y = X /\ [.a,b.] as Subset of REAL;
[.a,b.] is non empty closed_interval by A1,MEASURE5:14;
then
A3: [.a,b.] is bounded_above by INTEGRA1:3;
then
A4: Y is bounded_above by XBOOLE_1:17,XXREAL_2:43;
A5: X /\ [.a,b.] c= [.a,b.] by XBOOLE_1:17;
ex a being Element of R st Y is_<=_than a & for b being Element of R st
Y is_<=_than b holds a <<= b
proof
per cases;
suppose
A6: Y is empty;
reconsider x = a as Element of R by A1,A2,XXREAL_1:1;
take x;
thus Y is_<=_than x by A6;
let y be Element of R;
x <= y by A2,XXREAL_1:1;
hence thesis by Th3;
end;
suppose
A7: Y is non empty;
set c = the Element of Y;
A8: c in Y by A7;
reconsider c as Real;
A9: a<=c by A5,A8,XXREAL_1:1;
c <= upper_bound Y by A4,A7,SEQ_4:def 1;
then
A10: a <= upper_bound Y by A9,XXREAL_0:2;
upper_bound [.a,b.] = b by A1,JORDAN5A:19;
then upper_bound Y <= b by A3,A7,SEQ_4:48,XBOOLE_1:17;
then reconsider x = upper_bound Y as Element of R by A2,A10,XXREAL_1:1;
A11: for y being Element of R st Y is_<=_than y holds x <<= y
proof
let y be Element of R;
assume
A12: Y is_<=_than y;
for z being Real st z in Y holds z <= y
proof
let z being Real;
assume
A13: z in Y;
then reconsider z as Element of R by A2,XBOOLE_0:def 4;
z <<= y by A12,A13;
hence thesis by Th3;
end;
then upper_bound Y <= y by A7,SEQ_4:144;
hence thesis by Th3;
end;
take x;
for b being Element of R st b in Y holds b <<= x
proof
let b be Element of R;
assume b in Y;
then b <= upper_bound Y by A4,SEQ_4:def 1;
hence thesis by Th3;
end;
hence thesis by A11;
end;
end;
then ex_sup_of Y,R by YELLOW_0:15;
hence thesis by A2,YELLOW_0:50;
end;
registration
cluster -> complete for interval non empty RelStr;
coherence
proof
let R be interval non empty RelStr;
for X being Subset of R holds ex_sup_of X,R by Th8;
hence thesis by YELLOW_0:53;
end;
end;
registration
cluster -> distributive for Chain;
coherence
proof
let C be Chain;
for x,y,z being Element of C holds x "/\" (y "\/" z) = (x "/\" y) "\/"
(x "/\" z)
proof
let x,y,z be Element of C;
A1: x <= x;
per cases by WAYBEL_0:def 29;
suppose
A2: x <= y & x <= z & y <= z;
then
A3: x "/\" (y "\/" z) = x "/\" z by YELLOW_0:24
.= x by A2,YELLOW_0:25;
(x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A2,YELLOW_0:25
.= x "\/" x by A2,YELLOW_0:25
.= x by A1,YELLOW_0:24;
hence thesis by A3;
end;
suppose
A4: x <= y & x <= z & y >= z;
then
A5: x "/\" (y "\/" z) = x "/\" y by YELLOW_0:24
.= x by A4,YELLOW_0:25;
(x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A4,YELLOW_0:25
.= x "\/" x by A4,YELLOW_0:25
.= x by A1,YELLOW_0:24;
hence thesis by A5;
end;
suppose
A6: x <= y & x >= z & y <= z;
then z <= y by YELLOW_0:def 2;
then
A7: z = y by A6,YELLOW_0:def 3;
A8: x "/\" (y "\/" z) = x "/\" z by A6,YELLOW_0:24
.= z by A6,YELLOW_0:25;
(x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A6,YELLOW_0:25
.= x "\/" z by A6,YELLOW_0:25
.= x by A6,YELLOW_0:24;
hence thesis by A6,A7,A8,YELLOW_0:def 3;
end;
suppose
A9: x <= y & x >= z & y >= z;
then
A10: x "/\" (y "\/" z) = x "/\" y by YELLOW_0:24
.= x by A9,YELLOW_0:25;
(x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A9,YELLOW_0:25
.= x "\/" z by A9,YELLOW_0:25
.= x by A9,YELLOW_0:24;
hence thesis by A10;
end;
suppose
A11: x >= y & x <= z & y <= z;
then
A12: x "/\" (y "\/" z) = x "/\" z by YELLOW_0:24
.= x by A11,YELLOW_0:25;
(x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A11,YELLOW_0:25
.= y "\/" x by A11,YELLOW_0:25
.= x by A11,YELLOW_0:24;
hence thesis by A12;
end;
suppose
A13: x >= y & x <= z & y >= z;
then z >= y by YELLOW_0:def 2;
then
A14: z = y by A13,YELLOW_0:def 3;
A15: x "/\" (y "\/" z) = x "/\" y by A13,YELLOW_0:24
.= y by A13,YELLOW_0:25;
(x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A13,YELLOW_0:25
.= y "\/" x by A13,YELLOW_0:25
.= x by A13,YELLOW_0:24;
hence thesis by A13,A14,A15,YELLOW_0:def 3;
end;
suppose
A16: x >= y & x >= z & y <= z;
then
A17: x "/\" (y "\/" z) = x "/\" z by YELLOW_0:24
.= z by A16,YELLOW_0:25;
(x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A16,YELLOW_0:25
.= y "\/" z by A16,YELLOW_0:25
.= z by A16,YELLOW_0:24;
hence thesis by A17;
end;
suppose
A18: x >= y & x >= z & y >= z;
then
A19: x "/\" (y "\/" z) = x "/\" y by YELLOW_0:24
.= y by A18,YELLOW_0:25;
(x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A18,YELLOW_0:25
.= y "\/" z by A18,YELLOW_0:25
.= y by A18,YELLOW_0:24;
hence thesis by A19;
end;
end;
hence thesis;
end;
end;
registration
cluster -> Heyting for interval non empty RelStr;
coherence
proof
let R be interval non empty RelStr;
thus R is LATTICE;
let x be Element of R;
set f = x "/\";
f is sups-preserving
proof
let X be Subset of R;
assume ex_sup_of X,R;
A1: now
let b being Element of R such that
A2: b is_>=_than f.:X;
per cases;
suppose
A3: x is_>=_than X;
b is_>=_than X
proof
let a be Element of R;
assume
A4: a in X;
then x >>= a by A3;
then x "/\" a = a by YELLOW_0:25;
then
A5: a = f.a by WAYBEL_1:def 18;
f.a in f.:X by A4,FUNCT_2:35;
hence thesis by A2,A5;
end;
then
A6: b >>= sup X by YELLOW_0:32;
x >>= sup X by A3,YELLOW_0:32;
then x "/\" sup X = sup X by YELLOW_0:25;
hence f.sup X <<= b by A6,WAYBEL_1:def 18;
end;
suppose
not x is_>=_than X;
then consider a being Element of R such that
A7: a in X and
A8: not x >>= a;
A9: x <<= a by A8,WAYBEL_0:def 29;
a <<= sup X by A7,YELLOW_2:22;
then x <<= sup X by A9,ORDERS_2:3;
then x = x "/\"sup X by YELLOW_0:25;
then
A10: x = f.sup X by WAYBEL_1:def 18;
A11: f.a in f.:X by A7,FUNCT_2:35;
x = x "/\" a by A9,YELLOW_0:25
.= f.a by WAYBEL_1:def 18;
hence f.sup X <<= b by A2,A10,A11;
end;
end;
thus ex_sup_of f.:X,R by Th8;
f.sup X is_>=_than f.:X
proof
let a be Element of R;
A12: f.sup X = x "/\" sup X & x <<= x by WAYBEL_1:def 18,YELLOW_0:def 1;
assume a in f.:X;
then consider y being object such that
A13: y in the carrier of R and
A14: y in X & a = f.y by FUNCT_2:64;
reconsider y as Element of R by A13;
y <<= sup X & a = x "/\" y by A14,WAYBEL_1:def 18,YELLOW_2:22;
hence thesis by A12,YELLOW_3:2;
end;
hence thesis by A1,YELLOW_0:30;
end;
hence thesis by WAYBEL_1:17;
end;
end;
registration
cluster [.0,1 .] -> non empty;
coherence
by MEASURE5:14;
end;
registration
cluster RealPoset [.0,1 .] -> interval;
coherence
by Def3;
end;
begin :: Product of Heyting Lattices
theorem Th9:
for I being non empty set for J being RelStr-yielding non-Empty
reflexive-yielding ManySortedSet of I st for i being Element of I holds J.i is
sup-Semilattice holds product J is with_suprema
proof
let I being non empty set;
let J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
such that
A1: for i being Element of I holds J.i is sup-Semilattice;
set IT = product J;
for x,y being Element of IT ex z being Element of IT st x <= z & y <= z
& for z9 being Element of IT st x <= z9 & y <= z9 holds z <= z9
proof
let x,y being Element of IT;
deffunc U(Element of I) = x.$1 "\/" y.$1;
consider z be ManySortedSet of I such that
A2: for i be Element of I holds z.i = U(i) from PBOOLE:sch 5;
A3: for i being Element of I holds z.i is Element of J.i
proof
let i being Element of I;
z.i = x.i "\/" y.i by A2;
hence thesis;
end;
dom z = I by PARTFUN1:def 2;
then reconsider z as Element of product J by A3,WAYBEL_3:27;
take z;
for i being Element of I holds x.i <= z.i & y.i <= z.i
proof
let i being Element of I;
J.i is antisymmetric with_suprema RelStr & z.i = x.i "\/" y.i by A1,A2;
hence thesis by YELLOW_0:22;
end;
hence x <= z & y <= z by WAYBEL_3:28;
let z9 be Element of IT;
assume that
A4: x <= z9 and
A5: y <= z9;
for i being Element of I holds z.i <= z9.i
proof
let i being Element of I;
A6: z9.i >= y.i & z.i = x.i "\/" y.i by A2,A5,WAYBEL_3:28;
J.i is antisymmetric with_suprema RelStr & z9.i >= x.i by A1,A4,
WAYBEL_3:28;
hence thesis by A6,YELLOW_0:22;
end;
hence thesis by WAYBEL_3:28;
end;
hence thesis;
end;
theorem Th10:
for I being non empty set for J being RelStr-yielding non-Empty
reflexive-yielding ManySortedSet of I st for i being Element of I holds J.i is
Semilattice holds product J is with_infima
proof
let I being non empty set;
let J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
such that
A1: for i being Element of I holds J.i is Semilattice;
set IT = product J;
for x,y being Element of IT ex z being Element of IT st x >= z & y >= z
& for z9 being Element of IT st x >= z9 & y >= z9 holds z >= z9
proof
let x,y being Element of IT;
deffunc U(Element of I) = x.$1 "/\" y.$1;
consider z be ManySortedSet of I such that
A2: for i be Element of I holds z.i = U(i) from PBOOLE:sch 5;
A3: for i being Element of I holds z.i is Element of J.i
proof
let i being Element of I;
z.i = x.i "/\" y.i by A2;
hence thesis;
end;
dom z = I by PARTFUN1:def 2;
then reconsider z as Element of product J by A3,WAYBEL_3:27;
take z;
for i being Element of I holds x.i >= z.i & y.i >= z.i
proof
let i being Element of I;
J.i is antisymmetric with_infima RelStr & z.i = x.i "/\" y.i by A1,A2;
hence thesis by YELLOW_0:23;
end;
hence x >= z & y >= z by WAYBEL_3:28;
let z9 be Element of IT;
assume that
A4: x >= z9 and
A5: y >= z9;
for i being Element of I holds z.i >= z9.i
proof
let i being Element of I;
A6: z9.i <= y.i & z.i = x.i "/\" y.i by A2,A5,WAYBEL_3:28;
J.i is antisymmetric with_infima RelStr & x.i >= z9.i by A1,A4,
WAYBEL_3:28;
hence thesis by A6,YELLOW_0:23;
end;
hence thesis by WAYBEL_3:28;
end;
hence thesis;
end;
theorem Th11:
for I being non empty set for J being RelStr-yielding non-Empty
reflexive-yielding ManySortedSet of I st for i being Element of I holds J.i is
Semilattice for f,g being Element of product J, i being Element of I holds (f
"/\" g).i = (f.i) "/\" (g.i)
proof
let I being non empty set;
let J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
such that
A1: for i being Element of I holds J.i is Semilattice;
let f,g being Element of product J;
let i being Element of I;
A2: J.i is Semilattice by A1;
for i being Element of I holds J.i is antisymmetric by A1;
then
A3: product J is antisymmetric with_infima by A1,Th10,WAYBEL_3:30;
then g >= f "/\" g by YELLOW_0:23;
then
A4: g.i >= (f "/\" g).i by WAYBEL_3:28;
A5: (f "/\" g).i >= (f.i) "/\" (g.i)
proof
deffunc U(Element of I) = f.$1 "/\" g.$1;
consider z be ManySortedSet of I such that
A6: for i be Element of I holds z.i = U(i) from PBOOLE:sch 5;
A7: for i being Element of I holds z.i is Element of J.i
proof
let i being Element of I;
z.i = f.i "/\" g.i by A6;
hence thesis;
end;
dom z = I by PARTFUN1:def 2;
then reconsider z as Element of product J by A7,WAYBEL_3:27;
for i being Element of I holds z.i <= f.i & z.i <= g.i
proof
let i being Element of I;
J.i is antisymmetric with_infima RelStr & z.i = f.i "/\" g.i by A1,A6;
hence thesis by YELLOW_0:23;
end;
then z <= f & z <= g by WAYBEL_3:28;
then
A8: f "/\" g >= z by A3,YELLOW_0:23;
for i being Element of I holds (f "/\" g).i >= f.i "/\" g.i
proof
let i being Element of I;
f.i "/\" g.i = z.i by A6;
hence thesis by A8,WAYBEL_3:28;
end;
hence thesis;
end;
f >= f "/\" g by A3,YELLOW_0:23;
then f.i >= (f "/\" g).i by WAYBEL_3:28;
then (f "/\" g).i <= (f.i) "/\" (g.i) by A2,A4,YELLOW_0:23;
hence thesis by A2,A5,YELLOW_0:def 3;
end;
theorem Th12:
for I being non empty set for J being RelStr-yielding non-Empty
reflexive-yielding ManySortedSet of I st for i being Element of I holds J.i is
sup-Semilattice for f,g being Element of product J, i being Element of I holds
(f "\/" g).i = (f.i) "\/" (g.i)
proof
let I being non empty set;
let J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
such that
A1: for i being Element of I holds J.i is sup-Semilattice;
let f,g being Element of product J;
let i being Element of I;
A2: J.i is sup-Semilattice by A1;
for i being Element of I holds J.i is antisymmetric by A1;
then
A3: product J is antisymmetric with_suprema by A1,Th9,WAYBEL_3:30;
then g <= f "\/" g by YELLOW_0:22;
then
A4: g.i <= (f "\/" g).i by WAYBEL_3:28;
A5: (f "\/" g).i <= (f.i) "\/" (g.i)
proof
deffunc U(Element of I) = f.$1 "\/" g.$1;
consider z be ManySortedSet of I such that
A6: for i be Element of I holds z.i = U(i) from PBOOLE:sch 5;
A7: for i being Element of I holds z.i is Element of J.i
proof
let i being Element of I;
z.i = f.i "\/" g.i by A6;
hence thesis;
end;
dom z = I by PARTFUN1:def 2;
then reconsider z as Element of product J by A7,WAYBEL_3:27;
for i being Element of I holds z.i >= f.i & z.i >= g.i
proof
let i being Element of I;
J.i is antisymmetric with_suprema RelStr & z.i = f.i "\/" g.i by A1,A6;
hence thesis by YELLOW_0:22;
end;
then z >= f & z >= g by WAYBEL_3:28;
then
A8: f "\/" g <= z by A3,YELLOW_0:22;
for i being Element of I holds (f "\/" g).i <= f.i "\/" g.i
proof
let i being Element of I;
f.i "\/" g.i = z.i by A6;
hence thesis by A8,WAYBEL_3:28;
end;
hence thesis;
end;
f <= f "\/" g by A3,YELLOW_0:22;
then f.i <= (f "\/" g).i by WAYBEL_3:28;
then (f "\/" g).i >= (f.i) "\/" (g.i) by A2,A4,YELLOW_0:22;
hence thesis by A2,A5,YELLOW_0:def 3;
end;
theorem Th13:
for I being non empty set for J being RelStr-yielding non-Empty
reflexive-yielding ManySortedSet of I st for i being Element of I holds J.i is
Heyting complete LATTICE holds product J is complete Heyting
proof
let I be non empty set;
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
such that
A1: for i being Element of I holds J.i is Heyting complete LATTICE;
A2: for i being Element of I holds J.i is complete LATTICE by A1;
set H = product J;
reconsider H as complete LATTICE by A2,WAYBEL_3:31;
H = H;
hence product J is complete & product J is LATTICE;
let f be Element of product J;
reconsider g = f as Element of H;
reconsider F = f "/\" as Function of H,H;
A3: for i being Element of I holds J.i is Semilattice by A1;
F is sups-preserving
proof
let X be Subset of H;
reconsider Y = F.:X, X9 = X as Subset of product J;
reconsider sX = sup X as Element of product J;
assume ex_sup_of X, H;
thus ex_sup_of F.:X, H by YELLOW_0:17;
reconsider f1 = sup (F.:X), f2 = F.sup X as Element of product J;
A4: now
let x be object;
assume x in dom f1;
then reconsider i = x as Element of I by WAYBEL_3:27;
A5: J.i is complete Heyting LATTICE by A1;
then
A6: ex_sup_of pi(X9,i), J.i by YELLOW_0:17;
A7: ((f.i) "/\").:pi(X9,i) c= pi(Y,i)
proof
let b be object;
assume b in ((f.i) "/\").:pi(X9,i);
then consider f4 being object such that
f4 in dom ((f.i) "/\") and
A8: f4 in pi(X9,i) and
A9: b = ((f.i) "/\").f4 by FUNCT_1:def 6;
consider f5 being Function such that
A10: f5 in X9 and
A11: f4 = f5.i by A8,CARD_3:def 6;
reconsider f5 as Element of product J by A10;
(f "/\" f5) = f "/\". f5 by WAYBEL_1:def 18;
then
A12: (f "/\" f5) in f"/\" .: X by A10,FUNCT_2:35;
((f.i) "/\").f4 = (f.i) "/\" (f5.i) by A11,WAYBEL_1:def 18
.= (f "/\" f5).i by A3,Th11;
hence thesis by A9,A12,CARD_3:def 6;
end;
pi(Y,i) c= ((f.i) "/\").:pi(X9,i)
proof
let a be object;
assume a in pi(Y,i);
then consider f3 being Function such that
A13: f3 in Y and
A14: a = f3.i by CARD_3:def 6;
reconsider f3 as Element of product J by A13;
consider h being object such that
A15: h in dom F and
A16: h in X and
A17: f3=F.h by A13,FUNCT_1:def 6;
reconsider h as Element of product J by A15;
A18: (h.i) in pi(X9,i) by A16,CARD_3:def 6;
f3.i = (f "/\" h).i by A17,WAYBEL_1:def 18
.= f.i "/\" h.i by A3,Th11
.= (f.i "/\").(h.i) by WAYBEL_1:def 18;
hence thesis by A14,A18,FUNCT_2:35;
end;
then
A19: pi(Y,i) = ((f.i) "/\").:pi(X9,i) by A7;
(f.i) "/\" is lower_adjoint by A5,WAYBEL_1:def 19;
then
A20: (f.i) "/\" preserves_sup_of pi(X9,i) by A5,WAYBEL_0:def 33;
f2 = g "/\" sup X by WAYBEL_1:def 18;
then f2.i = (f.i) "/\" (sX.i) by A3,Th11
.= (f.i) "/\" sup pi(X9, i) by A2,WAYBEL_3:32
.= ((f.i) "/\").sup pi(X9,i) by WAYBEL_1:def 18
.= sup (((f.i) "/\").:pi(X9,i)) by A20,A6;
hence f1.x = f2.x by A2,A19,WAYBEL_3:32;
end;
dom f1 = I & dom f2 = I by WAYBEL_3:27;
hence thesis by A4,FUNCT_1:2;
end;
hence thesis by WAYBEL_1:17;
end;
registration
let A be non empty set;
let R be complete Heyting LATTICE;
cluster R |^ A -> Heyting;
coherence
proof
for i being Element of A holds (A --> R).i is complete Heyting LATTICE;
then product (A --> R) is complete Heyting by Th13;
hence thesis by YELLOW_1:def 5;
end;
end;
begin :: Lattice of Fuzzy Sets
definition
let A be non empty set;
func FuzzyLattice A -> Heyting complete LATTICE equals
(RealPoset [. 0,1 .])
|^ A;
coherence;
end;
theorem Th14:
for A being non empty set holds the carrier of FuzzyLattice A =
Funcs(A, [. 0, 1 .])
proof
let A be non empty set;
thus the carrier of FuzzyLattice A = Funcs (A, the carrier of RealPoset [. 0
,1 .]) by YELLOW_1:28
.= Funcs (A, [. 0,1 .]) by Def3;
end;
Lm1: for A being non empty set holds FuzzyLattice A is constituted-Functions
proof
let A be non empty set;
for a being Element of FuzzyLattice A holds a is Function
proof
let a be Element of FuzzyLattice A;
a in the carrier of FuzzyLattice A;
then a in Funcs(A, [. 0, 1 .]) by Th14;
then ex f being Function st a = f & dom f = A & rng f c= [. 0, 1 .] by
FUNCT_2:def 2;
hence thesis;
end;
hence thesis by MONOID_0:def 1;
end;
registration
let A be non empty set;
cluster FuzzyLattice A -> constituted-Functions;
coherence by Lm1;
end;
theorem Th15:
for R being complete Heyting LATTICE, X being Subset of R, y be
Element of R holds "\/"(X,R) "/\" y = "\/"({x "/\" y where x is Element of R: x
in X},R)
proof
let R be complete Heyting LATTICE, X be Subset of R, y be Element of R;
set Z = {y "/\" x where x is Element of R: x in X}, W = {x "/\" y where x is
Element of R: x in X};
A1: W c= Z
proof
let w be object;
assume w in W;
then ex x being Element of R st w = x "/\" y & x in X;
hence thesis;
end;
Z c= W
proof
let z be object;
assume z in Z;
then ex x being Element of R st z = y "/\" x & x in X;
hence thesis;
end;
then
( for z being Element of R holds z "/\" is lower_adjoint & ex_sup_of X,R
)& Z = W by A1,WAYBEL_1:def 19,YELLOW_0:17;
hence thesis by WAYBEL_1:63;
end;
Lm2: for X being non empty set for a being Element of FuzzyLattice X holds a
is Membership_Func of X
proof
let X be non empty set;
let a be Element of FuzzyLattice X;
a in the carrier of FuzzyLattice X;
then a in Funcs(X, [. 0,1 .]) by Th14;
then
A1: ex f being Function st a = f & dom f = X & rng f c= [. 0 ,1 .] by
FUNCT_2:def 2;
then reconsider a as PartFunc of X, [. 0,1 .] by RELSET_1:4;
reconsider a as PartFunc of X, REAL by RELSET_1:7;
a is Function of X,REAL by A1,FUNCT_2:def 1;
hence thesis;
end;
definition
let X be non empty set;
let a be Element of FuzzyLattice X;
func @a -> Membership_Func of X equals
a;
coherence by Lm2;
end;
Lm3: for X be non empty set for f be Membership_Func of X holds f is Element
of FuzzyLattice X
proof
let X be non empty set;
let f be Membership_Func of X;
dom f = X & rng f c= [. 0,1 .] by FUNCT_2:def 1,RELAT_1:def 19;
then f in Funcs(X, [. 0,1 .]) by FUNCT_2:def 2;
hence thesis by Th14;
end;
definition
let X be non empty set;
let f be Membership_Func of X;
func (X,f)@ -> Element of FuzzyLattice X equals
f;
coherence by Lm3;
end;
definition
let X be non empty set;
let f be Membership_Func of X;
let x be Element of X;
redefine func f.x -> Element of RealPoset [. 0,1 .]; :: redefines . (FUNCT_1, definition)
coherence
proof
0 <= f.x & f.x <= 1 by FUZZY_2:1;
then f.x in [. 0,1 .] by XXREAL_1:1;
hence thesis by Def3;
end;
end;
definition
let X,Y be non empty set;
let f be RMembership_Func of X,Y;
let x be Element of X, y be Element of Y;
redefine func f.(x,y) -> Element of RealPoset [. 0,1 .]; :: redefines . (BINOP_1, definition)
coherence
proof
f. [x,y] is Element of RealPoset [. 0,1 .];
hence thesis;
end;
end;
definition
let X be non empty set;
let f be Element of FuzzyLattice X;
let x be Element of X;
redefine func f.x -> Element of RealPoset [. 0,1 .]; :: redefines . (FUNCT_1, definition)
coherence
proof
0 <= @f.x by FUZZY_2:1;
hence thesis;
end;
end;
reserve C for non empty set,
c for Element of C,
f,g for Membership_Func of C,
s,t for Element of FuzzyLattice C;
theorem Th16:
(for c holds f.c <= g.c) iff (C,f)@ <<= (C,g)@
proof
A1: (RealPoset [. 0,1 .]) |^ C = product (C --> RealPoset [. 0,1 .]) by
YELLOW_1:def 5;
A2: (for c holds f.c <= g.c) implies (C,f)@ <<= (C,g)@
proof
set f9 = (C,f)@, g9 = (C,g)@;
reconsider f9,g9 as Element of product (C --> RealPoset [. 0,1 .]) by
YELLOW_1:def 5;
assume
A3: for c holds f.c <= g.c;
for c holds f9.c <<= g9.c by A3,Th3;
hence thesis by A1,WAYBEL_3:28;
end;
(C,f)@ <<= (C,g)@ implies for c holds f.c <= g.c
proof
reconsider ff = (C,f)@, gg = (C,g)@ as Element of product (C --> RealPoset
[. 0,1 .]) by YELLOW_1:def 5;
assume
A4: (C,f)@ <<= (C,g)@;
let c;
(C --> RealPoset [. 0,1 .]).c = RealPoset [. 0,1 .] & ff.c <<= gg.c by A1
,A4,WAYBEL_3:28;
hence thesis by Th3;
end;
hence thesis by A2;
end;
theorem
s <<= t iff for c holds @s.c <= @t.c
proof
(C,@s)@ = s & (C,@t)@ = t;
hence thesis by Th16;
end;
theorem Th18:
max(f,g) = (C,f)@ "\/" (C,g)@
proof
set fg = (C,f)@ "\/" (C,g)@, R = RealPoset [. 0,1 .], J = C --> R;
A1: (RealPoset [. 0,1 .]) |^ C = product (C --> RealPoset [. 0,1 .]) by
YELLOW_1:def 5;
now
let c;
( for c being Element of C holds J.c is sup-Semilattice)& J.c =
RealPoset [. 0 ,1 .];
hence (@fg).c = ((C,f)@.c) "\/" ((C,g)@.c) by A1,Th12
.= max(f.c, g.c);
end;
hence thesis by FUZZY_1:def 4;
end;
theorem
s "\/" t = max(@s, @t)
proof
(C,@s)@ = s & (C,@t)@ = t;
hence thesis by Th18;
end;
theorem Th20:
min(f,g) = (C,f)@ "/\" (C,g)@
proof
set fg = (C,f)@ "/\" (C,g)@, R = RealPoset [. 0,1 .], J = C --> R;
A1: (RealPoset [. 0,1 .]) |^ C = product (C --> RealPoset [. 0,1 .]) by
YELLOW_1:def 5;
now
let c;
( for c being Element of C holds J.c is Semilattice)& J.c = RealPoset
[. 0,1 .];
hence (@fg).c = ((C,f)@.c) "/\" ((C,g)@.c) by A1,Th11
.= min(f.c, g.c);
end;
hence thesis by FUZZY_1:def 3;
end;
theorem
s "/\" t = min(@s, @t)
proof
(C,@s)@ = s & (C,@t)@ = t;
hence thesis by Th20;
end;
begin :: Associativity of composition of fuzzy relations
scheme
SupDistributivity { L() -> complete LATTICE, X, Y() -> non empty set, F(set,
set) -> Element of L(), P,Q[set]}: "\/"({ "\/"({F(x,y) where y is Element of Y(
): Q[y]}, L()) where x is Element of X(): P[x] }, L()) = "\/"({F(x,y) where x
is Element of X(), y is Element of Y(): P[x] & Q[y]}, L()) proof
defpred R[set] means ex x being Element of X() st P[x] & for a being set
holds a in $1 iff ex y being Element of Y() st a = F(x,y) & Q[y];
A1: "\/" ({ "\/"(A,L()) where A is Subset of L(): R[A] },L()) = "\/" (union
{A where A is Subset of L(): R[A]}, L()) from YELLOW_3:sch 5;
A2: {F(x,y) where x is Element of X(), y is Element of Y(): P[x] & Q[y] }
c= union {A where A is Subset of L(): R[A]}
proof
let a be object;
assume a in {F(x,y) where x is Element of X(), y is Element of Y() : P[x
] & Q[y]};
then consider x being Element of X(), y being Element of Y() such that
A3: a = F(x,y) and
A4: P[x] and
A5: Q[y];
set A1 = {F(x,y9) where y9 is Element of Y(): Q[y9]};
A1 c= the carrier of L()
proof
let b be object;
assume b in A1;
then ex y9 being Element of Y() st b = F(x,y9) & Q[y9];
hence thesis;
end;
then reconsider A1 as Subset of L();
R[A1]
proof
take x;
thus P[x] by A4;
let a be set;
thus thesis;
end;
then
A6: A1 in {A where A is Subset of L(): R[A]};
a in A1 by A3,A5;
hence thesis by A6,TARSKI:def 4;
end;
A7: { "\/"({F(x,y) where y is Element of Y(): Q[y]}, L()) where x is
Element of X(): P[x] } c= { "\/"(A,L()) where A is Subset of L(): R[A] }
proof
let a be object;
assume a in { "\/"({F(x,y) where y is Element of Y(): Q[y]}, L()) where
x is Element of X(): P[x] };
then consider x being Element of X() such that
A8: a = "\/"({F(x,y) where y is Element of Y(): Q[y]}, L()) and
A9: P[x];
ex A1 being Subset of L() st a = "\/"(A1,L()) & R[A1]
proof
set A2 = {F(x,y) where y is Element of Y(): Q[y]};
A2 c= the carrier of L()
proof
let b be object;
assume b in A2;
then ex y being Element of Y() st b = F(x,y) & Q[y];
hence thesis;
end;
then reconsider A1 = A2 as Subset of L();
R[A1]
proof
take x;
thus P[x] by A9;
thus thesis;
end;
hence thesis by A8;
end;
hence thesis;
end;
A10: { "\/"(A,L()) where A is Subset of L(): R[A] } c= { "\/"({F(x,y) where
y is Element of Y(): Q[y]}, L()) where x is Element of X(): P[x] }
proof
let a be object;
assume a in { "\/"(A,L()) where A is Subset of L(): R[A] };
then consider A1 being Subset of L() such that
A11: a = "\/"(A1,L()) and
A12: R[A1];
consider x being Element of X() such that
A13: P[x] and
A14: for a being set holds a in A1 iff ex y being Element of Y() st a
= F(x,y) & Q[y] by A12;
now
let a be object;
a in {F(x,y) where y is Element of Y(): Q[y]} iff ex y being
Element of Y() st a = F(x,y) & Q[y];
hence a in A1 iff a in {F(x,y) where y is Element of Y(): Q[y]} by A14;
end;
then A1 = {F(x,y) where y is Element of Y(): Q[y]} by TARSKI:2;
hence thesis by A11,A13;
end;
union {A where A is Subset of L(): R[A]} c= {F(x,y) where x is Element
of X(), y is Element of Y(): P[x] & Q[y]}
proof
let a be object;
assume a in union {A where A is Subset of L(): R[A]};
then consider A1 be set such that
A15: a in A1 and
A16: A1 in {A where A is Subset of L(): R[A]} by TARSKI:def 4;
consider A2 being Subset of L() such that
A17: A1 = A2 and
A18: R[A2] by A16;
consider x being Element of X() such that
A19: P[x] and
A20: for a being set holds a in A2 iff ex y being Element of Y() st a =
F(x,y) & Q[y] by A18;
ex y being Element of Y() st a = F(x,y) & Q[y] by A15,A17,A20;
hence thesis by A19;
end;
then union {A where A is Subset of L(): R[A]} = {F(x,y) where x is Element
of X( ), y is Element of Y(): P[x] & Q[y]} by A2;
hence thesis by A1,A10,A7,XBOOLE_0:def 10;
end;
scheme
SupDistributivity9 { L() -> complete LATTICE, X, Y() -> non empty set, F(set
,set) -> Element of L(), P,Q[set]}: "\/"({ "\/"({F(x,y) where x is Element of X
(): P[x]},L()) where y is Element of Y(): Q[y] }, L()) = "\/"({F(x,y) where x
is Element of X(), y is Element of Y(): P[x] & Q[y]}, L()) proof
defpred R[set] means ex y being Element of Y() st Q[y] & for a being set
holds a in $1 iff ex x being Element of X() st a = F(x,y) & P[x];
A1: "\/" ({ "\/"(A,L()) where A is Subset of L(): R[A] },L()) = "\/" (union
{A where A is Subset of L(): R[A]}, L()) from YELLOW_3:sch 5;
A2: {F(x,y) where x is Element of X(), y is Element of Y(): P[x] & Q[y] }
c= union {A where A is Subset of L(): R[A]}
proof
let a be object;
assume a in {F(x,y) where x is Element of X(), y is Element of Y() : P[x
] & Q[y]};
then consider x being Element of X(), y being Element of Y() such that
A3: a = F(x,y) & P[x] and
A4: Q[y];
set A1 = {F(x9,y) where x9 is Element of X(): P[x9]};
A1 c= the carrier of L()
proof
let b be object;
assume b in A1;
then ex x9 being Element of X() st b = F(x9,y) & P[x9];
hence thesis;
end;
then reconsider A1 as Subset of L();
R[A1]
proof
take y;
thus Q[y] by A4;
let a be set;
thus thesis;
end;
then
A5: A1 in {A where A is Subset of L(): R[A]};
a in A1 by A3;
hence thesis by A5,TARSKI:def 4;
end;
A6: { "\/"({F(x,y) where x is Element of X(): P[x]}, L()) where y is
Element of Y(): Q[y] } c= { "\/"(A,L()) where A is Subset of L(): R[A] }
proof
let a be object;
assume a in { "\/"({F(x,y) where x is Element of X(): P[x]}, L()) where
y is Element of Y(): Q[y] };
then consider y being Element of Y() such that
A7: a = "\/"({F(x,y) where x is Element of X(): P[x]}, L()) and
A8: Q[y];
ex A1 being Subset of L() st a = "\/"(A1,L()) & R[A1]
proof
set A2 = {F(x,y) where x is Element of X(): P[x]};
A2 c= the carrier of L()
proof
let b be object;
assume b in A2;
then ex x being Element of X() st b = F(x,y) & P[x];
hence thesis;
end;
then reconsider A1 = A2 as Subset of L();
R[A1]
proof
take y;
thus Q[y] by A8;
thus thesis;
end;
hence thesis by A7;
end;
hence thesis;
end;
A9: { "\/"(A,L()) where A is Subset of L(): R[A] } c= { "\/"({F(x,y) where
x is Element of X(): P[x]}, L()) where y is Element of Y(): Q[y] }
proof
let a be object;
assume a in { "\/"(A,L()) where A is Subset of L(): R[A] };
then consider A1 being Subset of L() such that
A10: a = "\/"(A1,L()) and
A11: R[A1];
consider y being Element of Y() such that
A12: Q[y] and
A13: for a being set holds a in A1 iff ex x being Element of X() st a
= F(x,y) & P[x] by A11;
now
let a be object;
a in {F(x,y) where x is Element of X(): P[x]} iff ex x being
Element of X() st a = F(x,y) & P[x];
hence a in A1 iff a in {F(x,y) where x is Element of X(): P[x]} by A13;
end;
then A1 = {F(x,y) where x is Element of X(): P[x]} by TARSKI:2;
hence thesis by A10,A12;
end;
union {A where A is Subset of L(): R[A]} c= {F(x,y) where x is Element
of X(), y is Element of Y(): P[x] & Q[y]}
proof
let a be object;
assume a in union {A where A is Subset of L(): R[A]};
then consider A1 be set such that
A14: a in A1 and
A15: A1 in {A where A is Subset of L(): R[A]} by TARSKI:def 4;
consider A2 being Subset of L() such that
A16: A1 = A2 and
A17: R[A2] by A15;
consider y being Element of Y() such that
A18: Q[y] and
A19: for a being set holds a in A2 iff ex x being Element of X() st a =
F(x,y) & P[x] by A17;
ex x being Element of X() st a = F(x,y) & P[x] by A14,A16,A19;
hence thesis by A18;
end;
then union {A where A is Subset of L(): R[A]} = {F(x,y) where x is Element
of X( ), y is Element of Y(): P[x] & Q[y]} by A2;
hence thesis by A1,A9,A6,XBOOLE_0:def 10;
end;
scheme
FraenkelF9R9{ A() -> non empty set,B() -> non empty set, F1, F2(set,set) ->
set, P[set,set] } : { F1(u1,v1) where u1 is (Element of A()), v1 is Element of
B() : P[u1,v1] } = { F2(u2,v2) where u2 is (Element of A()), v2 is Element of B
() : P[u2,v2] }
provided
A1: for u being (Element of A()), v being Element of B() st P[u,v] holds
F1(u,v) = F2(u,v)
proof
set A = { F1(u1,v1) where u1 is (Element of A()), v1 is Element of B() : P[
u1,v1] }, C = { F2(u3,v3) where u3 is (Element of A()), v3 is Element of B() :
P[u3,v3] };
for a be object holds a in A iff a in C
proof
let a be object;
hereby
assume a in A;
then consider u being (Element of A()), v being Element of B() such that
A2: a = F1(u,v) and
A3: P[u,v];
a = F2(u,v) by A1,A2,A3;
hence a in C by A3;
end;
assume a in C;
then consider u being (Element of A()), v being Element of B() such that
A4: a = F2(u,v) and
A5: P[u,v];
a = F1(u,v) by A1,A4,A5;
hence thesis by A5;
end;
hence thesis by TARSKI:2;
end;
scheme
FraenkelF699R { A() -> non empty set, B() -> non empty set, F1, F2(set,set)
-> set, P[set,set], Q[set,set] } : { F1(u1,v1) where u1 is (Element of A()), v1
is Element of B() : P[u1,v1] } = { F2(u2,v2) where u2 is (Element of A()), v2
is Element of B() : Q[u2,v2] }
provided
A1: for u being (Element of A()), v being Element of B() holds P[u,v]
iff Q[u,v] and
A2: for u being (Element of A()), v being Element of B() st P[u,v] holds
F1(u,v) = F2(u,v)
proof
set A = { F1(u1,v1) where u1 is (Element of A()), v1 is Element of B() : P[
u1,v1] }, B = { F2(u2,v2) where u2 is (Element of A()), v2 is Element of B() :
Q[u2,v2] }, C = { F2(u3,v3) where u3 is (Element of A()), v3 is Element of B()
: P[u3,v3] };
A3: C = B from FRAENKEL:sch 4(A1);
A = C from FraenkelF9R9(A2);
hence thesis by A3;
end;
scheme
SupCommutativity { L() -> complete LATTICE, X, Y() -> non empty set, F1, F2(
set,set) -> Element of L(), P,Q[set]}: "\/"({ "\/"({F1(x,y) where y is Element
of Y(): Q[y]}, L()) where x is Element of X(): P[x] }, L()) = "\/"({ "\/"({F2(
x9,y9) where x9 is Element of X(): P[x9]}, L()) where y9 is Element of Y(): Q[
y9] }, L())
provided
A1: for x being Element of X(), y being Element of Y() st P[x] & Q[y]
holds F1(x,y) = F2(x,y)
proof
defpred X[set,set] means P[$1] & Q[$2];
A2: for x being Element of X(), y being Element of Y() holds X[x,y] iff X[x,
y];
A3: for x being Element of X(), y being Element of Y() st X[x,y] holds F1(x,
y) = F2(x,y) by A1;
A4: {F1(x9,y9) where x9 is Element of X(), y9 is Element of Y(): X[x9,y9]} =
{F2(x,y) where x is Element of X(), y is Element of Y(): X[x,y]} from
FraenkelF699R(A2,A3);
A5: "\/"({ "\/"({F1(x,y) where y is Element of Y(): Q[y]}, L()) where x is
Element of X(): P[x] }, L()) ="\/"({F1(x,y) where x is Element of X(), y is
Element of Y(): P[x] & Q[y]}, L()) from SupDistributivity;
"\/"({ "\/"({F2(x9,y9) where x9 is Element of X(): P[x9]}, L()) where y9
is Element of Y(): Q[y9] }, L()) ="\/"({F2(x9,y9) where x9 is Element of X(),
y9 is Element of Y(): P[x9] & Q[y9]}, L()) from SupDistributivity9
.="\/"({F1(x9,y9) where x9 is Element of X(), y9 is Element of Y(): P[x9
] & Q[y9]}, L()) by A4;
hence thesis by A5;
end;
Lm4: for X,Y,Z being non empty set for R being RMembership_Func of X,Y for S
being RMembership_Func of Y,Z for x being Element of X, z being Element of Z
holds rng min(R,S,x,z) =
the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y
& rng min(R,S,x,z) <> {}
proof
let X,Y,Z being non empty set;
let R being RMembership_Func of X,Y;
let S being RMembership_Func of Y,Z;
let x being Element of X, z being Element of Z;
set L = the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y;
A1: Y = dom min(R,S,x,z) & min(R,S,x,z) is PartFunc of dom min(R,S,x,z), rng
min (R,S,x,z) by FUNCT_2:def 1,RELSET_1:4;
for c be object holds c in L iff c in rng min(R,S,x,z)
proof
let c be object;
hereby
assume c in L;
then consider y being Element of Y such that
A2: c = R.(x,y) "/\" S.(y,z);
c = min(R,S,x,z).y by A2,FUZZY_4:def 2;
hence c in rng min(R,S,x,z) by A1,PARTFUN1:4;
end;
assume c in rng min(R,S,x,z);
then consider y being Element of Y such that
y in dom min(R,S,x,z) and
A3: c = min(R,S,x,z).y by PARTFUN1:3;
c = R.(x,y) "/\" S.(y,z) by A3,FUZZY_4:def 2;
hence thesis;
end;
hence rng min(R,S,x,z) = L by TARSKI:2;
ex d be set st d in rng min(R,S,x,z)
proof
set y = the Element of Y;
take min(R,S,x,z).y;
thus thesis by A1,PARTFUN1:4;
end;
hence rng min(R,S,x,z) <> {};
end;
theorem Th22:
for X,Y,Z being non empty set for R being RMembership_Func of X,
Y for S being RMembership_Func of Y,Z for x being Element of X, z being Element
of Z holds (R (#) S).(x,z) =
"\/"((the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y),
RealPoset [. 0,1 .])
proof
let X,Y,Z being non empty set;
let R being RMembership_Func of X,Y;
let S being RMembership_Func of Y,Z;
let x being Element of X, z being Element of Z;
set L = the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y;
[x,z] in [:X,Z:];
then
A1: (R (#) S).(x,z) = upper_bound(rng(min(R,S,x,z))) by FUZZY_4:def 3;
A2: for b being Element of RealPoset [. 0,1 .] st b is_>=_than L holds (R
(#) S).(x,z) <<= b
proof
let b be Element of RealPoset [. 0,1 .];
assume
A3: b is_>=_than the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y;
A4: rng min(R,S,x,z) c= [. 0,1 .] by RELAT_1:def 19;
A5: L = rng min(R,S,x,z) by Lm4;
A6: for r being Real st r in rng min(R,S,x,z) holds r <= b
proof
let r be Real;
assume
A7: r in rng min(R,S,x,z);
then reconsider r as Element of RealPoset [. 0,1 .] by A4,Def3;
r <<= b by A3,A5,A7;
hence thesis by Th3;
end;
rng min(R,S,x,z) <> {} by Lm4;
then upper_bound rng min(R,S,x,z) <= b by A6,SEQ_4:144;
hence thesis by A1,Th3;
end;
for b being Element of RealPoset [. 0,1 .] st b in L holds (R (#) S). [x
,z] >>= b
proof
let b be Element of RealPoset [. 0,1 .];
assume b in L;
then consider y being Element of Y such that
A8: b = R.(x,y) "/\" S.(y,z);
reconsider b as Real;
dom min(R,S,x,z) = Y & b = min(R,S,x,z).y
by A8,FUNCT_2:def 1,FUZZY_4:def 2;
then b <= upper_bound rng min(R,S,x,z) by FUZZY_4:1;
hence thesis by A1,Th3;
end;
then (R (#) S). [x,z] is_>=_than L;
hence thesis by A2,YELLOW_0:32;
end;
Lm5: for X,Y,Z being non empty set for R being RMembership_Func of X,Y for S
being RMembership_Func of Y,Z for x being Element of X, z being Element of Z
for a being Element of RealPoset [. 0,1 .] holds (R (#) S).(x,z) "/\" a = "\/"(
(the set of all R.(x,y) "/\" S.(y,z) "/\" a where y is Element of Y),
RealPoset [. 0,1 .])
proof
let X,Y,Z being non empty set;
let R being RMembership_Func of X,Y;
let S being RMembership_Func of Y,Z;
let x being Element of X, z being Element of Z;
let a being Element of RealPoset [. 0,1 .];
A1: the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y c=
the carrier of RealPoset [. 0,1 .]
proof
let d be object;
assume
d in the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y;
then ex t being Element of Y st d = R.(x,t) "/\" S.(t,z);
hence thesis;
end;
set A = {b "/\" a where b is Element of RealPoset [. 0,1 .]:
b in the set of all R.(x,y)
"/\" S.(y,z) where y is Element of Y};
set B = the set of all R.(x,y) "/\" S.(y,z) "/\" a where y is Element of Y;
A2: for c be object holds c in A iff c in B
proof
let c be object;
hereby
assume c in A;
then consider b being Element of RealPoset [. 0,1 .] such that
A3: c = b "/\" a and
A4: b in the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y;
ex y being Element of Y st b = R.(x,y) "/\" S.(y,z) by A4;
hence c in B by A3;
end;
assume c in B;
then consider y being Element of Y such that
A5: c = R.(x,y) "/\" S.(y,z) "/\" a;
R.(x,y) "/\" S.(y,z) in the set of all R.(x,y1) "/\" S.(y1,z)
where y1 is Element of Y;
hence thesis by A5;
end;
(R (#) S).(x,z) "/\" a = "\/"((the set of all R.(x,y) "/\" S.(y,z)
where y is Element of Y), RealPoset [. 0,1 .]) "/\" a by Th22
.= "\/"({b "/\" a where b is Element of RealPoset [. 0,1 .]:
b in the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y},
RealPoset [. 0,1 .]) by A1,Th15;
hence thesis by A2,TARSKI:2;
end;
Lm6: for X,Y,Z being non empty set for R being RMembership_Func of X,Y for S
being RMembership_Func of Y,Z for x being Element of X, z being Element of Z
for a being Element of RealPoset [. 0,1 .] holds a "/\" (R (#) S).(x,z) = "\/"(
(the set of all a "/\" R.(x,y) "/\" S.(y,z) where y is Element of Y),
RealPoset [. 0,1 .])
proof
let X,Y,Z being non empty set;
let R being RMembership_Func of X,Y;
let S being RMembership_Func of Y,Z;
let x being Element of X, z being Element of Z;
let a being Element of RealPoset [. 0,1 .];
set A = the set of all a "/\" R.(x,y) "/\" S.(y,z) where y is Element of Y;
set B = the set of all R.(x,y) "/\" S.(y,z) "/\" a where y is Element of Y;
for b be object holds b in A iff b in B
proof
let b be object;
hereby
assume b in A;
then consider y being Element of Y such that
A1: b = a "/\" R.(x,y) "/\" S.(y,z);
b = R.(x,y) "/\" S.(y,z) "/\" a by A1,LATTICE3:16;
hence b in B;
end;
assume b in B;
then consider y being Element of Y such that
A2: b = R.(x,y) "/\" S.(y,z) "/\" a;
b = a "/\" R.(x,y) "/\" S.(y,z) by A2,LATTICE3:16;
hence thesis;
end;
then A = B by TARSKI:2;
hence thesis by Lm5;
end;
theorem
for X,Y,Z,W being non empty set for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z for T being RMembership_Func of Z,W holds (
R (#) S) (#) T = R (#) (S (#) T)
proof
let X,Y,Z,W be non empty set;
let R be RMembership_Func of X,Y;
let S be RMembership_Func of Y,Z;
let T be RMembership_Func of Z,W;
A1: for x,w being object st x in X & w in W
holds ((R (#) S) (#) T).(x,w) = (R (#) (S (#) T)).(x,w)
proof
let x,w being object;
assume that
A2: x in X and
A3: w in W;
reconsider w as Element of W by A3;
reconsider x as Element of X by A2;
set A = the set of all "\/"((the set of all R.(x,y) "/\" S.(y,z) "/\"
T.(z,w)
where y is Element of Y), RealPoset [. 0,1 .]) where z is Element of Z;
set B = the set of all (R (#) S).(x,z) "/\" T.(z,w)
where z is Element of Z;
set C = the set of all "\/"((the set of all R.(x,y) "/\" S.(y,z) "/\"
T.(z,w) where z is Element of Z),
RealPoset [. 0,1 .]) where y is Element of Y;
set D = the set of all R.(x,y) "/\" ((S (#) T).(y,w))
where y is Element of Y;
defpred X[set] means not contradiction;
deffunc U(Element of Y,Element of Z) = R.(x,$1) "/\" S.($1,$2) "/\" T.($2,
w);
A4: for a be object holds a in A iff a in B
proof
let a be object;
hereby
assume a in A;
then consider z being Element of Z such that
A5: a = "\/"((the set of all R.(x,y) "/\" S.(y,z) "/\" T.(z,w)
where y is Element of Y), RealPoset [. 0,1 .]);
a = (R (#) S).(x,z) "/\" T.(z,w) by A5,Lm5;
hence a in B;
end;
assume a in B;
then consider z being Element of Z such that
A6: a = (R (#) S).(x,z) "/\" T.(z,w);
a = "\/"((the set of all R.(x,y) "/\" S.(y,z) "/\" T.(z,w)
where y is Element of Y), RealPoset [. 0,1 .]) by A6,Lm5;
hence thesis;
end;
A7: for y being Element of Y, z being Element of Z st X[y] & X[z] holds U
(y,z) = U(y,z);
A8: "\/"({"\/"({U(y,z) where z is Element of Z: X[z]}, RealPoset [. 0,1
.]) where y is Element of Y :X[y]}, RealPoset [. 0,1 .]) ="\/"({"\/"({U(y1,z1)
where y1 is Element of Y: X[y1]}, RealPoset [. 0,1 .]) where z1 is Element of Z
:X[z1]}, RealPoset [. 0,1 .]) from SupCommutativity(A7);
for c be object holds c in C iff c in D
proof
let c be object;
hereby
assume c in C;
then consider y being Element of Y such that
A9: c = "\/"((the set of all R.(x,y) "/\" S.(y,z) "/\" T.(z,w) where z is
Element of Z), RealPoset [. 0,1 .]);
c = R.(x,y) "/\" (S (#) T).(y,w) by A9,Lm6;
hence c in D;
end;
assume c in D;
then consider y being Element of Y such that
A10: c = R.(x,y) "/\" ((S (#) T).(y,w));
c = "\/"((the set of all R.(x,y) "/\" S.(y,z) "/\" T.(z,w)
where z is Element of Z),RealPoset [. 0,1 .]) by A10,Lm6;
hence thesis;
end;
then
A11: C = D by TARSKI:2;
((R (#) S) (#) T).(x,w) = "\/"((the set of all ((R (#) S).(x,z))
"/\" T.(z,w) where z
is Element of Z), RealPoset [. 0,1 .]) & (R (#) (S (#) T)).(
x, w) = "\/"((the set of all R.(x,y) "/\" ((S (#) T).(y,w))
where y is Element of Y), RealPoset [. 0,1 .]) by Th22;
hence thesis by A4,A11,A8,TARSKI:2;
end;
thus thesis by A1;
end;