begin
:: deftheorem Def1 defines is_less_than LFUZZY_1:def 1 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem
theorem Th5:
theorem Th6:
definition
let X be non
empty set ;
let f,
g be
Membership_Func of
X;
minredefine func min f,
g -> Element of
bool [:X,REAL :];
commutativity
for f, g being Membership_Func of X holds min f,g = min g,f
;
maxredefine func max f,
g -> Element of
bool [:X,REAL :];
commutativity
for f, g being Membership_Func of X holds max f,g = max g,f
;
end;
theorem
theorem
begin
:: deftheorem Def2 defines reflexive LFUZZY_1:def 2 :
:: deftheorem Def3 defines reflexive LFUZZY_1:def 3 :
:: deftheorem Def4 defines symmetric LFUZZY_1:def 4 :
:: deftheorem Def5 defines symmetric LFUZZY_1:def 5 :
:: deftheorem Def6 defines transitive LFUZZY_1:def 6 :
Lm1:
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) <> {} )
definition
let X be non
empty set ;
let R be
RMembership_Func of
X,
X;
redefine attr R is
transitive means
for
x,
y,
z being
Element of
X holds
(R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z];
compatibility
( R is transitive iff for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] )
end;
:: deftheorem defines transitive LFUZZY_1:def 7 :
:: deftheorem Def8 defines antisymmetric LFUZZY_1:def 8 :
theorem Th9:
theorem Th10:
theorem Th11:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
definition
let X be non
empty set ;
let R be
RMembership_Func of
X,
X;
let n be
natural number ;
canceled;func n iter R -> RMembership_Func of
X,
X means :
Def10:
ex
F being
Function of
NAT ,
Funcs [:X,X:],
[.0 ,1.] st
(
it = F . n &
F . 0 = Imf X,
X & ( for
k being
natural number ex
Q being
RMembership_Func of
X,
X st
(
F . k = Q &
F . (k + 1) = Q (#) R ) ) );
existence
ex b1 being RMembership_Func of X,X ex F being Function of NAT , Funcs [:X,X:],[.0 ,1.] st
( b1 = F . n & F . 0 = Imf X,X & ( for k being natural number ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) )
uniqueness
for b1, b2 being RMembership_Func of X,X st ex F being Function of NAT , Funcs [:X,X:],[.0 ,1.] st
( b1 = F . n & F . 0 = Imf X,X & ( for k being natural number ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) ) & ex F being Function of NAT , Funcs [:X,X:],[.0 ,1.] st
( b2 = F . n & F . 0 = Imf X,X & ( for k being natural number ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) ) holds
b1 = b2
end;
:: deftheorem LFUZZY_1:def 9 :
canceled;
:: deftheorem Def10 defines iter LFUZZY_1:def 10 :
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem
:: deftheorem defines TrCl LFUZZY_1:def 11 :
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
Lm2:
for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of
for x, z being Element of X holds { ((R . x,y) "/\" ((@ ("\/" Q,(FuzzyLattice [:X,X:]))) . y,z)) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" (pi Q,[y,z]),(RealPoset [.0 ,1.]))) where y is Element of X : verum }
theorem Th33:
Lm3:
for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of
for x, z being Element of X holds { ((R . [x,y]) "/\" ("\/" (pi Q,[y,z]),(RealPoset [.0 ,1.]))) where y is Element of X : verum } = { ("\/" { ((R . [x,y']) "/\" b) where b is Element of : b in pi Q,[y',z] } ,(RealPoset [.0 ,1.])) where y' is Element of X : verum }
Lm4:
for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of
for x, z being Element of X holds { ("\/" { ((R . [x,y]) "/\" b) where b is Element of : b in pi Q,[y,z] } ,(RealPoset [.0 ,1.])) where y is Element of X : verum } = { ("\/" { ((R . [x,y']) "/\" (r . [y',z])) where r is Element of : r in Q } ,(RealPoset [.0 ,1.])) where y' is Element of X : verum }
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) <> {} )
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 holds (R (#) S) . [x,z] = "\/" { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])
Lm7:
for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of
for x, z being Element of X holds { ("\/" { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.])) where r is Element of : r in Q } = { ("\/" { ((R . [x,y]) "/\" ((@ r') . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.])) where r' is Element of : r' in Q }
Lm8:
for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of
for x, z being Element of X holds { ("\/" { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.])) where r is Element of : r in Q } = { ((R (#) (@ r)) . [x,z]) where r is Element of : r in Q }
Lm9:
for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of
for x, z being Element of X holds { ((R (#) (@ r)) . [x,z]) where r is Element of : r in Q } = pi { (R (#) (@ r)) where r is Element of : r in Q } ,[x,z]
Lm10:
for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of
for x, z being Element of X holds "\/" { ("\/" { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of : r in Q } ,(RealPoset [.0 ,1.])) where y is Element of X : verum } ,(RealPoset [.0 ,1.]) = "\/" { ("\/" { ((R . [x,y]) "/\" (r' . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.])) where r' is Element of : r' in Q } ,(RealPoset [.0 ,1.])
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem