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

EXpReq11: for x being Real st exp_R x = 1 holds

x = 0

by SIN_COS7:29;

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 )

( (- 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) )

( (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) )

( (s - b) / a < (q - b) / (a + p) & (q - b) / (a + p) < (s - q) / (- p) )

proof end;

definition

let X be non empty set ;

ex b_{1} being set st

for f being object holds

( f in b_{1} iff f is Membership_Func of X )

for b_{1}, b_{2} being set st ( for f being object holds

( f in b_{1} iff f is Membership_Func of X ) ) & ( for f being object holds

( f in b_{2} iff f is Membership_Func of X ) ) holds

b_{1} = b_{2}

end;
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 for f being object holds

( f in it iff f is Membership_Func of X );

ex b

for f being object holds

( f in b

proof end;

uniqueness for b

( f in b

( f in b

b

proof end;

:: deftheorem Def1 defines Membership_Funcs FUZZY_5:def 1 :

for X being non empty set

for b_{2} being set holds

( b_{2} = Membership_Funcs X iff for f being object holds

( f in b_{2} iff f is Membership_Func of X ) );

for X being non empty set

for b

( b

( f in b

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 )

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;

:::: characteristic function (indicator function)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

( 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

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

( 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

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

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

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

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

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

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

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

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

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

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

:::: 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

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

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

{ 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

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

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

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

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

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

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

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

theorem :: FUZZY_5:62

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

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).|))

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

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

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

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

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

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

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

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 )

( (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 )

( (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))))

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))))

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

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).| ) )

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

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))))

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))))

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

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 )

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 )

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:91

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

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;