:: The Formal Construction of Fuzzy Numbers
:: by Adam Grabowski
::
:: Received December 31, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users


theorem RealNon: :: FUZNUM_1:1
for a, b being Real st a <= b holds
REAL \ ].a,b.[ <> {}
proof end;

theorem Ah1: :: FUZNUM_1:2
for a, b being Real holds (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . a = 0
proof end;

theorem Ab1: :: FUZNUM_1:3
for a, b being Real st b - a <> 0 holds
(AffineMap ((1 / (b - a)),(- (a / (b - a))))) . b = 1
proof end;

theorem Cb1: :: FUZNUM_1:4
for b, c being Real st c - b <> 0 holds
(AffineMap ((- (1 / (c - b))),(c / (c - b)))) . b = 1
proof end;

theorem Cb2: :: FUZNUM_1:5
for b, c being Real holds (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . c = 0
proof end;

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
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
proof end;

theorem :: FUZNUM_1:8
for a being Real holds rng (AffineMap (0,a)) = {a}
proof end;

theorem Andr1a: :: FUZNUM_1:9
for a being Real
for C being non empty Subset of REAL holds rng ((AffineMap (0,a)) | C) = {a}
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.]
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.[
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.]
proof end;

theorem Hope5: :: FUZNUM_1:13
for x being Real holds (AffineMap (0,0)) . x <> 1
proof end;

theorem :: FUZNUM_1:14
for b being Real holds (AffineMap (0,1)) . b = 1
proof end;

theorem Kici1: :: FUZNUM_1:15
for b, a being Real holds (AffineMap (0,b)) . a = b
proof end;

definition
let C be non empty set ;
mode FuzzySet of C is Membership_Func of C;
end;

definition
let C be non empty set ;
let F be FuzzySet of C;
attr F is normalized means :: FUZNUM_1:def 1
 ex x being Element of C st F . x = 1;
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 );

notation
let C be non empty set ;
let F be FuzzySet of C;
synonym normal F for normalized ;
end;

notation
let C be non empty set ;
let F be FuzzySet of C;
antonym subnormal F for normal ;
end;

definition
let C be non empty set ;
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 ) );
end;

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

registration
let C be non empty set ;
cluster V5([.0,1.]) Function-like V30(C, REAL ) strictly-normalized -> normalized for Element of K16(K17(C,REAL));
coherence
for b1 being FuzzySet of C st b1 is strictly-normalized holds
b1 is normalized ;
end;

definition
let C be non empty set ;
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 } is Subset of C
proof end;
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 } ;

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

registration
let C be non empty set ;
cluster UMF C -> normalized ;
coherence
UMF C is normalized
proof end;
end;

registration
let C be non empty set ;
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 b1 being FuzzySet of C st b1 is normalized
proof end;
end;

definition
let C be non empty set ;
let F be FuzzySet of C;
func Core F -> Subset of C equals :: FUZNUM_1:def 4
 { x where x is Element of C : F . x = 1 } ;
coherence
{ x where x is Element of C : F . x = 1 } is Subset of C
proof end;
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 } ;

theorem :: FUZNUM_1:17
for C being non empty set holds Core (UMF C) = C
proof end;

theorem CEmpty: :: FUZNUM_1:18
for C being non empty set holds Core (EMF C) = {}
proof end;

registration
let C be non empty set ;
cluster Core (EMF C) -> empty ;
coherence
Core (EMF C) is empty by CEmpty;
end;

theorem CCounter: :: FUZNUM_1:19
for C being non empty set
for F being FuzzySet of C holds Core F = F " {1}
proof end;

theorem :: FUZNUM_1:20
for C being non empty set
for F being FuzzySet of C holds Core F = 1 -cut F
proof end;

definition
let F be FuzzySet of REAL;
attr F is f-convex means :: FUZNUM_1:def 5
 for x1, x2, l being Real st 0 <= l & l <= 1 holds
F . ((l * x1) + ((1 - l) * x2)) >= min ((F . x1),(F . x2));
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)) );

UCon: UMF REAL is f-convex
proof end;

ECon: EMF REAL is f-convex
proof end;

registration
cluster UMF REAL -> f-convex ;
coherence
UMF REAL is f-convex by UCon;
cluster EMF REAL -> f-convex ;
coherence
EMF REAL is f-convex by ECon;
end;

definition
let C be non empty set ;
let F be FuzzySet of C;
func height F -> ExtReal equals :: FUZNUM_1:def 6
 sup (rng F);
coherence
sup (rng F) is ExtReal ;
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);

theorem HgtBnd: :: FUZNUM_1:21
for C being non empty set
for F being FuzzySet of C holds
( 0 <= height F & height F <= 1 )
proof end;

theorem :: FUZNUM_1:22
for C being non empty set
for F being FuzzySet of C st F is normalized holds
height F = 1
proof end;

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 ) )
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 ) )
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
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
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 ) )
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
proof end;

registration
cluster non trivial V49() V50() V51() closed closed_interval for Element of K16(REAL);
existence
ex b1 being Subset of REAL st
( not b1 is trivial & b1 is closed_interval & b1 is closed )
proof end;
end;

definition
let a, b, c be Real;
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.]) is FuzzySet of REAL
proof end;
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.]);

::definition let C; let a,b,c be Real;
:: 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;
theorem :: FUZNUM_1:29
for a, b, c being Real st a < b & b < c holds
TriangularFS (a,b,c) is strictly-normalized
proof end;

theorem :: FUZNUM_1:30
for a, b, c being Real st a < b & b < c holds
TriangularFS (a,b,c) is continuous
proof end;

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

theorem :: FUZNUM_1:31
for a, b, c, d being Real st a < b & b < c & c < d holds
TrapezoidalFS (a,b,c,d) is normalized
proof end;

theorem :: FUZNUM_1:32
for a, b, c, d being Real st a < b & b < c & c < d holds
TrapezoidalFS (a,b,c,d) is continuous
proof end;

definition
let F be FuzzySet of REAL;
attr F is triangular means :: FUZNUM_1:def 9
 ex a, b, c being Real st F = TriangularFS (a,b,c);
attr F is trapezoidal means :: FUZNUM_1:def 10
 ex a, b, c, d being Real st F = TrapezoidalFS (a,b,c,d);
end;

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

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

registration
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 b1 being FuzzySet of REAL st b1 is triangular
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 b1 being FuzzySet of REAL st b1 is trapezoidal
proof end;
end;