environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, XXREAL_1, CARD_1, RELAT_1, TARSKI, FUNCT_1, XXREAL_0, PARTFUN1, ARYTM_1, ARYTM_3, COMPLEX1, FUZZY_1, GRAPH_2, MEASURE5, MSALIMIT, FUZNUM_1, REAL_1, ORDINAL2, XXREAL_2, TREES_1, RCOMP_1, ZFMISC_1, NUMPOLY1, JGRAPH_2, FUNCT_4, PRE_TOPC, FCONT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, XCMPLX_0, XXREAL_2, COMPLEX1, XREAL_0, FUNCT_1, PARTFUN1, FCONT_1, RELSET_1, FUNCT_4, RCOMP_1, MEASURE5, FUZZY_1;
definitions XBOOLE_0, TARSKI, XXREAL_2;
theorems TARSKI, FUNCT_1, FUNCT_3, ABSVALUE, PARTFUN1, ZFMISC_1, XBOOLE_0, XBOOLE_1, COMPLEX1, XREAL_1, XXREAL_0, XXREAL_1, FUNCT_2, RELAT_1, MEASURE5, XREAL_0, XXREAL_2, FCONT_1, XCMPLX_1, FUZZY_2, FUNCT_4, RCOMP_1, ENUMSET1;
schemes ;
registrations RELSET_1, NUMBERS, XXREAL_0, MEMBERED, XBOOLE_0, VALUED_0, FUNCT_2, XREAL_0, ORDINAL1, FCONT_1, RELAT_1, TOPREALB, FUNCT_4, FUNCT_1, XCMPLX_0, NAT_1, RCOMP_1;
constructors HIDDEN, COMPLEX1, RFUNCT_1, INTEGRA1, SEQ_4, RELSET_1, FUZZY_1, FCONT_1, FUNCT_4;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities FUZZY_1, RCOMP_1;
expansions TARSKI, FCONT_1;
UCon:
UMF REAL is f-convex
ECon:
EMF REAL is f-convex
::
deftheorem TrDef defines
TriangularFS FUZNUM_1:def 7 :
for a, b, c being Real st a < b & b < c holds
TriangularFS (a,b,c) = (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]);
definition
let a,
b,
c,
d be
Real;
assume that Z1:
a < b
and Z2:
b < c
and Z3:
c < d
;
func TrapezoidalFS (
a,
b,
c,
d)
-> FuzzySet of
REAL equals :
TPDef:
((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]);
coherence
((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) is FuzzySet of REAL
end;
::
deftheorem TPDef defines
TrapezoidalFS FUZNUM_1:def 8 :
for a, b, c, d being Real st a < b & b < c & c < d holds
TrapezoidalFS (a,b,c,d) = ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]);
:: func TriangularFS (C,a,b,c) -> FuzzySet of C means
:: for x being Real st x in C holds
:: ((x <= a or c <= x) implies it.x = 0) &
:: (a <= x & x <= b implies it.x = (x-a)/(b-a)) &
:: (b <= x & x <= c implies it.x = (c-x)/(c-b));
:: correctness;
::end;