:: The Formal Construction of Fuzzy Numbers
:: by Adam Grabowski
::
:: Received December 31, 2014
:: Copyright (c) 2014-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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 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;
constructors COMPLEX1, RFUNCT_1, INTEGRA1, SEQ_4, RELSET_1, FUZZY_1, FCONT_1,
FUNCT_4;
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;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions XBOOLE_0, TARSKI, XXREAL_2;
equalities FUZZY_1, RCOMP_1;
expansions TARSKI, FCONT_1;
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;
begin :: Preliminaries: Affine Maps
theorem RealNon:
for a,b being Real st a <= b holds
REAL \ ].a,b.[ <> {}
proof
let a,b be Real;
assume a <= b;
consider c being Real such that
A1: c < a by XREAL_1:2;
A2: not c in ].a,b.[ by A1,XXREAL_1:4;
c in REAL by XREAL_0:def 1;
hence thesis by A2,XBOOLE_0:def 5;
end;
reserve a,b,c,x for Real;
theorem Ah1:
AffineMap (1/(b-a),-a/(b-a)).a = 0
proof
AffineMap (1/(b-a),-a/(b-a)).a = (1/(b-a))*a+-a/(b-a) by FCONT_1:def 4
.= (1/(b-a))*a+(-a)/(b-a) by XCMPLX_1:187
.= (1/(b-a))*a+a*((-1))/(b-a)
.= a*(1/(b-a))+a*((-1)/(b-a)) by XCMPLX_1:74
.= a*(1/(b-a)+(-1)/(b-a))
.= a*(1/(b-a)+-1/(b-a)) by XCMPLX_1:187
.= 0;
hence thesis;
end;
theorem Ab1:
b - a <> 0 implies
AffineMap (1/(b-a),-a/(b-a)).b = 1
proof
assume
A1: b - a <> 0;
AffineMap (1/(b-a),-a/(b-a)).b = (1/(b-a))*b+-a/(b-a) by FCONT_1:def 4
.= (b/(b-a))+-a/(b-a) by XCMPLX_1:99
.= (b/(b-a))+(-a)/(b-a) by XCMPLX_1:187
.= (b+-a)/(b-a) by XCMPLX_1:62
.= (1/(b-a))*(b+-a) by XCMPLX_1:99
.= 1 by XCMPLX_1:106,A1;
hence thesis;
end;
theorem Cb1:
c - b <> 0 implies
AffineMap (-1/(c-b),c/(c-b)).b = 1
proof
assume
A1: c - b <> 0;
AffineMap (-1/(c-b),c/(c-b)).b
= (-1/(c-b))*b+c/(c-b) by FCONT_1:def 4
.= ((-1)/(c-b))*b+c/(c-b) by XCMPLX_1:187
.= (((-1)*b)/(c-b))+c/(c-b) by XCMPLX_1:74
.= (-b+c)/(c-b) by XCMPLX_1:62
.= 1 by A1,XCMPLX_1:60;
hence thesis;
end;
theorem Cb2:
AffineMap (-1/(c-b),c/(c-b)).c = 0
proof
AffineMap (-1/(c-b),c/(c-b)).c
= (-1/(c-b))*c+c/(c-b) by FCONT_1:def 4
.= ((-1)/(c-b))*c+c/(c-b) by XCMPLX_1:187
.= (((-1)*c)/(c-b))+c/(c-b) by XCMPLX_1:74
.= (-c+c)/(c-b) by XCMPLX_1:62
.= 0;
hence thesis;
end;
theorem Hope3:
b - a <> 0 & AffineMap (1/(b-a),-a/(b-a)).x = 1 implies
x = b
proof
assume that
A0: b - a <> 0 and
A1: AffineMap (1/(b-a),-a/(b-a)).x = 1;
x in REAL & b in REAL by XREAL_0:def 1; then
A3: x in dom AffineMap (1/(b-a),-a/(b-a)) &
b in dom AffineMap (1/(b-a),-a/(b-a)) by FUNCT_2:def 1;
AffineMap (1/(b-a),-a/(b-a)).b = 1 by A0,Ab1;
hence thesis by A1,FUNCT_1:def 4,A3,A0;
end;
theorem Hope4:
c - b <> 0 & AffineMap (-1/(c-b),c/(c-b)).x = 1 implies
x = b
proof
assume that
A0: c - b <> 0 and
A1: AffineMap (-1/(c-b),c/(c-b)).x = 1;
x in REAL & b in REAL by XREAL_0:def 1; then
A3: x in dom AffineMap (-1/(c-b),c/(c-b)) &
b in dom AffineMap (-1/(c-b),c/(c-b)) by FUNCT_2:def 1;
AffineMap (-1/(c-b),c/(c-b)).b = 1 by A0,Cb1;
hence thesis by A1,FUNCT_1:def 4,A3,A0;
end;
theorem
rng AffineMap (0,a) = {a}
proof
set f = AffineMap (0,a);
thus rng f c= {a}
proof
let y be object;
assume y in rng f; then
consider x being object such that
A1: x in dom f & y = f.x by FUNCT_1:def 3;
reconsider x as Real by A1;
y = 0 * x + a by A1,FCONT_1:def 4 .= a;
hence thesis by TARSKI:def 1;
end;
let y be object;
assume
a0: y in {a};
0 in REAL by XREAL_0:def 1; then
A1: 0 in dom f by FUNCT_2:def 1;
y = 0 * 0 + a by a0,TARSKI:def 1
.= f.0 by FCONT_1:def 4;
hence thesis by FUNCT_1:def 3,A1;
end;
theorem Andr1a:
for C being non empty Subset of REAL holds
rng (AffineMap (0,a) | C) = {a}
proof
let C be non empty Subset of REAL;
set f = AffineMap (0,a) | C;
thus rng f c= {a}
proof
let y be object;
assume y in rng f; then
consider x being object such that
A1: x in dom f & y = f.x by FUNCT_1:def 3;
reconsider x as Real by A1;
y = AffineMap (0,a).x by A1,FUNCT_1:49; then
y = 0 * x + a by FCONT_1:def 4 .= a;
hence thesis by TARSKI:def 1;
end;
let y be object;
assume
a0: y in {a};
reconsider o = the Element of C as Real;
C c= REAL; then
C c= dom AffineMap(0,a) by FUNCT_2:def 1; then
a1: dom f = C by RELAT_1:62;
y = 0 * o + a by a0,TARSKI:def 1
.= AffineMap (0,a).o by FCONT_1:def 4
.= f.o by FUNCT_1:49;
hence thesis by FUNCT_1:def 3,a1;
end;
theorem Hope1:
b - a > 0 implies
rng ((AffineMap (1/(b-a),-a/(b-a)) | [.a,b.])) = [.0,1.]
proof
set f = AffineMap (1/(b-a),-a/(b-a));
set g = f | [.a,b.];
assume
A0: b - a > 0;
thus rng g c= [.0,1.]
proof
let y be object;
assume
Y0: y in rng g; then
consider x being object such that
A1: x in dom g and
A2: y = g.x by FUNCT_1:def 3;
Y1: x in [.a,b.] by A1,RELAT_1:57;
reconsider xx = x as Real by A1;
reconsider yy = y as Real by Y0;
S4: y = f.xx by FUNCT_1:47,A1,A2;
A4: a <= xx by Y1,XXREAL_1:1;
S2: f.a = 0 by Ah1;
S5: f.a <= f.xx by A4,FCONT_1:53,A0;
xx <= b by Y1,XXREAL_1:1; then
S6: f.xx <= f.b by A0,FCONT_1:53;
f.b = 1 by Ab1,A0;
hence thesis by S4,S2,S5,S6;
end;
let y be object;
assume
V1: y in [.0,1.]; then
reconsider yy = y as Real;
set A = 1 / (b-a);
set B = -a / (b-a);
L2: (f qua Function)" = AffineMap (A",-B/A) by A0,FCONT_1:56; then
L3: (f qua Function)".0 = A" * 0 + -B/A by FCONT_1:def 4
.= -(((-a) / (b-a))/(1 / (b-a))) by XCMPLX_1:187
.= -((-a) / 1) by XCMPLX_1:55,A0
.= a;
set x = (f qua Function)".yy;
reconsider xx = x as Real by L2;
X1: -B/A = -(((-a) / (b-a))/(1 / (b-a))) by XCMPLX_1:187
.= -((-a) / 1) by XCMPLX_1:55,A0
.= a;
L4: (f qua Function)".1 = A" * 1 + -B/A by FCONT_1:def 4,L2
.= 1/A + -B/A by XCMPLX_1:215
.= b-a + a by XCMPLX_1:52,X1
.= b;
J2: 0 <= yy & yy <= 1 by XXREAL_1:1,V1; then
J3: a <= xx by FCONT_1:53,L2,A0,L3;
xx <= b by FCONT_1:53,L2,A0,J2,L4; then
J4: x in [.a,b.] by J3;
j5: dom f = REAL by FUNCT_2:def 1;
T1: x in dom g by J4,j5,RELAT_1:57;
rng f = REAL by FCONT_1:55,A0; then
S2: yy in rng f by XREAL_0:def 1;
g.((f qua Function)".yy) = f.((f qua Function)".yy) by FUNCT_1:49,J4
.= yy by A0,S2,FUNCT_1:35;
hence thesis by T1,FUNCT_1:def 3;
end;
theorem
c - b > 0 implies
rng ((AffineMap (-1/(c-b),c/(c-b)) | ].b,c.])) = [.0,1.[
proof
set f = AffineMap (-1/(c-b),c/(c-b));
set g = f | ].b,c.];
assume
A0: c - b > 0;
thus rng g c= [.0,1.[
proof
let y be object;
assume
Y0: y in rng g; then
consider x being object such that
A1: x in dom g and
A2: y = g.x by FUNCT_1:def 3;
Y1: x in ].b,c.] by A1,RELAT_1:57;
reconsider xx = x as Real by A1;
reconsider yy = y as Real by Y0;
S4: y = f.xx by FUNCT_1:47,A1,A2;
A4: b < xx by Y1,XXREAL_1:2;
S2: f.b = 1 by Cb1,A0;
S5: f.b > f.xx by A4,FCONT_1:52,A0;
xx <= c by Y1,XXREAL_1:2; then
S6: f.xx >= f.c by A0,FCONT_1:54;
f.c = 0 by Cb2;
hence thesis by S4,S2,S5,S6;
end;
let y be object;
assume
V1: y in [.0,1.[; then
reconsider yy = y as Real;
set A = -1 / (c-b);
set B = c / (c-b);
L2: (f qua Function)" = AffineMap (A",-B/A) by A0,FCONT_1:56; then
L3: (f qua Function)".0 = A" * 0 + -B/A by FCONT_1:def 4
.= -((c / (c-b))/((-1) / (c-b))) by XCMPLX_1:187
.= -(c / -1) by XCMPLX_1:55,A0
.= c;
X1: -B/A = -((c / (c-b))/((-1) / (c-b))) by XCMPLX_1:187
.= -(c / -1) by XCMPLX_1:55,A0
.= c;
L4: (f qua Function)".1 = A" * 1 + -B/A by FCONT_1:def 4,L2
.= 1/A + -B/A by XCMPLX_1:215
.= 1/((-1)/(c-b)) + c by XCMPLX_1:187,X1
.= (c-b)/(-1) + c by XCMPLX_1:57
.= b;
set x = (f qua Function)".yy;
reconsider xx = x as Real by L2;
J2: 0 <= yy & yy < 1 by XXREAL_1:3,V1; then
J3: c >= xx by FCONT_1:54,L2,A0,L3;
xx > b by FCONT_1:52,L2,A0,J2,L4; then
J4: x in ].b,c.] by J3;
j5: dom f = REAL by FUNCT_2:def 1;
T1: x in dom g by J4,j5,RELAT_1:57;
rng f = REAL by FCONT_1:55,A0; then
S2: yy in rng f by XREAL_0:def 1;
set ff = (f qua Function)";
g.(ff.yy) = f.(ff.yy) by FUNCT_1:49,J4
.= yy by A0,S2,FUNCT_1:35;
hence thesis by T1,FUNCT_1:def 3;
end;
theorem Hope2a:
c - b > 0 implies
rng ((AffineMap (-1/(c-b),c/(c-b)) | [.b,c.])) = [.0,1.]
proof
set f = AffineMap (-1/(c-b),c/(c-b));
set g = f | [.b,c.];
assume
A0: c - b > 0;
thus rng g c= [.0,1.]
proof
let y be object;
assume
Y0: y in rng g; then
consider x being object such that
A1: x in dom g and
A2: y = g.x by FUNCT_1:def 3;
Y1: x in [.b,c.] by A1,RELAT_1:57;
reconsider xx = x as Real by A1;
reconsider yy = y as Real by Y0;
S4: y = f.xx by FUNCT_1:47,A1,A2;
A4: b <= xx by Y1,XXREAL_1:1;
S2: f.b = 1 by Cb1,A0;
S5: f.b >= f.xx by A4,FCONT_1:54,A0;
xx <= c by Y1,XXREAL_1:1; then
S6: f.xx >= f.c by A0,FCONT_1:54;
f.c = 0 by Cb2;
hence thesis by S4,S2,S5,S6;
end;
let y be object;
assume
V1: y in [.0,1.]; then
reconsider yy = y as Real;
set A = -1 / (c-b);
set B = c / (c-b);
L2: (f qua Function)" = AffineMap (A",-B/A) by FCONT_1:56,A0; then
L3: (f qua Function)".0 = A" * 0 + -B/A by FCONT_1:def 4
.= -((c / (c-b))/((-1) / (c-b))) by XCMPLX_1:187
.= -(c / -1) by XCMPLX_1:55,A0
.= c;
X1: -B/A = -((c / (c-b))/((-1) / (c-b))) by XCMPLX_1:187
.= -(c / -1) by XCMPLX_1:55,A0
.= c;
L4: (f qua Function)".1 = A" * 1 + -B/A by FCONT_1:def 4,L2
.= 1/A + -B/A by XCMPLX_1:215
.= 1/((-1)/(c-b)) + c by XCMPLX_1:187,X1
.= (c-b)/(-1) + c by XCMPLX_1:57
.= b;
set x = (f qua Function)".yy;
reconsider xx = x as Real by L2;
J2: 0 <= yy & yy <= 1 by XXREAL_1:1,V1; then
J3: c >= xx by FCONT_1:54,L2,A0,L3;
xx >= b by FCONT_1:54,L2,A0,J2,L4; then
J4: x in [.b,c.] by J3;
jj: dom f = REAL by FUNCT_2:def 1;
T1: x in dom g by J4,jj,RELAT_1:57;
rng f = REAL by FCONT_1:55,A0; then
S2: yy in rng f by XREAL_0:def 1;
set ff = (f qua Function)";
g.(ff.yy) = f.(ff.yy) by FUNCT_1:49,J4
.= yy by A0,S2,FUNCT_1:35;
hence thesis by T1,FUNCT_1:def 3;
end;
theorem Hope5:
(AffineMap (0,0)).x <> 1
proof
(AffineMap (0,0)).x = 0 * x + 0 by FCONT_1:def 4 .= 0;
hence thesis;
end;
theorem
AffineMap (0,1).b = 1
proof
AffineMap (0,1).b = 0*b + 1 by FCONT_1:def 4 .= 1;
hence thesis;
end;
theorem Kici1:
for a being Real holds AffineMap (0,b).a = b
proof
let a be Real;
AffineMap (0,b).a = 0 * a + b by FCONT_1:def 4 .= b;
hence thesis;
end;
begin :: Towards Development of Fuzzy Numbers
reserve C for non empty set;
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
ex x being Element of C st
F.x = 1;
end;
notation let C be non empty set;
let F be FuzzySet of C;
synonym F is normal for F is normalized;
end;
notation let C be non empty set;
let F be FuzzySet of C;
antonym F is subnormal↑ for F is normal;
end;
definition let C be non empty set;
let F be FuzzySet of C;
attr F is strictly-normalized means
ex x being Element of C st
F.x = 1 &
for y being Element of C st F.y = 1 holds y = x;
end;
registration let C be non empty set;
cluster strictly-normalized -> normalized for FuzzySet of C;
coherence;
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
{ x where x is Element of C : F.x >= alpha };
coherence
proof
set H = { x where x is Element of C : F.x >= alpha };
H c= C
proof
let y be object;
assume y in H; then
consider x being Element of C such that
A1: y = x & F.x >= alpha;
thus thesis by A1;
end;
hence thesis;
end;
end;
theorem AlphaCut1:
for F being FuzzySet of C,
alpha being Real holds
alpha-cut F = F " ([. alpha, 1 .])
proof
let F be FuzzySet of C,
alpha be Real;
thus alpha-cut F c= F " ([. alpha, 1 .])
proof
let x be object;
assume x in alpha-cut F; then
consider y being Element of C such that
A1: x = y & F.y >= alpha;
x in C by A1; then
A2: x in dom F by FUNCT_2:def 1; then
F.y in [. 0, 1 .] by A1,PARTFUN1:4; then
0 <= F.y & F.y <= 1 by XXREAL_1:1; then
F.y in [. alpha, 1 .] by A1;
hence thesis by A1,FUNCT_1:def 7,A2;
end;
let x be object;
assume
c2: x in F"([. alpha, 1 .]); then
x in dom F & F.x in [. alpha, 1 .] by FUNCT_1:def 7; then
alpha <= F.x & F.x <= 1 by XXREAL_1:1;
hence thesis by c2;
end;
registration let C;
cluster UMF C -> normalized;
coherence
proof
ex x being Element of C st (UMF C).x = 1
proof
take x = the Element of C;
thus thesis by FUNCT_3:def 3;
end;
hence thesis;
end;
end;
registration let C;
cluster normalized for FuzzySet of C;
existence
proof
take UMF C;
thus thesis;
end;
end;
definition let C;
let F be FuzzySet of C;
func Core F -> Subset of C equals
{ x where x is Element of C : F.x = 1 };
coherence
proof
set H = { x where x is Element of C : F.x = 1 };
H c= C
proof
let y be object;
assume y in H; then
consider x being Element of C such that
A1: y = x & F.x = 1;
thus thesis by A1;
end;
hence thesis;
end;
end;
theorem
Core UMF C = C
proof
thus Core UMF C c= C;
let x be object;
assume x in C; then
reconsider xx = x as Element of C;
(UMF C).xx = 1 by FUNCT_3:def 3;
hence thesis;
end;
theorem CEmpty:
Core EMF C = {}
proof
thus Core EMF C c= {}
proof
let x be object;
assume x in Core EMF C; then
consider xx being Element of C such that
A1: x = xx & (EMF C).xx = 1;
thus thesis by A1,FUNCT_3:def 3;
end;
thus thesis;
end;
registration let C;
cluster Core EMF C -> empty;
coherence by CEmpty;
end;
theorem CCounter:
for F being FuzzySet of C holds
Core F = F " {1}
proof
let F be FuzzySet of C;
thus Core F c= F " {1}
proof
let x be object;
assume x in Core F; then
consider xx being Element of C such that
A1: x = xx & F.xx = 1;
A2: F.xx in {1} by TARSKI:def 1,A1;
dom F = C by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:def 7,A2;
end;
let x be object;
assume
a1: x in F " {1}; then
A1: x in dom F & F.x in {1} by FUNCT_1:def 7;
reconsider xx = x as Element of C by a1;
F.xx = 1 by A1,TARSKI:def 1;
hence thesis;
end;
theorem
for F being FuzzySet of C holds
Core F = 1-cut F
proof
let F be FuzzySet of C;
1-cut F = F " ([. 1, 1 .]) by AlphaCut1
.= F " {1} by XXREAL_1:17;
hence thesis by CCounter;
end;
begin :: Convexity and the Height of a Fuzzy Set
definition let F be FuzzySet of REAL;
attr F is f-convex means
for x1, x2 being Real,
l being Real st 0 <= l & l <= 1 holds
F.(l*x1 + (1-l)*x2) >= min(F.x1,F.x2);
end;
UCon:
UMF REAL is f-convex
proof
for x1, x2 being Real,
l being Real st 0 <= l & l <= 1 holds
(UMF REAL).(l*x1 + (1-l)*x2) >= min((UMF REAL).x1,(UMF REAL).x2)
proof
let x1, x2 be Real,
l be Real;
set F = UMF REAL;
assume 0 <= l & l <= 1;
x1 in REAL & x2 in REAL by XREAL_0:def 1; then
A1: F.x1 = 1 & F.x2 = 1 by FUNCT_3:def 3;
l*x1 + (1-l)*x2 in REAL by XREAL_0:def 1;
hence thesis by A1,FUNCT_3:def 3;
end;
hence thesis;
end;
ECon:
EMF REAL is f-convex
proof
for x1, x2 being Real,
l being Real st 0 <= l & l <= 1 holds
(EMF REAL).(l*x1 + (1-l)*x2) >= min((EMF REAL).x1,(EMF REAL).x2)
proof
let x1, x2 be Real,
l be Real;
set F = EMF REAL;
assume 0 <= l & l <= 1;
A3: x1 in REAL & x2 in REAL by XREAL_0:def 1;
A1: F.x1 = {} & F.x2 = {} by FUNCT_3:def 3,A3;
l*x1 + (1-l)*x2 in REAL by XREAL_0:def 1;
hence thesis by A1,FUNCT_3:def 3;
end;
hence thesis;
end;
registration
cluster UMF REAL -> f-convex;
coherence by UCon;
cluster EMF REAL -> f-convex;
coherence by ECon;
end;
definition let C be non empty set;
let F be FuzzySet of C;
func height F -> ExtReal equals
sup rng F;
coherence;
end;
theorem HgtBnd:
for F being FuzzySet of C holds
0 <= height F & height F <= 1
proof
let F be FuzzySet of C;
B0: 0 is LowerBound of rng F
proof
let x be ExtReal;
assume x in rng F; then
consider xx being object such that
B1: xx in dom F & x = F.xx by FUNCT_1:def 3;
reconsider xx as Element of C by B1;
thus thesis by B1,FUZZY_2:1;
end;
b2: 1 is UpperBound of rng F
proof
let x be ExtReal;
assume x in rng F; then
consider xx being object such that
B1: xx in dom F & x = F.xx by FUNCT_1:def 3;
reconsider xx as Element of C by B1;
thus thesis by B1,FUZZY_2:1;
end;
inf rng F <= sup rng F by XXREAL_2:40;
hence thesis by b2,B0,XXREAL_2:def 4,XXREAL_2:def 3;
end;
theorem
for F being FuzzySet of C st
F is normalized holds height F = 1
proof
let F be FuzzySet of C;
assume F is normalized; then
consider x being Element of C such that
A1: F.x = 1;
x in C; then
x in dom F by FUNCT_2:def 1; then
A2: 1 <= height F by XXREAL_2:4,FUNCT_1:3,A1;
height F <= 1 by HgtBnd;
hence height F = 1 by A2,XXREAL_0:1;
end;
begin :: Pasting aka Glueing Lemmas
theorem
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
let f,g be PartFunc of REAL, REAL;
assume
A1: 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;
reconsider h = f +* g as PartFunc of REAL, REAL;
take h;
thus h = f +* g;
let x be Real;
J2: h | dom f = (g +* f) | dom f by FUNCT_4:34,PARTFUN1:def 4,A1
.= f;
assume x in dom f /\ dom g; then
ZR: x in dom f & x in dom g by XBOOLE_0:def 4; then
JJ: x in dom h by FUNCT_4:12;
for r being Real st 0 < r
ex s being Real st 0 < s &
for x1 being Real st x1 in dom h & |.x1-x.|<s holds
|.h.x1-h.x.| < r
proof
let r be Real;
set hf = h | dom f;
set hg = h | dom g;
SF: x in dom hf by RELAT_1:57,ZR,JJ;
Sf: x in dom hg by ZR;
assume
R0: 0 < r;
consider s2 being Real such that
SB: 0 < s2 & for x1 being Real st x1 in dom hf & |.x1-x.| < s2 holds
|.hf.x1 - hf.x.| < r / 2 by J2,ZR,A1,FCONT_1:3,R0;
consider s1 being Real such that
Sb: 0 < s1 & for x1 being Real st x1 in dom hg & |.x1-x.| < s1 holds
|.hg.x1 - hg.x.| < r / 2 by FCONT_1:3,ZR,A1,R0;
take s = min (s2,s1);
thus 0 < s by SB,Sb,XXREAL_0:15;
SS: r / 2 < r by XREAL_1:216,R0;
let x1 be Real;
assume
SC: x1 in dom h & |.x1-x.| < s; then
per cases by FUNCT_4:12;
suppose ZT: x1 in dom f & x1 in dom g;
i1: x1 in dom h by FUNCT_4:12,ZT; then
I1: x1 in dom hf by ZT,RELAT_1:57;
s <= s2 by XXREAL_0:17; then
|.x1-x.| < s2 by XXREAL_0:2,SC; then
SD: |.hf.x1-hf.x.| < r/2 by SB,i1,ZT,RELAT_1:57;
s1: hf.x1 = h.x1 by FUNCT_1:47,I1;
hf.x = h.x by FUNCT_1:47,SF;
hence thesis by SS,XXREAL_0:2,SD,s1;
end;
suppose ZT: x1 in dom f & not x1 in dom g; then
i1: x1 in dom h by FUNCT_4:12; then
I1: x1 in dom hf by ZT,RELAT_1:57;
s <= s2 by XXREAL_0:17; then
|.x1-x.| < s2 by XXREAL_0:2,SC; then
SD: |.hf.x1-hf.x.| < r/2 by SB,i1,ZT,RELAT_1:57;
s1: hf.x1 = h.x1 by FUNCT_1:47,I1;
hf.x = h.x by FUNCT_1:47,SF;
hence thesis by SS,XXREAL_0:2,SD,s1;
end;
suppose
P1: x1 in dom g;
x1 in dom hg by P1; then
P2: h.x1 = hg.x1 by FUNCT_1:47;
P3: h.x = hg.x by FUNCT_1:47,Sf;
s <= s1 by XXREAL_0:17; then
|.x1-x.| < s1 by XXREAL_0:2,SC; then
|.hg.x1-hg.x.| < r/2 by Sb,P1;
hence thesis by SS,XXREAL_0:2,P3,P2;
end;
end;
hence thesis by FCONT_1:3;
end;
theorem LemGlue:
for f,g being PartFunc of REAL, REAL st
f is continuous non empty & g is continuous non empty &
(ex a,b,c being Real st dom f = [.a,b.] & dom g = [.b,c.]) &
f tolerates g
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
let f,g be PartFunc of REAL, REAL;
assume
A1: f is continuous non empty & g is continuous non empty &
(ex a,b,c being Real st dom f = [.a,b.] & dom g = [.b,c.]) &
f tolerates g;
reconsider ff = f, gg = g as non empty continuous PartFunc of REAL, REAL
by A1;
consider a,b,c being Real such that
AB: dom f = [.a,b.] & dom g = [.b,c.] by A1;
dom ff <> {} & dom gg <> {}; then
Ab: a <= b & b <= c by XXREAL_1:29,AB;
AA: dom f /\ dom g = {b} by XXREAL_1:418,Ab,AB;
reconsider h = f +* g as PartFunc of REAL, REAL;
take h;
thus h = f +* g;
let x be Real;
J2: h | dom f = (g +* f) | dom f by FUNCT_4:34,A1
.= f;
assume
JJ: x in dom h; then
per cases by FUNCT_4:12;
suppose
J1: x in dom f;
set hf = h |dom f;
set hg = h |dom g;
for r being Real st 0 < r
ex s being Real st 0 < s &
for x1 being Real st x1 in dom h & |.x1-x.| < s holds |.h.x1-h.x.| < r
proof
let r be Real;
dom f c= dom h & dom g c= dom h by FUNCT_4:10; then
XX: dom hf = dom f & dom hg = dom g by RELAT_1:62;
SF: x in dom hf by RELAT_1:57,J1,JJ;
assume
R0: 0 < r; then
consider s2 being Real such that
SB: 0 < s2 & for x1 being Real st x1 in dom hf & |.x1-x.|<s2 holds
|.hf.x1-hf.x.| < r/2 by J1,J2,A1,FCONT_1:3;
KK: b in dom f /\ dom g by AA,TARSKI:def 1; then
KA: b in dom f & b in dom g by XBOOLE_0:def 4;
KI: b in dom hf & b in dom hg by XX,XBOOLE_0:def 4,KK;
consider s1 being Real such that
Sb: 0 < s1 & for x1 being Real st x1 in dom hg & |.x1-b.|<s1 holds
|.hg.x1-hg.b.| < r/2 by FCONT_1:3,R0,A1,KA;
take s = min (s2,s1);
thus 0 < s by SB,Sb,XXREAL_0:15;
SS: r/2 < r by XREAL_1:216,R0;
let x1 be Real;
assume
SC: x1 in dom h & |.x1-x.| < s;
s <= s2 by XXREAL_0:17; then
H1: |.x1-x.| < s2 by XXREAL_0:2,SC;
per cases by FUNCT_4:12,SC;
suppose
ZT: x1 in dom f; then
I1: x1 in dom hf by RELAT_1:57,SC;
SD: |.hf.x1-hf.x.| < r / 2 by SB,ZT,H1,RELAT_1:57,SC;
s1: hf.x1 = h.x1 by FUNCT_1:47,I1;
|.h.x1-h.x.| < r / 2 by SD,s1,FUNCT_1:47,SF;
hence thesis by SS,XXREAL_0:2;
end;
suppose
P1: x1 in dom g; then
x1 in dom hg; then
P2: h.x1 = hg.x1 by FUNCT_1:47;
P3: h.x = hf.x by FUNCT_1:47,SF;
s <= s1 by XXREAL_0:17; then
P6: |.x1-x.| < s1 by XXREAL_0:2,SC;
WA: hg.b = hf.b by J2,KK,A1,PARTFUN1:def 4;
M3: x + 0 <= b by XXREAL_1:1,J1,AB;
M7: b <= x1 & x1 <= c by XXREAL_1:1,P1,AB;
m0: x + 0 <= x1 by M7,XXREAL_0:2,M3;
b + 0 <= x1 by XXREAL_1:1,P1,AB; then
M1: |.x1 - b.| = x1 - b by ABSVALUE:def 1,XREAL_1:19;
M2: |.b - x.| = b - x by ABSVALUE:def 1,M3,XREAL_1:19;
M8: |.x1 - x.| = |.x1-b.| + |.b-x.|
by M1,M2,m0,ABSVALUE:def 1,XREAL_1:19; then
|.x1-b.| <= |.x1 - x.| by COMPLEX1:46,XREAL_1:31; then
|.x1-b.| < s1 by P6,XXREAL_0:2; then
KJ: |.hg.x1-hg.b.| < r / 2 by Sb,P1;
|.b-x.| <= |.x1 - x.| by M8,XREAL_1:31,COMPLEX1:46; then
|.b - x.| < s2 by H1,XXREAL_0:2; then
|.hf.b-hf.x.| < r / 2 by SB,KI; then
WW: |.hg.x1-hg.b.| + |.hf.b-hf.x.| < r / 2 + r / 2 by KJ,XREAL_1:8;
|.hg.x1-hf.x.| <= |.hg.x1-hg.b.| + |.hg.b-hf.x.| by COMPLEX1:63;
hence thesis by P2,P3,WA,XXREAL_0:2,WW;
end;
end;
hence thesis by FCONT_1:3;
end;
suppose
J1: x in dom g;
for r being Real st 0<r ex s being Real st 0<s &
for x1 being Real st x1 in dom h & |.x1-x.|<s holds |.h.x1-h.x.| < r
proof
let r be Real;
set hf = h |dom f;
set hg = h |dom g;
dom f c= dom h & dom g c= dom h by FUNCT_4:10; then
XX: dom hf = dom f & dom hg = dom g by RELAT_1:62;
SF: x in dom hg by J1;
assume
R0: 0 < r; then
consider s2 being Real such that
SB: 0 < s2 & for x1 being Real st x1 in dom hg & |.x1-x.|<s2 holds
|.hg.x1-hg.x.| < r/2 by J1,FCONT_1:3,A1;
KK: b in dom f /\ dom g by AA,TARSKI:def 1; then
KA: b in dom f & b in dom g by XBOOLE_0:def 4;
KI: b in dom hf & b in dom hg by XX,KK,XBOOLE_0:def 4;
consider s1 being Real such that
Sb: 0 < s1 & for x1 being Real st x1 in dom hf & |.x1-b.|<s1 holds
|.hf.x1-hf.b.| < r/2 by FCONT_1:3,R0,J2,A1,KA;
take s = min (s2,s1);
thus 0 < s by SB,Sb,XXREAL_0:15;
SS: r/2 < r by XREAL_1:216,R0;
let x1 be Real;
assume
SC: x1 in dom h & |.x1-x.| < s;
s <= s2 by XXREAL_0:17; then
H1: |.x1-x.| < s2 by XXREAL_0:2,SC;
per cases by FUNCT_4:12,SC;
suppose
ZT: x1 in dom g; then
I1: x1 in dom hg;
SD: |.hg.x1 - hg.x.| < r / 2 by SB,ZT,H1;
s1: hg.x1 = h.x1 by FUNCT_1:47,I1;
|.h.x1-h.x.| < r / 2 by SD,s1,FUNCT_1:47,SF;
hence thesis by SS,XXREAL_0:2;
end;
suppose
P1: x1 in dom f; then
x1 in dom hf by RELAT_1:57,SC; then
P2: h.x1 = hf.x1 by FUNCT_1:47;
P3: h.x = hg.x by FUNCT_1:47,SF;
s <= s1 by XXREAL_0:17; then
|.x1 - x.| < s1 by XXREAL_0:2,SC; then
P6: |.x - x1.| < s1 by COMPLEX1:60;
WA: hg.b = hf.b by J2,KK,A1,PARTFUN1:def 4;
M3: x - 0 >= b by XXREAL_1:1,J1,AB;
M7: a <= x1 & x1 <= b by XXREAL_1:1,P1,AB;
m0: x1 + 0 <= x by M7,XXREAL_0:2,M3;
b - 0 >= x1 by XXREAL_1:1,P1,AB; then
M1: |.b - x1.| = b - x1 by ABSVALUE:def 1,XREAL_1:11;
M2: |.x - b.| = x - b by ABSVALUE:def 1,M3,XREAL_1:11;
M8: |.x - x1.| = |.b-x1.| + |.x-b.|
by M1,M2,m0,ABSVALUE:def 1,XREAL_1:19; then
|.b - x1.| <= |.x - x1.| by COMPLEX1:46,XREAL_1:31; then
|.b - x1.| < s1 by P6,XXREAL_0:2; then
|.x1 - b.| < s1 by COMPLEX1:60; then
KJ: |.hf.x1 - hf.b.| < r / 2 by Sb,P1,RELAT_1:57,SC;
LK: |.b - x.| = |.x - b.| by COMPLEX1:60;
|.x - b.| <= |.x - x1.| by M8,XREAL_1:31,COMPLEX1:46; then
|.b - x.| <= |.x1 - x.| by COMPLEX1:60,LK; then
|.b - x.| < s2 by H1,XXREAL_0:2; then
|.hg.b - hg.x.| < r / 2 by SB,KI; then
WW: |.hf.x1 - hf.b.| + |.hg.b - hg.x.| < r / 2 + r / 2
by KJ,XREAL_1:8;
|.hf.x1-hg.x.| <= |.hf.x1-hf.b.| + |.hf.b-hg.x.| by COMPLEX1:63;
hence thesis by P2,P3,WA,XXREAL_0:2,WW;
end;
end;
hence thesis by FCONT_1:3;
end;
end;
theorem Glue:
for f,g being PartFunc of REAL, REAL st
f is continuous non empty &
g is continuous non 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
let f,g be PartFunc of REAL, REAL;
assume f is continuous non empty & g is continuous non empty &
(ex a,b,c being Real st dom f = [.a,b.] & dom g = [.b,c.]) &
f tolerates g; then
consider h being PartFunc of REAL, REAL such that
A2: h = f +* g & for x being Real st x in dom h holds h is_continuous_in x
by LemGlue;
thus thesis by A2;
end;
theorem Asi1:
for f, g being PartFunc of REAL, REAL st
g is non empty &
f = AffineMap (0,0) | (REAL \ ].a,b.[) &
dom g = [.a,b.] & g.a = 0 & g.b = 0 holds
f tolerates g
proof
let f, g be PartFunc of REAL, REAL;
assume
A1: g is non empty & f = (AffineMap (0,0)) | (REAL \ ].a,b.[) &
dom g = [.a,b.] & g.a = 0 & g.b = 0;
REAL \ ].a,b.[ c= REAL; then
REAL \ ].a,b.[ c= dom AffineMap (0,0) by FUNCT_2:def 1; then
A2: dom f = REAL \ ].a,b.[ by RELAT_1:62,A1
.= ].-infty,a.] \/ [.b,+infty.[ by XXREAL_1:398;
for x being object st x in dom f /\ dom g holds f.x = g.x
proof
let x be object;
K2: b < +infty by XXREAL_0:9,XREAL_0:def 1;
K3: -infty < a by XXREAL_0:12,XREAL_0:def 1;
assume
P1: x in dom f /\ dom g; then
x in ([.a,b.] /\ ].-infty,a.]) \/ ([.a,b.] /\ [.b,+infty.[)
by XBOOLE_1:23,A1,A2; then
x in {a} \/ ([.a,b.] /\ [.b,+infty.[)
by XXREAL_1:417,A1,XXREAL_1:29,K3; then
x in {a} \/ {b} by XXREAL_1:416,A1,XXREAL_1:29,K2; then
x in {a,b} by ENUMSET1:1; then
W1: g.x = 0 by A1,TARSKI:def 2;
reconsider xx = x as Real by P1;
x in dom f by P1,XBOOLE_0:def 4; then
f.x = AffineMap(0,0).xx by A1,FUNCT_1:47;
hence thesis by Kici1, W1;
end;
hence thesis by PARTFUN1:def 4;
end;
theorem Kluczyk:
for f, g being PartFunc of REAL, REAL st
g is continuous non 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
let f, g be PartFunc of REAL, REAL;
assume
A1: g is continuous non empty & f = (AffineMap (0,0)) | (REAL \ ].a,b.[) &
dom g = [.a,b.] & g.a = 0 & g.b = 0; then
KK: f tolerates g by Asi1;
set c = b;
take h = f +* g;
thus h = f +* g;
let x be Real;
U1: -infty < a by XXREAL_0:12,XREAL_0:def 1;
U3: b < +infty by XXREAL_0:9,XREAL_0:def 1;
REAL \ ].a,b.[ c= REAL; then
REAL \ ].a,b.[ c= dom AffineMap(0,0) by FUNCT_2:def 1; then
S1: dom f = REAL \ ].a,b.[ by A1,RELAT_1:62;
aa: (REAL \ ].a,b.[) /\ [.a,b.] = (].-infty,a.] \/ [.b,+infty.[) /\ [.a,b.]
by XXREAL_1:398
.= (].-infty,a.] /\ [.a,b.]) \/ ([.b,+infty.[ /\ [.a,b.])
by XBOOLE_1:23
.= {a} \/ ([.b,+infty.[ /\ [.a,b.]) by XXREAL_1:417,U1,XXREAL_1:29,A1
.= {a} \/ {b} by XXREAL_1:416,XXREAL_1:29,A1,U3
.= {a,b} by ENUMSET1:1;
a in dom f /\ dom g by aa,S1,A1,TARSKI:def 2; then
sx: a in dom f & a in dom g by XBOOLE_0:def 4;
nn: f.a = AffineMap(0,0).a by FUNCT_1:47,A1,sx
.= 0*a+0 by FCONT_1:def 4 .= 0;
b in dom f /\ dom g by aa,S1,A1,TARSKI:def 2; then
sy: b in dom f & b in dom g by XBOOLE_0:def 4; then
mn: f.b = AffineMap(0,0).b by FUNCT_1:47,A1
.= 0*b+0 by FCONT_1:def 4 .= 0;
Z7: dom f = ].-infty,a.] \/ [.b,+infty.[ by S1,XXREAL_1:398;
Z8: ].-infty,a.[ c= ].-infty,a.] by XXREAL_1:21;
xz: ].-infty,a.] c= dom f by XBOOLE_1:7,Z7; then
Z6: ].-infty,a.[ c= dom f by Z8;
z8: ].b,+infty.[ c= [.b,+infty.[ by XXREAL_1:22;
wz: [.b,+infty.[ c= dom f by XBOOLE_1:7,Z7; then
z6: ].b,+infty.[ c= dom f by z8;
assume x in dom h; then
R1: x in dom f or x in dom g by FUNCT_4:12;
set xx0 = x;
b2: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
b1: ].a,b.[ c= dom g by A1,XXREAL_1:25;
x in ].-infty,a.] or x in [.b,+infty.[ or x in [.a,b.]
by A1,R1,Z7,XBOOLE_0:def 3; then
x in ].-infty,a.[ \/ {a} or x in [.b,+infty.[ or x in [.a,b.]
by XXREAL_1:423; then
x in ].-infty,a.[ or x in {a} or x in [.b,+infty.[ or x in [.a,b.]
by XBOOLE_0:def 3; then
x in ].-infty,a.[ or x = a or x in {b} \/ ].b,+infty.[ or x in [.a,b.]
by XXREAL_1:427,TARSKI:def 1; then
x in ].-infty,a.[ or x = a or x in {b} or x in ].b,+infty.[ or
x in [.a,b.] by XBOOLE_0:def 3; then
x in ].-infty,a.[ or x = a or x = b or x in ].b,+infty.[ or
x in {a,b} \/ ].a,b.[
by XXREAL_1:29,XXREAL_1:128,TARSKI:def 1; then
x in ].-infty,a.[ or x = a or x = b or x in ].b,+infty.[ or
x in {a,b} or x in {a,b} or x in ].a,b.[ by XBOOLE_0:def 3; then
per cases by TARSKI:def 2;
suppose
FT: x = a;
for r being Real st 0 < r
ex s being Real st 0 < s &
for x1 being Real st x1 in dom h & |.x1-x.|<s holds |.h.x1-h.x.| < r
proof
let r be Real;
assume
H1: 0 < r; then
consider s1 being Real such that
WW: 0 < s1 &
for x1 being Real st x1 in dom g & |.x1-x.|<s1 holds |.g.x1-g.x.| < r
by FCONT_1:3,A1,sx,FT;
consider s2 being Real such that
W1: 0 < s2 &
for x1 being Real st x1 in dom f & |.x1-x.|<s2 holds |.f.x1-f.x.| < r
by FCONT_1:3,H1,FCONT_1:def 2,A1,sx,FT;
take s = min (s1,s2);
thus 0 < s by WW,W1,XXREAL_0:15;
O2: s <= s1 & s <= s2 by XXREAL_0:17;
let x1 be Real;
assume
O1: x1 in dom h & |.x1-x.| < s; then
per cases by FUNCT_4:12;
suppose
W2: x1 in dom f & not x1 in dom g; then
W3: h.x1 = f.x1 by FUNCT_4:11;
W4: h.x = f.x by A1,FT,nn,FUNCT_4:13,sx;
|.x1-x.| < s2 by O1,O2,XXREAL_0:2;
hence |.h.x1-h.x.| < r by W3,W4,W1,W2;
end;
suppose
W2: x1 in dom f & x1 in dom g; then
W3: h.x1 = g.x1 by FUNCT_4:13;
W4: h.x = g.x by FUNCT_4:13,sx,FT;
|.x1-x.| < s1 by O1,O2,XXREAL_0:2;
hence |.h.x1-h.x.| < r by W3,W4,W2,WW;
end;
suppose
W2: x1 in dom g; then
W3: h.x1 = g.x1 by FUNCT_4:13;
W4: h.x = g.x by FUNCT_4:13,FT,sx;
|.x1-x.| < s1 by O1,O2,XXREAL_0:2;
hence |.h.x1-h.x.| < r by W3,W4,W2,WW;
end;
end;
hence thesis by FCONT_1:3;
end;
suppose
FT: x = b;
for r being Real st 0<r
ex s being Real st 0<s &
for x1 being Real st x1 in dom h & |.x1-x.|<s holds |.h.x1-h.x.| < r
proof
let r be Real;
assume
H1: 0 < r; then
consider s1 being Real such that
WW: 0 < s1 &
for x1 being Real st x1 in dom g & |.x1-x.|<s1 holds |.g.x1-g.x.| < r
by FCONT_1:3,A1,sy,FT;
consider s2 being Real such that
W1: 0 < s2 &
for x1 being Real st x1 in dom f & |.x1-x.|<s2 holds |.f.x1-f.x.| < r
by FCONT_1:3,H1,FCONT_1:def 2,A1,sy,FT;
take s = min (s1,s2);
thus 0 < s by WW,W1,XXREAL_0:15;
O2: s <= s1 & s <= s2 by XXREAL_0:17;
let x1 be Real;
assume
O1: x1 in dom h & |.x1-x.|<s; then
per cases by FUNCT_4:12;
suppose
W2: x1 in dom f & not x1 in dom g; then
W3: h.x1 = f.x1 by FUNCT_4:11;
W4: h.x = f.x by mn,A1,FT,sy,FUNCT_4:13;
|.x1-x.| < s2 by O1,O2,XXREAL_0:2;
hence |.h.x1-h.x.| < r by W3,W4,W1,W2;
end;
suppose
W2: x1 in dom f & x1 in dom g; then
W3: h.x1 = g.x1 by FUNCT_4:13;
W4: h.x = g.x by FUNCT_4:13,sy,FT;
|.x1-x.| < s1 by O1,O2,XXREAL_0:2;
hence |.h.x1-h.x.| < r by W3,W4,W2,WW;
end;
suppose
W2: x1 in dom g; then
W3: h.x1 = g.x1 by FUNCT_4:13;
W4: h.x = g.x by FUNCT_4:13,FT,sy;
|.x1-x.| < s1 by O1,O2,XXREAL_0:2;
hence |.h.x1-h.x.| < r by W3,W4,W2,WW;
end;
end;
hence thesis by FCONT_1:3;
end;
suppose
B0: xx0 in ].-infty,a.[;
for N1 being Neighbourhood of h.xx0
ex N being Neighbourhood of xx0 st
for x1 being Real st x1 in dom h &
x1 in N holds h.x1 in N1
proof
let N1 be Neighbourhood of h.xx0;
set r = h.xx0;
reconsider N2 = N1 as Neighbourhood of f.xx0
by B0,Z8,xz,FUNCT_4:15,KK;
f is continuous by A1; then
consider Nx being Neighbourhood of xx0 such that
D0: for x1 being Real st x1 in dom f &
x1 in Nx holds f.x1 in N2 by FCONT_1:4,B0,Z6;
set rr = a - xx0;
Zz: xx0 + 0 < a by B0,XXREAL_1:233; then
Z1: rr > 0 by XREAL_1:20;
set rr2 = rr / 2;
set P1 = ].xx0-rr2, xx0+rr2.[;
xx0 / 2 < a / 2 by Zz,XREAL_1:74; then
z5:xx0 / 2 + a / 2 < a / 2 + a / 2 by XREAL_1:8;
P1 c= ].-infty,a.[ by XXREAL_1:263,z5; then
Y1:P1 c= dom f by Z8,xz;
reconsider P1 as Neighbourhood of xx0 by Z1,RCOMP_1:def 6;
consider N being Neighbourhood of xx0 such that
Y2:N c= Nx & N c= P1 by RCOMP_1:17;
take N;
let x1 be Real;
assume
D1:x1 in dom h & x1 in N; then
f.x1 in N2 by D0,Y2,Y1;
hence thesis by FUNCT_4:15,Y2,Y1,D1,KK;
end;
hence thesis by FCONT_1:4;
end;
suppose
B0: xx0 in ].a,b.[;
for N1 being Neighbourhood of h.xx0
ex N being Neighbourhood of xx0 st
for x1 being Real st x1 in dom h &
x1 in N holds h.x1 in N1
proof
let N1 be Neighbourhood of h.xx0;
set r = h.xx0;
reconsider N2 = N1 as Neighbourhood of g.xx0 by B0,A1,b2,FUNCT_4:13;
consider Nx being Neighbourhood of xx0 such that
D0: for x1 being Real st x1 in dom g &
x1 in Nx holds g.x1 in N2 by FCONT_1:4,B0,b2,A1;
set rr = min (xx0-a,b-xx0);
Zw: a < xx0 & xx0 < b by B0,XXREAL_1:4;
a - a < xx0 - a & b - xx0 > xx0 - xx0 by XREAL_1:14,Zw; then
Z1: rr > 0 by XXREAL_0:15;
set rr2 = rr / 2;
set P1 = ].xx0-rr2, xx0+rr2.[;
u1: rr2 < rr by Z1,XREAL_1:216;
u2: rr <= b - xx0 by XXREAL_0:17;
u3: xx0 + rr2 < xx0 + rr by u1,XREAL_1:8;
xx0 + rr <= xx0 + (b - xx0) by u2,XREAL_1:7; then
Z5: xx0 + rr2 < b by u3,XXREAL_0:2;
rr <= xx0 - a by XXREAL_0:17; then
rr2 < xx0 - a by XXREAL_0:2,u1; then
h1: xx0 - rr2 > xx0 - (xx0 - a) by XREAL_1:15;
y1: P1 c= ].a,b.[ by XXREAL_1:46,Z5,h1;
reconsider P1 as Neighbourhood of xx0 by Z1,RCOMP_1:def 6;
consider N being Neighbourhood of xx0 such that
Y2: N c= Nx & N c= P1 by RCOMP_1:17;
XX: N c= dom g by Y2,y1,b1;
take N;
let x1 be Real;
assume
D1: x1 in dom h & x1 in N;
x1 in Nx & x1 in dom g by Y2,y1,b1,D1; then
g.x1 in N2 by D0;
hence thesis by FUNCT_4:13,XX,D1;
end;
hence thesis by FCONT_1:4;
end;
suppose
B0: xx0 in ].b,+infty.[;
for N1 being Neighbourhood of h.xx0
ex N being Neighbourhood of xx0 st
for x1 being Real st x1 in dom h & x1 in N holds h.x1 in N1
proof
let N1 be Neighbourhood of h.xx0;
set r = h.xx0;
reconsider N2 = N1 as Neighbourhood of f.xx0
by B0,z6,FUNCT_4:15,A1,Asi1;
T1: f is continuous by A1;
consider Nx being Neighbourhood of xx0 such that
D0: for x1 being Real st x1 in dom f &
x1 in Nx holds f.x1 in N2 by FCONT_1:4,B0,z6,T1;
set rr = xx0 - b;
Zz: b + 0 < xx0 by B0,XXREAL_1:235; then
Z1: rr > 0 by XREAL_1:20;
set rr2 = rr / 2;
set P1 = ].xx0-rr2, xx0+rr2.[;
Z3: b / 2 < xx0 / 2 by Zz,XREAL_1:74;
xx0 / 2 + b / 2 > b / 2 + b / 2 by Z3,XREAL_1:8; then
P1 c= ].b,+infty.[ by XXREAL_1:247; then
Y1: P1 c= dom f by z8,wz;
reconsider P1 as Neighbourhood of xx0 by Z1,RCOMP_1:def 6;
consider N being Neighbourhood of xx0 such that
Y2: N c= Nx & N c= P1 by RCOMP_1:17;
take N;
let x1 be Real;
assume
D1: x1 in dom h & x1 in N; then
f.x1 in N2 by D0,Y2,Y1;
hence thesis by FUNCT_4:15,Y2,Y1,D1,KK;
end;
hence thesis by FCONT_1:4;
end;
end;
theorem
for f, g being PartFunc of REAL, REAL st
g is continuous non empty &
f = AffineMap (0,0) | (REAL \ ].a,b.[) &
dom g = [.a,b.] & g.a = 0 & g.b = 0 holds
f +* g is continuous
proof
let f, g be PartFunc of REAL, REAL;
assume g is continuous non empty &
f = AffineMap (0,0) | (REAL \ ].a,b.[) &
dom g = [.a,b.] & g.a = 0 & g.b = 0; then
consider h being PartFunc of REAL, REAL such that
A2: h = f +* g &
for x being Real st x in dom h holds h is_continuous_in x by Kluczyk;
thus thesis by A2;
end;
registration
cluster non trivial closed_interval closed for Subset of REAL;
existence
proof
take A = [.0,1.];
0 in A & 1 in A;
hence thesis by MEASURE5:def 3,ZFMISC_1:def 10;
end;
end;
begin :: Triangular and Trapezoidal Fuzzy Sets
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:
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
proof
k1: a + 0 < b by Z1;
k2: b + 0 < c by Z2;
set f1 = AffineMap (0,0) | (REAL \ ].a,c.[),
f2 = (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.]),
f3 = (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.]);
set f = f1 +* f2 +* f3;
REAL \ ].a,c.[ <> {} by RealNon,Z1,Z2,XXREAL_0:2; then
L1: rng f1 = {0} by Andr1a;
L2: rng f2 = [.0,1.] by k1,Hope1,XREAL_1:20;
L3: rng f3 = [.0,1.] by Hope2a,k2,XREAL_1:20;
rng (f1 +* f2) c= rng f1 \/ rng f2 by FUNCT_4:17; then
L5: rng (f1 +* f2) \/ rng f3 c= ({0} \/ [.0,1.]) \/ rng f3
by XBOOLE_1:13,L1,L2;
l6: rng f c= rng (f1 +* f2) \/ rng f3 by FUNCT_4:17;
[.0,0.] c= [.0,1.] by XXREAL_1:34; then
{0} c= [.0,1.] by XXREAL_1:17; then
{0} \/ [.0,1.] = [.0,1.] by XBOOLE_1:12; then
I3: rng f c= [.0,1.] by l6,L3,L5;
I5: dom f = dom (f1 +* f2) \/ dom f3 by FUNCT_4:def 1
.= dom f1 \/ dom f2 \/ dom f3 by FUNCT_4:def 1;
REAL \ ].a,c.[ c= REAL; then
i7: REAL \ ].a,c.[ c= dom AffineMap (0,0) by FUNCT_2:def 1;
O4: a < +infty & c < +infty by XXREAL_0:9,XREAL_0:def 1;
O3: a < c by Z1,Z2,XXREAL_0:2;
O5: -infty < a by XXREAL_0:12,XREAL_0:def 1;
[.a,b.] c= REAL; then
O1: [.a,b.] c= dom AffineMap (1/(b-a),-a/(b-a)) by FUNCT_2:def 1;
[.b,c.] c= REAL; then
O2: [.b,c.] c= dom AffineMap (-1/(c-b),c/(c-b)) by FUNCT_2:def 1;
dom f2 \/ dom f3 = [.a,b.] \/ dom f3 by RELAT_1:62,O1
.= [.a,b.] \/ [.b,c.] by RELAT_1:62,O2
.= [.a,c.] by XXREAL_1:165,Z1,Z2; then
dom f1 \/ (dom f2 \/ dom f3) = (REAL \ ].a,c.[) \/ [.a,c.]
by i7,RELAT_1:62
.= (].-infty,a.] \/ [.c,+infty.[) \/ [.a,c.] by XXREAL_1:398
.= ].-infty,a.] \/ ([.c,+infty.[ \/ [.a,c.]) by XBOOLE_1:4
.= ].-infty,a.] \/ [.a,+infty.[ by XXREAL_1:176,O3,O4
.= ].-infty,+infty.[ by XXREAL_1:172,O4,O5; then
dom f1 \/ dom f2 \/ dom f3 = REAL by XBOOLE_1:4,XXREAL_1:224;
hence thesis by FUNCT_2:2,I5,I3;
end;
end;
::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
for a,b,c being Real st a < b & b < c holds
TriangularFS (a,b,c) is strictly-normalized
proof
let a,b,c be Real;
set F = TriangularFS (a,b,c);
reconsider bb = b as Element of REAL by XREAL_0:def 1;
assume
Z1: a < b & b < c;
s0: bb in [.b,c.] by Z1;
S1: F = AffineMap (0,0) | (REAL \ ].a,c.[)
+* (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.])
+* (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.]) by Z1,TrDef;
s2: dom AffineMap (-1/(c-b),c/(c-b)) = REAL by FUNCT_2:def 1;
a + 0 < b by Z1; then
T1: b - a > 0 by XREAL_1:20;
b + 0 < c by Z1; then
t1: c - b > 0 by XREAL_1:20;
bb in [.b,c.] by Z1; then
bb in dom (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.]) by s2,RELAT_1:57; then
A1: F.bb = (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.]).bb by FUNCT_4:13,S1
.= (AffineMap (-1/(c-b),c/(c-b))).bb by FUNCT_1:49,s0
.= 1 by Cb1,t1;
for y being Element of REAL st F.y = 1 holds y = bb
proof
let y be Element of REAL;
assume
X0: F.y = 1;
per cases;
suppose
X1: y in [.a,b.]; then
per cases by XXREAL_1:7;
suppose
x1: y in [.a,b.[;
y in REAL; then
X3: y in dom AffineMap (1/(b-a),-a/(b-a)) by FUNCT_2:def 1;
X2: y in dom (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.])
by X3,X1,RELAT_1:57;
not y in [.b,c.] by x1,XBOOLE_0:3,XXREAL_1:95; then
not y in dom (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.])
by RELAT_1:57; then
F.y = (AffineMap (0,0) | (REAL \ ].a,c.[)
+* (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.])).y by FUNCT_4:11,S1
.= (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.]).y by FUNCT_4:13,X2; then
(AffineMap (1/(b-a),-a/(b-a))).y = 1 by X1,FUNCT_1:49,X0;
hence thesis by Hope3,T1;
end;
suppose y = b;
hence thesis;
end;
end;
suppose
X1: y in [.b,c.];
y in REAL; then
y in dom AffineMap (-1/(c-b),c/(c-b)) by FUNCT_2:def 1; then
y in dom (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.])
by X1,RELAT_1:57; then
F.y = (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.]).y
by FUNCT_4:13,S1; then
(AffineMap (-1/(c-b),c/(c-b))).y = 1 by X1,FUNCT_1:49,X0;
hence thesis by Hope4,t1;
end;
suppose
so: not (y in [.a,b.] or y in [.b,c.]); then
s1: not y in dom (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.]) &
not y in dom (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.]) by RELAT_1:57;
s8: ].a,c.[ c= [.a,c.] by XXREAL_1:25;
not y in [.a,b.] \/ [.b,c.] by so,XBOOLE_0:def 3; then
not y in [.a,c.] by XXREAL_1:165,Z1; then
s7: not y in ].a,c.[ by s8;
ss: y in REAL \ ].a,c.[ by s7,XBOOLE_0:def 5;
F.y = ((AffineMap (0,0) | (REAL \ ].a,c.[)
+* (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.]))).y by FUNCT_4:11,s1,S1
.= (AffineMap (0,0) | (REAL \ ].a,c.[)).y by FUNCT_4:11,s1
.= (AffineMap (0,0)).y by FUNCT_1:49,ss;
hence thesis by Hope5,X0;
end;
end;
hence thesis by A1;
end;
theorem
for a,b,c being Real st a < b & b < c holds
TriangularFS (a,b,c) is continuous
proof
let a,b,c be Real;
assume that
Z1: a < b and
Z2: b < c;
set F = TriangularFS (a,b,c);
S1: F = AffineMap (0,0) | (REAL \ ].a,c.[)
+* (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.])
+* (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.]) by Z1,Z2,TrDef;
set f1 = AffineMap (0,0);
set f = f1 | (REAL \ ].a,c.[);
set g1 = AffineMap (1/(b-a),-a/(b-a));
reconsider g = g1 | [.a,b.] as PartFunc of REAL, REAL;
set h1 = AffineMap (-1/(c-b),c/(c-b));
reconsider h = h1 | [.b,c.] as PartFunc of REAL, REAL;
[.a,b.] c= REAL; then
[.a,b.] c= dom g1 by FUNCT_2:def 1; then
J2: dom g = [.a,b.] by RELAT_1:62;
[.b,c.] c= REAL; then
h1: [.b,c.] c= dom h1 by FUNCT_2:def 1; then
J3: dom h = [.b,c.] by RELAT_1:62;
b in dom g by J2,Z1; then
j2: g is non empty;
b in dom h by J3,Z2; then
j3: h is non empty;
ff: for x being object st x in dom g /\ dom h holds g.x = h.x
proof
let x be object;
assume x in dom g /\ dom h; then
i1: x in {b} by XXREAL_1:418,Z1,Z2,J2,J3;
II: b in [.a,b.] & b in [.b,c.] by Z1,Z2;
a + 0 < b by Z1; then
I0: b - a > 0 by XREAL_1:20;
b + 0 < c by Z2; then
I2: c - b > 0 by XREAL_1:20;
h.x = h.b by i1,TARSKI:def 1
.= h1.b by FUNCT_1:49,II
.= 1 by Cb1, I2
.= g1.b by I0,Ab1
.= g.b by FUNCT_1:49,II
.= g.x by i1,TARSKI:def 1;
hence thesis;
end; then
fF: g tolerates h by PARTFUN1:def 4;
set gh = g +* h;
z1: dom gh = dom g \/ dom h by FUNCT_4:def 1
.= [.a,b.] \/ [.b,c.] by J2,h1,RELAT_1:62
.= [.a,c.] by XXREAL_1:165,Z1,Z2;
K2: a in [.a,b.] by Z1; then
W3: gh.a = g.a by FUNCT_4:15,PARTFUN1:def 4,ff,J2
.= g1.a by FUNCT_1:49,K2
.= 0 by Ah1;
K1: c in [.b,c.] by Z2;
c in dom h by J3,Z2; then
gh.c = h.c by FUNCT_4:13
.= h1.c by K1,FUNCT_1:49
.= 0 by Cb2; then
consider hh being PartFunc of REAL, REAL such that
TT: hh = f +* gh &
for x being Real st x in dom hh holds hh is_continuous_in x
by W3,Kluczyk,fF,z1,Glue,J2,j2,j3,J3;
hh = F by TT,FUNCT_4:14,S1;
hence thesis by TT;
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:
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
proof
k1: a + 0 < b by Z1;
k3: b < d by Z2,Z3,XXREAL_0:2;
set f1 = AffineMap (0,0) | (REAL \ ].a,d.[),
f2 = (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.]),
f3 = (AffineMap (0,1) | [.b,c.]),
f4 = (AffineMap (-1/(d-c),d/(d-c)) | [.c,d.]);
set f = f1 +* f2 +* f3 +* f4;
a < c by Z1,Z2,XXREAL_0:2; then
REAL \ ].a,d.[ <> {} by RealNon,Z3,XXREAL_0:2; then
L1: rng f1 = {0} by Andr1a;
L2: rng f2 = [.0,1.] by k1,Hope1,XREAL_1:20;
b in [.b,c.] by Z2; then
L3: rng f3 = {1} by Andr1a;
c + 0 < d by Z3; then
L4: rng f4 = [.0,1.] by Hope2a,XREAL_1:20;
Ss: rng (f1 +* f2) c= rng f1 \/ rng f2 by FUNCT_4:17;
rng (f1 +* f2 +* f3) c= rng (f1 +* f2) \/ rng f3 by FUNCT_4:17; then
d6: rng (f1 +* f2 +* f3) \/ rng f4 c=
rng (f1 +* f2) \/ rng f3 \/ rng f4 by XBOOLE_1:13;
rng f c= rng (f1 +* f2 +* f3) \/ rng f4 by FUNCT_4:17; then
l6: rng f c= rng (f1 +* f2) \/ rng f3 \/ rng f4 by d6;
[.0,0.] c= [.0,1.] by XXREAL_1:34; then
Hh: {0} c= [.0,1.] by XXREAL_1:17;
[.1,1.] c= [.0,1.] by XXREAL_1:34; then
{1} c= [.0,1.] by XXREAL_1:17; then
hx: {1} \/ [.0,1.] = [.0,1.] by XBOOLE_1:12;
ss: rng (f1 +* f2) c= [.0,1.] by Hh,Ss,L1,L2,XBOOLE_1:12;
sk: rng f c= rng (f1 +* f2) \/ [.0,1.] by hx,L3,XBOOLE_1:4,L4,l6;
rng (f1 +* f2) \/ [.0,1.] c= [.0,1.] \/ [.0,1.] by ss,XBOOLE_1:13; then
I3: rng f c= [.0,1.] by sk;
I5: dom f = dom (f1 +* f2 +* f3) \/ dom f4 by FUNCT_4:def 1
.= dom (f1 +* f2) \/ dom f3 \/ dom f4 by FUNCT_4:def 1
.= dom f1 \/ dom f2 \/ dom f3 \/ dom f4 by FUNCT_4:def 1;
REAL \ ].a,d.[ c= REAL; then
i7: REAL \ ].a,d.[ c= dom AffineMap (0,0) by FUNCT_2:def 1;
O4: a < +infty & c < +infty & d < +infty by XXREAL_0:9,XREAL_0:def 1;
a < c by Z1,Z2,XXREAL_0:2; then
O6: a < d by Z3,XXREAL_0:2;
O5: -infty < a by XXREAL_0:12,XREAL_0:def 1;
[.a,b.] c= REAL; then
O1: [.a,b.] c= dom AffineMap (1/(b-a),-a/(b-a)) by FUNCT_2:def 1;
[.b,c.] c= REAL; then
j1: [.b,c.] c= dom AffineMap (0,1) by FUNCT_2:def 1;
[.c,d.] c= REAL; then
OO: [.c,d.] c= dom AffineMap (-1/(d-c),d/(d-c)) by FUNCT_2:def 1;
d2: dom f3 \/ dom f4 = [.b,c.] \/ dom f4 by j1,RELAT_1:62
.= [.b,c.] \/ [.c,d.] by RELAT_1:62,OO
.= [.b,d.] by XXREAL_1:165,Z2,Z3;
d3: dom f2 \/ dom f3 \/ dom f4 = dom f2 \/ (dom f3 \/ dom f4) by XBOOLE_1:4
.= [.a,b.] \/ [.b,d.] by d2,O1,RELAT_1:62
.= [.a,d.] by XXREAL_1:165,k3,Z1;
dom f1 \/ (dom f2 \/ dom f3) \/ dom f4 =
dom f1 \/ ((dom f2 \/ dom f3) \/ dom f4) by XBOOLE_1:4
.= (REAL \ ].a,d.[) \/ [.a,d.] by d3,i7,RELAT_1:62
.= (].-infty,a.] \/ [.d,+infty.[) \/ [.a,d.] by XXREAL_1:398
.= ].-infty,a.] \/ ([.d,+infty.[ \/ [.a,d.]) by XBOOLE_1:4
.= ].-infty,a.] \/ [.a,+infty.[ by XXREAL_1:176,O4,O6
.= ].-infty,+infty.[ by XXREAL_1:172,O4,O5; then
dom f1 \/ dom f2 \/ dom f3 \/ dom f4 = REAL by XBOOLE_1:4,XXREAL_1:224;
hence thesis by FUNCT_2:2,I5,I3;
end;
end;
theorem
for a,b,c,d being Real st a < b & b < c & c < d holds
TrapezoidalFS (a,b,c,d) is normalized
proof
let a,b,c,d be Real;
set F = TrapezoidalFS (a,b,c,d);
reconsider bb = c as Element of REAL by XREAL_0:def 1;
assume
Z1: a < b & b < c & c < d;
s0: bb in [.c,d.] by Z1;
S1: F = 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.]) by Z1,TPDef;
s2: dom AffineMap (-1/(d-c),d/(d-c)) = REAL by FUNCT_2:def 1;
c + 0 < d by Z1; then
t1: d - c > 0 by XREAL_1:20;
bb in [.c,d.] by Z1; then
bb in dom (AffineMap (-1/(d-c),d/(d-c)) | [.c,d.]) by s2,RELAT_1:57; then
F.bb = (AffineMap (-1/(d-c),d/(d-c)) | [.c,d.]).bb by FUNCT_4:13,S1
.= (AffineMap (-1/(d-c),d/(d-c))).bb by FUNCT_1:49,s0
.= 1 by Cb1,t1;
hence thesis;
end;
theorem
for a,b,c,d being Real st a < b & b < c & c < d holds
TrapezoidalFS (a,b,c,d) is continuous
proof
let a,b,c,d be Real;
assume that
Z1: a < b and
Z2: b < c and
Z3: c < d;
set F = TrapezoidalFS (a,b,c,d);
S1: F = 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.]) by Z1,Z2,Z3,TPDef;
set f1 = AffineMap (0,0);
set f = f1 | (REAL \ ].a,d.[);
set g1 = AffineMap (1/(b-a),-a/(b-a));
reconsider g = g1 | [.a,b.] as PartFunc of REAL, REAL;
set h1 = AffineMap (-1/(d-c),d/(d-c));
reconsider h = h1 | [.c,d.] as PartFunc of REAL, REAL;
set i1 = AffineMap (0,1);
reconsider i = i1 | [.b,c.] as PartFunc of REAL, REAL;
[.a,b.] c= REAL; then
d9: [.a,b.] c= dom g1 by FUNCT_2:def 1; then
J2: dom g = [.a,b.] by RELAT_1:62;
[.c,d.] c= REAL; then
d3: [.c,d.] c= dom h1 by FUNCT_2:def 1; then
J3: dom h = [.c,d.] by RELAT_1:62;
[.b,c.] c= REAL; then
d8: [.b,c.] c= dom i1 by FUNCT_2:def 1; then
JW: dom i = [.b,c.] by RELAT_1:62;
b in dom g by J2,Z1; then
j2: g is non empty;
c in dom h by J3,Z3; then
j3: h is non empty;
ff: for x being object st x in dom g /\ dom i holds g.x = i.x
proof
let x be object;
assume x in dom g /\ dom i; then
i1: x in {b} by XXREAL_1:418,Z1,Z2,J2,JW;
II: b in [.a,b.] & b in [.b,c.] by Z1,Z2;
a + 0 < b by Z1; then
I0: b - a > 0 by XREAL_1:20;
i.x = i.b by i1,TARSKI:def 1
.= i1.b by FUNCT_1:49,II
.= 1 by Kici1
.= g1.b by I0,Ab1
.= g.b by FUNCT_1:49,II
.= g.x by i1,TARSKI:def 1;
hence thesis;
end;
set gh = g +* i;
z1: dom gh = dom g \/ dom i by FUNCT_4:def 1
.= [.a,b.] \/ [.b,c.] by d9,RELAT_1:62,JW
.= [.a,c.] by XXREAL_1:165,Z1,Z2;
V5: a < c by XXREAL_0:2,Z1,Z2; then
PS: a in dom gh by z1; then
reconsider gh as non empty PartFunc of REAL, REAL;
K2: a in [.a,b.] by Z1; then
W3: gh.a = g.a by FUNCT_4:15,PARTFUN1:def 4,ff,J2
.= g1.a by FUNCT_1:49,K2
.= 0 by Ah1;
P3: c in [.b,c.] by Z2;
K1: c in [.c,d.] by Z3;
N3: dom h = [.c,d.] by d3,RELAT_1:62;
c + 0 < d by Z3; then
MN: d - c > 0 by XREAL_1:20;
N4: h.c = h1.c by FUNCT_1:49,K1
.= 1 by Cb1,MN;
KK: d in [.c,d.] by Z3; then
N5: h.d = h1.d by FUNCT_1:49
.= 0 by Cb2;
NN: gh is continuous by Glue,ff,j2,J2,JW,d8,P3,PARTFUN1:def 4;
M1: for x being object st x in dom gh /\ dom h holds gh.x = h.x
proof
let x be object;
assume x in dom gh /\ dom h; then
ll: x in {c} by XXREAL_1:418,Z3,V5,J3,z1; then
gh.x = gh.c by TARSKI:def 1
.= i.c by FUNCT_4:13,P3,JW
.= i1.c by FUNCT_1:49,P3
.= h.c by N4,Kici1
.= h.x by ll,TARSKI:def 1;
hence thesis;
end; then
fG: gh tolerates h by PARTFUN1:def 4;
set ghi = gh +* h;
V3: dom ghi = dom gh \/ dom h by FUNCT_4:def 1
.= [.a,c.] \/ [.c,d.] by z1,d3,RELAT_1:62
.= [.a,d.] by XXREAL_1:165,Z3,V5;
V4: ghi.a = 0 by FUNCT_4:15,M1,PARTFUN1:def 4,PS,W3;
ghi.d = 0 by N3,FUNCT_4:13,KK,N5; then
consider hh being PartFunc of REAL, REAL such that
TT: hh = f +* ghi &
for x being Real st x in dom hh holds hh is_continuous_in x
by Kluczyk,V3,V4,Glue,NN,j3,z1,J3,fG;
hh = f +* (g +* i) +* h by FUNCT_4:14,TT
.= f +* g +* i +* h by FUNCT_4:14;
hence thesis by TT,S1;
end;
definition let F be FuzzySet of REAL;
attr F is triangular means
ex a,b,c being Real st F = TriangularFS (a,b,c);
attr F is trapezoidal means
ex a,b,c,d being Real st F = TrapezoidalFS (a,b,c,d);
end;
registration
cluster triangular for FuzzySet of REAL;
existence
proof
take TriangularFS (0,1,2);
thus thesis;
end;
cluster trapezoidal for FuzzySet of REAL;
existence
proof
take TrapezoidalFS (0,1,2,3);
thus thesis;
end;
end;