Mechanized Mathematics and Its Applications, Works in Progress

Deﬁnition for Set of Membership Functions (Mitsuishi T.)

Regular Paper

メンバシップ関数集合の定義といくつかのメンバシップ関数の諸性質
On the Formalizations of Deﬁnition for Set ofMembership Functions and Several Types ofMembership Functions
三石 貴志 1,*
Takashi Mitsuishi1,*
1 流通科学大学経済学部
1 Faculty of Commerce, University of Marketing and Distribution Sciences,
3-1 Gakuen Nishimachi, Kobe, Japan* takashi mitsuishi@red.umds.ac.jp
Proof checked by Mizar Version: 8.1.10 and MML Version: 5.57.1355
Received: December 8, 2020. Accepted: April 30, 2021.

Abstract
In this study, valious sets of membership functions (fuzzy sets) are formalized. At
ﬁrst, the set of membership functions [1,2] is deﬁned. Next, sine curve, cosine curve andGaussian function that renges are limited to interval [0, 1] are formalized. On the other,not only curve membership functions mentioned above but also membership functions
composed of straight lines like triangular and trapezoidal are formalized. Moreover
diﬀerent from the deﬁnition in [3] fomalizations of triangular and trapezoidal function
composed of two straight lines, minimum function and maxmum functions are proposed.

1

はじめに
ファジィ推論における IF-THEN ルールは複数のファジィ集合（メンバシップ関数）によって構成されている．それゆえ IF-THEN ルールはメンバシップ関数の対とみなされてよい．ファジィ推論やファジィ制御の結果の適否は IF-THEN ルールの設定によるところが大きく，構成するメンバシップ関数が適切に選ばれることによって，ファジィ推論や制御は良好な結果を得る．筆者らはファジィ制御の最適制御に関する研究を行っており，最MMA-WiP (2021), vol.3, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.2 - ISSN 2434-5458 (Online)

1/16

Mechanized Mathematics and Its Applications, Works in Progress

Deﬁnition for Set of Membership Functions (Mitsuishi T.)

適制御問題を汎関数の最小化問題に帰着させて，最適制御を与える IF-THEN ルールの存在性を証明した [4]．
本アーティクルはそれらの成果を MIZAR システムを使って検証するために，メンバ
シップ関数（ファジィ集合）の集合を定義した．その他，三角関数やグラフが折れ線になる区分線形関数を用いたメンバシップ関数の諸性質の定式化を行った．

MIZAR におけるメンバシップ関数とファジィ集合

2

MIZAR においてファジィ理論は筆者らによって [1] により形式化が始まった．そこで，
メンバシップ関数は以下の [FUZZY 1 mode] のように値域が [0, 1] である関数として定義された．

Listing 1. FUZZY 1 modedeﬁnition
let C be non empty set ;mode Membership Func of C is [.0,1.] −valued Function of C,REAL;
end;

当初，ファジィ集合は同論文 [1] 内で集合の要素（変数）とそのメンバシップ関数値との対として次のように定義された．

Let C be a non empty set and let h be a membership function of C.
A set is called a FuzzySet of C, h if :(Def.2)

It = [: C, h◦ C :].

この定義を用いたファジィ集合論が収録された FUZZY 1，FUZZY 2 および FUZZY 4の一部の定義，定理は変更され，アーティクル FUZZY 3 は現在削除され欠番となっている．FUZZY 3 が削除された後に，以下の [FUZNUM 1 mode] にてメンバシップ関数（Membership Func）とファジィ集合（FuzzySet）は同一視することとされた．

Listing 2. FUZNUM 1 modedeﬁnition
let C be non empty set ;mode FuzzySet of C is Membership Func of C;
end;

3

メンバシップ関数の形式化

3.1

メンバシップ関数（ファジィ集合）の集合の定義

本アーティクルではメンバシップ関数の集合を以下のように定義した．これにより，ファジィ集合族 [FUZZY 5:2] が定式化された．

MMA-WiP (2021), vol.3, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.2 - ISSN 2434-5458 (Online)

2/16

Mechanized Mathematics and Its Applications, Works in Progress

Deﬁnition for Set of Membership Functions (Mitsuishi T.)

Listing 3. FUZZY 5:def 1, FUZZY 5:2
deﬁnition
let X be non empty set;func Membership Funcs (X) −> set means :: FUZZY 5:def 1
for f being object holds f in it iﬀ f is Membership Func of X ;end;theorem :: FUZZY 5:2
Membership Funcs (REAL) ={f where f is Function of REAL,REAL : f is FuzzySet of REAL};

3.2

種々のメンバシップ関数集合

ファジィ理論の実用化に際し，様々なメンバシップ関数が用いられる．その中には，三角型形や台形型，S 型，Z 型のように直線のみで構成された関数や，釣鐘型のような三角関数やガウス関数の値域を [0, 1] に限定した関数がある．以下の定理では，それらの集合
が [FUZZY 5:def 1] で定義した Membership Funcs の部分集合になっていることを示す．

Listing 4. FUZZY 5:15,35,57,61
theorem :: FUZZY 5:15
for g be Function of REAL,REAL holds{f where f is Function of REAL,REAL : for x be Real holds f.x= min(1,max(0, g.x))} c= Membership Funcs (REAL);
theorem :: FUZZY 5:35
{f where f is Function of REAL,REAL, a,b,c,d is Real: for x be Real holds f.x= max(0,min(1, c∗sin(a∗x+b)+d))}c= Membership Funcs (REAL);
theorem :: FUZZY 5:57
{f where f is Function of REAL,REAL, a,b,c is Real: b <> 0 & for x be Real holds f.x= max(0,min(1, exp R(−(x−a)ˆ2/(2∗bˆ2))+c))}
c= Membership Funcs (REAL);
theorem :: FUZZY 5:61
{f where f is Function of REAL,REAL, a,b is Real: for x be Real holds f.x= max(0,min(1, AﬃneMap (a,b).x))}
c= Membership Funcs (REAL);

3.3

メンバシップ関数のリプシッツ連続性

IF-THEN ルールを構成するファジィ集合（前件部）のメンバシップ関数のリプシッツ
連続性は，ファジィ制御における状態方程式の解の存在性のための必要条件の一つとなる [4]．そこで種々のメンバシップ関数のリプシッツ連続性を証明した．以下の定理は任意の関数に対して頭切り計算のリプシッツ連続性を導く．また c = 1, d = 0 とすれば任意の関数の値域を [0, 1] に変換が可能で，その関数のリプシッツ連続性の証明に適用しうる．

Listing 5. FUZZY 5:13,69
theorem :: FUZZY 5:13
for a,b,c,d being Real holds |. max(c,min(d,a)) − max(c,min(d,b)) .| <= |. a−b .|;theorem :: FUZZY 5:69
for f be Function of REAL,REAL, a,b,c be Real st( b <> 0 & for x be Real holds f.x= max(0,min(1, c∗(1−|.(x−a)/b.|))) ) holds f is Lipschitzian;

MMA-WiP (2021), vol.3, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.2 - ISSN 2434-5458 (Online)

3/16

Mechanized Mathematics and Its Applications, Works in Progress

Deﬁnition for Set of Membership Functions (Mitsuishi T.)

以下の任意の実数 x に対する不等式 | sin x| ≤ |x|（[FUZZY 5:40]）は，Lagrange The-

orem と三角関数の導関数 [ROLLE:4, SIN COS:64] より導かれた [5, 6]．
Listing 6. ROLLE:4, SIN COS:64
theorem :: ROLLE:4
for x, t being Real st 0 < t holds
for f being PartFunc of REAL,REAL st [.x,(x + t).] c= dom f & f | [.x,(x + t).] is continuous &f is diﬀerentiable on ].x,(x + t).[ holds
ex s being Real st ( 0 < s & s < 1 & f . (x + t) = (f . x) + (t ∗ (diﬀ (f,(x + (s ∗ t))))) )；theorem Th63: :: SIN COS:64
for p being Real holds( sin is diﬀerentiable in p & diﬀ (sin,p) = cos . p );Listing 7. FUZZY 5:40
theorem :: FUZZY 5:40
for x being Real holds |. sin x .| <= |.x.|;

これにより，三角関数を用いたメンバシップ関数のリプシッツ連続性が示せた．

Listing 8. FUZZY 5:45
theorem :: FUZZY 5:45
for f be Function of REAL,REAL, a,b,c,d be Real stfor x be Real holds f.x= max(0,min(1, c∗sin(a∗x+b)+d)) holds f is Lipschitzian;

3.4

周期関数型メンバシップ関数

ファジィ推論やファジィ制御の対象事項として，方向や時間，色彩等は十分該当し得る．これらの事項を表すメンバシップ関数（ファジィ集合）は周期性を有する [7]．そこ
で，それらの推論・制御手法の MIZAR による数学的検証の道具となるべく，周期関数型
メンバシップ関数を正弦関数によって定式化した．以下の定理は正弦関数によるメンバ
シップ関数が周期関数型メンバシップ関数であることを示し，特に [FUZZY 5:28] はその周期が 2πia であることを表している．

Listing 9. FUZZY 5:28,29
theorem :: FUZZY 5:28
for F being Function of REAL,REAL, a,b,c,d being Real, i be Integer sta<>0 & i<>0 & for x be Real holds F.x= max(0,min(1, c∗sin(a∗x+b)+d)) holds F is (2 ∗ PI)/a ∗ i −periodic;
theorem :: FUZZY 5:29
for F being Function of REAL,REAL, a,b,c,d being Real stfor x be Real holds F.x= max(0,min(1, c∗sin(a∗x+b)+d)) holds F is periodic;

本アーティクルでは正弦についてのみであるが，余弦についても同様の定理が得られる．これについては今後必要に応じて形式化していく．

MMA-WiP (2021), vol.3, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.2 - ISSN 2434-5458 (Online)

4/16

Mechanized Mathematics and Its Applications, Works in Progress

3.5

Deﬁnition for Set of Membership Functions (Mitsuishi T.)

三角形型，台形型メンバシップ関数

三角形型および台形型メンバシップ関数は [3] にて以下のように定義されている．三角形および台形の頂点の座標，つまり適合度が 0 や 1 の定義域の値によって定義している．以下，AﬃneMap(a, b) = ax + b である．

Listing 10. FUZNUM 1:def 7,8
deﬁnition
let a, b, c be Real;assume that Z1: a < b and Z2: b < c ;func TriangularFS (a,b,c) −> FuzzySet of REAL equals :TrDef: :: FUZNUM 1:def 7(((AﬃneMap (0,0)) | (REAL \ ].a,c.[)) +∗ ((AﬃneMap ((1 / (b − a)),(− (a / (b − a))))) | [.a,b.])) +∗ ((AﬃneMap ((− (1/ (c − b))),(c / (c − b)))) | [.b,c.]);end;
deﬁnition
let a, b, c, d be Real;assume that Z1: a < b and Z2: b < c and Z3: c < d ;func TrapezoidalFS (a,b,c,d) −> FuzzySet of REAL equals :TPDef: :: FUZNUM 1:def 8((((AﬃneMap (0,0)) | (REAL \ ].a,d.[)) +∗ ((AﬃneMap ((1 / (b − a)),(− (a / (b − a))))) | [.a,b.])) +∗ ((AﬃneMap (0,1)) |[.b,c.])) +∗ ((AﬃneMap ((− (1 / (d − c))),(d / (d − c)))) | [.c,d.]);end;

一方，本アーティクルでは上述のファジィ集合を傾きの異なる 2 本の直線の方程式とMIN，MAX 演算で構成している．つまり，上記の直線の傾き a および切片 b によって定義をした．両者の等しさは下記の定理にて示されている．

Listing 11. FUZZY 5:80,86
theorem :: FUZZY 5:80
for a,b,p,q be Real st a > 0 & p > 0 & (1−b)/a < (1−q)/(−p) holds
for x be Real holds (TrapezoidalFS ((−b)/a,(1−b)/a,(1−q)/(−p),q/p)).x= max(0,min(1, ( (AﬃneMap (a,b) |].−infty,(q−b)/(a+p).[) +∗ (AﬃneMap (−p,q)|[.(q−b)/(a+p),+infty.[) ) .x ));theorem :: FUZZY 5:86
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, ( (AﬃneMap ( 1/(b−a),− a/(b−a) )|].−infty,b.[) +∗ (AﬃneMap ( − 1/(c−b),c/(c−b) )|[.b,+infty.[) ).x ));ファジィ推論において，各ルールの推論結果のメンバシップ関数を MAX 演算や和算を使って合成する計算をする際，[FUZZY 5:80] の表記のほうが扱いやすいと考える．
以下の定理は三角型および台形型メンバシップ関数のリプシッツ連続性を示している．

Listing 12. FUZZY 5:88
theorem :: FUZZY 5:88
for a,b,p,q be Real, f be Function of REAL,REAL sta>0&p>0&
for x be Real holds
f.x = max(0,min(1, ( ((AﬃneMap (a,b))|(].−infty,(q−b)/(a+p).[)) +∗ ((AﬃneMap (−p,q))|([.(q−b)/(a+p),+infty.[)) ) .x ))holds f is Lipschitzian;

この定理では，最小値 0 以上，最大値 1 以下と定めているが，別の定理にて任意の実数で成立していることを示している．さらにこの定理により，グラフが折れ線となっている区分線形関数を用いたメンバシップ関数のリプシッツ連続性が得られた．このことは，

MMA-WiP (2021), vol.3, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.2 - ISSN 2434-5458 (Online)

5/16

Mechanized Mathematics and Its Applications, Works in Progress

Deﬁnition for Set of Membership Functions (Mitsuishi T.)

メンバシップ関数を MAX 演算や和算を使って合成した後の関数のリプシッツ連続性を与えるものである．

4

まとめ
メンバシップ関数の集合を定義し，実用にて頻繁に使用されるメンバシップ関数の定式化を行った．また，三角形型，台形型のメンバシップ関数を 2 直線の傾きと切片，MIN，

MAX 演算を用いて定式化した．これによって，重心計算などの演算の際に区分線形関数の係数が煩雑になるのを回避できる．
今後はメンバシップ関数集合のコンパクト性とその上に定義された推論計算の汎関数としての連続性に関するアーティクルをそれぞれ作成し，ファジィ最適制御の存在性の検
証を行う．

参考文献
[1] Mitsuishi T, Endou N, Shidama Y. The Concept of Fuzzy Set and Membership
Function and Basic Properties of Fuzzy Set Operation. Formalized Mathematics. 2001;9(2):351–356. Available from: http://fm.mizar.org/2001-9/pdf9-2/
fuzzy_1.pdf.
[2] Mitsuishi T, Wasaki K, Shidama Y. Basic Properties of Fuzzy Set Operation andMembership Function. Formalized Mathematics. 2001;9(2):357–362. Available from:http://fm.mizar.org/2001-9/pdf9-2/fuzzy_2.pdf.
[3] Grabowski A. The Formal Construction of Fuzzy Numbers. Formalized Mathematics. 2014;22(4):321–327.
[4] Mitsuishi T, Shimada N, Homma T, Ueda M, Kochizawa M, Shidama Y. Continuity
of approximate reasoning using fuzzy number under Lukasiewicz t-norm. In: 2015
IEEE 7th International Conference on Cybernetics and Intelligent Systems (CIS)and IEEE Conference on Robotics, Automation and Mechatronics (RAM); 2015. p.
71–74.
[5] Kotowicz J, Raczkowski K, Sadowski P. Average Value Theorems for Real Functions of One Variable. Formalized Mathematics. 1990;1(4):803–805. Available from:http://fm.mizar.org/1990-1/pdf1-4/rolle.pdf.
[6] Yang Y, Shidama Y. Trigonometric Functions and Existence of Circle Ratio. Formalized Mathematics. 1998;7(2):255–263. Available from: http://fm.mizar.org/
1998-7/pdf7-2/sin_cos.pdf.
[7] Mitsuishi T. Uncertain Defuzziﬁed Value of Periodic Membership Function. In:
2018 International Electrical Engineering Congress (iEECON); 2018. p. 1–4.

MMA-WiP (2021), vol.3, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.2 - ISSN 2434-5458 (Online)

6/16

Mechanized Mathematics and Its Applications, Works in Progress

Deﬁnition for Set of Membership Functions (Mitsuishi T.)

Mizar article information
Works in Progress
FUZZY 5 Set of Membership Functions
by Takashi Mitsuishi
Summary: We have been working on the formalization of the fuzzy logic. In [1], wedeﬁned membership function and encoded some theorems concerning the membershipfunctions. In this article, we present formalization of the set of membership functions.
First, we deﬁne the set of membership function and show the membership functions
whose graphs are various shapes for example, sine, cosine and piecewise linear function.
Next, we describe continuity and periodicity of membership function. Moreover diﬀerent
from the deﬁnition in [3] fomalizations of triangular and trapezoidal function composedof two straight lines, minimum function and maxmum functions are proposed.
Listing 13. FUZZY 5 - abstract
environvocabularies NUMBERS, XBOOLE 0, SUBSET 1, XXREAL 1, CARD 1, RELAT 1, TARSKI,FUNCT 1, XXREAL 0, PARTFUN1, ARYTM 1, ARYTM 3, COMPLEX1, FUZZY 1,
MSALIMIT, FUZNUM 1, REAL 1, ORDINAL2, FCONT 1,SQUARE 1,FUNCT 3,
RCOMP 1, NUMPOLY1, JGRAPH 2, FUNCT 4,FUNCT 7, SIN COS,POWER, FUNCT 9,
INT 1,VALUED 1, FDIFF 1, SIN COS9, FUZZY 5;
notations TARSKI, XBOOLE 0, SUBSET 1, RELSET 1, NUMBERS,COMPLEX1, RELAT 1,
SQUARE 1, STRUCT 0, NORMSP 1, METRIC 1, FUNCT 1, ORDINAL1, INT 1,
XCMPLX 0,XXREAL 0,XREAL 0, XXREAL 2, VALUED 1,PARTFUN1, FUNCT 2,
FUNCT 3, FUNCT 4,FUNCT 9, FDIFF 1, MEMBERED, FINSEQ 1, FINSEQ 2,
SIN COS, RCOMP 1, MEASURE5, RFUNCT 1, PRE TOPC, COMPTS 1, TOPMETR,TAYLOR 1, POWER, SIN COS9, FCONT 1, FUZZY 1,FUZNUM 1,LFUZZY 1;
constructors ZFMISC 1, SUBSET 1, FUNCT 1, XCMPLX 0, XXREAL 0, XREAL 0,
COMPLEX1, RFUNCT 1, INTEGRA1, SEQ 4, RELSET 1, FUZZY 1, FCONT 1,
FUNCT 4,FUZNUM 1,NUMPOLY1,LFUZZY 1,RELAT 1,SIN COS,XXREAL 3,NUMBERS,SIN COS6,TOPMETR,SQUARE 1,TAYLOR 1,POWER, COMPTS 1, RCOMP 1, FINSEQ 1,
FINSEQ 2, INT 1,ORDINAL1,FUNCT 9, FDIFF 1, SIN COS9,STRUCT 0, NORMSP 1,
METRIC 1, VALUED 1, PARTFUN1;
registrations RELSET 1, NUMBERS, XXREAL 0, MEMBERED, XBOOLE 0, VALUED 0,
VALUED 1, FUNCT 2, XREAL 0, ORDINAL1, FCONT 1, RELAT 1, TOPREALB,FUNCT 4, FUNCT 1, XCMPLX 0, NAT 1, RCOMP 1,FUZNUM 1,NUMPOLY1,LFUZZY 1,SIN COS,XXREAL 3, SIN COS6, TOPMETR, SQUARE 1, SIN COS3,
CARD 3, INT 1, SUBSET 1, SIN COS9, NORMSP 1,PARTFUN1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM ;deﬁnitions XBOOLE 0, TARSKI, XXREAL 2, FUZNUM 1, NUMPOLY1, FUZZY 1,
RELAT 1, XXREAL 3, NUMBERS, SIN COS6, TOPMETR, SQUARE 1, COMPTS 1,
RCOMP 1, STRUCT 0, INT 1, SUBSET 1, SIN COS9, VALUED 1, XXREAL 0,
SIN COS, FCONT 1,FUNCT 3,PARTFUN1;
equalities FUZZY 1, RCOMP 1,FUZNUM 1,NUMPOLY1,RELAT 1,XXREAL 3,
NUMBERS,SIN COS6,SQUARE 1,FUNCT 4;
expansions TARSKI, FCONT 1,FUZNUM 1,NUMPOLY1,FUZZY 1,RELAT 1,XXREAL 3,
NUMBERS,SQUARE 1,FUNCT 4;
theorems TARSKI, FUNCT 1, ABSVALUE, XBOOLE 0,POWER,TAYLOR 1,SIN COS,COMPLEX1, XXREAL 1,XREAL 0,FCONT 1, XCMPLX 1, RCOMP 1, FUZNUM 1,
FUNCT 9, SIN COS4,ROLLE,FDIFF 1,VALUED 1,SIN COS3, SQUARE 1,
XXREAL 0, FUNCT 4, XREAL 1, FUNCT 2, FUNCT 3, SIN COS6,FUZZY 1;
schemes FUNCT 2;
begin:::: set of membership functions
deﬁnition
let X be non empty set ;MMA-WiP (2021), vol.3, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.2 - ISSN 2434-5458 (Online)

7/16

Mechanized Mathematics and Its Applications, Works in Progress

Deﬁnition for Set of Membership Functions (Mitsuishi T.)

func Membership Funcs (X) −> set means:: FUZZY 5:def 1
for f being object holds
f in it iﬀ f is Membership Func of X ;end;theorem :: FUZZY 5:1
for X be non empty set, x be object
st x in Membership Funcs (X)holds
ex f be Membership Func of X st x = f & dom f = X;
theorem :: FUZZY 5:2
Membership Funcs (REAL)={f where f is Function of REAL,REAL : f is FuzzySet of REAL};:::: characteristic function (indicator function)
theorem :: FUZZY 5:3
for A,X be non empty set holds{chi (A,X)} c= Membership Funcs (X);theorem :: FUZZY 5:4{chi([.a,b.],REAL) where a,b is Real : a <= b}c= Membership Funcs (REAL);
theorem :: FUZZY 5:5{chi(A,REAL) where A is Subset of REAL : A c= REAL}
c= Membership Funcs (REAL);
theorem :: FUZZY 5:6{f where f is FuzzySet of REAL : ex A be Subset of REAL st f=chi(A,REAL) }c= Membership Funcs (REAL);:::: membership functions using min (max) operation
theorem :: FUZZY 5:7
for f,g be Function of REAL,REAL, a being Real st
g is continuous & for x be Real holds f.x= min(a, g.x)
holds f is continuous;
theorem :: FUZZY 5:8
for F,f,g be Function of REAL,REAL stf is continuous & g is continuous &for x be Real holds F.x= min(f.x, g.x)
holds
F is continuous;
theorem :: FUZZY 5:9
for F,f,g be Function of REAL,REAL stf is continuous & g is continuous &for x be Real holds F.x= max(f.x, g.x)
holds
F is continuous;
theorem :: FUZZY 5:10
for f,g be Function of REAL,REAL,
a being Real st
g is continuous & for x be Real holds f.x= max(a, g.x)
holds f is continuous;
theorem :: FUZZY 5:11
for f,g be Function of REAL,REAL, a,b being Real st
g is continuous & for x be Real holds f.x= max(a,min(b, g.x))
holds f is continuous;
theorem :: FUZZY 5:12

MMA-WiP (2021), vol.3, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.2 - ISSN 2434-5458 (Online)

8/16

Mechanized Mathematics and Its Applications, Works in Progress

Deﬁnition for Set of Membership Functions (Mitsuishi T.)

for f,g be Function of REAL,REAL st
g is continuous & for x be Real holds f.x= max(0,min(1, g.x))
holds f is continuous;
theorem :: FUZZY 5:13
for a,b,c,d being Real holds|. max(c,min(d,a)) − max(c,min(d,b)) .| <= |. a−b .|;theorem :: FUZZY 5:14:: LeMM01Lip:
for r,s be Real, f be Function of REAL,REAL stfor x be Real holds f.x= max(r,min(s,x))
holds
f is Lipschitzian;theorem :: FUZZY 5:15
for g be Function of REAL,REAL holds{f where f is Function of REAL,REAL :for x be Real holds f.x= min(1,max(0, g.x))}
c= Membership Funcs (REAL);
theorem :: FUZZY 5:16
{f where f,g is Function of REAL,REAL :for x be Real holds f.x= max(0,min(1, g.x))}
c= Membership Funcs (REAL);
theorem :: FUZZY 5:17
for f,g be Function of REAL,REAL st(for x be Real holds f.x= max(0,min(1, g.x)))
holds
f is FuzzySet of REAL;
theorem :: FUZZY 5:18
for f,g be Function of REAL,REAL st(for x be Real holds f.x= min(1,max(0, g.x)))
holds f is FuzzySet of REAL;:::: fuzzy Set from trigonometric function
theorem :: FUZZY 5:19
{f where f is Function of REAL,REAL :ex a,b be Real st for th be Real holds f.th= 1/2∗sin(a∗th+b)+1/2}
c= Membership Funcs (REAL);
theorem :: FUZZY 5:20
{f where f is Function of REAL,REAL, a,b is Real:for th be Real holds f.th= 1/2∗sin(a∗th+b)+1/2}
c=Membership Funcs (REAL);
theorem :: FUZZY 5:21
for a,b be Real, f be Function of REAL,REAL st(for th be Real holds f.th= 1/2∗sin(a∗th+b)+1/2)
holds f is FuzzySet of REAL;
theorem :: FUZZY 5:22
{f where f is Function of REAL,REAL :ex a,b be Real st for th be Real holds f.th= 1/2∗cos(a∗th+b)+1/2}
c= Membership Funcs (REAL);
theorem :: FUZZY 5:23
for a,b be Real, f be Function of REAL,REAL st(for th be Real holds f.th= 1/2∗cos(a∗th+b)+1/2)
holds f is FuzzySet of REAL;
theorem :: FUZZY 5:24
for a,b be Real, f be FuzzySet of REAL st(a<>0 & for th be Real holds f.th= 1/2∗sin(a∗th+b)+1/2)
holds
f is normalized;

MMA-WiP (2021), vol.3, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.2 - ISSN 2434-5458 (Online)

9/16

Mechanized Mathematics and Its Applications, Works in Progress

Deﬁnition for Set of Membership Functions (Mitsuishi T.)

theorem :: FUZZY 5:25:: TrF10:
for f be FuzzySet of REAL stf in {f where f is Function of REAL,REAL :ex a,b be Real st a<>0 & for th be Real holds f.th= 1/2∗sin(a∗th+b)+1/2}
holds
f is normalized;
theorem :: FUZZY 5:26
for f be FuzzySet of REAL
for a,b be Real st a<>0 & for th be Real holds f.th= 1/2∗cos(a∗th+b)+1/2
holds
f is normalized;
theorem :: FUZZY 5:27
for f be FuzzySet of REAL stf in {f where f is Function of REAL,REAL :ex a,b be Real st a<>0 & for th be Real holds f.th= 1/2∗cos(a∗th+b)+1/2}
holds
f is normalized;:::: periodicity of membership functions
theorem :: FUZZY 5:28
for F being Function of REAL,REAL, a,b,c,d being Real, i be Integer sta<>0 & i<>0 & for x be Real holds F.x= max(0,min(1, c∗sin(a∗x+b)+d))holds
F is (2 ∗ PI)/a ∗ i −periodic;
theorem :: FUZZY 5:29
for F being Function of REAL,REAL, a,b,c,d being Real stfor x be Real holds F.x= max(0,min(1, c∗sin(a∗x+b)+d))holds
F is periodic;
theorem :: FUZZY 5:30
{f where f is Function of REAL,REAL :ex a,b be Real st for th be Real holds f.th= max(0, sin(a∗th+b))}c= Membership Funcs (REAL);
theorem :: FUZZY 5:31
for a,b be Real, f be Function of REAL,REAL st(for x be Real holds f.x= max(0, sin(a∗x+b)))
holds f is FuzzySet of REAL;
theorem :: FUZZY 5:32
{f where f is Function of REAL,REAL :ex a,b be Real st for x be Real holds f.x= max(0, cos(a∗x+b))}c= Membership Funcs (REAL);
theorem :: FUZZY 5:33
for a,b be Real, f be Function of REAL,REAL st(for x be Real holds f.x = max(0, cos(a∗x+b)))
holds f is FuzzySet of REAL;
theorem :: FUZZY 5:34
{f where f is Function of REAL,REAL, a,b,c,d is Real:for x be 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 be Real holds f.x= max(0,min(1, g.x))};theorem :: FUZZY 5:35
{f where f is Function of REAL,REAL, a,b,c,d is Real:for x be Real holds f.x= max(0,min(1, c∗sin(a∗x+b)+d))}c= Membership Funcs (REAL);
theorem :: FUZZY 5:36
for f being Function of REAL,REAL, a,b,c,d being Real st

MMA-WiP (2021), vol.3, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.2 - ISSN 2434-5458 (Online)

10/16

Mechanized Mathematics and Its Applications, Works in Progress

Deﬁnition for Set of Membership Functions (Mitsuishi T.)

for x be Real holds f.x= max(0,min(1, c∗sin(a∗x+b)+d))
holds f is FuzzySet of REAL;
theorem :: FUZZY 5:37
{f where f is Function of REAL,REAL, a,b,c,d is Real:for x be 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 be Real holds f.x= max(0,min(1, g.x))};theorem :: FUZZY 5:38
{f where f is Function of REAL,REAL, a,b,c,d is Real:for x be Real holds f.x= max(0,min(1, c∗arctan(a∗x+b)+d))}c= Membership Funcs (REAL);
theorem :: FUZZY 5:39
for f being Function of REAL,REAL, a,b,c,d being Real stfor x be Real holds f.x= max(0,min(1, c∗arctan(a∗x+b)+d))
holds f is FuzzySet of REAL;
theorem :: FUZZY 5:40
for x being Real holds|. sin x .| <= |.x.|;
theorem :: FUZZY 5:41
for x,y being Real holds |. sin x − sin y .| <= |.x−y.|;theorem :: FUZZY 5:42
for f be Function of REAL,REAL, a,b be Real stfor th be Real holds f.th = 1/2∗sin(a∗th+b)+1/2
holds f is continuous;
theorem :: FUZZY 5:43
for f be Function of REAL,REAL, a,b be Real stfor x be Real holds f.x = 1/2∗sin(a∗x+b)+1/2
holds f is continuous;
theorem :: FUZZY 5:44
for f be Function of REAL,REAL, a,b,c,d,r,s be Real stfor x be Real holds f.x= max(r,min(s, c∗sin(a∗x+b)+d))
holds f is Lipschitzian;theorem :: FUZZY 5:45
for f be Function of REAL,REAL, a,b,c,d be Real stfor x be Real holds f.x= max(0,min(1, c∗sin(a∗x+b)+d))
holds f is Lipschitzian;:::: membership functions from Gaussian function
theorem :: FUZZY 5:46
for a,b be Real, f be Function of REAL,REAL st(b <> 0 & for x be Real holds f.x= exp R(−(x−a)ˆ2/(2∗bˆ2)))holds
f is FuzzySet of REAL;
theorem :: FUZZY 5:47
for a,b be Real, f be Function of REAL,REAL st(b <> 0 & for x be Real holds f.x= exp(−(x−a)ˆ2/(2∗bˆ2)))holds
f is FuzzySet of REAL;
theorem :: FUZZY 5:48
for a,b be Real st b<>0 holds{f where f is Function of REAL,REAL :for x be Real holds f.x= exp(−(x−a)ˆ2/(2∗bˆ2))}
c= Membership Funcs (REAL);
theorem :: FUZZY 5:49
for a,b be Real, f be FuzzySet of REAL st

MMA-WiP (2021), vol.3, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.2 - ISSN 2434-5458 (Online)

11/16

Mechanized Mathematics and Its Applications, Works in Progress

Deﬁnition for Set of Membership Functions (Mitsuishi T.)(for x be Real holds f.x= exp(−(x−a)ˆ2/(2∗bˆ2)))holds
f is normalized;
theorem :: FUZZY 5:50
for x be Real st exp R x = 1 holds x = 0;
theorem :: FUZZY 5:51
for x be Real st exp x = 1 holds x = 0;
theorem :: FUZZY 5:52:: GauF02:
for a,b be Real, f be FuzzySet of REAL st(b<>0 & for x be Real holds f.x= exp(−(x−a)ˆ2/(2∗bˆ2)))holds
f is strictly−normalized;
theorem :: FUZZY 5:53
for a,b be Real, f be Function of REAL,REAL st(b<>0 & for x be Real holds f.x= exp R(−(x−a)ˆ2/(2∗bˆ2)))holds
f is continuous;
theorem :: FUZZY 5:54
for a,b,c,r,s be Real, f be Function of REAL,REAL st( b<>0 & for x be Real holds f.x= max(r,min(s, exp R(−(x−a)ˆ2/(2∗bˆ2))+c)) )holds
f is continuous;
theorem :: FUZZY 5:55
for a,b,c be Real, f be Function of REAL,REAL st( b<>0 & for x be Real holds f.x= max(0,min(1, exp R(−(x−a)ˆ2/(2∗bˆ2))+c)) )holds
f is continuous;
theorem :: FUZZY 5:56
for a,b,c be Real, f be Function of REAL,REAL st( b<>0 & for x be Real holds f.x= max(0,min(1, exp R(−(x−a)ˆ2/(2∗bˆ2))+c)) )holds
f is FuzzySet of REAL;
theorem :: FUZZY 5:57
{f where f is Function of REAL,REAL, a,b,c is Real:b <> 0 & for x be Real holds f.x= max(0,min(1, exp R(−(x−a)ˆ2/(2∗bˆ2))+c))}
c= Membership Funcs (REAL);:::: S or Z type Membership function
theorem :: FUZZY 5:58
for f be Function of REAL,REAL, a,b,r,s be Real stfor x be Real holds f.x= max(r,min(s, AﬃneMap (a,b).x))
holds f is Lipschitzian;theorem :: FUZZY 5:59
for f be Function of REAL,REAL, a,b be Real stfor x be Real holds f.x= max(0,min(1, AﬃneMap (a,b).x))
holds f is Lipschitzian;theorem :: FUZZY 5:60:: MM70:
for f be Function of REAL,REAL, a,b be Real stfor x be Real holds f.x= max(0,min(1, AﬃneMap (a,b).x))
holds f is FuzzySet of REAL;
theorem :: FUZZY 5:61
{f where f is Function of REAL,REAL, a,b is Real:for x be Real holds f.x= max(0,min(1, AﬃneMap (a,b).x))}
c= Membership Funcs (REAL);

MMA-WiP (2021), vol.3, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.2 - ISSN 2434-5458 (Online)

12/16

Mechanized Mathematics and Its Applications, Works in Progress

Deﬁnition for Set of Membership Functions (Mitsuishi T.):::: symmetrical Triangular or Trapezoidal Fuzzy Sets
theorem :: FUZZY 5:62
for a,b be Real, f be Function of REAL,REAL st(for x be Real holds f.x = max(0,1−|.(x−a)/b.|))holds f is FuzzySet of REAL;
theorem :: FUZZY 5:63
for a,b be Real st b > 0 holds
for x be Real holds
TriangularFS (a−b,a,a+b).x = max(0,1−|.(x−a)/b.|);theorem :: FUZZY 5:64
for a,b be Real, f be FuzzySet of REAL stb > 0 & (for x be Real holds f.x = max(0,1−|.(x−a)/b.|))holds f is triangular;
theorem :: FUZZY 5:65:: TR8:
for a,b be Real, f be FuzzySet of REAL stb > 0 & (for x be Real holds f.x = max(0,1−|.(x−a)/b.|))holds f is strictly−normalized;
theorem :: FUZZY 5:66
for f be Function of REAL,REAL, a,b,c be Real st( b <> 0 & for x be Real holds f.x= max(0,min(1, c∗(1−|.(x−a)/b.|))) )holds f is FuzzySet of REAL;
theorem :: FUZZY 5:67
for f be Function of REAL,REAL, a,b be Real stb>0 & for x be Real holds f.x = max(0,1−|.(x−a)/b.|)holds f is continuous;
theorem :: FUZZY 5:68
for f be Function of REAL,REAL, a,b,c,r,s be Real st( b <> 0 & for x be Real holds f.x= max(r,min(s, c∗(1−|.(x−a)/b.|))) )holds f is Lipschitzian;theorem :: FUZZY 5:69
for f be Function of REAL,REAL, a,b,c be Real st( b <> 0 & for x be Real holds f.x= max(0,min(1, c∗(1−|.(x−a)/b.|))) )holds f is Lipschitzian;theorem :: FUZZY 5:70
{f where f is Function of REAL,REAL, a,b is Real:b > 0 & for x be Real holds f.x = max(0,1−|.(x−a)/b.|)}c= Membership Funcs (REAL);
theorem :: FUZZY 5:71
{f where f is Function of REAL,REAL, a,b,c,d is Real:b <> 0 & for x be Real holds f.x= max(0,min(1, c∗(1−|.(x−a)/b.|)))}
c= Membership Funcs (REAL);:::: asymmetry Trapezoidal or Triangular membership function
theorem :: FUZZY 5:72
for a,b,p,q,s be Real holds( AﬃneMap (a,b)|].−infty,s.[ ) +∗ ( AﬃneMap (p,q)|[.s,+infty.[ )is Function of REAL,REAL;
theorem :: FUZZY 5:73:: asymTT1:
for a,b,p,q be Real, f be Function of REAL,REAL stfor x be Real holds
f.x = max(0,min(1, ( ((AﬃneMap (a,b))|(].−infty,(q−b)/(a−p).[)) +∗((AﬃneMap (p,q))|([.(q−b)/(a−p),+infty.[)) ) .x ))holds f is FuzzySet of REAL;
theorem :: FUZZY 5:74

MMA-WiP (2021), vol.3, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.2 - ISSN 2434-5458 (Online)

13/16

Mechanized Mathematics and Its Applications, Works in Progress

Deﬁnition for Set of Membership Functions (Mitsuishi T.)

for a,b,p,q be Real sta > 0 & p > 0 & (−b)/a < q/pholds (−b)/a < (q−b)/(a+p) & (q−b)/(a+p) < q/p & (a∗q+b∗p)/(a+p) > 0;
theorem :: FUZZY 5:75
for a,b,c be 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;
theorem :: FUZZY 5:76
for a,b,c,d be 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;
theorem :: FUZZY 5:77
for a,b,p,q,s be Real sta > 0 & p > 0 & (s−b)/a = (s−q)/(−p)
holds (s−b)/a= (q−b)/(a+p) & (s−q)/(−p) = (q−b)/(a+p);
theorem :: FUZZY 5:78
for a,b,p,q be Real sta > 0 & p > 0 & (−b)/a < q/p & (1−b)/a = (1−q)/(−p) holds
for x be Real holds(TriangularFS ((−b)/a,(1−b)/a,q/p)).x= max(0,min(1, ((AﬃneMap (a,b) |].−infty,(q−b)/(a+p).[) +∗(AﬃneMap (−p,q)|[.(q−b)/(a+p),+infty.[)).x ));theorem :: FUZZY 5:79
for a,b,p,q,s be Real sta > 0 & p > 0 & (s−b)/a < (s−q)/(−p) holds(s−b)/a < (q−b)/(a+p) & (q−b)/(a+p) < (s−q)/(−p) ;theorem :: FUZZY 5:80
for a,b,p,q be Real sta > 0 & p > 0 & (1−b)/a < (1−q)/(−p) holds
for x be Real holds(TrapezoidalFS ((−b)/a,(1−b)/a,(1−q)/(−p),q/p)).x= max(0,min(1, ( (AﬃneMap (a,b) |].−infty,(q−b)/(a+p).[) +∗(AﬃneMap (−p,q)|[.(q−b)/(a+p),+infty.[) ) .x ));theorem :: FUZZY 5:81
for x,y be Real st x >= 0 & x <= yholds |.x.| <= |.y.|;theorem :: FUZZY 5:82
for x,y be Real st x <= 0 & y <= xholds |.x.| <= |.y.|;theorem :: FUZZY 5:83
for a,b,p,q be Real, f be Function of REAL,REAL st a > 0 & p > 0 &f = (AﬃneMap (a,b)|].−infty,(q−b)/(a+p).[) +∗(AﬃneMap (−p,q)|[.(q−b)/(a+p),+infty.[)holds f is Lipschitzian;theorem :: FUZZY 5:84
for a,b,p,q be Real st a > 0 & p > 0
holds
ex r being Real st(0<r&( for x1, x2 being Real st
x1 in dom ((AﬃneMap (a,b)|].−infty,(q−b)/(a+p).[)+∗ (AﬃneMap (−p,q)|[.(q−b)/(a+p),+infty.[)) &x2 in dom ((AﬃneMap (a,b)|].−infty,(q−b)/(a+p).[)+∗ (AﬃneMap (−p,q)|[.(q−b)/(a+p),+infty.[)) holds|. ((AﬃneMap (a,b)|].−infty,(q−b)/(a+p).[)

MMA-WiP (2021), vol.3, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.2 - ISSN 2434-5458 (Online)

14/16

Mechanized Mathematics and Its Applications, Works in Progress

Deﬁnition for Set of Membership Functions (Mitsuishi T.)+∗ (AﬃneMap (−p,q)|[.(q−b)/(a+p),+infty.[)) . x1
− ((AﬃneMap (a,b)|].−infty,(q−b)/(a+p).[)+∗ (AﬃneMap (−p,q)|[.(q−b)/(a+p),+infty.[)) . x2.|<= r ∗ |.(x1 − x2).| ) );theorem :: FUZZY 5:85
for a,b,p,q,r,s be Real, f be Function of REAL,REAL sta>0&p>0&
for x be Real holds
f.x = max(r,min(s, ( (AﬃneMap (a,b)|].−infty,(q−b)/(a+p).[) +∗(AﬃneMap (−p,q)|[.(q−b)/(a+p),+infty.[) ) .x ))holds f is Lipschitzian;theorem :: FUZZY 5:86
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, ( (AﬃneMap ( 1/(b−a),− a/(b−a) )|].−infty,b.[) +∗(AﬃneMap ( − 1/(c−b),c/(c−b) )|[.b,+infty.[) ).x ));theorem :: FUZZY 5:87
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, ((AﬃneMap ( 1/(b−a),− a/(b−a) )|].−infty,(b∗d−a∗c)/(d−c+b−a).[) +∗(AﬃneMap ( − 1/(d−c),d/(d−c) )|[.(b∗d−a∗c)/(d−c+b−a),+infty.[) ).x ));theorem :: FUZZY 5:88
for a,b,p,q be Real, f be Function of REAL,REAL sta>0&p>0&
for x be Real holds
f.x = max(0,min(1, ( ((AﬃneMap (a,b))|(].−infty,(q−b)/(a+p).[)) +∗((AﬃneMap (−p,q))|([.(q−b)/(a+p),+infty.[)) ) .x ))holds f is Lipschitzian;theorem :: FUZZY 5:89
for a, b, c being Real st a < b & b < c holds
TriangularFS (a,b,c) is Lipschitzian;theorem :: FUZZY 5:90
for a, b, c, d being Real st a < b & b < c & c < d holds
TrapezoidalFS (a,b,c,d) is Lipschitzian;theorem :: FUZZY 5:91
for a,b,p,q be Real, f be FuzzySet of REAL sta > 0 & p > 0 & (−b)/a < q/p & (1−b)/a = (1−q)/(−p) &for x be Real holds
f.x= max(0,min(1, ( (AﬃneMap (a,b) |].−infty,(q−b)/(a+p).[) +∗(AﬃneMap (−p,q)|[.(q−b)/(a+p),+infty.[) ) .x ))holds f is triangular & f is strictly−normalized;
theorem :: FUZZY 5:92
for a,b,p,q be Real, f be FuzzySet of REAL sta > 0 & p > 0 & (1−b)/a < (1−q)/(−p) &for x be Real holds
f.x= max(0,min(1, ( (AﬃneMap (a,b) |].−infty,(q−b)/(a+p).[) +∗(AﬃneMap (−p,q)|[.(q−b)/(a+p),+infty.[) ) .x ))holds f is trapezoidal & f is normalized;
theorem :: FUZZY 5:93
{f where f is FuzzySet of REAL:f is triangular}
c= Membership Funcs (REAL);
theorem :: FUZZY 5:94
{TriangularFS (a,b,c) where a,b,c is Real : a < b & b < c}

MMA-WiP (2021), vol.3, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.2 - ISSN 2434-5458 (Online)

15/16

Mechanized Mathematics and Its Applications, Works in Progress

Deﬁnition for Set of Membership Functions (Mitsuishi T.)

c= Membership Funcs (REAL);
theorem :: FUZZY 5:95
{f where f is FuzzySet of REAL:f is trapezoidal}
c= Membership Funcs (REAL);
theorem :: FUZZY 5:96
{TrapezoidalFS (a,b,c,d) where a,b,c,d is Real : a < b & b < c & c < d}c= Membership Funcs (REAL);

MMA-WiP (2021), vol.3, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.2 - ISSN 2434-5458 (Online)

16/16