:: 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 b₁ being FuzzySet of C st b₁ is strictly-normalized holds
b₁ 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 b₁ being FuzzySet of C st b₁ 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 b₁ being Subset of REAL st
( not b₁ is trivial & b₁ is closed_interval & b₁ 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 b₁ being FuzzySet of REAL st b₁ 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 b₁ being FuzzySet of REAL st b₁ is trapezoidal

proof end;

end;