environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, VALUED_0, FUZZY_1, FUZZY_2, LATTICE3, SUBSET_1, FUNCT_1, XXREAL_0, RELAT_1, ZFMISC_1, TARSKI, VALUED_1, RELAT_2, FUZZY_4, CARD_1, LATTICES, PARTFUN1, LFUZZY_0, EQREL_1, XXREAL_1, SEQ_4, FUNCT_3, FUNCT_7, FUNCT_2, ARYTM_3, STRUCT_0, QC_LANG1, CARD_3, FUNCOP_1, REWRITE1, WAYBEL_0, NEWTON, ORDINAL2, LATTICE2, WAYBEL_1, NAT_1, LFUZZY_1, REAL_1, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, DOMAIN_1, PARTFUN1, CARD_3, RELAT_2, BINOP_1, FUNCT_3, RFUNCT_1, SUBSET_1, XREAL_0, NAT_1, SEQ_4, VALUED_0, RCOMP_1, RELSET_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, WAYBEL_3, FUZZY_1, FUZZY_2, FUZZY_4, FUNCOP_1, LFUZZY_0, XXREAL_0;
definitions TARSKI, XBOOLE_0, FUZZY_1;
theorems XBOOLE_0, ZFMISC_1, WAYBEL_1, RELAT_1, LATTICE3, YELLOW_0, TARSKI, SEQ_4, YELLOW_2, WAYBEL_3, CARD_3, YELLOW_1, FUNCOP_1, FUZZY_2, FUZZY_4, FUNCT_3, FUZZY_1, PARTFUN1, LFUZZY_0, RELAT_2, ORDINAL1, XXREAL_0, BINOP_1, RELSET_1, FUNCT_2;
schemes FRAENKEL, RECDEF_1, NAT_1, LFUZZY_0;
registrations XBOOLE_0, SUBSET_1, XREAL_0, NAT_1, MEMBERED, STRUCT_0, LATTICE3, MONOID_0, YELLOW_1, WAYBEL10, WAYBEL17, LFUZZY_0, RELAT_1, FUNCT_2, NUMBERS, FUZZY_1, RELSET_1, VALUED_0, ORDINAL1, CARD_1;
constructors HIDDEN, DOMAIN_1, SQUARE_1, RFUNCT_1, MONOID_0, WAYBEL_3, FUZZY_2, FUZZY_4, LFUZZY_0, SEQ_4, RELSET_1, FUNCOP_1, FUZZY_1;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
equalities BINOP_1;
expansions FUZZY_1;
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;
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;
let n be
Nat;
existence
ex b1 being RMembership_Func of X,X ex F being sequence of (Funcs ([:X,X:],[.0,1.])) st
( b1 = F . n & F . 0 = Imf (X,X) & ( for k being Nat 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 sequence of (Funcs ([:X,X:],[.0,1.])) st
( b1 = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) ) & ex F being sequence of (Funcs ([:X,X:],[.0,1.])) st
( b2 = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) ) holds
b1 = b2
end;
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 }
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.]))