:: Lattice of Fuzzy Sets
:: by Takashi Mitsuishi and Grzegorz Bancerek
::
:: Received August 12, 2003
:: Copyright (c) 2003 Association of Mizar Users
:: deftheorem Def1 defines real LFUZZY_0:def 1 :
:: deftheorem Def2 defines interval LFUZZY_0:def 2 :
theorem Th1: :: LFUZZY_0:1
theorem Th2: :: LFUZZY_0:2
:: deftheorem Def3 defines RealPoset LFUZZY_0:def 3 :
theorem Th3: :: LFUZZY_0:3
theorem :: LFUZZY_0:4
theorem :: LFUZZY_0:5
theorem Th6: :: LFUZZY_0:6
theorem Th7: :: LFUZZY_0:7
theorem Th8: :: LFUZZY_0:8
theorem Th9: :: LFUZZY_0:9
theorem Th10: :: LFUZZY_0:10
theorem Th11: :: LFUZZY_0:11
theorem Th12: :: LFUZZY_0:12
theorem Th13: :: LFUZZY_0:13
:: deftheorem defines FuzzyLattice LFUZZY_0:def 4 :
theorem Th14: :: LFUZZY_0:14
Lm1:
for A being non empty set holds FuzzyLattice A is constituted-Functions
theorem Th15: :: LFUZZY_0:15
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: :: LFUZZY_0:16
theorem :: LFUZZY_0:17
theorem Th18: :: LFUZZY_0:18
theorem :: LFUZZY_0:19
theorem Th20: :: LFUZZY_0:20
theorem :: LFUZZY_0:21
scheme :: LFUZZY_0:sch 3
FraenkelF'R'{
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 :: LFUZZY_0:sch 4
FraenkelF6''R{
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 :: LFUZZY_0:sch 5
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(x',y') where x' is Element of F2() : P1[x'] } ,F1()) where y' is Element of F3() : P2[y'] } ,
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: :: LFUZZY_0:22
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 :: LFUZZY_0:23