begin
:: deftheorem Def1 defines real LFUZZY_0:def 1 :
:: deftheorem Def2 defines interval LFUZZY_0:def 2 :
theorem Th1:
theorem Th2:
:: deftheorem Def3 defines RealPoset LFUZZY_0:def 3 :
theorem Th3:
theorem
theorem
theorem Th6:
theorem Th7:
theorem Th8:
begin
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
begin
:: deftheorem defines FuzzyLattice LFUZZY_0:def 4 :
theorem Th14:
Lm1:
for A being non empty set holds FuzzyLattice A is constituted-Functions
theorem Th15:
Lm2:
for X being non empty set
for a being Element of (FuzzyLattice X) holds a is Membership_Func of X
:: deftheorem defines @ LFUZZY_0:def 5 :
Lm3:
for X being non empty set
for f being Membership_Func of X holds f is Element of (FuzzyLattice X)
:: deftheorem defines @ LFUZZY_0:def 6 :
theorem Th16:
theorem
theorem Th18:
theorem
theorem Th20:
theorem
begin
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 being Element of (RealPoset [.0 ,1.]) holds x is Real
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 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) <> {} )
theorem Th22:
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 ((R (#) S) . x,z) "/\" a = "\/" { (((R . x,y) "/\" (S . y,z)) "/\" a) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])
Lm7:
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.])
theorem