:: by Adam Grabowski

::

:: Received December 31, 2014

:: Copyright (c) 2014-2017 Association of Mizar Users

theorem Hope3: :: FUZNUM_1:6

for a, b, x being Real st b - a <> 0 & (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x = 1 holds

x = b

x = b

proof end;

theorem Hope4: :: FUZNUM_1:7

for b, c, x being Real st c - b <> 0 & (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . x = 1 holds

x = b

x = b

proof end;

theorem Hope1: :: FUZNUM_1:10

for a, b being Real st b - a > 0 holds

rng ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) = [.0,1.]

rng ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) = [.0,1.]

proof end;

theorem :: FUZNUM_1:11

for b, c being Real st c - b > 0 holds

rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | ].b,c.]) = [.0,1.[

rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | ].b,c.]) = [.0,1.[

proof end;

theorem Hope2a: :: FUZNUM_1:12

for b, c being Real st c - b > 0 holds

rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) = [.0,1.]

rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) = [.0,1.]

proof end;

:: deftheorem defines normalized FUZNUM_1:def 1 :

for C being non empty set

for F being FuzzySet of C holds

( F is normalized iff ex x being Element of C st F . x = 1 );

for C being non empty set

for F being FuzzySet of C holds

( F is normalized iff ex x being Element of C st F . x = 1 );

definition

let C be non empty set ;

let F be FuzzySet of C;

end;
let F be FuzzySet of C;

attr F is strictly-normalized means :: FUZNUM_1:def 2

ex x being Element of C st

( F . x = 1 & ( for y being Element of C st F . y = 1 holds

y = x ) );

ex x being Element of C st

( F . x = 1 & ( for y being Element of C st F . y = 1 holds

y = x ) );

:: deftheorem defines strictly-normalized FUZNUM_1:def 2 :

for C being non empty set

for F being FuzzySet of C holds

( F is strictly-normalized iff ex x being Element of C st

( F . x = 1 & ( for y being Element of C st F . y = 1 holds

y = x ) ) );

for C being non empty set

for F being FuzzySet of C holds

( F is strictly-normalized iff ex x being Element of C st

( F . x = 1 & ( for y being Element of C st F . y = 1 holds

y = x ) ) );

registration

let C be non empty set ;

for b_{1} being FuzzySet of C st b_{1} is strictly-normalized holds

b_{1} is normalized
;

end;
cluster V5([.0,1.]) Function-like V30(C, REAL ) strictly-normalized -> normalized for Element of K16(K17(C,REAL));

coherence for b

b

definition

let C be non empty set ;

let F be FuzzySet of C;

let alpha be Real;

{ x where x is Element of C : F . x >= alpha } is Subset of C

end;
let F be FuzzySet of C;

let alpha be Real;

func alpha -cut F -> Subset of C equals :: FUZNUM_1:def 3

{ x where x is Element of C : F . x >= alpha } ;

coherence { x where x is Element of C : F . x >= alpha } ;

{ x where x is Element of C : F . x >= alpha } is Subset of C

proof end;

:: deftheorem defines -cut FUZNUM_1:def 3 :

for C being non empty set

for F being FuzzySet of C

for alpha being Real holds alpha -cut F = { x where x is Element of C : F . x >= alpha } ;

for C being non empty set

for F being FuzzySet of C

for alpha being Real holds alpha -cut F = { x where x is Element of C : F . x >= alpha } ;

theorem AlphaCut1: :: FUZNUM_1:16

for C being non empty set

for F being FuzzySet of C

for alpha being Real holds alpha -cut F = F " [.alpha,1.]

for F being FuzzySet of C

for alpha being Real holds alpha -cut F = F " [.alpha,1.]

proof end;

registration
end;

registration

let C be non empty set ;

ex b_{1} being FuzzySet of C st b_{1} is normalized

end;
cluster V1() V4(C) V5( REAL ) V5([.0,1.]) non empty Function-like total V30(C, REAL ) V39() V40() V41() normalized for Element of K16(K17(C,REAL));

existence ex b

proof end;

definition

let C be non empty set ;

let F be FuzzySet of C;

coherence

{ x where x is Element of C : F . x = 1 } is Subset of C

end;
let F be FuzzySet of C;

coherence

{ x where x is Element of C : F . x = 1 } is Subset of C

proof end;

:: deftheorem defines Core FUZNUM_1:def 4 :

for C being non empty set

for F being FuzzySet of C holds Core F = { x where x is Element of C : F . x = 1 } ;

for C being non empty set

for F being FuzzySet of C holds Core F = { x where x is Element of C : F . x = 1 } ;

registration
end;

:: deftheorem defines f-convex FUZNUM_1:def 5 :

for F being FuzzySet of REAL holds

( F is f-convex iff for x1, x2, l being Real st 0 <= l & l <= 1 holds

F . ((l * x1) + ((1 - l) * x2)) >= min ((F . x1),(F . x2)) );

for F being FuzzySet of REAL holds

( F is f-convex iff for x1, x2, l being Real st 0 <= l & l <= 1 holds

F . ((l * x1) + ((1 - l) * x2)) >= min ((F . x1),(F . x2)) );

UCon: UMF REAL is f-convex

proof end;

ECon: EMF REAL is f-convex

proof end;

:: deftheorem defines height FUZNUM_1:def 6 :

for C being non empty set

for F being FuzzySet of C holds height F = sup (rng F);

for C being non empty set

for F being FuzzySet of C holds height F = sup (rng F);

theorem :: FUZNUM_1:23

for f, g being PartFunc of REAL,REAL st f is continuous & g is continuous & ex x being object st

( (dom f) /\ (dom g) = {x} & ( for x being object st x in (dom f) /\ (dom g) holds

f . x = g . x ) ) holds

ex h being PartFunc of REAL,REAL st

( h = f +* g & ( for x being Real st x in (dom f) /\ (dom g) holds

h is_continuous_in x ) )

( (dom f) /\ (dom g) = {x} & ( for x being object st x in (dom f) /\ (dom g) holds

f . x = g . x ) ) holds

ex h being PartFunc of REAL,REAL st

( h = f +* g & ( for x being Real st x in (dom f) /\ (dom g) holds

h is_continuous_in x ) )

proof end;

theorem LemGlue: :: FUZNUM_1:24

for f, g being PartFunc of REAL,REAL st f is continuous & not f is empty & g is continuous & not g is empty & ex a, b, c being Real st

( dom f = [.a,b.] & dom g = [.b,c.] ) & f tolerates g holds

ex h being PartFunc of REAL,REAL st

( h = f +* g & ( for x being Real st x in dom h holds

h is_continuous_in x ) )

( dom f = [.a,b.] & dom g = [.b,c.] ) & f tolerates g holds

ex h being PartFunc of REAL,REAL st

( h = f +* g & ( for x being Real st x in dom h holds

h is_continuous_in x ) )

proof end;

theorem Glue: :: FUZNUM_1:25

for f, g being PartFunc of REAL,REAL st f is continuous & not f is empty & g is continuous & not g is empty & ex a, b, c being Real st

( dom f = [.a,b.] & dom g = [.b,c.] ) & f tolerates g holds

f +* g is continuous

( dom f = [.a,b.] & dom g = [.b,c.] ) & f tolerates g holds

f +* g is continuous

proof end;

theorem Asi1: :: FUZNUM_1:26

for a, b being Real

for f, g being PartFunc of REAL,REAL st not g is empty & f = (AffineMap (0,0)) | (REAL \ ].a,b.[) & dom g = [.a,b.] & g . a = 0 & g . b = 0 holds

f tolerates g

for f, g being PartFunc of REAL,REAL st not g is empty & f = (AffineMap (0,0)) | (REAL \ ].a,b.[) & dom g = [.a,b.] & g . a = 0 & g . b = 0 holds

f tolerates g

proof end;

theorem Kluczyk: :: FUZNUM_1:27

for a, b being Real

for f, g being PartFunc of REAL,REAL st g is continuous & not g is empty & f = (AffineMap (0,0)) | (REAL \ ].a,b.[) & dom g = [.a,b.] & g . a = 0 & g . b = 0 holds

ex h being PartFunc of REAL,REAL st

( h = f +* g & ( for x being Real st x in dom h holds

h is_continuous_in x ) )

for f, g being PartFunc of REAL,REAL st g is continuous & not g is empty & f = (AffineMap (0,0)) | (REAL \ ].a,b.[) & dom g = [.a,b.] & g . a = 0 & g . b = 0 holds

ex h being PartFunc of REAL,REAL st

( h = f +* g & ( for x being Real st x in dom h holds

h is_continuous_in x ) )

proof end;

theorem :: FUZNUM_1:28

for a, b being Real

for f, g being PartFunc of REAL,REAL st g is continuous & not g is empty & f = (AffineMap (0,0)) | (REAL \ ].a,b.[) & dom g = [.a,b.] & g . a = 0 & g . b = 0 holds

f +* g is continuous

for f, g being PartFunc of REAL,REAL st g is continuous & not g is empty & f = (AffineMap (0,0)) | (REAL \ ].a,b.[) & dom g = [.a,b.] & g . a = 0 & g . b = 0 holds

f +* g is continuous

proof end;

registration

existence

ex b_{1} being Subset of REAL st

( not b_{1} is trivial & b_{1} is closed_interval & b_{1} is closed )

end;
ex b

( not b

proof end;

definition

let a, b, c be Real;

assume that

Z1: a < b and

Z2: 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.]) is FuzzySet of REAL

end;
assume that

Z1: a < b and

Z2: b < c ;

func TriangularFS (a,b,c) -> FuzzySet of REAL equals :TrDef: :: FUZNUM_1:def 7

(((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]);

coherence (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.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.]) is FuzzySet of REAL

proof end;

:: 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.]);

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 ;

((((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;
assume that

Z1: a < b and

Z2: b < c and

Z3: c < d ;

func TrapezoidalFS (a,b,c,d) -> FuzzySet of REAL equals :TPDef: :: FUZNUM_1:def 8

((((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.]);

((((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

proof 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.]);

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.]);

definition

let F be FuzzySet of REAL;

end;
attr F is trapezoidal means :: FUZNUM_1:def 10

ex a, b, c, d being Real st F = TrapezoidalFS (a,b,c,d);

ex a, b, c, d being Real st F = TrapezoidalFS (a,b,c,d);

:: deftheorem defines triangular FUZNUM_1:def 9 :

for F being FuzzySet of REAL holds

( F is triangular iff ex a, b, c being Real st F = TriangularFS (a,b,c) );

for F being FuzzySet of REAL holds

( F is triangular iff ex a, b, c being Real st F = TriangularFS (a,b,c) );

:: deftheorem defines trapezoidal FUZNUM_1:def 10 :

for F being FuzzySet of REAL holds

( F is trapezoidal iff ex a, b, c, d being Real st F = TrapezoidalFS (a,b,c,d) );

for F being FuzzySet of REAL holds

( F is trapezoidal iff ex a, b, c, d being Real st F = TrapezoidalFS (a,b,c,d) );

registration

ex b_{1} being FuzzySet of REAL st b_{1} is triangular

ex b_{1} being FuzzySet of REAL st b_{1} is trapezoidal
end;

cluster V1() V4( REAL ) V5( REAL ) V5([.0,1.]) non empty Function-like total V30( REAL , REAL ) V39() V40() V41() triangular for Element of K16(K17(REAL,REAL));

existence ex b

proof end;

cluster V1() V4( REAL ) V5( REAL ) V5([.0,1.]) non empty Function-like total V30( REAL , REAL ) V39() V40() V41() trapezoidal for Element of K16(K17(REAL,REAL));

existence ex b

proof end;

:: 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;