:: Isosceles Triangular and Isosceles Trapezoidal Membership Functions Using Centroid Method
:: by Takashi Mitsuishi
::
:: Received March 31, 2023
:: Copyright (c) 2023-2025 Association of Mizar Users

Lm6: for a, c being Real st c > 0 holds
a in ['(a - c),(a + c)']

proof end;

theorem Th6: :: FUZZY_7:1

for a, b, c, d being Real st a < b & b < c & c < d holds
['a,d'] \ ['b,c'] c= ['a,b'] \/ ['c,d']

proof end;

theorem :: FUZZY_7:2

for a, b, c, d being Real holds [.a,d.] \ [.b,c.] c= [.a,b.[ \/ ].c,d.]

proof end;

theorem :: FUZZY_7:3

for a, b, c, d being Real st a < b & b < c & c < d holds
[.a,d.] \ [.b,c.] c= [.a,b.] \/ [.c,d.]

proof end;

Th8X: for a, b, c, d being Real st a <= b & b < c & c <= d holds
[.a,b.[ \/ ].c,d.] c= [.a,d.] \ [.b,c.]

proof end;

theorem :: FUZZY_7:4

for p, q, r, s being Real st p < r & r <= s & s < q holds
[.r,s.] c< [.p,q.]

proof end;

Lm5: for a, b, c, x being Real holds b - |.((b * (x - a)) / c).| <= b

proof end;

theorem :: FUZZY_7:5

for f, g being Function of REAL,REAL st f is continuous & g is continuous holds
max (f,g) is continuous

proof end;

theorem :: FUZZY_7:6

for f, g being Function of REAL,REAL st f is continuous & g is continuous holds
min (f,g) is continuous

proof end;

theorem :: FUZZY_7:7

for A, B being non empty closed_interval Subset of REAL holds
( not B c< A or lower_bound A < lower_bound B or upper_bound B < upper_bound A )

proof end;

theorem Th12: :: FUZZY_7:8

for A, B being non empty closed_interval Subset of REAL st B c= A holds
( lower_bound A <= lower_bound B & upper_bound B <= upper_bound A )

proof end;

theorem :: FUZZY_7:9

for r being Real
for f, g being Function of REAL,REAL holds r (#) (f +* g) = (r (#) f) +* (r (#) g)

proof end;

theorem Th27: :: FUZZY_7:10

for A being non empty Subset of REAL
for r being Real
for f being Function of REAL,REAL holds (r (#) f) | A = r (#) (f | A)

proof end;

theorem :: FUZZY_7:11

for A being non empty Subset of REAL
for r being Real
for f being PartFunc of REAL,REAL st A c= dom f holds
(r (#) f) | A = r (#) (f | A)

proof end;

theorem :: FUZZY_7:12

for s being Real
for f, g being Function of REAL,REAL holds (f | ].-infty,s.]) +* (g | [.s,+infty.[) is Function of REAL,REAL

proof end;

theorem Th28: :: FUZZY_7:13

for a, b, r being Real holds r (#) (AffineMap (a,b)) = AffineMap ((r * a),(r * b))

proof end;

theorem :: FUZZY_7:14

for s being Real
for f, g being Function of REAL,REAL holds
( dom ((f | ].-infty,s.]) +* (g | [.s,+infty.[)) = REAL & dom ((f | ].-infty,s.[) +* (g | [.s,+infty.[)) = REAL )

proof end;

theorem Th1: :: FUZZY_7:15

for a, b, c being Real st b > 0 & c > 0 holds
for x being Real holds (((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) . x = b - |.((b * (x - a)) / c).|

proof end;

theorem :: FUZZY_7:16

for a, b, c being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & ( for x being Real holds f . x = b - |.((b * (x - a)) / c).| ) holds
f = ((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)

proof end;

theorem :: FUZZY_7:17

for a, b being Real st a > 0 holds
|.(AffineMap (a,b)).| = (- ((AffineMap (a,b)) | ].-infty,((- b) / a).[)) +* ((AffineMap (a,b)) | [.((- b) / a),+infty.[)

proof end;

theorem :: FUZZY_7:18

for a, b being Real st a < 0 holds
|.(AffineMap (a,b)).| = ((AffineMap (a,b)) | ].-infty,((- b) / a).[) +* (- ((AffineMap (a,b)) | [.((- b) / a),+infty.[))

proof end;

theorem Lm20A: :: FUZZY_7:19

for a, b, c being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) holds
for x being Real st not x in ['(a - c),(a + c)'] holds
f . x = 0

proof end;

theorem Th3: :: FUZZY_7:20

for a, b, c being Real
for f, g being Function of REAL,REAL st a < b & b < c holds
((f | ].-infty,b.]) +* (g | [.b,+infty.[)) | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.])

proof end;

theorem Th4: :: FUZZY_7:21

for a, b, c being Real
for f being Function of REAL,REAL st b > 0 & c > 0 holds
(((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) | [.(a - c),(a + c).] = ((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(a - c),a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,(a + c).])

proof end;

theorem :: FUZZY_7:22

for a, b, c being Real
for f being Function of REAL,REAL st a < b & b < c & f is_integrable_on ['a,c'] & f | ['a,c'] is bounded holds
( f is_integrable_on ['a,b'] & f is_integrable_on ['b,c'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & integral (f,a,c) = (integral (f,a,b)) + (integral (f,b,c)) )

proof end;

Th11X: for a, b, c, d being Real
for f being Function of REAL,REAL st a <= b & b < c & c <= d & f is_integrable_on ['a,d'] & f | ['a,d'] is bounded & ( for x being Real st x in ['a,b'] \/ ['c,d'] holds
f . x = 0 ) holds
centroid (f,['a,d']) = centroid (f,['b,c'])

proof end;

theorem :: FUZZY_7:23

for a, b, c, d being Real
for f being Function of REAL,REAL st a < b & b < c & c < d & f is_integrable_on ['a,d'] & f | ['a,d'] is bounded & ( for x being Real st x in ['a,b'] \/ ['c,d'] holds
f . x = 0 ) holds
centroid (f,['a,d']) = centroid (f,['b,c'])

proof end;

theorem Th17: :: FUZZY_7:24

for A, B being non empty closed_interval Subset of REAL
for f being Function of REAL,REAL st lower_bound B <> upper_bound B & B c= A & f is_integrable_on A & f | A is bounded & ( for x being Real st x in A \ B holds
f . x = 0 ) & f . (lower_bound B) = 0 & f . (upper_bound B) = 0 holds
centroid (f,A) = centroid (f,B)

proof end;

theorem :: FUZZY_7:25

for a, c being Real
for f being Function of REAL,REAL st c > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / c).|)) ) holds
f is triangular FuzzySet of REAL

proof end;

Lm1: for a, b, c being Real
for f being Function of REAL,REAL st b > 1 & ( for x being Real holds f . x = min (1,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
f is normalized FuzzySet of REAL

proof end;

Lm2: for a, b, c being Real
for f being Function of REAL,REAL st b > 1 & c > 0 & ( for x being Real holds f . x = min (1,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
f is trapezoidal FuzzySet of REAL

proof end;

theorem :: FUZZY_7:26

for a, b, c being Real
for f being Function of REAL,REAL st b > 1 & c > 0 & ( for x being Real holds f . x = min (1,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
( f is trapezoidal FuzzySet of REAL & f is normalized FuzzySet of REAL ) by Lm1, Lm2;

theorem :: FUZZY_7:27

for a, b, c being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) holds
f = b (#) (TriangularFS ((a - c),a,(a + c)))

proof end;

theorem Th14: :: FUZZY_7:28

for a, b, c being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) holds
f is Lipschitzian

proof end;

theorem Th15: :: FUZZY_7:29

for a, b, c being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & f | ['(a - c),(a + c)'] = ((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(lower_bound ['(a - c),(a + c)']),(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))).]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))),(upper_bound ['(a - c),(a + c)']).]) holds
centroid (f,['(a - c),(a + c)']) = a

proof end;

Lm16: for a, b, c being Real st b > 0 & c > 0 holds
for x being Real st x in ['(a - c),(a + c)'] holds
0 <= b - |.((b * (x - a)) / c).|

proof end;

theorem Th16: :: FUZZY_7:30

for a, b, c being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) holds
f | ['(a - c),(a + c)'] = ((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(lower_bound ['(a - c),(a + c)']),(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))).]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))),(upper_bound ['(a - c),(a + c)']).])

proof end;

theorem Th19: :: FUZZY_7:31

for a, b, c being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) holds
centroid (f,['(a - c),(a + c)']) = a

proof end;

theorem Lm20: :: FUZZY_7:32

for A being non empty closed_interval Subset of REAL
for a, b, c being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) holds
( f is_integrable_on A & f | A is bounded )

proof end;

theorem Lm20B: :: FUZZY_7:33

for a, b, c being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) holds
( f . (lower_bound ['(a - c),(a + c)']) = 0 & f . (a - c) = 0 & f . (upper_bound ['(a - c),(a + c)']) = 0 & f . (a + c) = 0 )

proof end;

theorem :: FUZZY_7:34

for A being non empty closed_interval Subset of REAL
for a, b, c being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & ['(a - c),(a + c)'] c= A & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) holds
centroid (f,A) = a

proof end;

theorem Lm21: :: FUZZY_7:35

for a, b, c being Real st a < b & b < c & b - a = c - b holds
centroid ((TriangularFS (a,b,c)),['a,c']) = b

proof end;

theorem Lm21L: :: FUZZY_7:36

for A being non empty closed_interval Subset of REAL
for a, b, c being Real st a < b & b < c holds
( TriangularFS (a,b,c) is_integrable_on A & (TriangularFS (a,b,c)) | A is bounded )

proof end;

theorem :: FUZZY_7:37

for a, b, c, d being Real st a < b & b < c & b - a = c - b & d <> 0 holds
centroid ((d (#) (TriangularFS (a,b,c))),['a,c']) = b

proof end;

theorem Lm22c: :: FUZZY_7:38

for A being non empty closed_interval Subset of REAL
for a, b, c, d being Real st a < b & b < c & c < d holds
( TrapezoidalFS (a,b,c,d) is_integrable_on A & (TrapezoidalFS (a,b,c,d)) | A is bounded )

proof end;

theorem Lm22d: :: FUZZY_7:39

for A being non empty closed_interval Subset of REAL
for a, b, c, d, r being Real st a < b & b < c & c < d holds
r (#) (TrapezoidalFS (a,b,c,d)) is_integrable_on A

proof end;

theorem :: FUZZY_7:40

for a1, c, a2, d being Real
for f being Function of REAL,REAL st c > 0 & d > 0 & a1 < a2 & f = (d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)))) | ['(a1 - c),(a2 + c)'] holds
f is_integrable_on ['(a1 - c),(a2 + c)']

proof end;

theorem Lm22b1p: :: FUZZY_7:41

for a, b, c being Real
for f, g being Function of REAL,REAL
for h being PartFunc of REAL,REAL st a <= b & b <= c & f is continuous & g is continuous & h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) & f . b = g . b & [.a,c.] c= dom h holds
h | [.a,c.] is continuous

proof end;

theorem :: FUZZY_7:42

for a, b, p, q being Real
for f being Function of REAL,REAL st a <> p & f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) holds
f is Lipschitzian

proof end;

theorem Th26p: :: FUZZY_7:43

for a, b, c being Real
for f, g, h being Function of REAL,REAL st a <= b & b <= c & f is continuous & g is continuous & h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) & f . b = g . b holds
integral (((id REAL) (#) h),['a,c']) = (integral (((id REAL) (#) f),['a,b'])) + (integral (((id REAL) (#) g),['b,c']))

proof end;

theorem LmSymTrape2: :: FUZZY_7:44

for a, b, c, d, r being Real st a < b & b < c & c < d holds
(((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) = (TrapezoidalFS (a,b,c,d)) | [.a,d.]

proof end;

theorem :: FUZZY_7:45

for a, b, c, d, r being Real st a < b & b < c & c < d holds
TrapezoidalFS (a,b,c,d) = ((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((TrapezoidalFS (a,b,c,d)) | [.a,d.])

proof end;

theorem LmSymTrape4: :: FUZZY_7:46

for a, b, c, d, r being Real st a < b & b < c & c < d holds
(((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.]) = (r (#) (TrapezoidalFS (a,b,c,d))) | [.a,d.]

proof end;

theorem SymTrape: :: FUZZY_7:47

for a1, c, a2, d being Real st c > 0 & d > 0 & a1 < a2 holds
(((AffineMap ((d / c),(- ((d / c) * (a1 - c))))) | [.(a1 - c),a1.]) +* ((AffineMap (0,d)) | [.a1,a2.])) +* ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))) | [.a2,(a2 + c).]) = (d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)))) | ['(a1 - c),(a2 + c)']

proof end;

Lm29n1: for a1, c, a2, d being Real st c > 0 & d > 0 & a1 < a2 holds
((integral (((id REAL) (#) (AffineMap ((d / c),(- ((d / c) * (a1 - c)))))),['(a1 - c),a1'])) + (integral (((id REAL) (#) (AffineMap (0,d))),['a1,a2']))) + (integral (((id REAL) (#) (AffineMap ((- (d / c)),((d / c) * (a2 + c))))),['a2,(a2 + c)'])) = (((1 / 2) * d) * ((c + a2) - a1)) * (a1 + a2)

proof end;

Lm29n: for a1, c, a2, d being Real
for f being Function of REAL,REAL st c > 0 & d > 0 & a1 < a2 & f | [.(a1 - c),(a2 + c).] = (((AffineMap ((d / c),(- ((d / c) * (a1 - c))))) | [.(a1 - c),a1.]) +* ((AffineMap (0,d)) | [.a1,a2.])) +* ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))) | [.a2,(a2 + c).]) holds
integral (((id REAL) (#) f),['(a1 - c),(a2 + c)']) = ((integral (((id REAL) (#) (AffineMap ((d / c),(- ((d / c) * (a1 - c)))))),['(a1 - c),a1'])) + (integral (((id REAL) (#) (AffineMap (0,d))),['a1,a2']))) + (integral (((id REAL) (#) (AffineMap ((- (d / c)),((d / c) * (a2 + c))))),['a2,(a2 + c)']))

proof end;

theorem Lm29d1: :: FUZZY_7:48

for a1, c, a2, d being Real st c > 0 & d > 0 & a1 < a2 holds
((integral ((AffineMap ((d / c),(- ((d / c) * (a1 - c))))),['(a1 - c),a1'])) + (integral ((AffineMap (0,d)),['a1,a2']))) + (integral ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))),['a2,(a2 + c)'])) = d * ((a2 - a1) + c)

proof end;

theorem Lm29d: :: FUZZY_7:49

for a1, c, a2, d being Real
for f being Function of REAL,REAL st c > 0 & d > 0 & a1 < a2 & f | [.(a1 - c),(a2 + c).] = (((AffineMap ((d / c),(- ((d / c) * (a1 - c))))) | [.(a1 - c),a1.]) +* ((AffineMap (0,d)) | [.a1,a2.])) +* ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))) | [.a2,(a2 + c).]) holds
integral (f,['(a1 - c),(a2 + c)']) = ((integral ((AffineMap ((d / c),(- ((d / c) * (a1 - c))))),['(a1 - c),a1'])) + (integral ((AffineMap (0,d)),['a1,a2']))) + (integral ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))),['a2,(a2 + c)']))

proof end;

theorem :: FUZZY_7:50

for a1, c, a2, d being Real st c > 0 & d > 0 & a1 < a2 holds
centroid ((d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)))),['(a1 - c),(a2 + c)']) = (a1 + a2) / 2

proof end;