environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, RELAT_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_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;
registrations SUBSET_1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, LATTICE3, YELLOW_0, MONOID_0, YELLOW_1, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL10, WAYBEL17, ORDERS_4, ORDERS_2, FUNCOP_1;
constructors HIDDEN, DOMAIN_1, SQUARE_1, LATTICE3, MONOID_0, ORDERS_3, WAYBEL_1, WAYBEL_3, INTEGRA1, FUZZY_4, SEQ_4, RELSET_1, FUZZY_1, BINOP_2;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, REAL;
equalities XBOOLE_0, BINOP_1;
expansions TARSKI, XBOOLE_0, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, BINOP_1;
Lm1:
for A being non empty set holds FuzzyLattice A is constituted-Functions
Lm2:
for X being non empty set
for a being Element of (FuzzyLattice X) holds a is Membership_Func of X
Lm3:
for X being non empty set
for f being Membership_Func of X holds f is Element of (FuzzyLattice X)
scheme
SupDistributivity{
F1()
-> complete LATTICE,
F2()
-> non
empty set ,
F3()
-> non
empty set ,
F4(
set ,
set )
-> Element of
F1(),
P1[
set ],
P2[
set ] } :
"\/" (
{ ("\/" ( { F4(x,y) where y is Element of F3() : P2[y] } ,F1())) where x is Element of F2() : P1[x] } ,
F1())
= "\/" (
{ F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } ,
F1())
scheme
SupDistributivity9{
F1()
-> complete LATTICE,
F2()
-> non
empty set ,
F3()
-> non
empty set ,
F4(
set ,
set )
-> Element of
F1(),
P1[
set ],
P2[
set ] } :
"\/" (
{ ("\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1())) where y is Element of F3() : P2[y] } ,
F1())
= "\/" (
{ F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } ,
F1())
scheme
FraenkelF9R9{
F1()
-> non
empty set ,
F2()
-> non
empty set ,
F3(
set ,
set )
-> set ,
F4(
set ,
set )
-> set ,
P1[
set ,
set ] } :
{ F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } = { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2] }
provided
A1:
for
u being
Element of
F1()
for
v being
Element of
F2() st
P1[
u,
v] holds
F3(
u,
v)
= F4(
u,
v)
scheme
FraenkelF699R{
F1()
-> non
empty set ,
F2()
-> non
empty set ,
F3(
set ,
set )
-> set ,
F4(
set ,
set )
-> set ,
P1[
set ,
set ],
P2[
set ,
set ] } :
{ F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } = { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] }
provided
A1:
for
u being
Element of
F1()
for
v being
Element of
F2() holds
(
P1[
u,
v] iff
P2[
u,
v] )
and A2:
for
u being
Element of
F1()
for
v being
Element of
F2() st
P1[
u,
v] holds
F3(
u,
v)
= F4(
u,
v)
scheme
SupCommutativity{
F1()
-> complete LATTICE,
F2()
-> non
empty set ,
F3()
-> non
empty set ,
F4(
set ,
set )
-> Element of
F1(),
F5(
set ,
set )
-> Element of
F1(),
P1[
set ],
P2[
set ] } :
"\/" (
{ ("\/" ( { F4(x,y) where y is Element of F3() : P2[y] } ,F1())) where x is Element of F2() : P1[x] } ,
F1())
= "\/" (
{ ("\/" ( { F5(x9,y9) where x9 is Element of F2() : P1[x9] } ,F1())) where y9 is Element of F3() : P2[y9] } ,
F1())
provided
A1:
for
x being
Element of
F2()
for
y being
Element of
F3() st
P1[
x] &
P2[
y] holds
F4(
x,
y)
= F5(
x,
y)
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
for z being Element of Z holds
( rng (min (R,S,x,z)) = { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} )
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
for z being Element of Z
for a being Element of (RealPoset [.0,1.]) holds ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ,(RealPoset [.0,1.]))
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
for z being Element of Z
for a being Element of (RealPoset [.0,1.]) holds a "/\" ((R (#) S) . (x,z)) = "\/" ( { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))