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