:: Triangular Fuzzy Set Composed of Two Intersecting Affine Maps
:: by Takashi Mitsuishi
::
:: Received December 2, 2025
:: Copyright (c) 2025-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 4.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/4.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SUBSET_1, XXREAL_1, CARD_1, RELAT_1, FUNCT_1,
XXREAL_0, PARTFUN1, ARYTM_1, ARYTM_3, COMPLEX1, MEASURE5, FUZNUM_1,
REAL_1, ORDINAL2, XXREAL_2, JGRAPH_2, FUNCT_4, FCONT_1, INTEGRA5, SEQ_4,
VALUED_1, INTEGRA1, RFUNCT_3, FUZZY_6;
notations XBOOLE_0, SUBSET_1, RELAT_1, NUMBERS, XCMPLX_0, XXREAL_0, COMPLEX1,
XREAL_0, FUNCT_1, RELSET_1, VALUED_1, MEASURE5, PARTFUN1, FUNCT_2,
FCONT_1, FUNCT_3, INTEGRA1, RFUNCT_3, FUNCT_4, COMSEQ_2, SEQ_4, RCOMP_1,
INTEGRA5, FUZNUM_1, FUZZY_6;
constructors SEQ_4, RELSET_1, FCONT_1, FUNCT_4, FUZNUM_1, COMSEQ_2, NEWTON,
RFUNCT_3, INTEGRA1, INTEGRA5, FUZZY_6;
registrations RELSET_1, NUMBERS, XXREAL_0, MEMBERED, XBOOLE_0, VALUED_0,
VALUED_1, FUNCT_2, XREAL_0, ORDINAL1, FCONT_1, RELAT_1, FUNCT_1,
XCMPLX_0, NAT_1, FUZNUM_1, INTEGRA1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities RCOMP_1, INTEGRA5;
expansions FCONT_1, INTEGRA5;
theorems TARSKI, XBOOLE_0, FUNCT_1, PARTFUN1, XBOOLE_1, COMPLEX1, XREAL_1,
XXREAL_0, XXREAL_1, FUNCT_2, RELAT_1, XREAL_0, FCONT_1, XCMPLX_1,
FUNCT_4, VALUED_1, INTEGRA1, INTEGRA5, RFUNCT_3, SEQ_4, COMSEQ_2,
FUZZY_6, FUZNUM_1, FUZZY_7, FUZZY_8, MESFUN6C;
begin :: Triangular Fuzzy Set
Le1:
for p,s being Real st p > 0 & p * s < 0 holds p - s > 0
proof
let p,s be Real such that
A0: p > 0 and
A1: p*s < 0;
s < 0/p by A0,A1;
hence thesis by A0;
end;
theorem Th101:
for p,q,s,t being Real st p > 0 & p*s < 0 holds
t > q iff (t-q)/(p-s) > 0
proof
let p,q,s,t be Real such that
A1: p > 0 and
A2: p*s < 0;
A5s: s < 0/p by A1,A2;
thus t > q implies (t-q)/(p-s) > 0
proof
assume t > q;
then t-q > q-q by XREAL_1:9;
hence thesis by A5s,A1;
end;
assume (t-q)/(p-s) > 0;
then t-q > 0 by A5s,A1;
then t-q+q > 0+q by XREAL_1:6;
hence thesis;
end;
theorem
for p,q,s,t being Real st p > 0 & p*s < 0 holds
t < q iff (t-q)/(p-s) < 0
proof
let p,q,s,t be Real such that
A0: p > 0 and
A1: p*s < 0;
thus t < q implies (t-q)/(p-s) < 0
proof
assume t < q;
then (q -t)/(p-s) > 0 by Th101,A0,A1;
then -(q -t)/(p-s) < 0;
then (-(q -t))/(p-s) < 0 by XCMPLX_1:187;
hence thesis;
end;
assume A2:(t-q)/(p-s) < 0;
s < 0/p by A0,A1; then
t-q < 0 by A0,A2;
then t - q + q < 0 + q by XREAL_1:6;
hence thesis;
end;
theorem
for p,q,s,t being Real st
p > 0 & p*s < 0 holds
(p*t-q*s)/(p-s) < 0 iff -q/p > -t/s
proof
let p,q,s,t be Real such that
A0: p > 0 and
A2: p*s < 0;
A4: s < 0 by A0,A2;
thus (p*t-q*s)/(p-s) < 0 implies -q/p > -t/s
proof
assume
A3:(p*t-q*s)/(p-s) < 0;
p-s > 0 by Le1,A0,A2; then
p*t-q*s < 0 by A3; then
p*t-q*s-p*t < 0-p*t by XREAL_1:9; then
(-p)*t/s < (-q)*s/s by A4,XREAL_1:75; then
(-p)*t/s < (-q)*(s/s) by XCMPLX_1:74; then
-q > (-p)*t/s by A4,XCMPLX_1:88; then
(-q)/p > ((-p)*t/s)/p by A0,XREAL_1:74; then
(-q)/p > ((t/s)*(-p))/p by XCMPLX_1:74; then
(-q)/p > (t/s)*((-p)/p) by XCMPLX_1:74; then
(-q)/p > (t/s)*(-(p/p)) by XCMPLX_1:187; then
-q/p > -(t/s)*((p/p)) by XCMPLX_1:187;
hence thesis by XCMPLX_1:88,A0;
end;
assume -q/p > -t/s; then
(-q/p)*p > (-t/s)*p by XREAL_1:68,A0; then
(-q)/p*p > -t/s*p by XCMPLX_1:187; then
-q > (-t/s)*p by XCMPLX_1:87,A0; then
((-t/s)*p)*s > (-q)*s by XREAL_1:69,A4; then
((-t/s)*s)*p > (-q)*s; then
((-t)/s*s)*p > (-q)*s by XCMPLX_1:187; then
(-t)*p > (-q)*s by XCMPLX_1:87,A4; then
A8:(-t)*p - (-t)*p > (-q)*s - (-t)*p by XREAL_1:9;
p-s > 0 by Le1,A0,A2;
hence thesis by A8;
end;
theorem
for p,q,s,t being Real st
p > 0 & p*s < 0 holds
(p*t-q*s)/(p-s) > 0 iff -q/p < -t/s
proof
let p,q,s,t be Real such that
A0: p > 0 and
A2: p*s < 0;
A4: s < 0 by A0,A2;
thus (p*t-q*s)/(p-s) > 0 implies -q/p < -t/s
proof
assume A3: (p*t-q*s)/(p-s) > 0;
p-s > 0 by Le1,A0,A2; then
(p*t-q*s) > 0 by A3; then
p*t-q*s-p*t > 0-p*t by XREAL_1:9; then
(-p)*t/s > (-q)*s/s by A4,XREAL_1:75; then
(-p)*t/s > (-q)*(s/s) by XCMPLX_1:74; then
-q < (-p)*t/s by A4,XCMPLX_1:88; then
(-q)/p < ((-p)*t/s)/p by A0,XREAL_1:74; then
(-q)/p < ((t/s)*(-p))/p by XCMPLX_1:74; then
(-q)/p < (t/s)*((-p)/p) by XCMPLX_1:74; then
(-q)/p < (t/s)*(-(p/p)) by XCMPLX_1:187; then
-q/p < -(t/s)*((p/p)) by XCMPLX_1:187;
hence thesis by XCMPLX_1:88,A0;
end;
assume -q/p < -t/s; then
(-q/p)*p < (-t/s)*p by XREAL_1:68,A0; then
(-q)/p*p < -t/s*p by XCMPLX_1:187; then
-q < (-t/s)*p by XCMPLX_1:87,A0; then
((-t/s)*p)*s < (-q)*s by XREAL_1:69,A4; then
((-t/s)*s)*p < (-q)*s; then
((-t)/s*s)*p < (-q)*s by XCMPLX_1:187; then
(-t)*p < (-q)*s by XCMPLX_1:87,A4; then
A8:(-t)*p - (-t)*p < (-q)*s - (-t)*p by XREAL_1:9;
p-s > 0 by Le1,A0,A2;
hence thesis by A8;
end;
Th14:
for p,q,s,t being Real st p*s < 0 & p > 0 holds
(t-q)/(p-s) + t/s = (1/s)*((t*p-q*s)/(p-s)) &
(t-q)/(p-s) + q/p = (1/p)*((t*p-q*s)/(p-s))
proof
let p,q,s,t be Real;
assume
A2: p*s < 0 & p > 0; then
A7: p-s <> 0;
s < 0 by A2; then
PS: (t-q)/(p-s) + t/s
= ((t-q)*s + t*(p-s))/((p-s)*s) by XCMPLX_1:116,A2
.= (1/s)*((t*p-q*s)/(p-s)) by XCMPLX_1:103;
(t-q)/(p-s) + q/p
= ((t-q)*p + q*(p-s))/((p-s)*p) by XCMPLX_1:116,A7,A2
.= (t*p-q*s)/((p-s)*p);
hence thesis by XCMPLX_1:103,PS;
end;
theorem Th3:
for a, b being Real holds
a in REAL \ ].a,b.[ & b in REAL \ ].a,b.[
proof
let a, b be Real;
a <= a & -infty < a by XXREAL_0:12,XREAL_0:def 1;
then
a in ].-infty,a.]; then
a in ].-infty,a.] \/ [.b,+infty.[ by XBOOLE_0:def 3;
hence a in REAL \ ].a,b.[ by XXREAL_1:398;
b <= b & b < +infty by XXREAL_0:9,XREAL_0:def 1;
then
b in [.b,+infty.[; then
b in ].-infty,a.] \/ [.b,+infty.[ by XBOOLE_0:def 3;
hence b in REAL \ ].a,b.[ by XXREAL_1:398;
end;
theorem Th5:
for a, b, c, d being Real st a < b & b < c & c < d holds
(REAL \ ].a,d.[) /\ [.b,c.] = {}
proof
let a, b, c, d be Real;
assume A1:a < b & b < c & c < d;
thus (REAL \ ].a,d.[) /\ [.b,c.]
= (].-infty,a.] \/ [.d,+infty.[) /\ [.b,c.] by XXREAL_1:398
.= (].-infty,a.] /\ [.b,c.]) \/ ([.d,+infty.[ /\ [.b,c.]) by XBOOLE_1:23
.= {} \/ ([.d,+infty.[ /\ [.b,c.]) by XBOOLE_0:def 7,XXREAL_1:280,A1
.= {} by XBOOLE_0:def 7,XXREAL_1:277,A1;
end;
theorem
for p,q,s,t being Real st s <> p holds
AffineMap (p,q). ((t-q)/(p-s)) = AffineMap (s,t). ((t-q)/(p-s)) &
AffineMap (s,t). ((t-q)/(p-s)) = (p*t-q*s)/(p-s)
proof
let p,q,s,t be Real;
assume s <> p; then
A1: p - s <> 0;
A2: AffineMap (s,t). ((t-q)/(p-s))
= s*((t-q)/(p-s)) + t by FCONT_1:def 4
.= s*(t-q)/(p-s) + t by XCMPLX_1:74
.= s*(t-q)/(p-s) + t*((p-s)/(p-s)) by XCMPLX_1:88,A1
.= s*(t-q)/(p-s) + t*(p-s)/(p-s) by XCMPLX_1:74
.= (s*(t-q) + t*(p-s))/(p-s) by XCMPLX_1:62
.= (s*t-s*q + t*p-t*s)/(p-s);
AffineMap (p,q). ((t-q)/(p-s))
= p*((t-q)/(p-s)) + q by FCONT_1:def 4
.= p*(t-q)/(p-s) + q by XCMPLX_1:74
.= p*(t-q)/(p-s) + q *((p-s)/(p-s)) by XCMPLX_1:88,A1
.= p*(t-q)/(p-s) + q *(p-s)/(p-s) by XCMPLX_1:74
.= (p*(t-q) + q *(p-s))/(p-s) by XCMPLX_1:62
.= (p*t-p*q + q*p-q*s)/(p-s);
hence thesis by A2;
end;
theorem Th13:
for p,q,s,t being Real st p*s < 0 & p > 0 & (p*t-q*s)/(p-s) > 0
holds -q/p < (t-q)/(p-s) & (t-q)/(p-s) < -t/s & -q/p < -t/s
proof
let p,q,s,t be Real;
assume A2: p*s < 0 & p > 0; then
A7: p-s <> 0;
assume A3: (p*t-q*s)/(p-s) > 0;
A8:(t-q)/(p-s) + q/p
= ((t-q)*p + q*(p-s))/((p-s)*p) by XCMPLX_1:116,A7,A2
.= (1/p)*((t*p-q*s)/(p-s)) by XCMPLX_1:103;
A5s: (t-q)/(p-s) + q/p -q/p > 0 -q/p by XREAL_1:9,A8,A3,A2;
A9: s < 0 by A2; then
A10: (t-q)/(p-s) + t/s
= ((t-q)*s + t*(p-s))/((p-s)*s) by A2,XCMPLX_1:116
.= (1/s)*((t*p-q*s)/(p-s)) by XCMPLX_1:103;
(t-q)/(p-s) +t/s -t/s < 0 -t/s by XREAL_1:9,A10,A3,A9;
hence thesis by A5s,XXREAL_0:2;
end;
theorem Th500:
for r be Real, C,U being Subset of REAL,
f,g be Function of REAL,REAL holds
r (#) ((f | C) +* (g | U)) =
(r (#) (f | C)) +* (r (#) (g | U))
proof
let r be Real, C,U be Subset of REAL,
f,g be Function of REAL,REAL;
set f1 = r (#) ((f | C) +* (g | U));
set f2 = (r (#) (f | C)) +* (r (#) (g | U));
A3: dom f1 = dom ((f | C) +* (g | U)) by VALUED_1:def 5
.= dom ((f | C)) \/ dom(g | U) by FUNCT_4:def 1
.= C \/ dom(g | U) by FUNCT_2:def 1
.= C \/ U by FUNCT_2:def 1;
A1s:dom f2 = dom(r (#) (f | C)) \/ dom(r (#) (g | U))
by FUNCT_4:def 1
.= dom( (f | C)) \/ dom(r (#) (g | U)) by VALUED_1:def 5
.= dom( (f | C)) \/ dom((g | U)) by VALUED_1:def 5
.= C \/ dom((g | U)) by FUNCT_2:def 1
.= C \/ U by FUNCT_2:def 1;
for x being object st x in dom f1 holds f1 . x = f2 . x
proof
let x be object;
assume x in dom f1; then
reconsider x as Real by A3;
per cases;
suppose B1:x in U; then
B11: x in dom (g | U) by FUNCT_2:def 1;
B12: x in dom (r (#) (g | U)) by FUNCT_2:def 1,B1;
f1 . x = r * (((f | C) +* (g | U)).x) by VALUED_1:6
.= r*( (g | U).x ) by B11,FUNCT_4:13
.= (r (#) (g | U)).x by VALUED_1:6
.= f2.x by FUNCT_4:13,B12;
hence thesis;
end;
suppose B2: not x in U; then
B21: not x in dom(g | U);
B22: not x in dom (r (#) (g | U)) by B2;
f1 . x = r * (((f | C) +* (g | U)).x) by VALUED_1:6
.= r*( (f | C).x ) by B21,FUNCT_4:11
.= (r (#) (f | C)).x by VALUED_1:6
.= f2.x by B22,FUNCT_4:11;
hence thesis;
end;
end;
hence thesis by FUNCT_1:2,A1s,A3;
end;
:: ' centroid ' and area of continuous function
theorem FUZZY817: ::: see FUZZY_8:17
for f,g,h be Function of REAL,REAL, a,b,c be Real st
a <= b & b <= c & f is continuous & g is continuous &
h | [.a,c.] = f | [.a,b.] +* g | [.b,c.] &
integral(f,['a,b']) <> 0 & integral(g,['b,c']) <> 0 & f.b = g.b holds
centroid(h, ['a,c']) = 1 / integral(h,['a,c'])
* ( integral((id REAL)(#)f,['a,b']) + integral((id REAL)(#)g,['b,c']) )
proof
let f,g,h be Function of REAL,REAL, a,b,c be Real;
assume that
A1: a <= b & b <= c & f is continuous & g is continuous and
A2: h | [.a,c.] = f | [.a,b.] +* g | [.b,c.] and
A3: integral(f,['a,b']) <> 0 & integral(g,['b,c']) <> 0 and
A4: f.b = g.b;
thus
centroid(h, ['a,c']) = 1 / integral(h,['a,c'])
* ( centroid(f, ['a,b']) * integral(f,['a,b'])
+ centroid(g, ['b,c']) * integral(g,['b,c']) ) by FUZZY_8:17,A1,A2,A3,A4
.=1 / integral(h,['a,c'])
* ( integral((id REAL)(#)f,['a,b'])/integral(f,['a,b']) * integral(f,['a,b'])
+ centroid(g, ['b,c']) * integral(g,['b,c']) ) by FUZZY_6:def 1
.=1 / integral(h,['a,c'])
* ( integral((id REAL)(#)f,['a,b'])/integral(f,['a,b']) * integral(f,['a,b'])
+ integral((id REAL)(#)g,['b,c'])/integral(g,['b,c']) * integral(g,['b,c']) )
by FUZZY_6:def 1
.=1 / integral(h,['a,c']) * ( integral((id REAL)(#)f,['a,b'])
+ integral((id REAL)(#)g,['b,c'])/integral(g,['b,c']) * integral(g,['b,c']) )
by XCMPLX_1:87,A3
.=1 / integral(h,['a,c']) * ( integral((id REAL)(#)f,['a,b'])
+ integral((id REAL)(#)g,['b,c']) )
by XCMPLX_1:87,A3;
end;
:: TriangularFS by AffineMap (p,q) and AffineMap (s,t)
::
:: \ / y = p*x + q
:: \ /
:: \ /
:: / \ ( (t-q)/(p-s),(p*t-q*s)/(p-s) )
:: / \
:: / \ y = s*x + t
:: / \
::--------------------------
::- q/p - s/t
:: TriangularFS (a,b,c)
::
:: r ---- /\
:: / | \
:: / | \
:: / | \
:: / | \
::------------------------
:: a b c
theorem Th4:
for a,b,c be Real st a < b & b < c holds
TriangularFS (a,b,c) | [.a,c.]
= AffineMap (1 / (b - a), -(a / (b - a))) | [.a,b.]
+* AffineMap (- (1 / (c - b)), c / (c - b)) | [.b,c.]
proof
let a,b,c be Real;
assume
A1: a < b & b < c;
set fac = ( AffineMap (1 / (b - a), -(a / (b - a)))) | [.a,b.]
+* ( AffineMap (- (1 / (c - b)), c / (c - b))) | [.b,c.];
A6: dom fac
= dom (( AffineMap (1 / (b - a), -(a / (b - a)))) | [. a,b .])
\/ dom (( AffineMap (- (1 / (c - b)), c / (c - b))) | [. b,c .])
by FUNCT_4:def 1
.= [. a,b .] \/
dom (( AffineMap (- (1 / (c - b)), c / (c - b))) | [. b,c .])
by FUNCT_2:def 1
.= [. a,b .] \/ [. b,c .] by FUNCT_2:def 1
.= [. a,c .] by XXREAL_1:165,A1
.= dom (TriangularFS (a,b,c) | [.a,c.]) by FUNCT_2:def 1;
for x being object st x in dom (TriangularFS (a,b,c) | [.a,c.]) holds
(TriangularFS (a,b,c) | [.a,c.]) . x = fac . x
proof
let x be object;
assume A7: x in dom (TriangularFS (a,b,c) | [.a,c.]); then
reconsider x as Real;
(TriangularFS (a,b,c)| [.a,c.] ).x
= (TriangularFS (a,b,c) ).x by FUNCT_1:49,A7
.=( (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +*
((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +*
((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) ).x
by A1,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.] ))).x
by FUNCT_4:14;
hence thesis by FUNCT_4:13,A6,A7;
end;
hence thesis by FUNCT_1:2,A6;
end;
theorem
for a,b,c,r be Real, f be Function of REAL,REAL st a < b & b < c
holds
(r (#) TriangularFS (a,b,c)) | [.a,c.]
= (r (#) AffineMap (1 / (b - a), -(a / (b - a)))) | [.a,b.]
+* (r (#) AffineMap (- (1 / (c - b)), c / (c - b))) | [.b,c.]
proof
let a,b,c,r be Real, f be Function of REAL,REAL;
set fab = AffineMap (1 / (b - a), -(a / (b - a)));
set fbc = AffineMap (- (1 / (c - b)), c / (c - b));
assume A2: a < b & b < c;
hence
(r (#) TriangularFS (a,b,c)) | [.a,c.]
= (r (#) TriangularFS (a,b,c)) | ['a,c'] by XXREAL_0:2,INTEGRA5:def 3
.= r (#) (TriangularFS (a,b,c) | ['a,c']) by FUZZY_7:10
.= r (#) (TriangularFS (a,b,c) | [.a,c.]) by A2,XXREAL_0:2,INTEGRA5:def 3
.= r (#) (AffineMap (1 / (b - a), -(a / (b - a))) | [.a,b.]
+* AffineMap (- (1 / (c - b)), c / (c - b)) | [.b,c.]) by Th4,A2
.= (r (#) fab | [.a,b.]) +* (r (#) fbc | [.b,c.]) by Th500
.= (r (#) fab | ['a,b']) +* (r (#) fbc | [.b,c.]) by A2,INTEGRA5:def 3
.= (r (#) fab | ['a,b']) +* (r (#) fbc | ['b,c']) by A2,INTEGRA5:def 3
.= (r (#) fab) | ['a,b'] +* (r (#) fbc | ['b,c']) by FUZZY_7:10
.= (r (#) fab) | ['a,b'] +* (r (#) fbc) | ['b,c'] by FUZZY_7:10
.= (r (#) fab) | ['a,b'] +* (r (#) fbc) | [.b,c.] by A2,INTEGRA5:def 3
.= (r (#) fab) | [.a,b.] +* (r (#) fbc) | [.b,c.] by A2,INTEGRA5:def 3;
end;
theorem Th7:
for a,b,c,r be Real, f be Function of REAL,REAL st a < b & b < c &
for x being Real holds f.x = (r (#) TriangularFS (a,b,c)).x holds
f | [.a,c.] = (r (#) AffineMap (1 / (b - a), -(a / (b - a)))) | [.a,b.]
+* (r (#) AffineMap (- (1 / (c - b)), c / (c - b))) | [.b,c.]
proof
let a,b,c,r be Real, f be Function of REAL,REAL;
assume that
A1: a < b & b < c and
A3: for x being Real holds f.x = (r (#) TriangularFS (a,b,c)).x;
set fac = (r (#) AffineMap (1 / (b - a), -(a / (b - a)))) | [.a,b.]
+* (r (#) AffineMap (- (1 / (c - b)), c / (c - b))) | [.b,c.];
A6: dom fac
= dom ((r (#) AffineMap (1 / (b - a), -(a / (b - a)))) | [. a,b .])
\/ dom ((r (#) AffineMap (- (1 / (c - b)), c / (c - b))) | [. b,c .])
by FUNCT_4:def 1
.= [. a,b .] \/
dom ((r (#) AffineMap (- (1 / (c - b)), c / (c - b))) | [. b,c .])
by FUNCT_2:def 1
.= [. a,b .] \/ [. b,c .] by FUNCT_2:def 1
.= [. a,c .] by XXREAL_1:165,A1
.= dom (f | [.a,c.]) by FUNCT_2:def 1;
for x being object st x in dom (f | [.a,c.]) holds
(f | [.a,c.]) . x = fac . x
proof
let x be object;
assume A7: x in dom (f | [.a,c.]); then
reconsider x as Real;
set F = AffineMap (1 / (b - a), -(a / (b - a)));
(f | [.a,c.]) . x = f.x by A7,FUNCT_1:49
.= (r (#) TriangularFS (a,b,c)).x by A3
.= r * (TriangularFS (a,b,c).x) by VALUED_1:6
.= r * ((TriangularFS (a,b,c) | [.a,c.]).x) by A7,FUNCT_1:49
.= r * (((AffineMap (1 / (b - a), -(a / (b - a)))) | [.a,b.]
+* (AffineMap (- (1 / (c - b)), c / (c - b))) | [.b,c.]).x)
by A1,Th4
.= (r (#) (((AffineMap (1 / (b - a), -(a / (b - a)))) | [.a,b.]
+* (AffineMap (- (1 / (c - b)), c / (c - b))) | [.b,c.]))).x
by VALUED_1:6
.= ( ( r (#) (AffineMap (1 / (b - a), -(a / (b - a))) | [.a,b.]) )
+* (r (#) (AffineMap (- (1 / (c - b)), c/(c - b) ) | [.b,c.]) )) .x
by Th500
.= ((r (#) F) | [.a,b.]
+* (r (#) (AffineMap (- (1 / (c - b)), c/(c - b) ) | [.b,c.]) )) .x
by MESFUN6C:41
.= ((r (#) F) | [.a,b.]
+* (r (#) AffineMap (- (1 / (c - b)), c/(c - b)) ) | [.b,c.] ) .x
by MESFUN6C:41;
hence thesis;
end;
hence thesis by FUNCT_1:2,A6;
end;
theorem
for p,q,s,t being Real, f being Function of REAL,REAL st
p*s < 0 & p > 0 & (p*t-q*s)/(p-s) > 0 holds
( AffineMap (p,q) | [.-q/p,(t-q)/(p-s).] ) +*
( AffineMap (s,t) | [.(t-q)/(p-s),-t/s.] )
= ((p*t-q*s)/(p-s)) (#) (TriangularFS(-q/p,(t-q)/(p-s),-t/s)|[.-q/p,-t/s.])
proof
let p,q,s,t be Real, f be Function of REAL,REAL;
assume that
A2: p*s < 0 & p > 0 and
A3: (p*t-q*s)/(p-s) > 0;
set r = (p*t-q*s)/(p-s);
set b = (t-q)/(p-s);
set f = ((p*t-q*s)/(p-s)) (#) TriangularFS(-q/p,(t-q)/(p-s),-t/s);
A7: p-s <> 0 by A2;
A4: for x being Real holds
f.x = (((p*t-q*s)/(p-s)) (#) TriangularFS(-q/p,(t-q)/(p-s),-t/s)).x;
A8:(t-q)/(p-s) + q/p
= ((t-q)*p + q*(p-s))/((p-s)*p) by XCMPLX_1:116,A7,A2
.= (1/p)*((t*p-q*s)/(p-s)) by XCMPLX_1:103;
A5: -q/p < (t-q)/(p-s) by Th13,A2,A3;
A9: s < 0 by A2; then
A10: (t-q)/(p-s) + t/s
= ((t-q)*s + t*(p-s))/((p-s)*s) by XCMPLX_1:116,A2
.= (1/s)*((t*p-q*s)/(p-s)) by XCMPLX_1:103;
A6: (t-q)/(p-s) < -t/s by Th13,A2,A3;
A11: -q/p < -t/s by Th13,A2,A3;
B1: r*(1 / (b - (-q/p)))
= r*(1 / ( r/p )) by XCMPLX_1:99,A8
.= r* (p/r) by XCMPLX_1:57
.= p by XCMPLX_1:87,A3;
B2: r*(-((-q/p) / (b - (-q/p))))
= r*(-((-q/p) / ( r/p ))) by XCMPLX_1:99,A8
.= -r*( (-(q/p)) / (r/p) )
.= -r*(- ((q/p) / (r/p)) ) by XCMPLX_1:187
.= r*( (q/p) / (r/p) )
.= r*(q/r) by XCMPLX_1:55,A2
.= q by XCMPLX_1:87,A3;
B3: r*(- (1 / ((-t/s) - b)))
= r*(- (1 / -((t/s + b)) ))
.= r*(- (-1 / ((1/s)*(r)))) by XCMPLX_1:188,A10
.= r*( 1 / (r/s) ) by XCMPLX_1:99
.= r*( s/r ) by XCMPLX_1:57
.= s by XCMPLX_1:87,A3;
B4: r*((-t/s) / ((-t/s) - b))
= r*( (-t/s) / -(((t/s) + b)) )
.= r*( -(-t/s) / ((1/s)*r) ) by XCMPLX_1:188,A10
.= r*( -(-t/s) / (r/s) ) by XCMPLX_1:99
.= r*( -(-(t/s) / (r/s)) ) by XCMPLX_1:187
.= r*(t/r) by XCMPLX_1:55,A9
.= t by XCMPLX_1:87,A3;
((p*t-q*s)/(p-s)) (#) (TriangularFS(-q/p,(t-q)/(p-s),-t/s) | [.-q/p,-t/s.] )
= ((p*t-q*s)/(p-s)) (#) (TriangularFS(-q/p,(t-q)/(p-s),-t/s) | ['-q/p,-t/s'] )
by INTEGRA5:def 3,A11
.= ( ((p*t-q*s)/(p-s)) (#) TriangularFS(-q/p,(t-q)/(p-s),-t/s) )
| ['-q/p,-t/s'] by FUZZY_7:10
.= f | [.-q/p,-t/s.] by INTEGRA5:def 3,A11
.= (r (#) AffineMap (1 / (b - (-q/p)), -((-q/p) / (b - (-q/p)))))
| [.-q/p,(t-q)/(p-s).]
+* (r (#) AffineMap (- (1 / ((-t/s) - b)), (-t/s) / ((-t/s) - b)))
| [.(t-q)/(p-s),-t/s.] by A4,A5,A6,Th7
.= ( (r (#) AffineMap (1 / (b - (-q/p)), -((-q/p) / (b - (-q/p))))) )
| [.-q/p,(t-q)/(p-s).]
+* ( AffineMap (r*(- (1 / ((-t/s) - b))), r*((-t/s) / ((-t/s) - b))))
| [.(t-q)/(p-s),-t/s.] by FUZZY_7:13
.= (AffineMap (p, q) | [.-q/p,(t-q)/(p-s).] )
+* (AffineMap (s, t) | [.(t-q)/(p-s),-t/s.]) by B1,B2,B3,B4,FUZZY_7:13;
hence thesis;
end;
theorem Th15:
for p,q,s,t,x being Real st
p*s < 0 & p > 0 & (p*t-q*s)/(p-s) > 0 & not x in ].-q/p,-t/s.[ holds
( (AffineMap (p,q) | ].-infty,(t-q)/(p-s).])
+* (AffineMap (s,t) | [.(t-q)/(p-s),+infty.[) ).x <= 0
proof
let p,q,s,t,x be Real;
assume A1: p*s < 0 & p > 0;
assume A2: (p*t-q*s)/(p-s) > 0;
assume not x in ].-q/p,-t/s.[; then
per cases;
suppose B1:x <= -q/p; then
(-q/p)*p >= x*p by XREAL_1:64,A1; then
-(q/p*p) >= x*p; then
-q >= x*p by XCMPLX_1:87,A1; then
B3s: -q+q >= x*p+q by XREAL_1:6;
B4s: -q/p < (t-q)/(p-s) by A1,A2,Th13; then
B4:x < (t-q)/(p-s) by B1,XXREAL_0:2;
B2: x in ].-infty,(t-q)/(p-s).] by XXREAL_1:234,B1,XXREAL_0:2,B4s;
not x in dom ( (AffineMap (s,t) | [.(t-q)/(p-s),+infty.[) )
by XXREAL_1:236,B4; then
( (AffineMap (p,q) | ].-infty,(t-q)/(p-s).])
+* (AffineMap (s,t) | [.(t-q)/(p-s),+infty.[) ).x
= (AffineMap (p,q) | ].-infty,(t-q)/(p-s).]).x by FUNCT_4:11
.= AffineMap (p,q) .x by FUNCT_1:49,B2;
hence thesis by B3s,FCONT_1:def 4;
end;
suppose C1:-t/s <= x;
C33:s < 0 by A1; then
x*s <= (-t/s)*s by C1,XREAL_1:65; then
x*s <= -t/s*s; then
x*s <= -t by XCMPLX_1:87,C33; then
C3s: x*s + t <= -t+t by XREAL_1:6;
(t-q)/(p-s) < -t/s by A1,A2,Th13; then
C2: x in [.(t-q)/(p-s),+infty.[ by XXREAL_1:236,C1,XXREAL_0:2;
then
x in dom ( AffineMap (s,t) | [.(t-q)/(p-s),+infty.[ )
by FUNCT_2:def 1; then
( (AffineMap (p,q) | ].-infty,(t-q)/(p-s).])
+* (AffineMap (s,t) | [.(t-q)/(p-s),+infty.[) ).x
= (AffineMap (s,t) | [.(t-q)/(p-s),+infty.[).x by FUNCT_4:13
.= AffineMap (s,t) .x by FUNCT_1:49,C2;
hence thesis by C3s,FCONT_1:def 4;
end;
end;
Th17:
for a,b,c be Real st a < b & b < c holds
( 1/(b - a) )*( -(1/(c - b)) ) < 0 & 1/(b - a) > 0 &
( (1/(b - a))*(c/(c - b)) - (-(a/(b - a)))*(-(1/(c - b))) )
/((1/(b - a))-(-(1/(c - b)))) > 0
proof
let a,b,c be Real;
assume A1: a < b & b < c; then
a < c by XXREAL_0:2; then
A4s:a-a < c-a by XREAL_1:9;
A2s:b-a > a-a & c-b > b-b by A1,XREAL_1:9;
( (1/(b - a))*(c/(c - b)) - (-(a/(b - a)))*(-(1/(c - b))) )
/((1/(b - a))-(-(1/(c - b))))
= ( (1*c)/((b - a)*(c - b)) - (a/(b - a))*(1/(c - b)) )
/ (1/(b - a)+1/(c - b)) by XCMPLX_1:76
.= ( c/((b - a)*(c - b)) - (a*1)/((b - a)*(c - b)) )
/ (1/(b - a)+1/(c - b)) by XCMPLX_1:76
.= ( c/((b - a)*(c - b)) - (a*1)/((b - a)*(c - b)) )
/ ( (1*(c - b) + 1*(b - a))/((b - a)*(c - b)) ) by XCMPLX_1:116,A2s
.= ( (c-a)/((b - a)*(c - b)) )/( (c - a)/((b - a)*(c - b)) ) by XCMPLX_1:120
.=1 by XCMPLX_1:60,A2s,A4s;
hence thesis by A2s;
end;
theorem Th16:
for a,b,c,x be Real st a < b & b < c & not x in ].a,c.[ holds
( AffineMap ( 1/(b - a), -(a/(b - a)) ) | ].-infty,b.]
+* AffineMap ( -(1/(c - b)), c/(c - b) ) | [.b,+infty.[ ).x <= 0
proof
let a,b,c,x be Real;
assume that
A1: a < b & b < c and
A2: not x in ].a,c.[;
A6s: b-a > a-a & c-b > b-b by A1,XREAL_1:9;
a < c by XXREAL_0:2,A1; then
A7s: a-a < c-a by XREAL_1:9;
set p = 1/(b - a);
set q = -(a/(b - a));
set s = -(1/(c - b));
set t = c/(c - b);
A3:(t-q)/(p-s)
= ((c/(c - b))-(-(a/(b - a))))/( 1/(b - a) + 1/(c - b) )
.= ( c/(c - b) + a/(b - a) ) /
( (1*(c - b) + 1*(b - a))/((b - a)*(c - b)) ) by XCMPLX_1:116,A6s
.= ( ((c*(b - a)) + (a*(c - b))) / ((c - b)*(b - a)) ) /
( (1*(c - b) + 1*(b - a))/((b - a)*(c - b)) ) by XCMPLX_1:116,A6s
.= ( (b*(c-a)) / ((c - b)*(b - a)) ) / ( (c - a)/((b - a)*(c - b)) )
.= ( b*( (c-a) / ((c - b)*(b - a))) ) / ( (c - a)/((b - a)*(c - b)) )
by XCMPLX_1:74
.= b*(( (c-a)/((c - b)*(b - a)) ) / ( (c-a)/((b - a)*(c - b)) ) )
by XCMPLX_1:74
.= b*1 by XCMPLX_1:60,A7s,A6s
.= b;
A4: -q/p
= -( (-a)/(b - a) ) / (1/(b - a)) by XCMPLX_1:187
.= (-( (-a)/(b - a)) ) / (1/(b - a)) by XCMPLX_1:187
.= ( a/(b - a) ) / (1/(b - a)) by XCMPLX_1:190
.= ( a/(b - a) ) * (b - a) by XCMPLX_1:100
.= a by XCMPLX_1:87,A6s;
-t/s = (c/(c - b)) / (1/(c - b)) by XCMPLX_1:189
.= (c/(c - b)) *(c - b) by XCMPLX_1:100
.= c by XCMPLX_1:87,A6s; then
p*s < 0 & p > 0 & (p*t-q*s)/(p-s) > 0 & not x in ].-q/p,-t/s.[
by Th17,A1,A4,A2;
hence thesis by A3,Th15;
end;
theorem Th18:
for a,b,c,x be Real st a < b & b < c & x in [.a,c.] holds
TriangularFS (a,b,c).x >= 0
proof
let a,b,c,x be Real;
assume A1: a < b & b < c & x in [.a,c.]; then
A2s: b-a > a-a & c-b > b-b by XREAL_1:9;
D11: a <= x & x <= c by XXREAL_1:1,A1; then
CXs:a-a <= x-a & x-x <= c - x by XREAL_1:9;
per cases;
suppose b < x; then
x in [.b,c.] by D11; then
TriangularFS (a,b,c) . x
= AffineMap (- (1 / (c - b)), c / (c - b)).x by A1,FUZZY_8:47
.= (- (1 / (c - b)))*x + c / (c - b) by FCONT_1:def 4
.= - (x*(1 / (c - b))) + c / (c - b)
.= - (x*1 / (c - b)) + c / (c - b) by XCMPLX_1:74
.= (- x) / (c - b) + c / (c - b) by XCMPLX_1:187
.= ((- x) + c) / (c - b) by XCMPLX_1:62
.= ( c-x) / (c - b);
hence thesis by A2s,CXs;
end;
suppose x <= b; then
x in [.a,b.] by D11; then
TriangularFS (a,b,c) . x
= AffineMap (1 / (b - a), -(a / (b - a))).x by A1,FUZZY_8:46
.= (1 / (b - a))*x + (-(a / (b - a))) by FCONT_1:def 4
.= x*(1 / (b - a)) -a / (b - a)
.= x*1 / (b - a) -a / (b - a) by XCMPLX_1:74
.= x / (b - a) + -a / (b - a)
.= x / (b - a) + (-a) / (b - a) by XCMPLX_1:187
.= (x+-a)/(b - a) by XCMPLX_1:62
.= (x-a)/(b - a);
hence thesis by A2s,CXs;
end;
end;
theorem Th19:
for a,b,c be Real, f be Function of REAL,REAL
st a < b & b < c &
f = (AffineMap ( 1/(b - a), -(a/(b - a)) ) | ].-infty,b.]
+* AffineMap ( -(1/(c - b)), c/(c - b) ) | [.b,+infty.[ ) holds
max+ f = TriangularFS (a,b,c)
proof
let a,b,c be Real, f be Function of REAL,REAL;
assume that
A1:a < b & b < c and
A2:f = (AffineMap ( 1/(b - a), -(a/(b - a)) ) | ].-infty,b.]
+* AffineMap ( -(1/(c - b)), c/(c - b) ) | [.b,+infty.[ );
A3: dom (max+ f) = dom f by RFUNCT_3:def 10
.= REAL by FUNCT_2:def 1;
A31: REAL = dom (TriangularFS (a,b,c)) by FUNCT_2:def 1;
for x being object st x in dom (TriangularFS (a,b,c)) holds
( TriangularFS (a,b,c) ).x = (max+ f).x
proof
let x be object;
assume B1: x in dom TriangularFS (a,b,c); then
reconsider x as Real;
A6: (max+ f) . x = max+ (f.x) by RFUNCT_3:def 10,A3,B1
.= max(f.x,0) by RFUNCT_3:def 1;
per cases;
suppose D1: x in [. a,c .]; then
D2: f.x
= ( (AffineMap ( 1/(b - a), -(a/(b - a)) ) | ].-infty,b.]
+* AffineMap ( -(1/(c - b)), c/(c - b) ) | [.b,+infty.[ ) | [. a,c .]) .x
by FUNCT_1:49,A2
.= (AffineMap ( 1/(b - a), -(a/(b - a)) ) | [.a,b.]
+* AffineMap ( -(1/(c - b)), c/(c - b) ) | [.b,c.] ) .x
by FUZZY_7:20,A1
.= ( TriangularFS (a,b,c) | [.a,c.] ).x by Th4,A1
.= TriangularFS (a,b,c) . x by FUNCT_1:49,D1;
f.x >= 0 by D2,A1,D1,Th18;
hence thesis by D2,XXREAL_0:def 10,A6;
end;
suppose not x in [. a,c .]; then
x < a or c < x; then
C1: not x in ]. a,c .[ by XXREAL_1:4; then
C2s: f.x <= 0 by A1,Th16,A2;
TriangularFS (a,b,c).x
= AffineMap (0,0).x by FUZZY_8:48,C1,A1
.= 0*x+0 by FCONT_1:def 4;
hence thesis by C2s,A6,XXREAL_0:def 10;
end;
end;
hence thesis by FUNCT_1:2,A3,A31;
end;
theorem
for a,b,c,r be Real, f be Function of REAL,REAL
st a < b & b < c & r > 0 &
f = r (#) (AffineMap ( 1/(b - a), -(a/(b - a)) ) | ].-infty,b.]
+* AffineMap ( -(1/(c - b)), c/(c - b) ) | [.b,+infty.[ ) holds
max+ f = r (#) TriangularFS (a,b,c)
proof
let a,b,c,r be Real, f be Function of REAL,REAL;
assume that
A1:a < b & b < c and
R1: r > 0 and
A2:f = r (#) (AffineMap ( 1/(b - a), -(a/(b - a)) ) | ].-infty,b.]
+* AffineMap ( -(1/(c - b)), c/(c - b) ) | [.b,+infty.[ );
A3: dom (max+ f) = dom f by RFUNCT_3:def 10
.= REAL by FUNCT_2:def 1;
A31: REAL = dom (r (#) TriangularFS (a,b,c)) by FUNCT_2:def 1;
set F = (AffineMap ( 1/(b - a), -(a/(b - a)) ) | ].-infty,b.]
+* AffineMap ( -(1/(c - b)), c/(c - b) ) | [.b,+infty.[ );
reconsider F as Function of REAL,REAL by FUZZY_7:12;
for x being object st x in dom (r (#) TriangularFS (a,b,c)) holds
(r (#) TriangularFS (a,b,c) ).x = (max+ f).x
proof
let x be object;
assume B1: x in dom (r (#) TriangularFS (a,b,c)); then
reconsider x as Real;
dom F = REAL by FUNCT_2:def 1; then
A7s:dom (max+ F) = REAL by RFUNCT_3:def 10;
A6: (max+ f) . x
= max+ (f.x) by RFUNCT_3:def 10,A3,B1
.= max((r (#) F).x,0) by A2,RFUNCT_3:def 1
.= max(r * (F.x),0) by VALUED_1:6
.= (((r * (F.x)) + 0) + |.((r * (F.x)) - 0).|) / 2 by COMPLEX1:74
.= (r * (F.x) + |. r .| * |.(F.x).|) / 2 by COMPLEX1:65
.= (r * (F.x) + r * |.(F.x).|) / 2 by COMPLEX1:43,R1;
(r (#) TriangularFS (a,b,c) ).x
= r * ( (TriangularFS (a,b,c)).x ) by VALUED_1:6
.= r * ( (max+ (F)).x ) by A1,Th19
.= r * (max+ (F.x)) by RFUNCT_3:def 10,A7s,B1
.= r * max(F.x,0) by RFUNCT_3:def 1
.= r * (((F.x + 0) + |.(F.x) - 0.|) / 2) by COMPLEX1:74
.= r * ((F.x + |. F.x .|) / 2);
hence thesis by A6;
end;
hence thesis by FUNCT_1:2,A3,A31;
end;
theorem Th26:
for p,q,s,t being Real, f being Function of REAL,REAL st
p*s < 0 & p > 0 & (p*t-q*s)/(p-s) > 0 &
for x being Real holds
f.x = ( (AffineMap (p,q) | ].-infty,(t-q)/(p-s).])
+* (AffineMap (s,t) | [.(t-q)/(p-s),+infty.[) ).x
holds
max+ f = (p*t-q*s)/(p-s) (#) ( TriangularFS(-q/p,(t-q)/(p-s),-t/s) )
proof
let p,q,s,t be Real, f be Function of REAL,REAL;
assume A1: p*s < 0 & p > 0;
assume A2: (p*t-q*s)/(p-s) > 0;
assume A3: for x being Real holds
f.x = ( (AffineMap (p,q) | ].-infty,(t-q)/(p-s).])
+* (AffineMap (s,t) | [.(t-q)/(p-s),+infty.[) ).x;
set r = (p*t-q*s)/(p-s);
dom (max+ f) = dom f by RFUNCT_3:def 10
.= REAL by FUNCT_2:def 1; then
A4: dom (max+ f) =
dom( (p*t-q*s)/(p-s) (#) ( TriangularFS(-q/p,(t-q)/(p-s),-t/s) ) )
by FUNCT_2:def 1;
A9: s < 0 by A1;
for x being object st x in dom (max+ f) holds
(max+ f) . x = ( r (#) ( TriangularFS(-q/p,(t-q)/(p-s),-t/s) ) ) . x
proof
let x be object;
assume A5:x in dom (max+ f); then
reconsider x as Real;
A6: (max+ f) . x = max+ (f.x) by RFUNCT_3:def 10,A5
.= max(f.x,0) by RFUNCT_3:def 1;
set a = -q/p;
set b = (t-q)/(p-s);
set c = -t/s;
A7: a < b & b < c by Th13,A1,A2;
per cases;
suppose x in ].-q/p,-t/s.[; then
B2: -q/p <= x & x <= -t/s by XXREAL_1:4;
per cases;
suppose B5: x < (t-q)/(p-s); then
B6: not x in dom (( AffineMap ( -1/(c-b), c/(c-b) ) | [.b,c.] ))
by XXREAL_1:1;
B4: x in [.a,b.] by B5,B2; then
B7: x in dom (AffineMap ( 1/(b-a), -a/(b-a) ) | [.a,b.] )
by FUNCT_2:def 1;
B8: not x in dom (AffineMap (s,t) | [.(t-q)/(p-s),+infty.[)
by B5,XXREAL_1:236;
B11: f.x = ( (AffineMap (p,q) | ].-infty,(t-q)/(p-s).])
+* (AffineMap (s,t) | [.(t-q)/(p-s),+infty.[) ).x by A3
.= (AffineMap (p,q) | ].-infty,(t-q)/(p-s).]).x by FUNCT_4:11,B8
.= (AffineMap (p,q) ).x by FUNCT_1:49,B5,XXREAL_1:234
.= p*x+q by FCONT_1:def 4;
(-q/p)*p <= x*p by B2,XREAL_1:64,A1; then
-(q/p*p) <= x*p; then
-q <= x*p by XCMPLX_1:87,A1; then
B10: -q+q <= x*p+q by XREAL_1:6;
( r (#) ( TriangularFS(-q/p,(t-q)/(p-s),-t/s) ) ) . x
= r * TriangularFS(-q/p,(t-q)/(p-s),-t/s).x by VALUED_1:6
.= r*( ( AffineMap (0,0) | (REAL \ ].a,c.[) ) +*
( AffineMap ( 1/(b-a), -a/(b-a) ) | [.a,b.] ) +*
( AffineMap ( -1/(c-b), c/(c-b) ) | [.b,c.] ) ).x by FUZNUM_1:def 7,A7
.= r*( ( AffineMap (0,0) | (REAL \ ].a,c.[) ) +*
( AffineMap ( 1/(b-a), -a/(b-a) ) | [.a,b.] ) ).x by FUNCT_4:11,B6
.= r*(AffineMap ( 1/(b-a), -a/(b-a) ) | [.a,b.]).x by FUNCT_4:13,B7
.= r*(AffineMap ( 1/(b-a), -a/(b-a) ) ).x by FUNCT_1:49,B4
.= r*((1/(b-a))*x + (-a/(b-a)) ) by FCONT_1:def 4
.= r*(1/((t-q)/(p-s)+q/p))*x + r*(-a/((t-q)/(p-s)+q/p))
.= r*(1/((1/p)*r))*x + r*(-a/((t-q)/(p-s)+q/p)) by A1,Th14
.= r*(1/((1/p)*r))*x + r*(-a/((1/p)*r)) by A1,Th14
.= r*( 1/(r/p) )*x + r*(-a/((1/p)*r)) by XCMPLX_1:99
.= r*( p/r )*x + r*(-a/((1/p)*r)) by XCMPLX_1:57
.= ( p )*x + r*(-a/((1/p)*r)) by XCMPLX_1:87,A2
.= ( p )*x + r*(-a/(r/p)) by XCMPLX_1:99
.= p*x + (-r*( (-(q/p)) / ( r/p ) ))
.= p*x + (-r*(- ((q/p) / ( r/p )) )) by XCMPLX_1:187
.= p*x + r*( (q/p) / ( r/p ) )
.= p*x + r*(q/r) by XCMPLX_1:55,A1
.= p*x + q by XCMPLX_1:87,A2;
hence thesis by XXREAL_0:def 10,B10,B11,A6;
end;
suppose B51:(t-q)/(p-s) <= x; then
x in [.(t-q)/(p-s),+infty.[ by XXREAL_1:236; then
B91: x in dom ( AffineMap (s,t) | [.(t-q)/(p-s),+infty.[ )
by FUNCT_2:def 1;
x*s >= (-t/s)*s by B2,XREAL_1:65,A9; then
x*s >= -t/s*s; then
x*s >= -t by XCMPLX_1:87,A9; then
B101s: x*s + t>= -t+t by XREAL_1:6;
B111: f.x = ( (AffineMap (p,q) | ].-infty,(t-q)/(p-s).])
+* (AffineMap (s,t) | [.(t-q)/(p-s),+infty.[) ).x by A3
.= (AffineMap (s,t) | [.(t-q)/(p-s),+infty.[).x by FUNCT_4:13,B91
.= (AffineMap (s,t) ).x by FUNCT_1:49,B51,XXREAL_1:236
.= s*x + t by FCONT_1:def 4;
B41: x in [.b,c.] by B51,B2; then
B71: x in dom ( AffineMap ( -1/(c-b), c/(c-b) ) | [.b,c.] )
by FUNCT_2:def 1;
( r (#) ( TriangularFS(-q/p,(t-q)/(p-s),-t/s) ) ) . x
= r * TriangularFS(-q/p,(t-q)/(p-s),-t/s).x by VALUED_1:6
.= r*( ( AffineMap (0,0) | (REAL \ ].a,c.[) ) +*
( AffineMap ( 1/(b-a), -a/(b-a) ) | [.a,b.] ) +*
( AffineMap ( -1/(c-b), c/(c-b) ) | [.b,c.] ) ).x by FUZNUM_1:def 7,A7
.= r*( AffineMap ( -1/(c-b), c/(c-b) ) | [.b,c.] ).x by FUNCT_4:13,B71
.= r*( AffineMap ( -1/(c-b), c/(c-b) ) ).x by FUNCT_1:49,B41
.= r*( (-1/(c-b))*x + c/(c-b)) by FCONT_1:def 4
.= r*((-1/(c-b))*x) + r*(c/(c-b))
.= r*(-1/(-(t/s+(t-q)/(p-s))))*x + r*c/(-(t/s+(t-q)/(p-s))) by XCMPLX_1:74
.= r*(-1/(-((1/s)*r)))*x + r*c/(-(t/s+(t-q)/(p-s))) by A1,Th14
.= r*(-1/(-((1/s)*r)))*x + r*c/(-((1/s)*r)) by A1,Th14
.= (r*(- (-1 / ((1/s)*(r)))))*x + r*c/(-((1/s)*r)) by XCMPLX_1:188
.= (r*( 1 / (r/s) ))*x + r*c/(-((1/s)*r)) by XCMPLX_1:99
.= (r*( s/r ))*x + r*c/(-((1/s)*r)) by XCMPLX_1:57
.= s*x + r*c/(-((1/s)*r)) by XCMPLX_1:87,A2
.= s*x + r*(c/(-((1/s)*r))) by XCMPLX_1:74
.= s*x + r*( -(-t/s) / ((1/s)*r) ) by XCMPLX_1:188
.= s*x + r*( -(-t/s) / (r/s) ) by XCMPLX_1:99
.= s*x + r*( - (-(t/s) / (r/s)) ) by XCMPLX_1:187
.= s*x + r*( (t/r) ) by XCMPLX_1:55,A9
.= s*x + t by XCMPLX_1:87,A2;
hence thesis by XXREAL_0:def 10,B101s,B111,A6;
end;
end;
suppose C1: not x in ].-q/p,-t/s.[; then
( (AffineMap (p,q) | ].-infty,(t-q)/(p-s).])
+* (AffineMap (s,t) | [.(t-q)/(p-s),+infty.[) ).x <= 0
by A1,A2,Th15; then
C2: f.x <= 0 by A3;
( r (#) ( TriangularFS(-q/p,(t-q)/(p-s),-t/s) ) ) . x
= r * TriangularFS(-q/p,(t-q)/(p-s),-t/s).x by VALUED_1:6
.= r * AffineMap (0,0).x by FUZZY_8:48,C1,A7
.= r * (0*x+0) by FCONT_1:def 4;
hence thesis by XXREAL_0:def 10,C2,A6;
end;
end;
hence thesis by FUNCT_1:2,A4;
end;
theorem Th6:
for a,b,c,r be Real, f be Function of REAL,REAL st a < b & b < c &
for x being Real holds f.x = (r (#) TriangularFS (a,b,c)).x holds
integral(f,['a,c']) = r*(c-a)/2
proof
let a,b,c,r be Real, f be Function of REAL,REAL;
assume that
A1: a < b & b < c and
A2: for x being Real holds f.x = (r (#) TriangularFS (a,b,c)).x;
A5: f | [.a,c.] = (r (#) AffineMap (1 / (b - a), -(a / (b - a)))) | [.a,b.]
+* (r (#) AffineMap (- (1 / (c - b)), c / (c - b))) | [.b,c.]
by Th7,A1,A2;
set fa = r (#) AffineMap (1 / (b - a), -(a / (b - a)));
set fc = r (#) AffineMap (- (1 / (c - b)), c / (c - b));
A7: b-a <> 0 & c-b <> 0 by A1;
A4: fa.b = r* ( AffineMap (1 / (b - a), -(a / (b - a))) ).b by VALUED_1:6
.= r* ( (1 / (b - a))*b + (-(a / (b - a))) ) by FCONT_1:def 4
.= r* ( (1 / (b - a))*b -a / (b - a) )
.= r* ( (b / (b - a)) -a / (b - a) ) by XCMPLX_1:99
.= r* ( (b-a)/(b-a) ) by XCMPLX_1:120
.= r*1 by XCMPLX_1:60,A7
.= r*( (c-b) / (c - b) ) by XCMPLX_1:60,A7
.= r*( c / (c - b) - (b / (c - b))) by XCMPLX_1:120
.= r*( c / (c - b) - (1 / (c - b)) * b) by XCMPLX_1:99
.= r*( (- (1 / (c - b))) * b + c / (c - b))
.= r* (AffineMap (- (1 / (c - b)), c / (c - b))).b by FCONT_1:def 4
.= fc.b by VALUED_1:6;
set ba = b - a;
set a1 = 1 / ba;
set b1 = -(a / ba);
set c1 = c - b;
thus
integral(f,['a,c']) = integral(fa,['a,b']) + integral(fc,['b,c'])
by FUZZY_8:11,A1,A4,A5
.= integral(AffineMap (r*(1 / (b - a)), r*(-(a / (b - a)))),['a,b'])
+ integral(fc,['b,c']) by FUZZY_7:13
.= (b-a)*( (r*a1)*(b+a)/2 + (r*b1) ) + integral(fc,['b,c']) by FUZZY_8:42,A1
.= (b-a)*( (r*a1)*(b+a)/2 + (r*b1) )
+ integral(AffineMap (r*(- (1 / (c - b))), r*(c /(c - b))),['b,c'])
by FUZZY_7:13
.= (b-a)*( (r*( 1 / (b - a) ))*(b+a)/2 + (r*(-(a / (b - a))) ) )
+ (c - b)* ( (r*(- (1 / (c - b)))) * (c+b)/2 + r*(c /(c - b)))
by FUZZY_8:42,A1
.= (b-a)*( r/ (b - a) *(b+a)/2 + (r*(-(a / (b - a))) ) )
+ (c - b)* ( (r*(- (1 / (c - b)))) * (c+b)/2 + r*(c /(c - b))) by XCMPLX_1:99
.= (b-a)*( r/ (b - a) *(b+a)/2 - (r*((a / (b - a))) ) )
+ (c - b)* (- (r*(1 / (c - b))) * (c+b)/2 + r*(c /(c - b)))
.= (b-a)*( r/ (b - a) *(b+a)/2 - (r*((a / (b - a))) ) )
+ (c - b)* ( - (r/(c - b)) * (c+b)/2 + r*(c /(c - b)) ) by XCMPLX_1:99
.= ( ba*((r / (b - a)) * (b+a)/2) - ba*(r*((a / (b - a))) ) )
+ ( c1 * (- (r/(c - b)) * (c+b)/2) + c1 * (r*(c /(c - b))) )
.= ( (ba*((r / (b - a))) * (b+a)/2) - ba*(r*((a / (b - a))) ) )
+ (c1 * (- (r/(c - b)) * (c+b)/2) + c1 * ( (r*c) /(c - b))) by XCMPLX_1:74
.= ( (ba*r) / (b - a) * (b+a)/2 - ba*(r*((a / (b - a))) ) )
+ (c1 * (- (r/(c - b)) * (c+b)/2) + c1 * ( (r*c) /(c - b) )) by XCMPLX_1:74
.= ( (ba*r) / (b - a) * (b+a)/2 - ba*(r*((a / (b - a))) ) )
+ (c1 * (- (r/(c - b)) * (c+b)/2 ) + c1 * (r*c) /(c - b)) by XCMPLX_1:74
.= (ba*r) / (b - a) * (b+a)/2 - ba*(r*((a / (b - a))) )
+ c1 * (- (r/(c - b)) * (c+b)/2 ) + c1 * (r*c) /(c - b)
.= (ba*r) / (b - a) * (b+a)/2 - ba*( (r*a) / (b - a) )
+ c1 * (- (r/(c - b)) * (c+b)/2 ) + c1 * (r*c) /(c - b) by XCMPLX_1:74
.= (ba*r) / (b - a) * (b+a)/2 - ba*( (r*a) / (b - a) ) -
c1 * (r/(c - b)) * (c+b)/2 + c1 * (r*c) /(c - b)
.= (ba*r) / (b - a) * (b+a)/2 - ba* ((r*a) / (b - a) ) -
(c1 * r) /(c - b) * (c+b)/2 + c1 * (r*c) /(c - b) by XCMPLX_1:74
.= r * (b+a)/2 - ba* ((r*a) / (b - a) ) -
(c1 * r) /(c - b) * (c+b)/2 + c1 * (r*c) /(c - b) by XCMPLX_1:89,A7
.= r * (b+a)/2 - ba* ((r*a) / (b - a)) -
r * (c+b)/2 + c1 * (r*c) /(c - b) by XCMPLX_1:89,A7
.= r * (b+a)/2 - ba* ((r*a) / (b - a)) -
r * (c+b)/2 + r*c by XCMPLX_1:89,A7
.= r * (b+a)/2 - (ba* (r*a) )/ (b - a) -
r * (c+b)/2 + r*c by XCMPLX_1:74
.= r * (b+a)/2 - r*a - r * (c+b)/2 + r*c by XCMPLX_1:89,A7
.= r*(c-a)/2;
end;
theorem
for a,b,c be Real st a < b & b < c holds
integral(TriangularFS (a,b,c) | ['a,c']) = (c-a)/2
proof
let a,b,c be Real;
assume A1:a < b & b < c;
set f = TriangularFS (a,b,c);
A2: for x being Real holds f.x = (1 (#) f).x
proof
let x be Real;
thus (1 (#) f).x = 1 * (f.x) by VALUED_1:6
.= f.x;
end;
integral(f,['a,c']) = 1*(c-a)/2 by A2,A1,Th6;
hence integral(f | ['a,c']) = (c-a)/2;
end;
Th901:
for a,b,c,r be Real st a < b & b < c holds
( r (#) AffineMap (1 / (b - a), -(a / (b - a))) ).b
=( r (#) AffineMap (- (1 / (c - b)), c / (c - b)) ).b
proof
let a,b,c,r be Real;
set fa = r (#) AffineMap (1 / (b - a), -(a / (b - a)));
set fc = r (#) AffineMap (- (1 / (c - b)), c / (c - b));
assume a < b & b < c; then
A7: b-a <> 0 & c-b <> 0;
thus
fa.b = r* ( AffineMap (1 / (b - a), -(a / (b - a))) ).b by VALUED_1:6
.= r* ( (1 / (b - a))*b + (-(a / (b - a))) ) by FCONT_1:def 4
.= r* ( (1 / (b - a))*b -a / (b - a) )
.= r* ( (b / (b - a)) -a / (b - a) ) by XCMPLX_1:99
.= r* ( (b-a)/(b-a) ) by XCMPLX_1:120
.= r*1 by XCMPLX_1:60,A7
.= r*( (c-b) / (c - b) ) by XCMPLX_1:60,A7
.= r*( c / (c - b) - (b / (c - b))) by XCMPLX_1:120
.= r*( c / (c - b) - (1 / (c - b)) * b) by XCMPLX_1:99
.= r*( (- (1 / (c - b))) * b + c / (c - b) )
.= r* (AffineMap (- (1 / (c - b)), c / (c - b))).b by FCONT_1:def 4
.= fc.b by VALUED_1:6;
end;
Th902:
for a,b,r be Real st a < b holds
integral( r (#) AffineMap (1 / (b - a), -(a / (b - a))),['a,b'])
= r*(b-a)/2
proof
let a,b,r be Real;
assume A1: a < b; then
A7: b-a <> 0;
set a1 = 1 / (b - a);
set ba = b - a;
set b1 = -(a / (b - a));
integral( r (#) AffineMap (1 / (b - a), -(a / (b - a))),['a,b'])
= integral(AffineMap (r*(1 / (b - a)), r*(-(a / (b - a)))),['a,b'])
by FUZZY_7:13
.= (b-a)*( (r*a1)*(b+a)/2 + (r*b1) ) by FUZZY_8:42,A1
.= (b-a)*( r/ (b - a) *(b+a)/2 + (r*(-(a / (b - a))) ) ) by XCMPLX_1:99
.= ( (ba*((r / (b - a))) * (b+a)/2) - ba*(r*((a / (b - a))) ) )
.= ( (ba*r) / (b - a) * (b+a)/2 - ba*(r*((a / (b - a))) ) ) by XCMPLX_1:74
.= (ba*r) / (b - a) * (b+a)/2 - ba*( (r*a) / (b - a) ) by XCMPLX_1:74
.= r * (b+a)/2 - ba* ((r*a) / (b - a) ) by XCMPLX_1:89,A7
.= r * (b+a)/2 - ba* (r*a) / (b - a) by XCMPLX_1:74
.= r * (b+a)/2 - r*a by XCMPLX_1:89,A7;
hence thesis;
end;
Th903:
for b,c,r be Real st b < c holds
integral( (r (#) AffineMap (- (1 / (c - b)), c / (c - b))),['b,c'])
= r*(c-b)/2
proof
let b,c,r be Real;
set c1 = c - b;
assume A1: b < c; then
A7: c - b <> 0;
thus
integral( (r (#) AffineMap (- (1 / (c - b)), c / (c - b))),['b,c'])
= integral(AffineMap (r*(- (1 / (c - b))), r*(c /(c - b))),['b,c'])
by FUZZY_7:13
.= (c - b)* ( (r*(- (1 / (c - b)))) * (c+b)/2 + r*(c /(c - b)))
by FUZZY_8:42,A1
.= (c - b)* (- (r*(1 / (c - b))) * (c+b)/2 + r*(c /(c - b)))
.= (c - b)* ( - (r/(c - b)) * (c+b)/2 + r*(c /(c - b)) ) by XCMPLX_1:99
.= ( c1 * (- (r/(c - b)) * (c+b)/2) + c1 * (r*(c /(c - b))) )
.= (c1 * (- (r/(c - b)) * (c+b)/2) + c1 * ( (r*c) /(c - b) )) by XCMPLX_1:74
.= - c1 * (r/(c - b)) * (c+b)/2 + c1 * (r*c) /(c - b) by XCMPLX_1:74
.= - (c1 * r) /(c - b) * (c+b)/2 + c1 * (r*c) /(c - b) by XCMPLX_1:74
.= - r * (c+b)/2 + c1 * (r*c) /(c - b) by XCMPLX_1:89,A7
.= - r * (c+b)/2 + r*c by XCMPLX_1:89,A7
.= r*(c-b)/2;
end;
:: Centroid of Trianglar Function@(a+b+c)/3
theorem Th25:
for a,b,c,r be Real, f be Function of REAL,REAL st a < b & b < c & r <> 0 &
for x being Real holds f.x = (r (#) TriangularFS (a,b,c)).x holds
centroid(f,['a,c']) = (a+b+c)/3
proof
let a,b,c,r be Real, f be Function of REAL,REAL such that
A1: a < b & b < c and
A2: r <> 0 and
A3: for x being Real holds f.x = (r (#) TriangularFS (a,b,c)).x;
A4: f | [.a,c.] = (r (#) AffineMap (1 / (b - a), -(a / (b - a)))) | [.a,b.]
+* (r (#) AffineMap (- (1 / (c - b)), c / (c - b))) | [.b,c.]
by Th7,A1,A3;
set F = r (#) AffineMap (1 / (b - a), -(a / (b - a)));
set G = r (#) AffineMap (- (1 / (c - b)), c / (c - b));
A6: b-a > 0 & c - b > 0 by XREAL_1:50,A1;
A9: c - a <> 0 by A1;
r*(b - a)/2 <> 0 & r*(c - b)/2 <> 0
proof
per cases by A2;
suppose r > 0;
hence thesis by A6;
end;
suppose r < 0;
hence thesis by A6;
end;
end; then
integral(F,['a,b']) <> 0 & integral(G,['b,c']) <> 0 & F.b = G.b
by Th901,A1,Th902,Th903;
hence
centroid(f, ['a,c']) = 1 / integral(f,['a,c'])
* ( integral((id REAL)(#)F,['a,b'])
+ integral((id REAL)(#)G,['b,c']) ) by FUZZY817,A4,A1
.= 1 / integral(f,['a,c'])
* ( integral((id REAL)(#) AffineMap (r*(1/(b-a)),r*(-(a/(b-a)))),['a,b'])
+ integral((id REAL)(#)G,['b,c']) ) by FUZZY_7:13
.= 1 / integral(f,['a,c'])
* (integral((id REAL)(#) AffineMap (r*(1/(b-a)),r*(-(a/(b-a)))),['a,b'])
+integral((id REAL)(#) AffineMap (r*(-(1/(c-b))), r*(c/(c-b))),['b,c']) )
by FUZZY_7:13
.= 1 / integral(f,['a,c'])
* ( (b-a)*( (r*(1/(b-a))) * ( b*b + b*a + a*a)/3 + (r*(-(a/(b-a))))*(b+a)/2)
+integral((id REAL)(#) AffineMap (r*(-(1/(c-b))), r*(c/(c-b))),['b,c']))
by FUZZY_8:42,A1
.= 1 / integral(f,['a,c'])
* ( (b-a)*( (r*(1/(b-a))) * ( b*b + b*a + a*a)/3 + (r*(-(a/(b-a))))*(b+a)/2)
+ (c-b)*( (r*(-(1/(c-b))))*(c*c+c*b+b*b)/3 + (r*(c/(c-b)))*(c+b)/2) )
by FUZZY_8:42,A1
.= 1 / (r*(c-a)/2)
* ( (b-a)*(r*(1/(b-a))) * ( b*b + b*a + a*a)/3
+ (b-a)*(r*(-(a/(b-a))))*(b+a)/2
+ (c-b)*(r*(-(1/(c-b))))*(c*c+c*b+b*b)/3 + (c-b)*(r*(c/(c-b)))*(c+b)/2 )
by Th6,A1,A3
.= 1 / (r*(c-a)/2)
* ( (b-a)*(r*1/(b-a)) * ( b*b + b*a + a*a)/3 + (b-a)*(r*(-(a/(b-a))))*(b+a)/2
+ (c-b)*(r*(-(1/(c-b))))*(c*c+c*b+b*b)/3 + (c-b)*(r*(c/(c-b)))*(c+b)/2 )
by XCMPLX_1:74
.= 1/(r*(c-a)/2)
* ( (b-a)*(r/(b-a)) * (b*b+b*a+a*a)/3 -(b-a)*(r*(a/(b-a)))*(b+a)/2
- (c-b)*(r*(1/(c-b)))*(c*c+c*b+b*b)/3 + (c-b)*(r*c/(c-b))*(c+b)/2 )
by XCMPLX_1:74
.= 1/(r*(c-a)/2)
* ( (b-a)*(r/(b-a)) * (b*b+b*a+a*a)/3 -(b-a)*(r*a/(b-a))*(b+a)/2
- (c-b)*(r*(1/(c-b)))*(c*c+c*b+b*b)/3 + (c-b)*(r*c/(c-b))*(c+b)/2 )
by XCMPLX_1:74
.= 1/(r*(c-a)/2)
* ( (b-a)*(r/(b-a)) * (b*b+b*a+a*a)/3 -(b-a)*(r*a/(b-a))*(b+a)/2
- (c-b)*(r*1/(c-b))*(c*c+c*b+b*b)/3 + (c-b)*(r*c/(c-b))*(c+b)/2 )
by XCMPLX_1:74
.= 1/(r*(c-a)/2)
* ( r * (b*b+b*a+a*a)/3 -(b-a)*((r*a)/(b-a))*(b+a)/2
- (c-b)*(r/(c-b))*(c*c+c*b+b*b)/3 + (c-b)*(r*c/(c-b))*(c+b)/2 )
by XCMPLX_1:87,A6
.= 1/(r*(c-a)/2) * ( r * (b*b+b*a+a*a)/3 -(r*a)*(b+a)/2
- (c-b)*(r/(c-b))*(c*c+c*b+b*b)/3 + (c-b)*(r*c/(c-b))*(c+b)/2 )
by XCMPLX_1:87,A6
.= 1/(r*(c-a)/2) * ( r * (b*b+b*a+a*a)/3 -(r*a)*(b+a)/2
- r*(c*c+c*b+b*b)/3 + (c-b)*(r*c/(c-b))*(c+b)/2 ) by XCMPLX_1:87,A6
.= 1/((r*(c-a))/2) * ( r * (b*b+b*a+a*a)/3 -(r*a)*(b+a)/2
- r*(c*c+c*b+b*b)/3 + (r*c)*(c+b)/2 ) by XCMPLX_1:87,A6
.= 1*2/(r*(c-a)) * ( r * (b*b+b*a+a*a)/3 -(r*a)*(b+a)/2
- r*(c*c+c*b+b*b)/3 + (r*c)*(c+b)/2 ) by XCMPLX_1:77
.= 2/(r*(c-a)) * r *( (b*b+b*a+a*a)/3 -a*(b+a)/2
- (c*c+c*b+b*b)/3 + c*(c+b)/2 )
.= r/(r*(c-a)) * 2 *( (b*b+b*a+a*a)/3 -a*(b+a)/2
- (c*c+c*b+b*b)/3 + c*(c+b)/2 ) by XCMPLX_1:75
.= (r/r)/(c-a) * 2 *( (b*b+b*a+a*a)/3 -a*(b+a)/2
- (c*c+c*b+b*b)/3 + c*(c+b)/2 ) by XCMPLX_1:78
.= 1/(c-a) * 2 * ( (b*b+b*a+a*a)/3 -a*(b+a)/2
- (c*c+c*b+b*b)/3 + c*(c+b)/2 ) by XCMPLX_1:60,A2
.= 1/(c-a) * (c-a)*(b/3 + a/3 + c/3)
.= 1*(c-a)/(c-a) *(b/3 + a/3 + c/3) by XCMPLX_1:74
.= 1 * (b/3 + a/3 + c/3) by XCMPLX_1:60,A9
.= (a+b+c)/3;
end;
theorem
for p,q,s,t being Real, f,F being Function of REAL,REAL st
p*s < 0 & p > 0 & (p*t-q*s)/(p-s) > 0 &
f = (AffineMap (p,q) | ].-infty,(t-q)/(p-s).])
+* (AffineMap (s,t) | [.(t-q)/(p-s),+infty.[) & F = max+ f
holds
centroid(F,['-q/p,-t/s']) = (-q/p+(t-q)/(p-s)+-t/s)/3
proof
let p,q,s,t be Real, f,F be Function of REAL,REAL;
assume that
A1: p*s < 0 & p > 0 and
A0: (p*t-q*s)/(p-s) > 0 and
A2: f = ( (AffineMap (p,q) | ].-infty,(t-q)/(p-s).])
+* (AffineMap (s,t) | [.(t-q)/(p-s),+infty.[) ) and
A5: F = max+ f;
A3: -q/p < (t-q)/(p-s) & (t-q)/(p-s) < -t/s by Th13,A1,A0;
for x being Real holds
F.x = ((p*t-q*s)/(p-s) (#) TriangularFS (-q/p,(t-q)/(p-s),-t/s)).x
proof
let x be Real;
set ff = ( (AffineMap (p,q) | ].-infty,(t-q)/(p-s).])
+* (AffineMap (s,t) | [.(t-q)/(p-s),+infty.[) );
reconsider ff as Function of REAL,REAL by FUZZY_7:12;
for x being Real holds
ff.x = ( (AffineMap (p,q) | ].-infty,(t-q)/(p-s).])
+* (AffineMap (s,t) | [.(t-q)/(p-s),+infty.[) ).x;
hence thesis by Th26,A1,A0,A2,A5;
end;
hence centroid(F,['-q/p,-t/s']) = ((-q/p)+(t-q)/(p-s)+(-t/s))/3
by Th25,A3,A0;
end;
theorem Th24:
for A be non empty closed_interval Subset of REAL,
p,q,r,s,t,u be Real, f be Function of REAL,REAL st p*s < 0 & p > 0 &
for x be Real holds
f.x = max(r,min( u, ( (AffineMap (p,q) |].-infty,(t-q)/(p-s).]) +*
(AffineMap (s,t) |[.(t-q)/(p-s),+infty.[) ) .x ))
holds f is Lipschitzian
proof
let A be non empty closed_interval Subset of REAL;
let p,q,r,s,t,u be Real;
let f be Function of REAL,REAL;
assume A1: p*s < 0 & p > 0;
assume A2: for x be Real holds
f.x = max(r,min( u, ( (AffineMap (p,q) |].-infty,(t-q)/(p-s).]) +*
(AffineMap (s,t) |[.(t-q)/(p-s),+infty.[) ) .x ));
A3: p <> s by A1;
set F = (AffineMap (p,q) |].-infty,(t-q)/(p-s).]) +*
(AffineMap (s,t) |[.(t-q)/(p-s),+infty.[);
reconsider F as Function of REAL,REAL by FUZZY_7:12;
F is Lipschitzian by A3,FUZZY_7:42; then
consider r2 being Real such that
C1: 0 < r2 and
C2: for x1, x2 being Real st x1 in dom F & x2 in dom F holds
|.(F . x1) - (F . x2).| <= r2 * |. x1 - x2 .|;
C3: dom F = REAL by FUNCT_2:def 1
.= dom f by FUNCT_2:def 1;
ex r1 being Real st
( 0 < r1 &
( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.(f . x1) - (f . x2).| <= r1 * |. x1 - x2 .| ) )
proof
take r2;
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.(f . x1) - (f . x2).| <= r2 * |. x1 - x2 .|
proof
let x1, x2 be Real;
assume x1 in dom f & x2 in dom f; then
C3X: |.(F . x1) - (F . x2).| <= r2 * |. x1 - x2 .| by C2,C3;
A4: |.(f . x1) - (f . x2).|
= |. ( max(r,min(u,F.x1)) ) - (f . x2) .| by A2
.= |. ( max(r,min(u,F.x1)) ) - (max(r,min(u,F.x2))) .| by A2
.= |. (r+min(u,F.x1)+|.r-min(u,F.x1).|)/2 - (max(r,min(u,F.x2))) .|
by COMPLEX1:74
.= |. (r+min(u,F.x1)+|.r-min(u,F.x1).|)/2
- (r+min(u,F.x2)+|.r-min(u,F.x2).|)/2 .| by COMPLEX1:74
.= |. ( min(u,F.x1)+|.r-min(u,F.x1).|
- min(u,F.x2) - |.r-min(u,F.x2).| )*(1/2) .|
.= |. min(u,F.x1) - min(u,F.x2) +|.r-min(u,F.x1).| - |.r-min(u,F.x2).| .|
* |. (1/2) .| by COMPLEX1:65
.= |. (min(u,F.x1) - min(u,F.x2))
+(|.r-min(u,F.x1).| - |.r-min(u,F.x2).|) .| * (1/2) by COMPLEX1:43;
A5: |.(f . x1) - (f . x2).| <=
( |. min(u,F.x1) - min(u,F.x2).|
+|. |.r-min(u,F.x1).| - |.r-min(u,F.x2).| .| )*(1/2)
by A4,XREAL_1:64, COMPLEX1:56;
|. |.r-min(u,F.x1).| - |.r-min(u,F.x2).| .|
+ |. min(u,F.x1) - min(u,F.x2).| <=
|. (r-min(u,F.x1)) - (r-min(u,F.x2)) .|
+ |. min(u,F.x1) - min(u,F.x2).| by XREAL_1:6,COMPLEX1:64;
then
A6s: ( |. |.r-min(u,F.x1).| - |.r-min(u,F.x2).| .|
+ |. min(u,F.x1) - min(u,F.x2).| )*(1/2) <=
(|. (r-min(u,F.x1)) - (r-min(u,F.x2)) .|
+ |. min(u,F.x1) - min(u,F.x2).| )*(1/2) by XREAL_1:64;
A7s: |. (r-min(u,F.x1)) - (r-min(u,F.x2)) .| =
|. (r - ((u + F.x1) - |. u - F.x1 .|)/2)
- (r-min(u,F.x2)) .| by COMPLEX1:73
.= |. (r - ((u + F.x1) - |. u - F.x1 .|)/2)
- (r- ((u + F.x2) - |. u - F.x2 .|)/2 ) .| by COMPLEX1:73
.= |. (1/2)*((F.x2 - F.x1) + (|. u - F.x1 .| - |. u - F.x2 .|)) .|
.= |. 1/2.|* |.((F.x2 - F.x1) + (|. u - F.x1 .| - |. u - F.x2 .|)) .|
by COMPLEX1:65
.= (1/2)* |.(F.x2 - F.x1) + (|. u - F.x1 .| - |. u - F.x2 .|) .|
by COMPLEX1:43;
|. min(u,F.x1) - min(u,F.x2).|
= |. ((u+F.x1)- |.u-F.x1.|)/2 - min(u,F.x2) .| by COMPLEX1:73
.= |. (u+F.x1- |.u-F.x1.|)/2 -((u+F.x2)- |.u-F.x2.|)/2.| by COMPLEX1:73
.= |. ( F.x1-F.x2 -|.u-F.x1.| + |.u-F.x2.|)*(1/2).|
.= |. ( F.x1-F.x2 -|.u-F.x1.| + |.u-F.x2.|).|*|.(1/2).| by COMPLEX1:65
.= |. ( F.x1-F.x2) -(|.u-F.x1.| -|.u-F.x2.|).|*(1/2) by COMPLEX1:43;
then
|.(f . x1) - (f . x2).| <=
(1/4)* ( |.(F.x2 - F.x1) + (|. u - F.x1 .| - |. u - F.x2 .|) .|
+ |. -((F.x2 - F.x1) + (|. u - F.x1 .| - |. u - F.x2 .|)).| )
by A7s,A6s,A5,XXREAL_0:2; then
A8s: |.(f . x1) - (f . x2).| <=
(1/4)* ( |.(F.x2 - F.x1) + (|. u - F.x1 .| - |. u - F.x2 .|) .|
+ |. (F.x2 - F.x1) + (|. u - F.x1 .| - |. u - F.x2 .|).| ) by COMPLEX1:52;
(1/2)*|.(F.x2 - F.x1) + (|. u - F.x1 .| - |. u - F.x2 .|) .| <=
(1/2)*(|.(F.x2 - F.x1).| + |. |. u - F.x1 .| - |. u - F.x2 .| .|)
by XREAL_1:64,COMPLEX1:56; then
A9: |.(f . x1) - (f . x2).| <=
(1/2)*(|.(F.x2 - F.x1).| + |. |. u - F.x1 .| - |. u - F.x2 .| .|)
by A8s,XXREAL_0:2;
|. |. u - F.x1 .| - |. u - F.x2 .| .| <=
|. ( u - F.x1 ) - ( u - F.x2 ) .| by COMPLEX1:64; then
|. |. u - F.x1 .| - |. u - F.x2 .| .| <=
|. -( F.x1 - F.x2 ) .|; then
|. |. u - F.x1 .| - |. u - F.x2 .| .| <= |. (F.x1 - F.x2) .|
by COMPLEX1:52; then
|. |. u - F.x1 .| - |. u - F.x2 .| .| + |. F.x1 - F.x2 .| <=
|. F.x1 - F.x2 .| + |. F.x1 - F.x2 .| by XREAL_1:6;
then
(1/2)*(|. - ( F.x2 - F.x1 ) .| + |. |. u - F.x1 .| - |. u - F.x2 .| .|)<=
(1/2)* (2*|. ( F.x1 - F.x2 ) .|) by XREAL_1:64; then
(1/2)*(|. ( F.x2 - F.x1 ) .| + |. |. u - F.x1 .| - |. u - F.x2 .| .|)<=
(1/2)* (2*|. ( F.x1 - F.x2 ) .|) by COMPLEX1:52; then
|.(f . x1) - (f . x2).| <=
(1/2)* (2*|. ( F.x1 - F.x2 ) .|) by XXREAL_0:2,A9;
hence |.(f . x1) - (f . x2).| <= r2 * |. x1 - x2 .| by XXREAL_0:2,C3X;
end;
hence thesis by C1;
end;
hence thesis;
end;
theorem
for A be non empty closed_interval Subset of REAL,
p,q,r,s,t,u be Real, f be Function of REAL,REAL st p*s < 0 & p > 0 &
for x be Real holds
f.x = max(r,min( u, ( (AffineMap (p,q) |].-infty,(t-q)/(p-s).]) +*
(AffineMap (s,t) |[.(t-q)/(p-s),+infty.[) ) .x ))
holds f is_integrable_on A & f | A is bounded
proof
let A be non empty closed_interval Subset of REAL;
let p,q,r,s,t,u be Real;
let f be Function of REAL,REAL;
assume A1: p*s < 0 & p > 0;
assume A2: for x be Real holds
f.x = max(r,min( u, ( (AffineMap (p,q) |].-infty,(t-q)/(p-s).]) +*
(AffineMap (s,t) |[.(t-q)/(p-s),+infty.[) ) .x ));
B1:dom f = REAL by FUNCT_2:def 1;
A4: f is Lipschitzian by Th24,A1,A2;
reconsider f as PartFunc of REAL,REAL;
f | A is continuous by A4;
hence thesis by INTEGRA5:10,INTEGRA5:11,B1;
end;
begin :: Trapezoidal Fuzzy Set
:: ___________
:: /|\ / |\
:: / | \ / | \
:: / | X | \
:: / | / \ | \
:: / |/ \| \
:: ------------------------------
:: a b c d
theorem Th20:
for a, b, c, d being Real st a < b & b < c & c < d holds
(for x be object st x in [.a,b.] holds
TrapezoidalFS (a,b,c,d).x = ( AffineMap (1 / (b - a),- (a / (b - a)))).x )
proof
let a, b, c, d be Real;
assume A1:a < b & b < c & c < d; then
AA: b-a <> 0;
set f0 = AffineMap (0,0) | (REAL \ ].a,d.[);
set fab=AffineMap (1 / (b - a),- (a / (b - a))) | [.a,b.];
set fbc=(AffineMap (0,1)) | [.b,c.];
set fcd=AffineMap ( - (1 / (d - c)), d / (d - c) ) | [.c,d.];
(for x be object st x in [.a,b.] holds
TrapezoidalFS (a,b,c,d).x = ( AffineMap (1 / (b - a),- (a / (b - a))) ).x )
proof
let x be object;
assume A3:x in [.a,b.]; then
reconsider x as Real;
a <= x & x <= b by A3,XXREAL_1:1; then
x < c by A1,XXREAL_0:2; then
A2: not x in dom fcd by XXREAL_1:1;
A4:for x being object st x in (dom (f0+*fab)) /\ (dom fbc) holds
(f0+*fab) . x = fbc . x
proof
let x be object;
assume B1: x in (dom (f0+*fab)) /\ (dom fbc); then
reconsider x as Real;
B2s:(dom (f0+*fab)) /\ (dom fbc)
= (dom f0 \/ dom fab) /\ (dom fbc) by FUNCT_4:def 1
.= ((REAL \ ].a,d.[) \/ dom fab) /\ (dom fbc) by FUNCT_2:def 1
.= ((REAL \ ].a,d.[) \/ [.a,b.]) /\ (dom fbc) by FUNCT_2:def 1
.= ((REAL \ ].a,d.[) \/ [.a,b.]) /\ [.b,c.] by FUNCT_2:def 1
.= ((REAL \ ].a,d.[) /\ [.b,c.]) \/ ([.a,b.]/\ [.b,c.]) by XBOOLE_1:23
.= {} \/ ([.a,b.]/\ [.b,c.]) by Th5,A1
.= [.max(a,b),min(b,c).] by XXREAL_1:140
.= [.b,min(b,c).] by XXREAL_0:def 10,A1
.= [.b,b.] by XXREAL_0:def 9,A1
.= {b} by XXREAL_1:17;
B3: b in [.b,c.] by A1;
B4: b in [.a,b.] by A1; then
B6: b in dom fab by FUNCT_2:def 1;
B5: (f0+*fab) . x
= (f0+*fab) . b by B2s,B1,TARSKI:def 1
.= fab.b by FUNCT_4:13, B6
.= AffineMap (1 / (b - a),- (a / (b - a))).b by FUNCT_1:49,B4
.= b*(1 / (b - a))+(- a*1 / (b - a)) by FCONT_1:def 4
.= b*(1 / (b - a))+(- a*(1 / (b - a))) by XCMPLX_1:74
.= (b-a)*(1 / (b - a))
.= ((b-a)*1) / (b - a) by XCMPLX_1:74
.= 1 by AA,XCMPLX_1:60;
fbc . x = fbc .b by B2s,B1,TARSKI:def 1
.= AffineMap (0,1).b by FUNCT_1:49,B3
.= 0*b+1 by FCONT_1:def 4;
hence thesis by B5;
end;
x in (REAL \ ].a,d.[) \/ [.a,b.] by XBOOLE_0:def 3,A3;
then
x in (REAL \ ].a,d.[) \/ dom fab by FUNCT_2:def 1;
then
x in dom f0 \/ dom fab by FUNCT_2:def 1;
then
A5: x in dom (f0+*fab) by FUNCT_4:def 1;
A6: x in dom fab by A3,FUNCT_2:def 1;
TrapezoidalFS (a,b,c,d).x
= (f0+*fab+*fbc+*fcd).x by FUZNUM_1:def 8,A1
.= (f0+*fab+*fbc).x by FUNCT_4:11,A2
.= (f0+*fab).x by FUNCT_4:15,A4,A5,PARTFUN1:def 4
.= fab.x by FUNCT_4:13,A6;
hence thesis by FUNCT_1:49,A3;
end;
hence thesis;
end;
theorem Th21:
for a, b, c, d being Real st a < b & b < c & c < d holds
(for x be object st x in [.b,c.] holds
TrapezoidalFS (a,b,c,d).x = AffineMap (0,1).x)
proof
let a, b, c, d be Real;
assume A1:a < b & b < c & c < d; then
AA: d-c <> 0;
A11: a < c & b < d by A1,XXREAL_0:2;
set f0 = AffineMap (0,0) | (REAL \ ].a,d.[);
set fab=AffineMap (1 / (b - a),- (a / (b - a))) | [.a,b.];
set fbc=(AffineMap (0,1)) | [.b,c.];
set fcd=AffineMap ( - (1 / (d - c)), d / (d - c) ) | [.c,d.];
(for x be object st x in [.b,c.] holds
TrapezoidalFS (a,b,c,d).x = AffineMap (0,1).x)
proof
let x be object;
assume A2:x in [.b,c.]; then
reconsider x as Real;
TT:for x being object st x in (dom (f0+*fab+*fbc)) /\ (dom fcd) holds
(f0+*fab+*fbc) . x = fcd . x
proof
let x be object;
assume B1:x in (dom (f0+*fab+*fbc)) /\ (dom fcd); then
reconsider x as Real;
x in (dom (f0+*fab+*fbc)) /\ [.c,d.] by B1,FUNCT_2:def 1;
then
x in (dom (f0+*fab) \/ dom fbc ) /\ [.c,d.] by FUNCT_4:def 1;
then
x in (dom f0 \/ dom fab \/ dom fbc ) /\ [.c,d.] by FUNCT_4:def 1;
then
x in ((dom f0 \/ dom fab) /\ [.c,d.]) \/ (dom fbc /\ [.c,d.])
by XBOOLE_1:23; then
x in (dom f0 /\ [.c,d.]) \/ (dom fab /\ [.c,d.]) \/ (dom fbc /\ [.c,d.])
by XBOOLE_1:23; then
x in ((REAL \ ].a,d.[) /\ [.c,d.]) \/ (dom fab /\ [.c,d.])
\/ (dom fbc /\ [.c,d.]) by FUNCT_2:def 1;
then
x in ((REAL \ ].a,d.[) /\ [.c,d.]) \/ ([.a,b.] /\ [.c,d.])
\/ (dom fbc /\ [.c,d.]) by FUNCT_2:def 1;
then
x in ((REAL \ ].a,d.[) /\ [.c,d.]) \/ ([.a,b.] /\ [.c,d.])
\/ ([.b,c.] /\ [.c,d.]) by FUNCT_2:def 1;
then
x in ((REAL \ ].a,d.[) /\ [.c,d.]) \/ ([.a,b.] /\ [.c,d.])
\/ ([.max(b,c),min(c,d).]) by XXREAL_1:140;
then
x in ((REAL \ ].a,d.[) /\ [.c,d.]) \/ [.max(a,c),min(b,d).]
\/ ([.max(b,c),min(c,d).]) by XXREAL_1:140;
then
x in ((REAL \ ].a,d.[) /\ [.c,d.]) \/ [.max(a,c),min(b,d).]
\/ ([.c,min(c,d).]) by XXREAL_0:def 10,A1;
then
x in ((REAL \ ].a,d.[) /\ [.c,d.]) \/ [.c,min(b,d).]
\/ ([.c,min(c,d).])
by XXREAL_0:def 10,A1,XXREAL_0:2;
then
x in ((REAL \ ].a,d.[) /\ [.c,d.]) \/ [.c,min(b,d).]
\/ ([.c,c.]) by XXREAL_0:def 9,A1;
then
x in ((REAL \ ].a,d.[) /\ [.c,d.]) \/ [.c,b.] \/ [.c,c.]
by XXREAL_0:def 9,A1,XXREAL_0:2; then
x in ((].-infty,a.] \/ [.d,+infty.[) /\ [.c,d.]) \/ [.c,b.] \/ [.c,c.]
by XXREAL_1:398; then
x in (].-infty,a.] /\ [.c,d.]) \/ ([.d,+infty.[ /\ [.c,d.])
\/ [.c,b.] \/ [.c,c.] by XBOOLE_1:23; then
x in (].-infty,a.] /\ [.c,d.]) \/ ([.d,+infty.[ /\ [.c,d.])
\/ {} \/ [.c,c.] by XXREAL_1:29,A1; then
x in (].-infty,a.] /\ [.c,d.]) \/ ([.d,+infty.[ /\ [.c,d.])
or x in [.c,c.] by XBOOLE_0:def 3; then
x in {} \/ ([.d,+infty.[ /\ [.c,d.])
or x in [.c,c.] by XBOOLE_0:def 7,XXREAL_1:280,A11; then
(x in [.d,+infty.[ & x in [.c,d.]) or x in [.c,c.] by XBOOLE_0:def 4;
then
((d <= x & x < +infty) & (c <= x & x<= d)) or x in [.c,c.]
by XXREAL_1:1,XXREAL_1:3; then
per cases;
suppose x in [.d,d.]; then
D2s: x in {d} by XXREAL_1:17;
D3: not d in dom fbc by XXREAL_1:1,A1;
D4: not d in dom fab by XXREAL_1:1,A11;
D6: d in [.c,d.] by A1;
DD: (f0+*fab+*fbc) . x = (f0+*fab+*fbc) . d by D2s,TARSKI:def 1
.= (f0+*fab) . d by FUNCT_4:11,D3
.= (f0) . d by FUNCT_4:11,D4
.= AffineMap (0,0).d by FUNCT_1:49,Th3
.= 0*d+0 by FCONT_1:def 4;
fcd . x = fcd.d by D2s,TARSKI:def 1
.= AffineMap ( - (1 / (d - c)), d / (d - c) ).d by FUNCT_1:49,D6
.= (- (1 / (d - c)))*d + d / (d - c) by FCONT_1:def 4
.= - d*(1 / (d - c)) + d / (d - c)
.= - (d*1 / (d - c)) + d / (d - c) by XCMPLX_1:74
.= 0;
hence thesis by DD;
end;
suppose x in [.c,c.]; then
C2s: x in {c} by XXREAL_1:17;
C4: c in [.b,c.] by A1; then
C3: c in dom fbc by FUNCT_2:def 1;
C5: c in [.c,d.] by A1;
CC: (f0+*fab+*fbc) . x = (f0+*fab+*fbc) . c by C2s,TARSKI:def 1
.= fbc . c by FUNCT_4:13,C3
.= AffineMap (0,1).c by FUNCT_1:49,C4
.= 0*c+1 by FCONT_1:def 4
.= 1;
fcd . x = fcd.c by C2s,TARSKI:def 1
.= AffineMap ( - (1 / (d - c)), d / (d - c) ).c by C5,FUNCT_1:49
.= ( - (1 / (d - c)))*c+ d / (d - c) by FCONT_1:def 4
.= d*1 / (d - c) + ( - c*(1 / (d - c)))
.= d*(1 / (d - c)) + ( - c*(1 / (d - c))) by XCMPLX_1:74
.= (d-c)*(1 / (d - c))
.= ((d-c)*1) / (d - c) by XCMPLX_1:74
.= 1 by AA,XCMPLX_1:60;
hence thesis by CC;
end;
end;
A4: x in dom fbc by A2,FUNCT_2:def 1;
x in dom (f0+*fab) or x in dom fbc by A2,FUNCT_2:def 1;
then
x in dom (f0+*fab) \/ dom fbc by XBOOLE_0:def 3; then
A5: x in dom (f0+*fab+*fbc) by FUNCT_4:def 1;
TrapezoidalFS (a,b,c,d).x
= (f0+*fab+*fbc+*fcd).x by FUZNUM_1:def 8,A1
.= (f0+*fab+*fbc).x by FUNCT_4:15,A5,TT,PARTFUN1:def 4
.= fbc.x by FUNCT_4:13,A4;
hence thesis by FUNCT_1:49,A2;
end;
hence thesis;
end;
theorem Th22:
for a, b, c, d being Real st a < b & b < c & c < d holds
(for x be object st x in [.c,d.] holds
TrapezoidalFS (a,b,c,d).x
= ( AffineMap (- (1 / (d - c)), d / (d - c)) ).x )
proof
let a, b, c, d be Real;
assume A1:a < b & b < c & c < d;
set f0 = AffineMap (0,0) | (REAL \ ].a,d.[);
set fab=AffineMap (1 / (b - a),- (a / (b - a))) | [.a,b.];
set fbc=(AffineMap (0,1)) | [.b,c.];
set fcd=AffineMap ( - (1 / (d - c)), d / (d - c) ) | [.c,d.];
for x be object st x in [.c,d.] holds
TrapezoidalFS (a,b,c,d).x
= ( AffineMap (- (1 / (d - c)), d / (d - c)) ).x
proof
let x be object;
assume A2:x in [.c,d.]; then
A3: x in dom fcd by FUNCT_2:def 1;
thus TrapezoidalFS (a,b,c,d).x
= (f0+*fab+*fbc+*fcd).x by FUZNUM_1:def 8,A1
.= fcd.x by FUNCT_4:13,A3
.= ( AffineMap (- (1 / (d - c)), d / (d - c)) ).x by A2,FUNCT_1:49;
end;
hence thesis;
end;
theorem Th23:
for a, b, c, d being Real st a < b & b < c & c < d holds
(for x be Real st not x in [.a,d.] holds
TrapezoidalFS (a,b,c,d).x = 0 )
proof
let a, b, c, d be Real;
assume A1:a < b & b < c & c < d; then
AA: a < c & b < d by XXREAL_0:2;
set f0 = AffineMap (0,0) | (REAL \ ].a,d.[);
set fab=AffineMap (1 / (b - a),- (a / (b - a))) | [.a,b.];
set fbc=(AffineMap (0,1)) | [.b,c.];
set fcd=AffineMap ( - (1 / (d - c)), d / (d - c) ) | [.c,d.];
for x be Real st not x in [.a,d.] holds TrapezoidalFS (a,b,c,d).x = 0
proof
let x be Real;
assume not x in [.a,d.]; then
per cases;
suppose B1: x < a; then
x < c by XXREAL_0:2,AA; then
A4: not x in dom fcd by XXREAL_1:1;
x < b by A1,B1,XXREAL_0:2; then
A5: not x in dom fbc by XXREAL_1:1;
A6: not x in dom fab by B1,XXREAL_1:1;
-infty < x by XXREAL_0:12,XREAL_0:def 1; then
x in ].-infty,a.] or x in [.d,+infty.[ by B1; then
x in ].-infty,a.] \/ [.d,+infty.[ by XBOOLE_0:def 3; then
A7: x in (REAL \ ].a,d.[) by XXREAL_1:398;
(TrapezoidalFS (a,b,c,d)).x
= (f0+*fab+*fbc+*fcd).x by FUZNUM_1:def 8,A1
.= (f0+*fab+*fbc).x by FUNCT_4:11,A4
.= (f0+*fab).x by FUNCT_4:11,A5
.= f0.x by FUNCT_4:11,A6
.= AffineMap (0,0).x by FUNCT_1:49,A7
.= 0*x+0 by FCONT_1:def 4;
hence thesis;
end;
suppose C1: d < x; then
A4: not x in dom fcd by XXREAL_1:1;
c < x by A1,C1,XXREAL_0:2; then
A5: not x in dom fbc by XXREAL_1:1;
b < x by XXREAL_0:2,AA,C1; then
A6: not x in dom fab by XXREAL_1:1;
x < +infty by XXREAL_0:9,XREAL_0:def 1; then
x in ].-infty,a.] or x in [.d,+infty.[ by C1; then
x in ].-infty,a.] \/ [.d,+infty.[ by XBOOLE_0:def 3; then
A7: x in (REAL \ ].a,d.[) by XXREAL_1:398;
(TrapezoidalFS (a,b,c,d)).x
= (f0+*fab+*fbc+*fcd).x by FUZNUM_1:def 8,A1
.= (f0+*fab+*fbc).x by FUNCT_4:11,A4
.= (f0+*fab).x by FUNCT_4:11,A5
.= f0.x by FUNCT_4:11,A6
.= AffineMap (0,0).x by FUNCT_1:49,A7
.= 0*x+0 by FCONT_1:def 4;
hence thesis;
end;
end;
hence thesis;
end;
theorem
for a, b, c, d being Real st a < b & b < c & c < d holds
TriangularFS (a,b,c) + TriangularFS (b,c,d) = TrapezoidalFS (a,b,c,d)
proof
let a, b, c, d be Real;
assume
A1: a < b & b < c & c < d; then
CB: b-b < c - b by XREAL_1:9;
A2: dom (TriangularFS (a,b,c) + TriangularFS (b,c,d))
= dom (TriangularFS (a,b,c)) /\ dom(TriangularFS (b,c,d)) by VALUED_1:def 1
.= REAL /\ dom(TriangularFS (b,c,d)) by FUNCT_2:def 1
.= REAL /\ REAL by FUNCT_2:def 1
.= dom TrapezoidalFS (a,b,c,d) by FUNCT_2:def 1;
for x being object st x in dom ( TrapezoidalFS (a,b,c,d) ) holds
(TriangularFS (a,b,c) + TriangularFS (b,c,d)) . x
= TrapezoidalFS (a,b,c,d) . x
proof
let x be object;
assume A3: x in dom ( TrapezoidalFS (a,b,c,d) ); then
reconsider x as Real;
A4:(TriangularFS (a,b,c) + TriangularFS (b,c,d)) . x
= TriangularFS (a,b,c).x + TriangularFS (b,c,d) . x by VALUED_1:def 1,A2,A3;
per cases;
suppose x in [.a,d.]; then
B01: a <= x & x <= d by XXREAL_1:1;
per cases;
suppose B1: c <= x; then
B11: x in [.c,d.] by B01;
not x in ].a,c.[ by B1,XXREAL_1:4; then
TriangularFS (a,b,c).x
= AffineMap (0,0).x by FUZZY_8:48,A1
.= 0*x+0 by FCONT_1:def 4; then
(TriangularFS (a,b,c) + TriangularFS (b,c,d)) . x
= AffineMap (- (1 / (d - c)), d / (d - c)).x by B11,A1,FUZZY_8:47,A4;
hence thesis by Th22,B11,A1;
end;
suppose B2: x < c;
per cases;
suppose b <= x; then
B211: x in [.b,c.] by B2;
(TriangularFS (a,b,c) + TriangularFS (b,c,d)) . x
= TriangularFS (a,b,c).x + TriangularFS (b,c,d) . x
by VALUED_1:def 1,A2,A3
.= TriangularFS (a,b,c).x + AffineMap (1 / (c - b), -(b / (c - b))).x
by B211,A1,FUZZY_8:46
.= AffineMap (- (1 / (c - b)), c / (c - b)).x
+ AffineMap (1 / (c - b), -(b / (c - b))).x by B211,A1,FUZZY_8:47
.= AffineMap (- (1 / (c - b)), c / (c - b)).x
+ ((1/(c-b))*x + (-(b / (c-b))) ) by FCONT_1:def 4
.= (- (1 / (c - b)))*x + c / (c - b)
+ ( (1/(c-b))*x + (-(b / (c-b))) ) by FCONT_1:def 4
.= c / (c-b) - b / (c-b)
.= (c-b) / (c-b) by XCMPLX_1:120
.= 0*x + 1 by XCMPLX_1:60,CB
.= AffineMap (0,1).x by FCONT_1:def 4
.= TrapezoidalFS (a,b,c,d).x by B211,A1,Th21;
hence thesis;
end;
suppose B22: x < b; then
B221: x in [.a,b.] by B01;
not x in ].b,d.[ by XXREAL_1:4,B22; then
(TriangularFS (a,b,c) + TriangularFS (b,c,d)) . x
= TriangularFS (a,b,c).x + AffineMap (0,0).x by A4,A1,FUZZY_8:48
.= AffineMap (1 / (b - a), -(a / (b - a))).x
+ AffineMap (0,0).x by A1,B221,FUZZY_8:46
.= AffineMap (1 / (b - a), -(a / (b - a))).x
+ (0*x + 0) by FCONT_1:def 4
.= TrapezoidalFS (a,b,c,d).x by A1,Th20,B221;
hence thesis;
end;
end;
end;
suppose not x in [.a,d.]; then
per cases;
suppose C11: x < a; then
C12: not x in ].a,c.[ by XXREAL_1:4;
C14: not x in [.a,d.] by XXREAL_1:1,C11;
x < b by A1,C11,XXREAL_0:2; then
C13: not x in ].b,d.[ by XXREAL_1:4;
(TriangularFS (a,b,c) + TriangularFS (b,c,d)) . x
= TriangularFS (a,b,c).x + TriangularFS (b,c,d).x by VALUED_1:def 1,A2,A3
.= TriangularFS (a,b,c).x + AffineMap (0,0).x by A1,C13,FUZZY_8:48
.= AffineMap (0,0).x + AffineMap (0,0).x by A1,C12,FUZZY_8:48
.= AffineMap (0,0).x + (0*x+0) by FCONT_1:def 4
.= (0*x+0) + 0 by FCONT_1:def 4
.= TrapezoidalFS (a,b,c,d) . x by C14,A1,Th23;
hence thesis;
end;
suppose C2: d < x; then
C21: not x in ].b,d.[ by XXREAL_1:4;
C22: not x in [.a,d.] by XXREAL_1:1,C2;
c < x by A1,C2,XXREAL_0:2; then
C23: not x in ].a,c.[ by XXREAL_1:4;
(TriangularFS (a,b,c) + TriangularFS (b,c,d)) . x
= TriangularFS (a,b,c).x + TriangularFS (b,c,d).x by VALUED_1:def 1,A2,A3
.= TriangularFS (a,b,c).x + AffineMap (0,0).x by A1,C21,FUZZY_8:48
.= AffineMap (0,0).x + AffineMap (0,0).x by A1,C23,FUZZY_8:48
.= AffineMap (0,0).x + (0*x+0) by FCONT_1:def 4
.= (0*x+0) + 0 by FCONT_1:def 4
.= TrapezoidalFS (a,b,c,d) . x by C22,A1,Th23;
hence thesis;
end;
end;
end;
hence thesis by A2,FUNCT_1:2;
end;
begin :: Related Properties about the Integral of Two Connected Functions
reserve A for non empty closed_interval Subset of REAL;
theorem
for a,b,c being Real, f,g be Function of ['a,c'],REAL st
a <= b & b <= c holds
(f | [.a,b.] +* g | [.b,c.]) is Function of ['a,c'],REAL
proof
let a,b,c be Real, f,g be Function of ['a,c'],REAL;
assume A1: a <= b & b <= c;
set g1 = f | [.a,b.];
set g2 = g | [.b,c.];
set F = f | [.a,b.] +* g | [.b,c.];
B1:dom f = ['a,c'] by FUNCT_2:def 1
.= [.a,c.] by INTEGRA5:def 3,XXREAL_0:2,A1;
B2: dom (g) = ['a,c'] by FUNCT_2:def 1
.= [.a,c.] by INTEGRA5:def 3,XXREAL_0:2,A1;
D1: dom F = (dom g1) \/ (dom g2) by FUNCT_4:def 1
.= [.a,b.] \/ dom g2 by B1,RELAT_1:62, XXREAL_1:34,A1
.= [.a,b.] \/ [.b,c.] by B2,RELAT_1:62, XXREAL_1:34,A1
.= [. a,c .] by XXREAL_1:165,A1
.= ['a,c'] by INTEGRA5:def 3,XXREAL_0:2,A1;
for x being object st x in ['a,c'] holds F . x in REAL
by XREAL_0:def 1;
hence F is Function of ['a,c'],REAL by FUNCT_2:3,D1;
end;
theorem
for a,b,c being Real, f,g be Function of ['a,c'],REAL st
a <= b & b <= c &
f | ['a,c'] is bounded & g | ['a,c'] is bounded
holds
( (f| [.a,b.]) +* (g | [.b,c.]) ) | ['a,c'] is bounded
proof
let a,b,c be Real, f,g be Function of ['a,c'],REAL;
assume A1: a <= b & b <= c;
assume A2:f | ['a,c'] is bounded & g | ['a,c'] is bounded;
set g1 = f | [.a,b.];
set g2 = g | [.b,c.];
set h = (f | [.a,b.] +* g | [.b,c.]);
ex r being Real st for y being set st y in dom (h | ['a,c']) holds
|.(h | ['a,c']).y.| < r
proof
consider r being Real such that
C1: for y being set st y in dom (f | ['a,c']) holds |.(f | ['a,c']).y.| < r
by COMSEQ_2:def 3,A2;
consider r1 being Real such that
C2: for y being set st y in dom (g | ['a,c']) holds |.(g | ['a,c']).y.| < r1
by COMSEQ_2:def 3,A2;
take max(r,r1);
for x being set st x in dom (h | ['a,c']) holds
|. (h | ['a,c']).x .| < max(r,r1)
proof
let x be set;
assume
B1: x in dom (h | ['a,c']);
D1: ['a,c'] = dom (f | ['a,c']) by FUNCT_2:def 1;
D2: ['a,c'] = dom (g | ['a,c']) by FUNCT_2:def 1;
B2: x in ['a,c'] by B1;
reconsider x as Real by B1;
x in [.a,c.] by INTEGRA5:def 3,A1,XXREAL_0:2,B2; then
BB2: a <= x & x <= c by XXREAL_1:1;
per cases;
suppose S1: x < b; then
not x in dom ( g | [.b,c.] ) by XXREAL_1:1; then
E1: |. (h | ['a,c']).x .|
= |. (f| [.a,b.]).x .| by FUNCT_4:11
.= |. (f | ['a,c']).x .| by FUNCT_1:49,XXREAL_1:1,BB2,S1;
r <= max(r,r1) by XXREAL_0:25;
hence thesis by XXREAL_0:2,E1,C1,B1, D1;
end;
suppose S2: x >= b; then
D3: x in [.b,c.] by BB2;
dom g = ['a,c'] by FUNCT_2:def 1
.= [.a,c.] by INTEGRA5:def 3,XXREAL_0:2,A1; then
D4: x in dom (g|[.b,c.]) by D3, RELAT_1:62,XXREAL_1:34,A1;
E2: |. (h | ['a,c']).x .|
= |. (g|[.b,c.]).x .| by FUNCT_4:13,D4
.= |. (g | ['a,c']).x .| by FUNCT_1:49,BB2,XXREAL_1:1,S2;
r1 <= max(r,r1) by XXREAL_0:25;
hence thesis by XXREAL_0:2,C2,B1, D2,E2;
end;
end;
hence thesis;
end;
hence thesis by COMSEQ_2:def 3;
end;
theorem
for a being Real, f, g being Function of REAL,REAL
st f | A is bounded & g | A is bounded & a in A
holds
(( f | ].-infty,a.[ ) +* ( g | [.a,+infty.[ )) | ['lower_bound A,a']
is bounded &
(( f | ].-infty,a.[ ) +* ( g | [.a,+infty.[ )) | ['a,upper_bound A']
is bounded
proof
let a be Real, f, g be Function of REAL,REAL;
assume that
A1: f | A is bounded and
A2: g | A is bounded and
A3: a in A;
a in [.(lower_bound A),(upper_bound A).] by INTEGRA1:4,A3;
then
A31: (lower_bound A) <= a & a <= (upper_bound A) by XXREAL_1:1;
set F = ( f | ].-infty,a.[ ) +* ( g | [.a,+infty.[ );
set LBa = ['lower_bound A,a'];
set aUB = ['a,upper_bound A'];
BO:ex r being Real st for y being set st y in dom (F | LBa) holds
|.(F | LBa).y.| < r
proof
consider r being Real such that
C1: for y being set st y in dom (f | A) holds |.(f | A).y.| < r
by COMSEQ_2:def 3,A1;
consider r1 being Real such that
C2: for y being set st y in dom (g | A) holds |.(g | A).y.| < r1
by COMSEQ_2:def 3,A2;
take max(r,r1);
for x being set st x in dom (F | LBa) holds
|. (F | LBa).x .| < max(r,r1)
proof
let x be set;
assume x in dom (F | LBa); then
B1: x in LBa by RELAT_1:57;
D1: A = dom (f | A) by FUNCT_2:def 1;
D2: A = dom (g | A) by FUNCT_2:def 1;
reconsider x as Real by B1;
x in [.lower_bound A,a .] by INTEGRA5:def 3,B1,A31; then
lower_bound A <= x & x <= a by XXREAL_1:1; then
lower_bound A <= x & x <= upper_bound A by XXREAL_0:2,A31; then
x in [.(lower_bound A),(upper_bound A).]; then
B11: x in A by INTEGRA1:4;
per cases;
suppose S1: x < a; then
B4: not ( x in dom (g|[.a,+infty.[)) by XXREAL_1:236;
E1: |. (F | LBa).x .| = |. F.x .| by FUNCT_1:49,B1
.= |. (f|].-infty,a.[).x .| by FUNCT_4:11,B4
.= |. (f ).x .| by FUNCT_1:49,XXREAL_1:233,S1
.= |. (f | A).x .| by FUNCT_1:49,B11;
r <= max(r,r1) by XXREAL_0:25;
hence thesis by XXREAL_0:2,E1,C1,D1, B11;
end;
suppose S2: x >= a; then
x in [.a,+infty.[ by XXREAL_1:236; then
D4: x in dom (g|[.a,+infty.[) by FUNCT_2:def 1;
E2: |. (F | LBa).x .| = |. F.x .| by FUNCT_1:49,B1
.= |. (g|[.a,+infty.[).x .| by FUNCT_4:13,D4
.= |. g.x .| by FUNCT_1:49,XXREAL_1:236,S2
.= |. (g | A).x .| by FUNCT_1:49,B11;
r1 <= max(r,r1) by XXREAL_0:25;
hence thesis by XXREAL_0:2,C2, D2,E2,B11;
end;
end;
hence thesis;
end;
ex r being Real st for y being set st y in dom (F | aUB) holds
|.(F | aUB).y.| < r
proof
consider r being Real such that
C1: for y being set st y in dom (f | A) holds |.(f | A).y.| < r
by COMSEQ_2:def 3,A1;
consider r1 being Real such that
C2: for y being set st y in dom (g | A) holds |.(g | A).y.| < r1
by COMSEQ_2:def 3,A2;
take max(r,r1);
for x being set st x in dom (F | aUB) holds
|. (F | aUB).x .| < max(r,r1)
proof
let x be set;
assume x in dom (F | aUB); then
B1: x in aUB by RELAT_1:57; then
reconsider x as Real;
D1: A = dom (f | A) by FUNCT_2:def 1;
D2: A = dom (g | A) by FUNCT_2:def 1;
x in [.a, upper_bound A .] by INTEGRA5:def 3,B1,A31;
then
a <= x & x <= upper_bound A by XXREAL_1:1; then
lower_bound A <= x & x <= upper_bound A by XXREAL_0:2,A31;
then
x in [.(lower_bound A),(upper_bound A).]; then
B11: x in A by INTEGRA1:4;
per cases;
suppose S1: x < a; then
B4: not ( x in dom (g|[.a,+infty.[)) by XXREAL_1:236;
E1: |. (F | aUB).x .| = |. F.x .| by FUNCT_1:49,B1
.= |. (f|].-infty,a.[).x .| by FUNCT_4:11,B4
.= |. (f ).x .| by FUNCT_1:49,XXREAL_1:233,S1
.= |. (f | A).x .| by FUNCT_1:49,B11;
r <= max(r,r1) by XXREAL_0:25;
hence thesis by XXREAL_0:2,E1,C1,D1, B11;
end;
suppose S2: x >= a; then
x in [.a,+infty.[ by XXREAL_1:236; then
D4: x in dom (g|[.a,+infty.[) by FUNCT_2:def 1;
E2: |. (F | aUB).x .| = |. F.x .| by FUNCT_1:49,B1
.= |. (g|[.a,+infty.[).x .| by FUNCT_4:13,D4
.= |. g.x .| by FUNCT_1:49,XXREAL_1:236,S2
.= |. (g | A).x .| by FUNCT_1:49,B11;
r1 <= max(r,r1) by XXREAL_0:25;
hence thesis by XXREAL_0:2,C2, D2,E2,B11;
end;
end;
hence thesis;
end;
hence thesis by BO,COMSEQ_2:def 3;
end;
theorem
for a being Real, f, g, h being Function of REAL,REAL st
f | A is bounded & f is_integrable_on A &
g | A is bounded & g is_integrable_on A &
a in A & h = ( f | ].-infty,a.] ) +* ( g | [.a,+infty.[ ) & f.a = g.a
holds
h is_integrable_on [' lower_bound A, a '] &
h is_integrable_on [' a, upper_bound A ']
proof
let a be Real, f, g, h be Function of REAL,REAL;
assume that
A1: f | A is bounded & f is_integrable_on A and
A2: g | A is bounded & g is_integrable_on A and
A3: a in A and
A4: h = ( f | ].-infty,a.] ) +* ( g | [.a,+infty.[ ) and
A40: f.a = g.a;
A5: ['lower_bound A, upper_bound A']
= [.lower_bound A,upper_bound A.] by INTEGRA5:def 3,SEQ_4:11
.= A by INTEGRA1:4;
a in [.lower_bound A,upper_bound A.] by INTEGRA5:def 3,SEQ_4:11,A3,A5;
then
B1: lower_bound A <= a & a <= upper_bound A by XXREAL_1:1;
B11: lower_bound A <= upper_bound A by SEQ_4:11;
B21a: dom f = REAL by FUNCT_2:def 1;
B22a: dom g = REAL by FUNCT_2:def 1;
B51:dom (f | (['lower_bound A, a']) ) = ['lower_bound A,a'] by FUNCT_2:def 1
.= dom (h | (['lower_bound A, a']) ) by FUNCT_2:def 1;
B5g: for x being object st x in dom (f | ['lower_bound A,a'] ) holds
(f | ['lower_bound A,a'] ) . x = (h | (['lower_bound A,a']) ) . x
proof
let x be object;
assume D1: x in dom (f | ['lower_bound A,a'] ); then
x in ['lower_bound A,a']; then
reconsider x as Element of REAL;
D1f: dom (f | ['lower_bound A,a'] )
= ['lower_bound A,a'] by FUNCT_2:def 1
.= [.lower_bound A,a.] by INTEGRA5:def 3,B1; then
D7: lower_bound A <= x & x <= a by XXREAL_1:1,D1;
D3u:for x being object st
x in (dom( f | ].-infty,a.] ) /\ dom( g | [.a,+infty.[ ))
holds ( f | ].-infty,a.] ).x = ( g | [.a,+infty.[ ) . x
proof
let x be object;
assume T1: x in (dom( f | ].-infty,a.] ) /\ dom( g | [.a,+infty.[ ));
T2: (dom( f | ].-infty,a.] ) /\ dom( g | [.a,+infty.[ ))
= ].-infty,a.] /\ dom( g | [.a,+infty.[ ) by FUNCT_2:def 1
.= ].-infty,a.] /\ [.a,+infty.[ by FUNCT_2:def 1
.= [.a,a.] by XXREAL_1:272
.= {a} by XXREAL_1:17; then
( f | ].-infty,a.] ).x
= ( f | ].-infty,a.] ) . a by TARSKI:def 1,T1
.= f.a by FUNCT_1:49,XXREAL_1:234
.= (g | [.a,+infty.[) . a by FUNCT_1:49,XXREAL_1:236,A40;
hence thesis by TARSKI:def 1,T1,T2;
end;
x in ].-infty,a.] by XXREAL_1:234,D7; then
D4: x in dom (f | ].-infty,a.]) by FUNCT_2:def 1;
(f | ['lower_bound A,a'] ) . x = f.x by FUNCT_1:49,D1
.= (f | ].-infty,a.] ) . x by FUNCT_1:49,XXREAL_1:234,D7
.= ( ( f | ].-infty,a.] ) +* ( g | [.a,+infty.[ )).x
by D4,FUNCT_4:15,D3u,PARTFUN1:def 4
.= (h | ([.lower_bound A,a.]) ) . x by FUNCT_1:49,A4,D1f,D1;
hence thesis by INTEGRA5:def 3,B1;
end;
B61: dom (g | (['a, upper_bound A']) )
= ['a, upper_bound A'] by FUNCT_2:def 1
.= dom (h | (['a, upper_bound A']) ) by FUNCT_2:def 1;
B6f:for x being object st x in dom (g | ['a, upper_bound A']) holds
(g | ['a, upper_bound A']) . x = (h | ['a, upper_bound A'] ) . x
proof
let x be object;
assume E1: x in dom (g | ['a, upper_bound A']); then
x in ['a, upper_bound A']; then
reconsider x as Element of REAL;
E2x: dom (g | ['a, upper_bound A'] )
= ['a, upper_bound A'] by FUNCT_2:def 1
.= [.a, upper_bound A.] by INTEGRA5:def 3,B1; then
E3x:a <= x by XXREAL_1:1,E1; then
x in [.a,+infty.[ by XXREAL_1:236; then
E4: x in dom ( g | [.a,+infty.[ ) by FUNCT_2:def 1;
(g | ['a, upper_bound A']) . x = g.x by FUNCT_1:49,E1
.= ( g | [.a,+infty.[ ).x by FUNCT_1:49,E3x,XXREAL_1:236
.= h.x by A4,FUNCT_4:13,E4
.= (h | [.a, upper_bound A.] ) . x by FUNCT_1:49,E2x,E1;
hence thesis by INTEGRA5:def 3,B1;
end;
B77:f is_integrable_on ['lower_bound A, a']
by B11,FUZZY_8:13,B21a,A5,A1,A3;
g is_integrable_on ['a, upper_bound A']
by B11,FUZZY_8:13,B22a,A5,A2,A3;
hence h is_integrable_on ['lower_bound A, a'] &
h is_integrable_on ['a, upper_bound A']
by B77,B6f,FUNCT_1:2,B61,B5g,B51;
end;
theorem
for a being Real, f, g, h being Function of REAL,REAL st
f | A is bounded & f is_integrable_on A &
g | A is bounded & g is_integrable_on A &
a in A & h = ( f | ].-infty,a.] ) +* ( g | [.a,+infty.[ ) & f.a = g.a
holds
integral (h,A)
= integral (f,['lower_bound A, a']) + integral (g,['a,upper_bound A'])
proof
let a be Real, f, g, h be Function of REAL,REAL;
assume that
A1: f | A is bounded & f is_integrable_on A and
A2: g | A is bounded & g is_integrable_on A and
A3: a in A and
A4: h = ( f | ].-infty,a.] ) +* ( g | [.a,+infty.[ ) and
A40: f.a = g.a;
set AA = ['lower_bound A, upper_bound A'];
A5: ['lower_bound A, upper_bound A']
= [.lower_bound A,upper_bound A.] by INTEGRA5:def 3,SEQ_4:11
.= A by INTEGRA1:4; then
a in [.lower_bound A,upper_bound A.] by INTEGRA5:def 3,SEQ_4:11,A3;
then lower_bound A <= a & a <= upper_bound A by XXREAL_1:1;
hence thesis by A40,A4,FUZZY_8:16,A2,A1,A5;
end;