Mechanized Mathematics and Its Applications, Works in Progress

Centroids of Membership Functions (Mitsuishi T.)

Regular Paper

二等辺三角形型および等脚台形型メンバシップ関数の重心法を用いた非ファジィ化値
Centroids of Isosceles Triangular and Isosceles
Trapezoidal Membership Functions
三石 貴志 1,*
Takashi Mitsuishi1,*
1 長野大学企業情報学部
1 Faculty of Business and Informatics, Nagano University,
Shimonogo 658-1, Ueda, Japan* takashi-mitsuishi@nagano.ac.jp
Proof checked by Mizar Version: 8.1.11 and MML Version: 5.68.1412
Received: December 1, 2022. Accepted: March 14, 2023.

Abstract
The centroids of isosceles triangular and trapezoidal membership functions are mentioned in this paper. We proved the agreement of the same function expressed withdifferent parameters and formalized those centroid with those parameters. In addition,
various properties of membership functions on intervals where the endpoints of thedomain are fixed and on general intervals are formalized.

1

はじめに
ファジィ集合を表すメンバシップ関数の形状は，大別すると z 型，π 型，s 型の 3 種類がある．そのうち π 型には，直線のみで構成される三角型，台形型などがあり，シグモイ
ド関数やガウス関数などの曲線で構成される釣り鐘型と呼ばれる形状も提案されている．
設計者の主観で決定する場合が多い前件部変数値に対するメンバシップ関数値の妥当性の判断は困難であり，そのため IF-THEN ルールをいかなる形状の関数で構成するかは，ファジィ最適化問題としてさまざまな研究がなされてきた [1] [2]．そのような背景により，従来実用においては，推論計算の容易さから三角型，台形型のメンバシップ関数が適用されてきた．そして左右非対称な形状に必要性がない場合には，左右対称な二等辺三

MMA-WiP (2023), vol.5, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.1 - ISSN 2434-5458 (Online)

1/13

Mechanized Mathematics and Its Applications, Works in Progress

Centroids of Membership Functions (Mitsuishi T.)

角形，等脚台形が多く用いられている．そこで本研究では，これらのメンバシップ関数の形式化とともに重心法による非ファジィ化値の形式化を行った．
非ファジィ化の手続きは通常推論結果に対して施すものであるが，和算やＭＡＸ演算で複数のメンバシップ関数を計算したファジィ推論結果の関数が二等辺三角形，等脚台形になることは稀である．しかしながら Center of Sums 法，面積法，高さ法，密度モーメ
ント法では，推論計算（非ファジィ化）において IF-THEN ルールを構成するファジィ集
合のメンバシップ関数の重心（非ファジィ化値）を用いている [3–5]．

2

非ファジィ化値の存在区間
後述のメンバシップ関数の重心法による非ファジィ化値は，一般的な表現を用いると，座標平面の横軸上にある図形の底辺に該当する部分の区間に存在する．
メンバシップ関数値が 0 となる，いわゆる関数のグラフによる図形の外側にあたる定義域には非ファジィ化値は存在しない．そこで次の 2 つの定理はそれらの区間を関数の定義域から除外することが可能であることを証明している．後述する定理で示す三角形型
や台形型メンバシップ関数の centroid（重心法による非ファジィ化値）の計算 [6] において，非ファジィ化の区間を三角形，台形の底にあたる区間としている．これらの証明に用いるため以下の定理は，非ファジィ化されるメンバシップ関数の定義域を非ファジィ化値が存在する区間に限定できることを表している．

Listing 1. FUZZY 7:17, FUZZY 7:21
theorem :: FUZZY 7:17
for a,b,c,d be Real, f be Function of REAL,REAL sta < b & b < c & c < d & f is integrable on [’a,d’] & f | [’a,d’] is bounded & for x be Real st x in [’a,b’] \/ [’c,d’]holds f.x = 0 holds centroid(f,[’a,d’]) = centroid(f,[’b,c’]);theorem :: FUZZY 7:21
for A,B be non empty closed interval Subset of REAL, f be Function of REAL,REAL stlower bound B <> upper bound B & B c= A & f is integrable on A & f | A is bounded &(for x be 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);

つまり上記 Listing 1 は，b ∈ [a, c] とし，閉区間 [a, c] の部分集合 [b, c]([a, b]) において
メンバシップ関数 f が f (x) = 0 であるとき，この区間には重心値が存在ぜず，その区間を省いて非ファジィ化値を計算する区間を [a, b]([b, c]) とできることを表している．

3

二等辺三角形型および等脚台形型メンバシップ関数
article [7] において，図 1 のような三角型，台形型メンバシップ関数は関数値が 1 ま

たは 0 となる定義域の値をパラメータとして以下のように TriangularFS，TrapezoidalFSの形式で定義されている．

Listing 2. FUZNUM 1:def 7, 8
deﬁnition
let a, b, c be Real;assume that
Z1: a < b andZ2: b < c ;MMA-WiP (2023), vol.5, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.1 - ISSN 2434-5458 (Online)

2/13

Mechanized Mathematics and Its Applications, Works in Progress

Centroids of Membership Functions (Mitsuishi T.)

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.]);coherence
proof end;
end;
deﬁnition
let a, b, c, d be Real;assume that
Z1: a < b andZ2: b < c andZ3: 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.]);coherence
proof end;
end;

b
1

1

1

a

b

a b

c

c d

a-c

a

a+c

図 1. Triangular Membership Functions and Trapezoidal Membership Function

Listing 3. FUZNUM 1:def 9
deﬁnition
let F be FuzzySet of REAL;
attr F is triangular means :: FUZNUM 1:def 9
ex a, b, c being Real st F = TriangularFS (a,b,c);
attr F is trapezoidal means :: FUZNUM 1:def 10
ex a, b, c, d being Real st F = TrapezoidalFS (a,b,c,d);end;

本研究では MAX 演算と絶対値記号を用いて，図 1 のような座標平面上において底辺の長さが 2c(c > 0) で，頂点の座標が (a, b) である二等辺三角形型の関数 f (x) を形式化した．

b(x − a)f (x) = max 0, b −
c


(1)

式 (1) の絶対値の内側の関数は以下のように区分線形関数 [8] として表した．

Listing 4. FUZZY 7:4
theorem :: FUZZY 7:4
for a,b,c be Real st b > 0 & c > 0 holds
for x be Real holds( AﬃneMap ( b/c,b−a∗b/c) | ]. −infty,a .]+∗ AﬃneMap (−b/c,b+a∗b/c) | [. a,+infty .[ ).x = b − |. b∗(x−a)/c .|;MMA-WiP (2023), vol.5, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.1 - ISSN 2434-5458 (Online)

3/13

Mechanized Mathematics and Its Applications, Works in Progress

Centroids of Membership Functions (Mitsuishi T.)

さらに区分的線形関数は Mizar で積分を形式化するうえで比較的使いやすい AffineMap
を用いる [9]．
以下の定理は，上述の二等辺三角形型の関数の頂点の座標が (a, 1) であるとき，三角型メンバシップ関数であることを示している．つまり上述の Listing 3 を満足している．

Listing 5. FUZZY 7:3
theorem :: FUZZY 7:3
for a,c be Real, f be Function of REAL,REAL st c > 0 & ( for x be Real holds f.x = max(0, 1 − |. (x−a)/c .|) )holds f is FuzzySet of REAL & f is triangular FuzzySet of REAL;

一方，台形型メンバシップ関数は三角形型メンバシップ関数に MIN 関数による頭切り(clipping method) を適用して表現が可能である．式 (1) で示される二等辺三角形メンバ
シップ関数に MIN 関数を使って関数値１で頭切りをすると台形型メンバシップ関数の条
件を満足する．

Listing 6. FUZZY 7:6
theorem :: FUZZY 7:6
for a,b,c be Real, f be Function of REAL,REAL stb > 1 & c > 0 & ( for x be Real holds f.x = min(1, max(0, b − |. b∗(x−a)/c .|)) ) holds
f is FuzzySet of REAL & f is trapezoidal FuzzySet of REAL & f is normalized FuzzySet of REAL;

4

Lipschitz 連続性
筆者らはファジィ制御の最適制御存在性の証明において，ファジィ推論結果の前件部

変数に関する Lipschitzian 連続性の考察を行った [10, 11]．以下の 2 定理は，今後それらの証明の Mizar による検証に適用される見込みである．1 つめは本稿で形式化したメンバ
シップ関数に対するもので，他方は区分的線形関数に対するものである．

Listing 7. FUZZY 7:24, FUZZY 7:38
theorem :: FUZZY 7:24
for a,b,c be Real, f be Function of REAL,REAL stb > 0 & c > 0 & (for x be Real holds f.x = max(0,b−|. b∗(x−a)/c .|)) holds
f is Lipschitzian;theorem :: FUZZY 7:38
for a,b,p,q be Real, f be Function of REAL,REAL st a <> p &f = (AﬃneMap (a,b)|].−infty,(q−b)/(a−p).]) +∗ (AﬃneMap (p,q)|[.(q−b)/(a−p),+infty.[) holds
f is Lipschitzian;5

二等辺三角形型および等脚台形型関数の重心
明らかに二等辺三角形型関数の重心法による非ファジィ化値はその頂点から底辺に下した垂線の足の座標である．以下の定理でその事実を形式化している．

Listing 8. FUZZY 7:25, FUZZY 7:26, FUZZY 7:27
theorem :: FUZZY 7:25

MMA-WiP (2023), vol.5, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.1 - ISSN 2434-5458 (Online)

4/13

Mechanized Mathematics and Its Applications, Works in Progress

Centroids of Membership Functions (Mitsuishi T.)

for a,b,c be Real, f be Function of REAL,REAL st b > 0 & c > 0 &f | [’a−c,a+c’]= ( AﬃneMap ( b/c,b−a∗b/c) |[. lower bound [’a−c,a+c’], ((b+a∗b/c) − (b−a∗b/c))/((b/c)−(−b/c)) .] )+∗ ( AﬃneMap (−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;theorem :: FUZZY 7:26
for a,b,c be Real, f be Function of REAL,REAL st b > 0 & c > 0 &( for x be Real holds f.x = max(0, b − |. b∗(x−a)/c .|) ) holds
f | [’a−c,a+c’] =( AﬃneMap ( b/c,b−a∗b/c) | [. lower bound [’a−c,a+c’], (b+a∗b/c − (b−a∗b/c))/((b/c)−(−b/c)) .] )+∗ ( AﬃneMap (−b/c,b+a∗b/c) | [. (b+a∗b/c − (b−a∗b/c))/((b/c)−(−b/c)), upper bound [’a−c,a+c’] .] );theorem :: FUZZY 7:27
for a,b,c be Real, f be Function of REAL,REAL stb > 0 & c > 0 & ( for x be Real holds f.x = max(0,b−|. b∗(x−a)/c .|) ) holds centroid (f,[’a−c,a+c’]) = a;上の定理は頂点の座標が (a, b) の二等辺三角形型の関数の重心を求めている．これについて，b = 1 とすることによってメンバシップ関数として扱うことができる．最初の定理で区分的線形関数で表された二等辺三角形型メンバシップ関数の重心が a であることを証明し，次の定理でその関数が（1）の形に変換されること用いて証明された．
以下の定理は Listing 2 の形式で表される二等辺三角形型メンバシップ関数の重心が bであることを示している．

Listing 9. FUZZY 7:31, FUZZY 7:33
theorem :: FUZZY 7:31
for a,b,c be Real st a < b & b < c & b−a = c−b holds centroid (TriangularFS (a,b,c),[’a,c’]) = b;theorem :: FUZZY 7:33
for a,b,c,d be Real st a < b & b < c & b−a = c−b & d <> 0 holds centroid (d (#) TriangularFS (a,b,c),[’a,c’]) = b;

等脚台形型メンバシップ関数の重心が上底（下底）の中点であることは自明である．以下の定理はその事実を形式化した．

Listing 10. FUZZY 7:36, FUZZY 7:48, FUZZY 7:49
theorem :: FUZZY 7:36
for a1,c,a2,d be Real, f be Function of REAL,REAL stc > 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’];theorem :: FUZZY 7:48
for a1,c,a2,d be Real, f be Function of REAL,REAL st c > 0 & d > 0 & a1 < a2 &f | [.a1−c,a2+c.] = AﬃneMap(d/c,−(d/c)∗(a1 − c)) | [.a1−c,a1.] +∗AﬃneMap(0,d) | [.a1 ,a2.] +∗AﬃneMap(−d/c, (d/c)∗(a2 + c)) | [.a2,a2+c.]
holds
integral( f,[’a1−c,a2+c’]) =integral( AﬃneMap(d/c,−(d/c)∗(a1 − c)), [’a1− c,a1’]) +integral( AﬃneMap(0,d) , [’a1 ,a2’]) +integral( AﬃneMap(−d/c, (d/c)∗(a2 + c)) , [’a2,a2+c’]) ;theorem :: FUZZY 7:49
for a1,c,a2,d be 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;

ここで用いられている等脚台形型関数は上底の長さが a2−a1，下底の長さが a2−a1+2c，MMA-WiP (2023), vol.5, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.1 - ISSN 2434-5458 (Online)

5/13

Mechanized Mathematics and Its Applications, Works in Progress

高さが d である．その重心はCentroids of Membership Functions (Mitsuishi T.)

a1 + a2

すればメンバシップ関数となる．

62である．二等辺三角形型と同様で，特に d = 1 とまとめ
本研究では，二等辺三角形型および等脚台形型メンバシップ関数の重心法による非ファ

ジィ化値の形式化を行った．いずれの重心も対象の軸と定義域との交点の座標であることは自明であるが，関数の積分やメンバシップ関数の定義域などの関連定理は今後の非ファジィ化計算の形式化に役に立つことが期待できる．メンバシップ関数に限らず，π 型の関数の形状が対象であるという概念の一般化や形式化は今後の課題としたい．さらに，本稿により後件部のメンバシップ関数の和算・MAX 演算を伴わない Center of Sums 法などのファジィ推論の入力値に対する連続性の検証が可能になった．こちらの Mizar による検証も今後の課題としたい．最後に，対称（線対象，点対称など）の概念の形式化が今後必要かの議論を課題としたい．

参考文献[1] Nomura H, Wakami N. A Method to Determine Fuzzy Inference Rules by a Genetic
Algorithm. The IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences (Japanese edition) A. 1994 09;77(9):p1241–1249.
Available from: https://cir.nii.ac.jp/crid/1520853835208335104.
[2] Fukuda T, Hasegawa Y, Shimojima K. StructureOrganizationof Hierarchical Fuzzy
Modelusing Genetic Algorithm. Japan Society for Fuzzy Theory and Systems.
1995;7(5):988–996.
[3] ROSS TJ. Fuzzy Logic With Engineering Application. John Wiley and Sons Ltd;2010.
[4] Van Leekwijck W, Kerre EE. Defuzzification: criteria and classification. Fuzzy sets
and systems. 1999;108(2):159–178.
[5] KATAFUCHI T, ASAI K, FUJITA H. Investigation of Deffuzification in Fuzzy
Inference : Proposal of a New Defuzzification Method (in Japanese). Medical
Imaging and Information Sciences. 2001;18(1):19–30.
[6] Mitsuishi T. Definition of Centroid Method as Defuzzification. Formalized Mathematics. 2022;30(2):129–138.
[7] Grabowski A. Basic Formal Properties of Triangular Norms and Conorms. Formalized Mathematics. 2017;25(2):93–100.

MMA-WiP (2023), vol.5, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.1 - ISSN 2434-5458 (Online)

6/13

Mechanized Mathematics and Its Applications, Works in Progress[8] Mitsuishi T.

Centroids of Membership Functions (Mitsuishi T.)

Some Properties of Membership Functions Composed of

Triangle Functions and Piecewise Linear Functions.
matics. 2021;29(2):103–115.

Available from:

Formalized Mathe-https://doi.org/10.2478/

forma-2021-0011.
[9] Raczkowski K, Sadowski P. Real Function Continuity. Formalized Mathematics. 1990;1(4):787–791. Available from: http://fm.mizar.org/1990-1/pdf1-4/
fcont_1.pdf.
[10] Mitsuishi T, Terashima T, Shimada N, Homma T, Shidama Y. SIRMs fuzzy approximate reasoning using L-R fuzzy number as premise valuable. In: 2013 8thInternational Conference on System of Systems Engineering; 2013. p. 25–27.
[11] 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.

Mizar article information
Works in Progress
FUZZY 7 Isosceles Triangular and Isosceles Trapezoidal Membership Functions
by Takashi Mitsuishi
Summary: The centroids of isosceles triangular and isosceles trapezoidal membershipfunctions are mentioned in this paper. We proved the agreement of the same function
expressed with different parameters and formalized those centroid with those parameters. In addition, various properties of membership functions on intervals where theendpoints of the domain are fixed and on general intervals are formalized.
Listing 11. FUZZY 7 - abstract
environvocabularies NUMBERS, XBOOLE 0, SUBSET 1, XXREAL 1, CARD 1, RELAT 1, TARSKI,FUNCT 1, XXREAL 0, PARTFUN1, ARYTM 1, ARYTM 3, COMPLEX1,
MEASURE5, FUZNUM 1, REAL 1, ORDINAL2, XXREAL 2,FUNCT 7,
JGRAPH 2, FUNCT 4, FCONT 1,SQUARE 1,SIN COS,
VALUED 1,FDIFF 1, INTEGRA1,INTEGRA5,SEQ 4,
POLYEQ 3,NEWTON, MSALIMIT,NUMPOLY1, FUZZY 6;
notationsTARSKI, XBOOLE 0, SUBSET 1, NEWTON, RELAT 1,
ORDINAL1,NUMBERS, SQUARE 1, BINOP 1, NORMSP 1,METRIC 1,
INT 1, XCMPLX 0,XXREAL 0, COMPLEX1,XXREAL 2,XREAL 0,
REAL 1, RELSET 1,
PBOOLE, MEASURE5, PARTFUN1, FUNCT 2,
PARTFUN2, FUNCT 1, FCONT 1,
FUNCT 3,INTEGRA1,INTEGRA2, RFUNCT 3,
FUNCOP 1, NAT 1, VALUED 0, VALUED 1, FUNCT 4,
ARYTM 2, ARYTM 1, ARYTM 0, COMSEQ 2, FDIFF 1,
MEMBERED, FINSEQ 1, FINSEQ 2, SEQ 2, SEQ 4,

MMA-WiP (2023), vol.5, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.1 - ISSN 2434-5458 (Online)

7/13

Mechanized Mathematics and Its Applications, Works in Progress

Centroids of Membership Functions (Mitsuishi T.)

SIN COS, RFUNCT 1, POLYEQ 3,
RVSUM 1,RCOMP 1, TOPMETR, TAYLOR 1, PRE TOPC, TOPS 2, POLYDIFF,
INTEGRA5,COUSIN2, DOMAIN 1, TSEP 1, TMAP 1,
FUZZY 1,FUZNORM1,FUZNUM 1, FUZZY 6;
theorems
TARSKI, XBOOLE 0, FUNCT 1, ABSVALUE,COMPLEX1, XREAL 1, XXREAL 0, XXREAL 1, FUNCT 2, RELAT 1,
XREAL 0, FCONT 1, XCMPLX 1, FUNCT 4,
FDIFF 1,VALUED 1,INTEGRA1,INTEGRA5,
NEWTON,INTEGRA4, INTEGRA6,SEQ 4, COUSIN2,POLYEQ 3, FUZZY 5, FUZZY 6,FUZNUM 1;
constructors
XBOOLE 0, ZFMISC 1, SUBSET 1, FUNCT 1, FUNCT 2, XCMPLX 0,
XXREAL 0, XREAL 0,
COMPLEX1, RFUNCT 1, SEQ 4, RELSET 1, FUZZY 1, FCONT 1,
FUNCT 4,FUZNUM 1,
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,
FDIFF 1, NORMSP 1,METRIC 1,VALUED 1,PARTFUN1,MEASURE5,
COMSEQ 2, PARTFUN2,POLYDIFF,PREPOWER,NEWTON,RFUNCT 3,FUZNORM1, BINOP 1, BINOP 2,INTEGRA1,INTEGRA2,INTEGRA3,INTEGRA5,
COUSIN2,SEQ 1,SEQ 2,RVSUM 1, NAT 1,
XXREAL 2, EXTREAL1, MESFUNC5,TOPS 2, CONNSP 1,
TMAP 1, PCOMPS 1,REAL 1,ARYTM 1,ARYTM 0,PBOOLE,FUNCOP 1,FUNCT 3,
POLYEQ 3,FUZZY 5,FUZZY 6,MEMBERED;
registrations RELSET 1, NUMBERS, XXREAL 0, MEMBERED, XBOOLE 0, VALUED 0,
VALUED 1,COMSEQ 2,PDIFFEQ1,FDIFF 1,FUZZY 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,INTEGRA1,MEASURE5,COMSEQ 1,
FDIFF 2,POLYDIFF,PREPOWER,NEWTON,RFUNCT 3,FUZNORM1,INTEGRA2,RFUNCT 1,
SEQ 2,SEQ 1,RVSUM 1,NAT 3, PRE TOPC, METRIC 1, BORSUK 1, CONNSP 1,
EXTREAL1, SUPINF 1, SUPINF 2 ,XXREAL 1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM ;deﬁnitions XBOOLE 0, TARSKI, XXREAL 2,FUZNUM 1,
FUZZY 1,RELAT 1,
XXREAL 3,NUMBERS,SIN COS6,TOPMETR,SQUARE 1, COMPTS 1, RCOMP 1,
FCONT 1,INT 1,SUBSET 1,VALUED 1,XXREAL 0,SIN COS,
PARTFUN1,INTEGRA1,INTEGRA2,INTEGRA3,INTEGRA5,MEASURE5,FUNCT 2,RFUNCT 1,
BINOP 1,FUZNORM1,SEQ 1,SEQ 2,COMSEQ 2,FINSEQ 1,NAT 1,TAYLOR 1,FUZZY 6,
RVSUM 1;equalities FUZZY 1, RCOMP 1,FUZNUM 1,
RELAT 1,XXREAL 3,
NUMBERS,SIN COS6,SQUARE 1,FUNCT 4,RFUNCT 1,INTEGRA1,INTEGRA2;
expansions TARSKI, FCONT 1,FUZNUM 1,
FUZZY 1,RELAT 1,XXREAL 3,
NUMBERS,SQUARE 1,FUNCT 4,RFUNCT 1,INTEGRA1,INTEGRA2;
schemes FUNCT 2;
begin
reserve A for non empty closed interval Subset of REAL;
theorem :: FUZZY 7:1
for f,g be Function of REAL,REAL stf is continuous & g is continuous

MMA-WiP (2023), vol.5, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.1 - ISSN 2434-5458 (Online)

8/13

Mechanized Mathematics and Its Applications, Works in Progress

Centroids of Membership Functions (Mitsuishi T.)

holds
max(f,g) is continuous;
theorem :: FUZZY 7:2
for f,g be Function of REAL,REAL stf is continuous & g is continuous
holds
min(f,g) is continuous;
theorem :: FUZZY 7:3
for a,c be Real, f be Function of REAL,REAL stc > 0 & ( for x be Real holds f.x = max(0, 1 − |. (x−a)/c .|) )holds
f is FuzzySet of REAL & f is triangular FuzzySet of REAL;
theorem :: FUZZY 7:4
for a,b,c be Real st b > 0 & c > 0
holds
for x be Real holds( AﬃneMap ( b/c,b−a∗b/c) | ]. −infty,a .]+∗ AﬃneMap (−b/c,b+a∗b/c) | [. a,+infty .[ ).x = b − |. b∗(x−a)/c .|;theorem :: FUZZY 7:5
for a,b,c be Real, f be Function of REAL,REAL stb>0&c>0&(for x be Real holds f.x = b−|. b∗(x−a)/c .|) holds
f = AﬃneMap (b/c,b−a∗b/c) | ]. −infty,a .]+∗ AﬃneMap (−b/c,b+a∗b/c) | [. a,+infty .[;theorem :: FUZZY 7:6
for a,b,c be Real, f be Function of REAL,REAL stb>1&c>0&( for x be Real holds f.x = min(1, max(0, b − |. b∗(x−a)/c .|)) )holds
f is FuzzySet of REAL &f is trapezoidal FuzzySet of REAL &f is normalized FuzzySet of REAL;
theorem :: FUZZY 7:7
for s be Real, f,g being Function of REAL,REAL holdsdom ( ( f | ].−infty,s.] ) +∗ ( g | [.s,+infty.[ ) ) = REAL &dom ( ( f | ].−infty,s.[ ) +∗ ( g | [.s,+infty.[ ) ) = REAL;
theorem :: FUZZY 7:8
for a,b being Real holds( a > 0 implies|. AﬃneMap (a,b) .| = (− (AﬃneMap(a,b) | ].−infty,(−b)/a.[))+∗ (AﬃneMap(a,b) | [.(−b)/a,+infty.[) );theorem :: FUZZY 7:9
for a,b being Real holds( a < 0 implies|. AﬃneMap (a,b) .| = ( (AﬃneMap(a,b) | ].−infty,(−b)/a.[ ))+∗ − (AﬃneMap(a,b) | [.(−b)/a,+infty.[ ) );theorem :: FUZZY 7:10
for a,b,c be Real, f be Function of REAL,REAL stb>0&c>0&(for x be Real holds f.x = max(0, b − |. b∗(x−a)/c .|)) holds
for x be Real st not x in [’a−c,a+c’] holds f.x = 0;
theorem :: FUZZY 7:11
for a,b,c be Real, f,g be Function of REAL,REAL sta < b & b < c holds(f | ]. −infty,b .] +∗ g | [. b,+infty .[ ) | [. a,c .]= (f | [. a,b .]) +∗ (g | [. b,c .]);
theorem :: FUZZY 7:12
for a,b,c be Real, f be Function of REAL,REAL st

MMA-WiP (2023), vol.5, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.1 - ISSN 2434-5458 (Online)

9/13

Mechanized Mathematics and Its Applications, Works in Progress

Centroids of Membership Functions (Mitsuishi T.)b>0&c>0holds( AﬃneMap ( b/c,b−a∗b/c) | ]. −infty,a .]+∗ AﬃneMap (−b/c,b+a∗b/c) | [. a,+infty .[ ) | [. a−c,a+c .]= AﬃneMap ( b/c,b−a∗b/c) | [. a−c,a .]+∗ AﬃneMap (−b/c,b+a∗b/c) | [. a,a+c .];theorem :: FUZZY 7:13
for a,b,c,d be Real st a < b & b < c & c < d holds[’a,d’] \ [’b,c’] c= [’a,b’] \/ [’c,d’];theorem :: FUZZY 7:14
for a,b,c,d be Real st a < b & b < c & c < d holds[. a,d .] \ [. b,c .] c= [. a,b .] \/ [. c,d .];theorem :: FUZZY 7:15
for a,b,c,d be Real st a < b & b < c & c < d holds[. a,d .] \ [. b,c .] = [. a,b .[ \/ ]. c,d .];theorem :: FUZZY 7:16
for a,b,c be Real, f be Function of REAL,REAL sta < 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));theorem :: FUZZY 7:17
for a,b,c,d be Real, f be Function of REAL,REAL sta<b&b<c&c<d&f is integrable on [’a,d’] & f | [’a,d’] is bounded &for x be Real st x in [’a,b’] \/ [’c,d’] holds f.x = 0
holds
centroid(f,[’a,d’]) = centroid(f,[’b,c’]);theorem :: FUZZY 7:18
for p, q, r, s being Real st p < r & r <= s & s < qholds[.r,s.] c< [.p,q.];theorem :: FUZZY 7:19
for A,B be non empty closed interval Subset of REAL
st B c< A holds
lower bound A < lower bound B or
upper bound B < upper bound A;
theorem :: FUZZY 7:20
for A,B be non empty closed interval Subset of REAL st
B c= A holds
lower bound A <= lower bound B & upper bound B <= upper bound A;
theorem :: FUZZY 7:21
for A,B be non empty closed interval Subset of REAL,
f be 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 be 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);
theorem :: FUZZY 7:22
for a,b,c be Real st c >= 0 holdsc ∗ max (a, b) = max (c∗a, c∗b) & c ∗ min (a, b) = min (c∗a, c∗b);theorem :: FUZZY 7:23 ::Th13:
for a,b,c be Real, f be Function of REAL,REAL stb>0&c>0&( for x be Real holds f.x = max(0, b − |. b∗(x−a)/c .|) ) holds
f = b (#) (TriangularFS (a−c,a,a+c));

MMA-WiP (2023), vol.5, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.1 - ISSN 2434-5458 (Online)

10/13

Mechanized Mathematics and Its Applications, Works in Progress

Centroids of Membership Functions (Mitsuishi T.)

theorem :: FUZZY 7:24
for a,b,c be Real, f be Function of REAL,REAL stb > 0 & c > 0 & (for x be Real holds f.x = max(0,b−|. b∗(x−a)/c .|)) holds
f is Lipschitzian;theorem :: FUZZY 7:25
for a,b,c be Real, f be Function of REAL,REAL stb>0&c>0&f | [’a−c,a+c’] =( AﬃneMap ( b/c,b−a∗b/c) |[. lower bound [’a−c,a+c’], ((b+a∗b/c) − (b−a∗b/c))/((b/c)−(−b/c)) .] )+∗ ( AﬃneMap (−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;theorem :: FUZZY 7:26
for a,b,c be Real, f be Function of REAL,REAL stb>0&c>0&( for x be Real holds f.x = max(0, b − |. b∗(x−a)/c .|) ) holds
f | [’a−c,a+c’] =( AﬃneMap ( b/c,b−a∗b/c) |[. lower bound [’a−c,a+c’], (b+a∗b/c − (b−a∗b/c))/((b/c)−(−b/c)) .] )+∗ ( AﬃneMap (−b/c,b+a∗b/c) |[. (b+a∗b/c − (b−a∗b/c))/((b/c)−(−b/c)), upper bound [’a−c,a+c’] .] );theorem :: FUZZY 7:27
for a,b,c be Real, f be Function of REAL,REAL st b > 0 & c > 0 &( for x be Real holds f.x = max(0,b−|. b∗(x−a)/c .|) ) holds
centroid (f,[’a−c,a+c’]) = a;theorem :: FUZZY 7:28
for a,b,c be Real, f be Function of REAL,REAL stb>0&c>0&(for x be Real holds f.x = max(0,b−|. b∗(x−a)/c .|))
holds
f is integrable on A & f | A is bounded;theorem :: FUZZY 7:29
for a,b,c be Real, f be Function of REAL,REAL stb>0&c>0&(for x be 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;
theorem :: FUZZY 7:30 ::Th20:
for a,b,c be Real, f be Function of REAL,REAL stb > 0 & c > 0 & [’a−c,a+c’] c= A &(for x be Real holds f.x = max(0,b−|. b∗(x−a)/c .|))
holds
centroid (f,A) = a;theorem :: FUZZY 7:31
for a,b,c be Real st a < b & b < c & b−a = c−b holds
centroid (TriangularFS (a,b,c),[’a,c’]) = b;theorem :: FUZZY 7:32
for a,b,c be Real st a < b & b < cholds
TriangularFS (a,b,c) is integrable on A &TriangularFS (a,b,c) | A is bounded;theorem :: FUZZY 7:33
for a,b,c,d be Real st a < b & b < c & b−a = c−b & d <> 0 holds
centroid (d (#) TriangularFS (a,b,c),[’a,c’]) = b;

MMA-WiP (2023), vol.5, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.1 - ISSN 2434-5458 (Online)

11/13

Mechanized Mathematics and Its Applications, Works in Progress

Centroids of Membership Functions (Mitsuishi T.)

theorem :: FUZZY 7:34
for a,b,c,d be Real st a < b & b < c & c < dholds
TrapezoidalFS (a,b,c,d) is integrable on A &TrapezoidalFS (a,b,c,d) | A is bounded;theorem :: FUZZY 7:35
for a,b,c,d,r be Real st a < b & b < c & c < dholdsr (#) TrapezoidalFS (a,b,c,d) is integrable on A;
theorem :: FUZZY 7:36
for a1,c,a2,d be Real, f be Function of REAL,REAL stc > 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’];theorem :: FUZZY 7:37
for a,b,c be Real, f,g be Function of REAL,REAL,
h be PartFunc of REAL,REAL sta <= 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 hholds h | [.a,c.] is continuous;
theorem :: FUZZY 7:38
for a,b,p,q be Real, f be Function of REAL,REAL st a <> p &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 7:39
for a,b,c be Real, f,g,h be Function of REAL,REAL
sta <= b & b <= c & f is continuous & g is continuous &h | [.a,c.] = (f| [.a,b.]) +∗ (g | [.b,c.]) & f.b = g.bholds
integral((id REAL) (#) h,[’a,c’])= integral((id REAL) (#) f,[’a,b’]) + integral((id REAL) (#) g,[’b,c’]);theorem :: FUZZY 7:40
for r be Real, f,g be Function of REAL,REAL holdsr (#) (f +∗ g) = (r (#) f) +∗ (r (#) g);
theorem :: FUZZY 7:41
for a, b, c, d, r be Real sta < b & b < c & c < d holds(((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.])= TrapezoidalFS (a,b,c,d) | [.a,d.];theorem :: FUZZY 7:42
for a, b, c, d, r be Real sta < b & b < c & c < d holds
TrapezoidalFS (a,b,c,d)= (AﬃneMap (0,0) | (REAL \ ].a,d.[)) +∗ TrapezoidalFS (a,b,c,d) | [.a,d.];theorem :: FUZZY 7:43
for r be Real, f be Function of REAL,REAL holds(r (#) f) | A = r (#) (f | A);theorem :: FUZZY 7:44
for r be Real, f be PartFunc of REAL,REAL st A c= dom f
holds(r (#) f) | A = r (#) (f | A);theorem :: FUZZY 7:45
for a, b, c, d, r be Real sta < b & b < c & c < d holds

MMA-WiP (2023), vol.5, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.1 - ISSN 2434-5458 (Online)

12/13

Mechanized Mathematics and Its Applications, Works in Progress

Centroids of Membership Functions (Mitsuishi T.)(r (#) AﬃneMap (1 / (b − a),− (a /(b−a)) ) ) | [.a,b.] +∗(r (#) AﬃneMap (0,1)) | [.b,c.] +∗(r (#) AﬃneMap ((− (1 / (d − c))),(d / (d − c)))) | [.c,d.]= ( r (#) TrapezoidalFS (a,b,c,d) ) | [.a,d.];theorem :: FUZZY 7:46 ::fuzzy618:
for s be Real, f,g being Function of REAL,REAL holds( f | ].−infty,s.] ) +∗ ( g | [.s,+infty.[ )is Function of REAL,REAL;
theorem :: FUZZY 7:47
for a,b,r being Real holdsr (#) (AﬃneMap (a,b)) = AﬃneMap (r∗a,r∗b);
theorem :: FUZZY 7:48
for a1,c,a2,d be Real, f be Function of REAL,REAL stc > 0 & d > 0 & a1 < a2 &f | [.a1−c,a2+c.] = AﬃneMap(d/c,−(d/c)∗(a1 − c)) | [.a1−c,a1.] +∗AﬃneMap(0,d) | [.a1 ,a2.] +∗AﬃneMap(−d/c, (d/c)∗(a2 + c)) | [.a2,a2+c.]
holds
integral( f,[’a1−c,a2+c’]) =integral( AﬃneMap(d/c,−(d/c)∗(a1 − c)), [’a1− c,a1’]) +integral( AﬃneMap(0,d) , [’a1 ,a2’]) +integral( AﬃneMap(−d/c, (d/c)∗(a2 + c)) , [’a2,a2+c’]) ;theorem :: FUZZY 7:49
for a1,c,a2,d be 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;

MMA-WiP (2023), vol.5, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.1 - ISSN 2434-5458 (Online)

13/13