:: Some Properties of Membership Functions Composed of Triangle Functions and Piecewise Linear Functions
:: by Takashi Mitsuishi
::
:: Received June 30, 2021
:: Copyright (c) 2021 Association of Mizar Users

ABS1: for x, y being Real st x >= 0 & x <= y holds
|.x.| <= |.y.|
by TOPREAL6:2;

theorem LeMM01: :: FUZZY_5:1

for a, b, c, d being Real holds |.((max (c,(min (d,a)))) - (max (c,(min (d,b))))).| <= |.(a - b).|

proof end;

theorem LmSin1: :: FUZZY_5:2

for x being Real holds |.(sin x).| <= |.x.|

proof end;

theorem LmSin2: :: FUZZY_5:3

for x, y being Real holds |.((sin x) - (sin y)).| <= |.(x - y).|

proof end;

EXpReq11: for x being Real st exp_R x = 1 holds
x = 0
by SIN_COS7:29;

theorem EXpReq12: :: FUZZY_5:4

for x being Real st exp x = 1 holds
x = 0

proof end;

theorem asymTT2: :: FUZZY_5:5

for a, b, p, q being Real st a > 0 & p > 0 & (- b) / a < q / p holds
( (- b) / a < (q - b) / (a + p) & (q - b) / (a + p) < q / p & ((a * q) + (b * p)) / (a + p) > 0 )

proof end;

theorem asymTT3: :: FUZZY_5:6

for a, b, p, q, s being Real st a > 0 & p > 0 & (s - b) / a = (s - q) / (- p) holds
( (s - b) / a = (q - b) / (a + p) & (s - q) / (- p) = (q - b) / (a + p) )

proof end;

theorem asymTT4: :: FUZZY_5:7

for a, b, p, q, s being Real st a > 0 & p > 0 & (s - b) / a < (s - q) / (- p) holds
( (s - b) / a < (q - b) / (a + p) & (q - b) / (a + p) < (s - q) / (- p) )

proof end;

definition

let X be non empty set ;

func Membership_Funcs X -> set means :Def1: :: FUZZY_5:def 1
for f being object holds
( f in it iff f is Membership_Func of X );

existence
ex b₁ being set st
for f being object holds
( f in b₁ iff f is Membership_Func of X )

proof end;

uniqueness
for b₁, b₂ being set st ( for f being object holds
( f in b₁ iff f is Membership_Func of X ) ) & ( for f being object holds
( f in b₂ iff f is Membership_Func of X ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Membership_Funcs FUZZY_5:def 1 :
for X being non empty set
for b₂ being set holds
( b₂ = Membership_Funcs X iff for f being object holds
( f in b₂ iff f is Membership_Func of X ) );

theorem LM1: :: FUZZY_5:8

for X being non empty set
for x being object st x in Membership_Funcs X holds
ex f being Membership_Func of X st
( x = f & dom f = X )

proof end;

theorem :: FUZZY_5:9

Membership_Funcs REAL = { f where f is Function of REAL,REAL : f is FuzzySet of REAL }

proof end;

:::: characteristic function (indicator function)

theorem :: FUZZY_5:10

for A, X being non empty set holds {(chi (A,X))} c= Membership_Funcs X

proof end;

theorem :: FUZZY_5:11

{ (chi ([.a,b.],REAL)) where a, b is Real : a <= b } c= Membership_Funcs REAL

proof end;

theorem :: FUZZY_5:12

{ (chi (A,REAL)) where A is Subset of REAL : A c= REAL } c= Membership_Funcs REAL

proof end;

theorem :: FUZZY_5:13

{ f where f is FuzzySet of REAL : ex A being Subset of REAL st f = chi (A,REAL) } c= Membership_Funcs REAL

proof end;

:::: membership functions using min (max) operation

theorem MMcon1: :: FUZZY_5:14

for f, g being Function of REAL,REAL
for a being Real st g is continuous & ( for x being Real holds f . x = min (a,(g . x)) ) holds
f is continuous

proof end;

theorem :: FUZZY_5:15

for F, f, g being Function of REAL,REAL st f is continuous & g is continuous & ( for x being Real holds F . x = min ((f . x),(g . x)) ) holds
F is continuous

proof end;

theorem MMcon2: :: FUZZY_5:16

for F, f, g being Function of REAL,REAL st f is continuous & g is continuous & ( for x being Real holds F . x = max ((f . x),(g . x)) ) holds
F is continuous

proof end;

theorem MMcon3: :: FUZZY_5:17

for f, g being Function of REAL,REAL
for a being Real st g is continuous & ( for x being Real holds f . x = max (a,(g . x)) ) holds
f is continuous

proof end;

theorem MMcon4: :: FUZZY_5:18

for f, g being Function of REAL,REAL
for a, b being Real st g is continuous & ( for x being Real holds f . x = max (a,(min (b,(g . x)))) ) holds
f is continuous

proof end;

theorem :: FUZZY_5:19

for f, g being Function of REAL,REAL st g is continuous & ( for x being Real holds f . x = max (0,(min (1,(g . x)))) ) holds
f is continuous by MMcon4;

theorem LmSin3: :: FUZZY_5:20

for f being Function of REAL,REAL
for a, b being Real st ( for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) ) holds
f is continuous

proof end;

theorem :: FUZZY_5:21

for f being Function of REAL,REAL
for a, b being Real st ( for x being Real holds f . x = ((1 / 2) * (sin ((a * x) + b))) + (1 / 2) ) holds
f is continuous by LmSin3;

theorem :: FUZZY_5:22

for r, s being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = max (r,(min (s,x))) ) holds
f is Lipschitzian

proof end;

theorem MM3: :: FUZZY_5:23

for g being Function of REAL,REAL holds { f where f is Function of REAL,REAL : for x being Real holds f . x = min (1,(max (0,(g . x)))) } c= Membership_Funcs REAL

proof end;

MM4: for g being Function of REAL,REAL holds { f where f is Function of REAL,REAL : for x being Real holds f . x = max (0,(min (1,(g . x)))) } c= Membership_Funcs REAL

proof end;

theorem MM41: :: FUZZY_5:24

{ f where f, g is Function of REAL,REAL : for x being Real holds f . x = max (0,(min (1,(g . x)))) } c= Membership_Funcs REAL

proof end;

theorem MM40: :: FUZZY_5:25

for f, g being Function of REAL,REAL st ( for x being Real holds f . x = max (0,(min (1,(g . x)))) ) holds
f is FuzzySet of REAL

proof end;

theorem :: FUZZY_5:26

for f, g being Function of REAL,REAL st ( for x being Real holds f . x = min (1,(max (0,(g . x)))) ) holds
f is FuzzySet of REAL

proof end;

:::: fuzzy Set from trigonometric function

theorem :: FUZZY_5:27

{ f where f is Function of REAL,REAL : ex a, b being Real st
for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) } c= Membership_Funcs REAL

proof end;

theorem TrF11: :: FUZZY_5:28

{ f where f is Function of REAL,REAL, a, b is Real : for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) } c= Membership_Funcs REAL

proof end;

theorem :: FUZZY_5:29

for a, b being Real
for f being Function of REAL,REAL st ( for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) ) holds
f is FuzzySet of REAL

proof end;

theorem TrF2: :: FUZZY_5:30

{ f where f is Function of REAL,REAL : ex a, b being Real st
for th being Real holds f . th = ((1 / 2) * (cos ((a * th) + b))) + (1 / 2) } c= Membership_Funcs REAL

proof end;

theorem :: FUZZY_5:31

for a, b being Real
for f being Function of REAL,REAL st ( for th being Real holds f . th = ((1 / 2) * (cos ((a * th) + b))) + (1 / 2) ) holds
f is FuzzySet of REAL

proof end;

theorem :: FUZZY_5:32

for a, b being Real
for f being FuzzySet of REAL st a <> 0 & ( for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) ) holds
f is normalized

proof end;

theorem :: FUZZY_5:33

for f being FuzzySet of REAL st f in { f where f is Function of REAL,REAL : ex a, b being Real st
( a <> 0 & ( for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) ) ) } holds
f is normalized

proof end;

theorem TrF22: :: FUZZY_5:34

for f being FuzzySet of REAL
for a, b being Real st a <> 0 & ( for th being Real holds f . th = ((1 / 2) * (cos ((a * th) + b))) + (1 / 2) ) holds
f is normalized

proof end;

theorem :: FUZZY_5:35

for f being FuzzySet of REAL st f in { f where f is Function of REAL,REAL : ex a, b being Real st
( a <> 0 & ( for th being Real holds f . th = ((1 / 2) * (cos ((a * th) + b))) + (1 / 2) ) ) } holds
f is normalized

proof end;

:::: periodicity of membership functions

theorem TrF160: :: FUZZY_5:36

for F being Function of REAL,REAL
for a, b, c, d being Real
for i being Integer st a <> 0 & i <> 0 & ( for x being Real holds F . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) ) holds
F is ((2 * PI) / a) * i -periodic

proof end;

theorem :: FUZZY_5:37

for F being Function of REAL,REAL
for a, b, c, d being Real st ( for x being Real holds F . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) ) holds
F is periodic

proof end;

theorem MM1: :: FUZZY_5:38

{ f where f is Function of REAL,REAL : ex a, b being Real st
for th being Real holds f . th = max (0,(sin ((a * th) + b))) } c= Membership_Funcs REAL

proof end;

theorem :: FUZZY_5:39

for a, b being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = max (0,(sin ((a * x) + b))) ) holds
f is FuzzySet of REAL

proof end;

theorem MM2: :: FUZZY_5:40

{ f where f is Function of REAL,REAL : ex a, b being Real st
for x being Real holds f . x = max (0,(cos ((a * x) + b))) } c= Membership_Funcs REAL

proof end;

theorem :: FUZZY_5:41

for a, b being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = max (0,(cos ((a * x) + b))) ) holds
f is FuzzySet of REAL

proof end;

theorem :: FUZZY_5:42

{ f where f is Function of REAL,REAL, a, b, c, d is Real : for x being Real holds f . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) } c= { f where f, g is Function of REAL,REAL : for x being Real holds f . x = max (0,(min (1,(g . x)))) }

proof end;

theorem MM5a: :: FUZZY_5:43

{ f where f is Function of REAL,REAL, a, b, c, d is Real : for x being Real holds f . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) } c= Membership_Funcs REAL

proof end;

theorem :: FUZZY_5:44

for f being Function of REAL,REAL
for a, b, c, d being Real st ( for x being Real holds f . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) ) holds
f is FuzzySet of REAL

proof end;

theorem MM60: :: FUZZY_5:45

{ f where f is Function of REAL,REAL, a, b, c, d is Real : for x being Real holds f . x = max (0,(min (1,((c * (arctan ((a * x) + b))) + d)))) } c= { f where f, g is Function of REAL,REAL : for x being Real holds f . x = max (0,(min (1,(g . x)))) }

proof end;

theorem :: FUZZY_5:46

{ f where f is Function of REAL,REAL, a, b, c, d is Real : for x being Real holds f . x = max (0,(min (1,((c * (arctan ((a * x) + b))) + d)))) } c= Membership_Funcs REAL by MM60, MM41;

theorem :: FUZZY_5:47

for f being Function of REAL,REAL
for a, b, c, d being Real st ( for x being Real holds f . x = max (0,(min (1,((c * (arctan ((a * x) + b))) + d)))) ) holds
f is FuzzySet of REAL

proof end;

theorem MMLip1: :: FUZZY_5:48

for f being Function of REAL,REAL
for a, b, c, d, r, s being Real st ( for x being Real holds f . x = max (r,(min (s,((c * (sin ((a * x) + b))) + d)))) ) holds
f is Lipschitzian

proof end;

theorem :: FUZZY_5:49

for f being Function of REAL,REAL
for a, b, c, d being Real st ( for x being Real holds f . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) ) holds
f is Lipschitzian by MMLip1;

:::: membership functions from Gaussian function

theorem GauF04: :: FUZZY_5:50

for a, b being Real
for f being Function of REAL,REAL st b <> 0 & ( for x being Real holds f . x = exp_R (- (((x - a) ^2) / (2 * (b ^2)))) ) holds
f is FuzzySet of REAL

proof end;

theorem GauF04complex: :: FUZZY_5:51

for a, b being Real
for f being Function of REAL,REAL st b <> 0 & ( for x being Real holds f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) ) holds
f is FuzzySet of REAL

proof end;

theorem :: FUZZY_5:52

for a, b being Real st b <> 0 holds
{ f where f is Function of REAL,REAL : for x being Real holds f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) } c= Membership_Funcs REAL

proof end;

theorem :: FUZZY_5:53

for a, b being Real
for f being FuzzySet of REAL st ( for x being Real holds f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) ) holds
f is normalized

proof end;

theorem :: FUZZY_5:54

for a, b being Real
for f being FuzzySet of REAL st b <> 0 & ( for x being Real holds f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) ) holds
f is strictly-normalized

proof end;

theorem GauF05: :: FUZZY_5:55

for a, b being Real
for f being Function of REAL,REAL st b <> 0 & ( for x being Real holds f . x = exp_R (- (((x - a) ^2) / (2 * (b ^2)))) ) holds
f is continuous

proof end;

theorem GauF06: :: FUZZY_5:56

for a, b, c, r, s being Real
for f being Function of REAL,REAL st b <> 0 & ( for x being Real holds f . x = max (r,(min (s,((exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c)))) ) holds
f is continuous

proof end;

theorem :: FUZZY_5:57

for a, b, c being Real
for f being Function of REAL,REAL st b <> 0 & ( for x being Real holds f . x = max (0,(min (1,((exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c)))) ) holds
f is continuous by GauF06;

theorem GauF07: :: FUZZY_5:58

for a, b, c being Real
for f being Function of REAL,REAL st b <> 0 & ( for x being Real holds f . x = max (0,(min (1,((exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c)))) ) holds
f is FuzzySet of REAL

proof end;

theorem :: FUZZY_5:59

{ f where f is Function of REAL,REAL, a, b, c is Real : ( b <> 0 & ( for x being Real holds f . x = max (0,(min (1,((exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c)))) ) ) } c= Membership_Funcs REAL

proof end;

:::: S or Z type Membership function

theorem MMLip3: :: FUZZY_5:60

for f being Function of REAL,REAL
for a, b, r, s being Real st ( for x being Real holds f . x = max (r,(min (s,((AffineMap (a,b)) . x)))) ) holds
f is Lipschitzian

proof end;

theorem :: FUZZY_5:61

for f being Function of REAL,REAL
for a, b being Real st ( for x being Real holds f . x = max (0,(min (1,((AffineMap (a,b)) . x)))) ) holds
f is Lipschitzian by MMLip3;

theorem :: FUZZY_5:62

for f being Function of REAL,REAL
for a, b being Real st ( for x being Real holds f . x = max (0,(min (1,((AffineMap (a,b)) . x)))) ) holds
f is FuzzySet of REAL by MM40;

theorem :: FUZZY_5:63

{ f where f is Function of REAL,REAL, a, b is Real : for x being Real holds f . x = max (0,(min (1,((AffineMap (a,b)) . x)))) } c= Membership_Funcs REAL

proof end;

:::: symmetrical Triangular or Trapezoidal Fuzzy Sets

theorem :: FUZZY_5:64

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

proof end;

LmABS: for a, x being Real st 0 <= a holds
( ( x <= - a or a <= x ) iff a <= |.x.| )

proof end;

theorem TR6: :: FUZZY_5:65

for a, b being Real st b > 0 holds
for x being Real holds (TriangularFS ((a - b),a,(a + b))) . x = max (0,(1 - |.((x - a) / b).|))

proof end;

theorem :: FUZZY_5:66

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

proof end;

theorem :: FUZZY_5:67

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

proof end;

theorem MM60: :: FUZZY_5:68

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

proof end;

theorem :: FUZZY_5:69

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

proof end;

theorem MMLip2: :: FUZZY_5:70

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

proof end;

theorem :: FUZZY_5:71

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

TR2XX: { (TriangularFS (a,b,c)) where a, b, c is Real : ( a < b & b < c ) } c= Membership_Funcs REAL

proof end;

theorem :: FUZZY_5:72

{ f where f is Function of REAL,REAL, a, b is Real : ( b > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) ) } c= Membership_Funcs REAL

proof end;

theorem :: FUZZY_5:73

{ f where f is Function of REAL,REAL, a, b, c, d is Real : ( b <> 0 & ( for x being Real holds f . x = max (0,(min (1,(c * (1 - |.((x - a) / b).|))))) ) ) } c= Membership_Funcs REAL

proof end;

:::: asymmetry Trapezoidal or Triangular membership function

theorem asymTT10: :: FUZZY_5:74

for a, b, p, q, s being Real holds ((AffineMap (a,b)) | ].-infty,s.[) +* ((AffineMap (p,q)) | [.s,+infty.[) is Function of REAL,REAL

proof end;

theorem :: FUZZY_5:75

for a, b, p, q being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[)) . x)))) ) holds
f is FuzzySet of REAL

proof end;

theorem TrAng1: :: FUZZY_5:76

for a, b, c being Real st a < b & b < c holds
( (TriangularFS (a,b,c)) . a = 0 & (TriangularFS (a,b,c)) . b = 1 & (TriangularFS (a,b,c)) . c = 0 )

proof end;

theorem TrZoi1: :: FUZZY_5:77

for a, b, c, d being Real st a < b & b < c & c < d holds
( (TrapezoidalFS (a,b,c,d)) . a = 0 & (TrapezoidalFS (a,b,c,d)) . b = 1 & (TrapezoidalFS (a,b,c,d)) . c = 1 & (TrapezoidalFS (a,b,c,d)) . d = 0 )

proof end;

theorem asymTT6: :: FUZZY_5:78

for a, b, p, q being Real st a > 0 & p > 0 & (- b) / a < q / p & (1 - b) / a = (1 - q) / (- p) holds
for x being Real holds (TriangularFS (((- b) / a),((1 - b) / a),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))

proof end;

theorem asymTT7: :: FUZZY_5:79

for a, b, p, q being Real st a > 0 & p > 0 & (1 - b) / a < (1 - q) / (- p) holds
for x being Real holds (TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))

proof end;

theorem asymTT50: :: FUZZY_5:80

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

proof end;

theorem asymTT51: :: FUZZY_5:81

for a, b, p, q being Real st a > 0 & p > 0 holds
ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom (((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) & x2 in dom (((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) holds
|.(((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x1) - ((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x2)).| <= r * |.(x1 - x2).| ) )

proof end;

theorem asymTT5: :: FUZZY_5:82

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

proof end;

theorem asymTT9: :: FUZZY_5:83

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

proof end;

theorem asymTT8: :: FUZZY_5:84

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

proof end;

theorem :: FUZZY_5:85

for a, b, p, q being Real
for f being Function of REAL,REAL st a > 0 & p > 0 & ( for x being Real holds f . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) ) holds
f is Lipschitzian by asymTT5;

theorem :: FUZZY_5:86

for a, b, c being Real st a < b & b < c holds
TriangularFS (a,b,c) is Lipschitzian

proof end;

theorem :: FUZZY_5:87

for a, b, c, d being Real st a < b & b < c & c < d holds
TrapezoidalFS (a,b,c,d) is Lipschitzian

proof end;

theorem :: FUZZY_5:88

for a, b, p, q being Real
for f being FuzzySet of REAL st a > 0 & p > 0 & (- b) / a < q / p & (1 - b) / a = (1 - q) / (- p) & ( for x being Real holds f . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) ) holds
( f is triangular & f is strictly-normalized )

proof end;

theorem :: FUZZY_5:89

for a, b, p, q being Real
for f being FuzzySet of REAL st a > 0 & p > 0 & (1 - b) / a < (1 - q) / (- p) & ( for x being Real holds f . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) ) holds
( f is trapezoidal & f is normalized )

proof end;

theorem :: FUZZY_5:90

{ f where f is FuzzySet of REAL : f is triangular } c= Membership_Funcs REAL

proof end;

theorem :: FUZZY_5:91

{ (TriangularFS (a,b,c)) where a, b, c is Real : ( a < b & b < c ) } c= Membership_Funcs REAL by TR2XX;

theorem :: FUZZY_5:92

{ f where f is FuzzySet of REAL : f is trapezoidal } c= Membership_Funcs REAL

proof end;

theorem :: FUZZY_5:93

{ (TrapezoidalFS (a,b,c,d)) where a, b, c, d is Real : ( a < b & b < c & c < d ) } c= Membership_Funcs REAL

proof end;