begin
:: deftheorem Def1 defines is_less_than LFUZZY_1:def 1 :
for X, Y being non empty set
for f, g being RMembership_Func of X,Y holds
( f is_less_than g iff for x being Element of X
for y being Element of Y holds f . x,y <= g . x,y );
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 :
for X being non empty set
for R being RMembership_Func of X,X holds
( R is reflexive iff R c= );
:: deftheorem Def3 defines reflexive LFUZZY_1:def 3 :
for X being non empty set
for R being RMembership_Func of X,X holds
( R is reflexive iff for x being Element of X holds R . x,x = 1 );
:: deftheorem Def4 defines symmetric LFUZZY_1:def 4 :
for X being non empty set
for R being RMembership_Func of X,X holds
( R is symmetric iff converse R = R );
:: deftheorem Def5 defines symmetric LFUZZY_1:def 5 :
for X being non empty set
for R being RMembership_Func of X,X holds
( R is symmetric iff for x, y being Element of X holds R . x,y = R . y,x );
:: deftheorem Def6 defines transitive LFUZZY_1:def 6 :
for X being non empty set
for R being RMembership_Func of X,X holds
( R is transitive iff R c= );
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 :
for X being non empty set
for R being RMembership_Func of X,X holds
( R is transitive iff for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] );
:: deftheorem Def8 defines antisymmetric LFUZZY_1:def 8 :
for X being non empty set
for R being RMembership_Func of X,X holds
( R is antisymmetric iff for x, y being Element of X st R . x,y <> 0 & R . y,x <> 0 holds
x = y );
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 :
for X being non empty set
for R being RMembership_Func of X,X
for n being natural number
for b4 being RMembership_Func of X,X holds
( b4 = n iter R iff ex F being Function of NAT ,(Funcs [:X,X:],[.0 ,1.]) st
( b4 = 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 ) ) ) );
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem
:: deftheorem defines TrCl LFUZZY_1:def 11 :
for X being non empty set
for R being RMembership_Func of X,X holds TrCl R = "\/" { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:]);
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 (FuzzyLattice [:X,X:])
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 (FuzzyLattice [:X,X:])
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,y9]) "/\" b) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[y9,z] } ,(RealPoset [.0 ,1.])) where y9 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 (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ("\/" { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[y,z] } ,(RealPoset [.0 ,1.])) where y is Element of X : verum } = { ("\/" { ((R . [x,y9]) "/\" (r . [y9,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0 ,1.])) where y9 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 (FuzzyLattice [:X,X:])
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 (FuzzyLattice [:X,X:]) : r in Q } = { ("\/" { ((R . [x,y]) "/\" ((@ r9) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.])) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q }
Lm8:
for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
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 (FuzzyLattice [:X,X:]) : r in Q } = { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
Lm9:
for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = pi { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : 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 (FuzzyLattice [:X,X:])
for x, z being Element of X holds "\/" { ("\/" { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0 ,1.])) where y is Element of X : verum } ,(RealPoset [.0 ,1.]) = "\/" { ("\/" { ((R . [x,y]) "/\" (r9 . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.])) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } ,(RealPoset [.0 ,1.])
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem