:: Triangular Fuzzy Set Composed of Two Intersecting Affine Maps
:: by Takashi Mitsuishi
::
:: Received December 2, 2025
:: Copyright (c) 2025-2026 Association of Mizar Users

Le1: for p, s being Real st p > 0 & p * s < 0 holds
p - s > 0

proof end;

theorem Th101: :: FUZZY_9:1

for p, q, s, t being Real st p > 0 & p * s < 0 holds
( t > q iff (t - q) / (p - s) > 0 )

proof end;

theorem :: FUZZY_9:2

for p, q, s, t being Real st p > 0 & p * s < 0 holds
( t < q iff (t - q) / (p - s) < 0 )

proof end;

theorem :: FUZZY_9:3

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

theorem :: FUZZY_9:4

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

theorem Th3: :: FUZZY_9:5

for a, b being Real holds
( a in REAL \ ].a,b.[ & b in REAL \ ].a,b.[ )

proof end;

theorem Th5: :: FUZZY_9:6

for a, b, c, d being Real st a < b & b < c & c < d holds
(REAL \ ].a,d.[) /\ [.b,c.] = {}

proof end;

theorem :: FUZZY_9:7

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

theorem Th13: :: FUZZY_9:8

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

theorem Th500: :: FUZZY_9:9

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

proof end;

:: ' centroid ' and area of continuous function

theorem FUZZY817: :: FUZZY_9:10

for f, g, h being Function of REAL,REAL
for a, b, c being 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 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: :: FUZZY_9:11

for a, b, c being 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 end;

theorem :: FUZZY_9:12

for a, b, c, r being Real
for f being 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 end;

theorem Th7: :: FUZZY_9:13

for a, b, c, r being Real
for f being 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 end;

theorem :: FUZZY_9:14

for p, q, s, t being Real
for 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 end;

theorem Th15: :: FUZZY_9:15

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

Th17: for a, b, c being 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 end;

theorem Th16: :: FUZZY_9:16

for a, b, c, x being 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 end;

theorem Th18: :: FUZZY_9:17

for a, b, c, x being Real st a < b & b < c & x in [.a,c.] holds
(TriangularFS (a,b,c)) . x >= 0

proof end;

theorem Th19: :: FUZZY_9:18

for a, b, c being Real
for f being 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 end;

theorem :: FUZZY_9:19

for a, b, c, r being Real
for f being 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 end;

theorem Th26: :: FUZZY_9:20

for p, q, s, t being Real
for 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 end;

theorem Th6: :: FUZZY_9:21

for a, b, c, r being Real
for f being 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 end;

theorem :: FUZZY_9:22

for a, b, c being Real st a < b & b < c holds
integral ((TriangularFS (a,b,c)) | ['a,c']) = (c - a) / 2

proof end;

Th901: for a, b, c, r being 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 end;

Th902: for a, b, r being Real st a < b holds
integral ((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))),['a,b']) = (r * (b - a)) / 2

proof end;

Th903: for b, c, r being Real st b < c holds
integral ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))),['b,c']) = (r * (c - b)) / 2

proof end;

:: Centroid of Trianglar Function@(a+b+c)/3

theorem Th25: :: FUZZY_9:23

for a, b, c, r being Real
for f being 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 end;

theorem :: FUZZY_9:24

for p, q, s, t being Real
for 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 end;

theorem Th24: :: FUZZY_9:25

for A being non empty closed_interval Subset of REAL
for p, q, r, s, t, u being Real
for f being Function of REAL,REAL st p * s < 0 & p > 0 & ( for x being 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 end;

theorem :: FUZZY_9:26

for A being non empty closed_interval Subset of REAL
for p, q, r, s, t, u being Real
for f being Function of REAL,REAL st p * s < 0 & p > 0 & ( for x being 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 end;

:: ___________
:: /|\ / |\
:: / | \ / | \
:: / | X | \
:: / | / \ | \
:: / |/ \| \
:: ------------------------------
:: a b c d

theorem Th20: :: FUZZY_9:27

for a, b, c, d being Real st a < b & b < c & c < d holds
for x being object st x in [.a,b.] holds
(TrapezoidalFS (a,b,c,d)) . x = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x

proof end;

theorem Th21: :: FUZZY_9:28

for a, b, c, d being Real st a < b & b < c & c < d holds
for x being object st x in [.b,c.] holds
(TrapezoidalFS (a,b,c,d)) . x = (AffineMap (0,1)) . x

proof end;

theorem Th22: :: FUZZY_9:29

for a, b, c, d being Real st a < b & b < c & c < d holds
for x being object st x in [.c,d.] holds
(TrapezoidalFS (a,b,c,d)) . x = (AffineMap ((- (1 / (d - c))),(d / (d - c)))) . x

proof end;

theorem Th23: :: FUZZY_9:30

for a, b, c, d being Real st a < b & b < c & c < d holds
for x being Real st not x in [.a,d.] holds
(TrapezoidalFS (a,b,c,d)) . x = 0

proof end;

theorem :: FUZZY_9:31

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

theorem :: FUZZY_9:32

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

proof end;

theorem :: FUZZY_9:33

for a, b, c being Real
for f, g being 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 end;

theorem :: FUZZY_9:34

for A being non empty closed_interval Subset of REAL
for a being Real
for 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 end;

theorem :: FUZZY_9:35

for A being non empty closed_interval Subset of REAL
for a being Real
for 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 end;

theorem :: FUZZY_9:36

for A being non empty closed_interval Subset of REAL
for a being Real
for 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 end;