Mechanized Mathematics and Its Applications, Works in Progress

Centroid Method as Defuzziﬁcation (Mitsuishi T.)

Regular Paper

重心法を用いた非ファジィ化計算の定義
On the Formalizations of Deﬁnition for Centroid
Method as Defuzziﬁcation
三石 貴志 1,*
Takashi Mitsuishi1,*
1 長野大学企業情報学部
1 Faculty of Business and Informatics, Nagano University658-1 Shimonogo, Ueda, Nagano, Japan* takashi-mitsuishi@nagano.ac.jp
Proof checked by Mizar Version: 8.1.11 and MML Version: 5.68.1412
Received: April 13, 2022. Accepted: May 26, 2022.

Abstract
In this study, the centroid method which is one of the fuzzy inference processes is formulated. The centroid method is the most popular defuzzied method. By this method,defuzzified crisp value is obtained from domain of membership function as weighted
average. Since the integral is used in centroid method, the integrability and bounded
properties of membership functions are also mentioned. In this paper, the properties ofpiecewise linear functions consisting of two straight lines are mainly described.

1

はじめに
ファジィ推論は入力された前件部変数に対して，ファジィ集合（メンバシップ関数）が出力される．あいまい性を有した出力値では実用において不適当であるため出力のメン
バシップ関数に非ファジィ化を行い，そのメンバシップ関数を表すのにもっとも適当なクリスプ値に変換する．非ファジィ化の方法でもっともよく用いられるのが重心法で他にもCenter of Sums 法，高さ法，密度モーメント法 [1–3] など多様に提案されている．本アー
ティクルでは重心法による非ファジィ化値を定義として形式化した．
ファジィ推論（Mamdani method，product-sum-gravity method）に使用される演算は主に数値と関数の積や頭切りといわれる MIN 演算，関数と関数との和算や MAX 演算などであるが [4, 5]，これらは Mizar Mathematical Library にてファジィ理論とは別に

MMA-WiP (2022), vol.4, no.5 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.5 - ISSN 2434-5458 (Online)

1/12

Mechanized Mathematics and Its Applications, Works in Progress

Centroid Method as Defuzziﬁcation (Mitsuishi T.)

形式化されている．稀にLukasiewicz の演算（限界積）が用いられる場合がある．この演
算は [6] にて形式化されている．そこで本研究では，これらの演算にて計算されたメンバ
シップ関数より重心法による非ファジィ化値を得るための諸性質，例えば定数倍や MIN・

MAX 演算後の積分可能性（非ファジィ化値の計算可能性）などについて言及している．
さらに通常の合成関数と異なる 2 つのグラフが交点でつながっている関数に関するいくつかの定理を形式化した．その具体例として区分的線形関数の非ファジィ化値を求める計算の形式化を行った．

2

メンバシップ関数の非ファジィ化
非ファジィ化法は重心法がもっとも広く用いられている．閉区間 A 上のメンバシップ

関数 µ(x) の非ファジィ化値 x∗ は，以下のように関数の定義域 A の値を関数値 µ(x) によって加重平均して定義域上の値を 1 つ求める方法である．

∫
xµ(x)dxx = ∫Aµ(x)dxA∗

本アーティクルでは，重心法によって非ファジィ化値を計算するために，閉区間 A 上の関数 f の重心値 x∗ = centroid(f,A) を以下のように定義した．

Listing 1. FUZZY 6:def 1
deﬁnition
let A be non empty closed interval Subset of REAL;
let f be Function of REAL,REAL;
assume thatf is integrable on A andf | A is bounded;func centroid (f,A) −> Real equals :: FUZZY 6:def 1
integral((id REAL)(#)f,A)/integral(f,A);
end;

f (x) = x なる恒等写像は，Mizar Mathematical Library では様々な関数の形式によって表記されているが，本アーティクルでは以下の関数を用いた [7]．

Listing 2. RELAT 1:def 10
deﬁnition
let X be set ;func id X −> Relation means :: RELAT 1:def 10
for x, y being object holds( [x,y] in it iﬀ ( x in X & x = y ) );end;

Listing 1 では，重心を求める関数の値域を [0, 1] に限定しておらずメンバシップ関数
でないものにも適用できる．

b ∈ [a, c] とする．閉区間 [a, c] の部分集合 [b, c]([a, b]) において f (x) = 0 であるとき，この区間には重心値が存在しない. したがって以下の定理は，その区間を分断して非ファジィ化値を計算する区間を [a, b]([b, c]) とすることができることを表している．

MMA-WiP (2022), vol.4, no.5 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.5 - ISSN 2434-5458 (Online)

2/12

Mechanized Mathematics and Its Applications, Works in Progress

Centroid Method as Defuzziﬁcation (Mitsuishi T.)

Listing 3. FUZZY 6:8, FUZZY 6:9
theorem :: FUZZY 6:8
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 & for x be Real st x in [’b,c’] holds f.x = 0 holds
centroid(f,[’a,c’]) = centroid(f,[’a,b’]);theorem :: FUZZY 6:9
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 & for x be Real st x in [’a,b’] holds f.x = 0 holds
centroid(f,[’a,c’]) = centroid(f,[’b,c’]);

上記定理の証明において，以下の定理 [8] が有用な道具となった．

Listing 4. INTEGRA6:17, INTEGRA6:18
theorem :: INTEGRA6:17
for a, b, c being Real for f being PartFunc of REAL,REAL sta <= b & f is integrable on [’a,b’] & f | [’a,b’] is bounded & [’a,b’] c= dom f & c in [’a,b’] holds( f is integrable on [’a,c’] & f is integrable on [’c,b’] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) );theorem :: INTEGRA6:18
for a, b, c, d being Real for f being PartFunc of REAL,REAL sta <= c & c <= d & d <= b & f is integrable on [’a,b’] & f | [’a,b’] is bounded & [’a,b’] c= dom f holds( f is integrable on [’c,d’] & f | [’c,d’] is bounded & [’c,d’] c= dom f );以下の定理は非ファジィ化関数を定数倍しても非ファジィ化値は変化しないことを示している．

Listing 5. FUZZY 6:32
theorem :: FUZZY 6:32
for r be Real, f be Function of REAL,REAL st r <> 0 & f is integrable on A & f | A is bounded holds
centroid((r (#) f),A) = centroid(f,A);

3

重心法のためのメンバシップ関数の積分に関する諸性質
メンバシップ関数の重心法による非ファジィ化値の存在に関連する性質として，閉区

間 A において関数 f の積分値が正の値であれば，その区間に f (c) > 0 となる c ∈ A が存在する定理を証明した．

Listing 6. FUZZY 6:10
theorem :: FUZZY 6:10
for f being Function of REAL,REAL st f is integrable on A & f | A is bounded & integral(f,A) > 0 holds
ex c being Real st c in A & f.c > 0;

Mamdani 推論法ではメンバシップ関数同士の MAX 演算が用いられ，前件部変数をファジィ数とした推論法 [9] ではメンバシップ関数同士の MIN 演算が用いられる．下記の定理は，関数同士の MAX・MIN 演算を積，和および絶対値の演算として表した．

Listing 7. FUZZY 6:12-15

MMA-WiP (2022), vol.4, no.5 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.5 - ISSN 2434-5458 (Online)

3/12

Mechanized Mathematics and Its Applications, Works in Progress

Centroid Method as Defuzziﬁcation (Mitsuishi T.)

theorem :: FUZZY 6:12
for f,g be Function of REAL,REAL holds min(f,g) = (1/2) (#) ((f + g) − abs(f − g));theorem :: FUZZY 6:13
for f,g be Function of REAL,REAL st f is integrable on A & f | A is bounded & g is integrable on A & g | A is bounded
holds min(f,g) is integrable on A & min(f,g) | A is bounded &integral(min(f,g),A) = (1/2)∗( integral(f,A) + integral(g,A) − integral(abs(f−g),A) );theorem :: FUZZY 6:14
for f,g be Function of REAL,REAL holds max(f,g) = (1/2) (#) (f + g + abs(f − g));theorem :: FUZZY 6:15
for f,g be Function of REAL,REAL st f is integrable on A & f | A is bounded & g is integrable on A & g | A is bounded
holds max(f,g) is integrable on A & max(f,g) | A is bounded &integral(max(f,g),A) = (1/2)∗( integral(f,A) + integral(g,A) + integral(abs(f−g),A) );以下の定理はファジィ推論において，前件部適合度を後件部のメンバシップ関数に反映させた後のメンバシップ関数の積分可能性を表し，その関数の重心が得られることを意味する．この定理は今後Lukasiewicz の演算（限界積）を用いた場合にも適用可能である．

Listing 8. FUZZY 6:17
theorem :: FUZZY 6:17
for r1,r2 be Real, f,F be Function of REAL,REAL stf is integrable on A & f | A is bounded & for x being Real holds F.x = min(r1, r2∗(f.x)) holds
F is integrable on A & F | A is bounded;4

区分的線形関数の非ファジィ化値
以下の定理は Lipschitz 連続な関数 f および g がある点 c において等しい値をとると

き，それらが c において結合した関数は再び Lipschitz 連続になることを示している．また一次関数の Lipschitz 連続性を，自明ではあるが今後の関連項目の証明のために形式化した．

Listing 9. FUZZY 6:26, FUZZY 6:27
theorem :: FUZZY 6:26 :::Lipschitzianfor c being Real, f,g,F be Function of REAL,REAL stf is Lipschitzian & g is Lipschitzian & f . c = g . c & F = (f | ].−infty,c.[) +∗ (g | [.c,+infty.[) holds F is Lipschitzian;theorem :: FUZZY 6:27
for a,b being Real holds (AﬃneMap (a,b)) is Lipschitzian;

Lsting 10 は，以下に示す傾きの異なる 2 本の直線が交点
区分線形関数 ax + b
f (x) =
 px + q

(
x≤
(
x≥

q−b
a−p
q−b

q−b
a−p

∈ A で結合している

)
)

a−p

MMA-WiP (2022), vol.4, no.5 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.5 - ISSN 2434-5458 (Online)

4/12

Mechanized Mathematics and Its Applications, Works in Progress

Centroid Method as Defuzziﬁcation (Mitsuishi T.)の閉区間 A における重心∫
a 3
xf (x)dx(t − s3 ) + 2b (t2 − s2 ) + p3 (u3 − t3 ) + 2q (s2 − t2 )∗x = ∫A= 3 a 2p2
2
2
f (x)dx
2 (t − s ) + b(t − s) + 2 (u − t ) + q(u − t)
Aを表している．ただし，a ̸= p であり，s = lower bound A は A の下界，t =u = upper bound A は A の上界である．

q−b
a−p

，

Listing 10. FUZZY 6:48
theorem :: FUZZY 6:48
for a,b,p,q,c,d,e being Real, f be Function of REAL,REAL sta <> p & f | A = AﬃneMap (a,b) | [.lower bound A,(q−b)/(a−p).] +∗ AﬃneMap (p,q) | [.(q−b)/(a−p),upper bound A.]& (q−b)/(a−p) in A holds
centroid(f,A) = ( 1/3∗a∗(((q−b)/(a−p))ˆ3 − (lower bound A)ˆ3) + 1/2∗b∗(((q−b)/(a−p))ˆ2 − (lower bound A)ˆ2)+ 1/3∗p∗((upper bound A)ˆ3 − ((q−b)/(a−p))ˆ3) + 1/2∗q∗((upper bound A)ˆ2 − ((q−b)/(a−p))ˆ2) )/ ( 1/2∗a∗(((q−b)/(a−p))ˆ2 −(lower bound A)ˆ2) + b∗((q−b)/(a−p) − lower bound A)+ 1/2∗p∗((upper bound A)ˆ2 −((q−b)/(a−p))ˆ2) + q∗(upper bound A −(q−b)/(a−p)) );5

まとめ
本研究では，ファジィ推論における非ファジィ化の一つ重心法の計算について形式化を行った．メンバシップ関数に対して適用される重心法ではあるが，形式化においてはその対象を値域が区間 [0, 1] の関数に限定していない．ファジィ推論の出力であるメンバ
シップ関数は，複数のメンバシップ関数の MAX 演算や和算による結合である場合が多い
ので，重心法の対象となるべく，2 つの関数が結合した関数の諸性質に多くの紙面を割いた．それに伴って，重心計算の分子の非積分関数である恒等写像とメンバシップ関数の積の積分可能性なども形式化された．本研究で形式化した重心法は SIRMs 推論法 [10] の非ファジィ化にも適用が可能である．アーティクルの最後の定理として，2 本の直線が結合した区分的線形関数の非ファジィ化値を示した．本稿以降のアーティクルでは，非線形関数に重心法を適用する計算の形式化を予定している．将来は重心法のメンバシップ関数集
合の上で定義された汎関数としての連続性に関する性質を形式化し，筆者らが証明した
ファジィ最適制御の存在性 [11] の検証を行う．

参考文献[1] ROSS TJ. Fuzzy Logic With Engineering Application. John Wiley and Sons Ltd;2010.
[2] Van Leekwijck W, Kerre EE. Defuzzification: criteria and classification. Fuzzy sets
and systems. 1999;108(2):159–178.
[3] 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.

MMA-WiP (2022), vol.4, no.5 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.5 - ISSN 2434-5458 (Online)

5/12

Mechanized Mathematics and Its Applications, Works in Progress

Centroid Method as Defuzziﬁcation (Mitsuishi T.)[4] MAMDANI EH. Application of fuzzy algorithms for control of simple dynamic
plant. Proc IEE. 1974;121(12):1585–1588.
[5] Mizumoto M. Improvement of fuzzy control (IV)-Case by product-sum-gravity
method. In: Proc. 6th Fuzzy System Symposium, 1990; 1990. p. 9–13.
[6] Grabowski A. Basic Formal Properties of Triangular Norms and Conorms. Formalized Mathematics. 2017;25(2):93–100.
[7] Woronowicz E. Relations and Their Basic Properties. Formalized Mathematics.
1990;1(1):73–83. Available from: http://fm.mizar.org/1990-1/pdf1-1/relat_
1.pdf.
[8] Endou N, Shidama Y, Yamazaki M. Integrability and the Integral of Partial Functions from R into R. Formalized Mathematics. 2006;14(4):207–212.
[9] 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.
[10] Seki H, Ishii H, Mizumoto M. On the Generalization of Single Input Rule Modules
Connected Type Fuzzy Reasoning Method. IEEE Transactions on Fuzzy Systems.
2008;16(5):1180–1187.
[11] Mitsuishi T, Shidama Y. Compactness of family of fuzzy sets in L2 space withapplication to optimal control. IEICE transactions on fundamentals of electronics,
communications and computer sciences. 2009;92(4):952–957.

Mizar article information
Works in Progress
FUZZY 6 Centroid Method for Defuzzification
by Takashi Mitsuishi
Summary: Fuzzy inference method outputs a fuzzy set (membership function) fora given premise variable. Membership functions are unsuitable for practical use andare converted to crisp values by defuzzification process. The centroid method is themost used method. Various other defuzzification methods such as the Center of Sums
method, the height method and the density moment method are proposed [1–3]. In thisarticle, we present formalization of defuzzified crisp value of membership function using
centroid method. And related theorems are formalized.
The operations used in Mamdani method and product-sum-gravity method aresimple and have already been formalized in Mizar Mathematical Library. Moreover
Lukasiewicz operations are in the article [6]. On the other, the integrability and boundedtheorems of the membership functions changed by these operations are described for

MMA-WiP (2022), vol.4, no.5 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.5 - ISSN 2434-5458 (Online)

6/12

Mechanized Mathematics and Its Applications, Works in Progress

Centroid Method as Defuzziﬁcation (Mitsuishi T.)

defuzzified value by centroid method. As a concrete example, we finally formalized thecalculation of defuzzified value of the piecewise linear function.
Listing 11. FUZZY 6 - 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,
MEASURE5, FUZNUM 1, REAL 1, ORDINAL2, XXREAL 2, JGRAPH 2, FUNCT 4,
FCONT 1,SQUARE 1, VALUED 1,FDIFF 1, INTEGRA1,INTEGRA5,SEQ 4, NAT 1,
PREPOWER,NEWTON,RFUNCT 3, CARD 3, MEASURE7, FINSEQ 1, POLYEQ 3, FUZZY 6;
notations TARSKI, 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, FUNCT 1, PBOOLE, RELSET 1,
MEASURE5, PARTFUN1, FUNCT 2,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, PREPOWER,FCONT 1, SIN COS, PARTFUN2, 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, BORSUK 1, FUZNORM1,FUZNUM 1;
theorems
XBOOLE 0,TARSKI, FUNCT 1, ABSVALUE, PARTFUN1, TAYLOR 1,
COMPLEX1, XREAL 1, XXREAL 0, XXREAL 1, FUNCT 2, RELAT 1,
XREAL 0, FCONT 1, XCMPLX 1, FUZZY 2, FUNCT 4, SUBSET 1,
FDIFF 1, VALUED 1, INTEGRA1, INTEGRA5, PREPOWER, NEWTON,INTEGRA6, SEQ 4, RFUNCT 3, INTEGRA2, INTEGRA9, COMSEQ 2,COUSIN2,RFUNCT 1,
FINSEQ 3, POLYEQ 3;
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,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,
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;
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;
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,
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,COMSEQ 2,FINSEQ 1,NAT 1,TAYLOR 1;
equalities FUZZY 1, RCOMP 1,FUZNUM 1,NUMPOLY1,RELAT 1,XXREAL 3,
NUMBERS,SIN COS6,SQUARE 1,FUNCT 4,RFUNCT 1;
expansions TARSKI, FCONT 1,FUZNUM 1,NUMPOLY1,FUZZY 1,RELAT 1,XXREAL 3,

MMA-WiP (2022), vol.4, no.5 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.5 - ISSN 2434-5458 (Online)

7/12

Mechanized Mathematics and Its Applications, Works in Progress

Centroid Method as Defuzziﬁcation (Mitsuishi T.)

NUMBERS,SQUARE 1,FUNCT 4,RFUNCT 1;
begin
reserve A for non empty closed interval Subset of REAL;
deﬁnition
let A be non empty closed interval Subset of REAL;
let f be Function of REAL,REAL;
assume thatf is integrable on A andf | A is bounded;func centroid (f,A) −> Real equals:: FUZZY 6:def 1
integral((id REAL)(#)f,A)/integral(f,A);
end;
theorem :: FUZZY 6:1
for a,b,c be Real st a < b & c > 0
holds centroid (AﬃneMap (0,c),[’a,b’]) = (a+b)/2;
theorem :: FUZZY 6:2
for a,b be Real holds(id REAL) is integrable on [’a,b’] & (id REAL) | [’a,b’] is bounded;theorem :: FUZZY 6:3(id REAL) is integrable on A & (id REAL) | A is bounded;theorem :: FUZZY 6:4
for e being Realfor f being PartFunc of REAL,REAL st
A c= dom f & ( for x being Real st x in A holds f . x = e ) holds( f is integrable on A & f | A is bounded &integral (f,(lower bound A),(upper bound A))= e ∗ ((upper bound A) − (lower bound A)) );theorem :: FUZZY 6:5
for f be Function of REAL,REAL st(for x be Real st x in A holds f.x = 0) holds
integral(f,A) = 0;
theorem :: FUZZY 6:6
for f be Function of REAL,REAL stf is integrable on A & f | A is bounded
holds(id REAL) (#) f is integrable on A &((id REAL) (#) f) | A is bounded;theorem :: FUZZY 6:7
for a,b,c be Real st a < b holds[’a,b’] c= [#]REAL & lower bound [’a,b’] = a & upper bound [’a,b’] = b;theorem :: FUZZY 6:8
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 &for x be Real st x in [’b,c’] holds f.x = 0
holds
centroid(f,[’a,c’]) = centroid(f,[’a,b’]);theorem :: FUZZY 6:9
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 &for x be Real st x in [’a,b’] holds f.x = 0
holds
centroid(f,[’a,c’]) = centroid(f,[’b,c’]);MMA-WiP (2022), vol.4, no.5 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.5 - ISSN 2434-5458 (Online)

8/12

Mechanized Mathematics and Its Applications, Works in Progress

Centroid Method as Defuzziﬁcation (Mitsuishi T.)

theorem :: FUZZY 6:10
for f being Function of REAL,REAL stf is integrable on A & f | A is bounded & integral(f,A) > 0
holds
ex c being Real st c in A & f.c > 0;
theorem :: FUZZY 6:11
for r be Real, f be FuzzySet of REAL, F be Function of REAL,REAL str > 0 & f is integrable on A & f | A is bounded &for x being Real holds F.x = min(r, f.x)
holds
integral(F,A) >= 0;
theorem :: FUZZY 6:12
for f,g be Function of REAL,REAL holds
min(f,g) = (1/2) (#) ((f + g) − abs(f − g));theorem :: FUZZY 6:13
for f,g be Function of REAL,REAL stf is integrable on A & f | A is bounded &g is integrable on A & g | A is bounded
holds
min(f,g) is integrable on A & min(f,g) | A is bounded &integral(min(f,g),A)= (1/2)∗( integral(f,A) + integral(g,A) − integral(abs(f−g),A) );theorem :: FUZZY 6:14
for f,g be Function of REAL,REAL holds
max(f,g) = (1/2) (#) (f + g + abs(f − g));theorem :: FUZZY 6:15
for f,g be Function of REAL,REAL stf is integrable on A & f | A is bounded &g is integrable on A & g | A is boundedholds
max(f,g) is integrable on A & max(f,g) | A is bounded &integral(max(f,g),A)= (1/2)∗( integral(f,A) + integral(g,A) + integral(abs(f−g),A) );theorem :: FUZZY 6:16
for r1,r2 be Real, f be Function of REAL,REAL stf is integrable on A & f | A is boundedholds
min(AﬃneMap(0,r1),(r2 (#) f)) is integrable on A &min(AﬃneMap(0,r1),(r2 (#) f)) | A is bounded;theorem :: FUZZY 6:17
for r1,r2 be Real, f,F be Function of REAL,REAL stf is integrable on A & f | A is bounded &for x being Real holds F.x = min(r1, r2∗(f.x))
holds
F is integrable on A & F | A is bounded;theorem :: FUZZY 6:18
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 6:19
for a,b,c being Real, f,g,F be Function of REAL,REAL sta <= b & b <= c &F = f | [.a,b.] +∗ g | [.b,c.]holds
F is Function of [’a,c’],REAL;
theorem :: FUZZY 6:20
for a,b,c being Real, f,g,F be Function of REAL,REAL sta <= b & b <= c & F = f | [.a,b.] +∗ g | [.b,c.]

MMA-WiP (2022), vol.4, no.5 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.5 - ISSN 2434-5458 (Online)

9/12

Mechanized Mathematics and Its Applications, Works in Progress

Centroid Method as Defuzziﬁcation (Mitsuishi T.)

holds
F = F | [. a,c .];theorem :: FUZZY 6:21
for a,b,c being Real, f,g,h be Function of REAL,REAL sta <= b & b <= c &f | [’a,c’] is bounded & g | [’a,c’] is bounded &h = (f| [.a,b.]) +∗ (g | [.b,c.]) & f.b = g.bholds
h | [’a,c’] is bounded;theorem :: FUZZY 6:22
for a,b,c being Real, f,g,h be Function of REAL,REAL sta <= b & b <= c &f | [’a,c’] is bounded & g | [’a,c’] is bounded &h | [.a,c.] = (f| [.a,b.]) +∗ (g | [.b,c.]) & f.b = g.bholds
h | [’a,c’] is bounded;theorem :: FUZZY 6:23
for c being Real, f,g be Function of REAL,REAL st
f | A is bounded & g | A is boundedholds( (f | ].−infty,c.[) +∗ (g | [.c,+infty.[) ) | A is bounded;theorem :: FUZZY 6:24
for a,b,c be Real, f,g,h,F 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.b & F = h | [.a,c.]holds
F is continuous;
theorem :: FUZZY 6:25
for A being non empty closed interval Subset of REAL,
f be Function of REAL,REAL stf is continuous holds f is integrable on A & f | A is bounded;theorem :: FUZZY 6:26
for c being Real, f,g,F be Function of REAL,REAL stf is Lipschitzian & g is Lipschitzian &f . c = g . c & F = (f | ].−infty,c.[) +∗ (g | [.c,+infty.[)holds F is Lipschitzian;theorem :: FUZZY 6:27
for a,b being Real holds (AﬃneMap (a,b)) is Lipschitzian;theorem :: FUZZY 6:28
for a,b,p,q being 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 6:29
for a,b,p,q being 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.[ )holdsf is integrable on A & f | A is bounded;theorem :: FUZZY 6:30
for a,b,p,q being Real st a <> p holds(AﬃneMap (a,b)) . ((q−b)/(a−p)) = (AﬃneMap (p,q)) . ((q−b)/(a−p));theorem :: FUZZY 6:31
for f be Membership Func of REAL holds f is bounded;theorem :: FUZZY 6:32
for r be Real, f be Function of REAL,REAL str <> 0 & f is integrable on A & f | A is bounded

MMA-WiP (2022), vol.4, no.5 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.5 - ISSN 2434-5458 (Online)

10/12

Mechanized Mathematics and Its Applications, Works in Progress

Centroid Method as Defuzziﬁcation (Mitsuishi T.)

holds
centroid((r (#) f),A) = centroid(f,A);theorem :: FUZZY 6:33
for a,b,c being Real, f,g,h be Function of REAL,REAL sta <= b & b <= c &f is integrable on [’a,c’] & f | [’a,c’] is bounded &g is integrable on [’a,c’] & g | [’a,c’] is bounded &h | [.a,c.] = (f| [.a,b.]) +∗ (g | [.b,c.]) &h is integrable on [’a,c’] & f.b = g.bholds
integral(h,[’a,c’]) = integral(f,[’a,b’]) + integral(g,[’b,c’]);theorem :: FUZZY 6:34
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 = (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 6:35
for c being Real, f,g be Function of REAL,REAL
holdsf|].−infty,c.[ +∗ g|[.c,+infty.[ = (f|].−infty,c.]) +∗ (g|[.c,+infty.[);theorem :: FUZZY 6:36
for c being Real, f,g be Function of REAL,REAL st
f | A is bounded & g | A is boundedholds( (f|].−infty,c.]) +∗ (g|[.c,+infty.[) ) | A is bounded;theorem :: FUZZY 6:37
for a,b,c being Real, f,g be Function of REAL,REAL st a <= c & c <= bholds
f | [.a,c.[ +∗ g | [.c,b.] = f | [.a,c.] +∗ g | [.c,b.];theorem :: FUZZY 6:38
for a,b,c being Real, f,g,h be Function of REAL,REAL sta <= c & h | [.a,c.] = (f| [.a,b.]) +∗ (g | [.b,c.]) & f.b = g.bholds( b <= a implies h | [.a,c.] = g | [.a,c.] ) &( c <= b implies h | [.a,c.] = f | [.a,c.] );theorem :: FUZZY 6:39
for b being Real, f,g,h be Function of REAL,REAL sth = (f| ].−infty,b.[) +∗ (g | [.b,+infty.[) & f.b = g.b holds( b <= lower bound A implies h | A = g | A ) &( upper bound A <= b implies h | A = f | A );theorem :: FUZZY 6:40
for a,b,p,q being 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.[ ) & (q−b)/(a−p) in A
holds
f | A = ( AﬃneMap (a,b) |[.lower bound A,(q−b)/(a−p).] )+∗ ( AﬃneMap (p,q) |[.(q−b)/(a−p),upper bound A.] );theorem :: FUZZY 6:41
for a,b being Real holds
AﬃneMap (a,b) | A is bounded & AﬃneMap (a,b) is integrable on A;
theorem :: FUZZY 6:42
for a,b,p,q being 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( (q−b)/(a−p) in A implies

MMA-WiP (2022), vol.4, no.5 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.5 - ISSN 2434-5458 (Online)

11/12

Mechanized Mathematics and Its Applications, Works in Progress

Centroid Method as Defuzziﬁcation (Mitsuishi T.)

integral(f,A) = integral(AﬃneMap (a,b),[’lower bound A,(q−b)/(a−p)’])+ integral(AﬃneMap (p,q),[’(q−b)/(a−p),upper bound A’]) )&( (q−b)/(a−p) <= lower bound A implies
integral(f,A) = integral(AﬃneMap (p,q),A) )&( (q−b)/(a−p) >= upper bound A implies
integral(f,A) = integral(AﬃneMap (a,b),A) );theorem :: FUZZY 6:43
for a,b,p,q being Real, f be Function of REAL,REAL st a <> p &f | A = (AﬃneMap (a,b) | [.lower bound A,(q−b)/(a−p).])+∗ (AﬃneMap (p,q) | [.(q−b)/(a−p),upper bound A.]) & (q−b)/(a−p) in A
holds
integral((id REAL) (#) f,A)
= integral((id REAL) (#) (AﬃneMap (a,b)),[’lower bound A,(q−b)/(a−p)’])+ integral((id REAL) (#) (AﬃneMap (p,q)),[’(q−b)/(a−p),upper bound A’]);
theorem :: FUZZY 6:44
for a,b being Real holds(id REAL) (#) (AﬃneMap (a,b)) = (a (#) ( #Z 2)) + (b (#) ( #Z 1));
theorem :: FUZZY 6:45
for a,b,c,d being Real st c <= d holds
integral((id REAL) (#) (AﬃneMap (a,b)),c,d)= 1/3∗a∗(d∗d∗d − c∗c∗c) + 1/2∗b∗(d∗d − c∗c);theorem :: FUZZY 6:46
for a,b being Real holds
AﬃneMap (a,b) = (a (#) ( #Z 1)) + (b (#) ( #Z 0));theorem :: FUZZY 6:47
for a,b,c,d being Real st c <= d holds
integral(AﬃneMap (a,b),c,d) = 1/2∗a∗(d∗d − c∗c) + b∗(d − c);theorem :: FUZZY 6:48
for a,b,p,q,c,d,e being Real, f be Function of REAL,REAL st a <> p &f | A = AﬃneMap (a,b) | [.lower bound A,(q−b)/(a−p).]+∗ AﬃneMap (p,q) | [.(q−b)/(a−p),upper bound A.] & (q−b)/(a−p) in A
holds
centroid(f,A) =( 1/3∗a∗(((q−b)/(a−p))ˆ3 − (lower bound A)ˆ3)+ 1/2∗b∗(((q−b)/(a−p))ˆ2 − (lower bound A)ˆ2)+ 1/3∗p∗((upper bound A)ˆ3 − ((q−b)/(a−p))ˆ3)+ 1/2∗q∗((upper bound A)ˆ2 − ((q−b)/(a−p))ˆ2) ) /( 1/2∗a∗(((q−b)/(a−p))ˆ2 −(lower bound A)ˆ2) + b∗((q−b)/(a−p) − lower bound A)+ 1/2∗p∗((upper bound A)ˆ2 −((q−b)/(a−p))ˆ2) + q∗(upper bound A −(q−b)/(a−p)) );theorem :: FUZZY 6:49
for f being Function of REAL,REAL holds
max+ f = max(AﬃneMap(0,0),f);

MMA-WiP (2022), vol.4, no.5 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.5 - ISSN 2434-5458 (Online)

12/12