Mechanized Mathematics and Its Applications, Works in Progress

Functional Spaces of Continuous Functions (Shidama Y.)

Regular Paper

C 空間の形式化について
On the Formalizations for Functional Spaces ofContinuous Functions
師玉 康成 1,*
Yasunari Shidama1,*
1 信州大学工学部, 長野県長野市若里 4-17-1
1 Faculty of Engineering, Shinshu University. 4-17-1 Wakasato, Nagano, Japan* shidama@cs.shinshu-u.ac.jp
Proof checked by Mizar Version: 8.1.10 5 and MML Version: 5.63.1382
Received: November 9, 2019. Revised: June 23, 2020. Accepted: October 10, 2020.

Abstract
In this paper, we formalized the Functional Spaces which are constructed from allnorm space value continuous functions defined on a topological space. First, we provethat this Functional Space is complete in the case of the functions range set is complete.
Next, we formalized the Ascoli-Arzelà’s theorem, and proved this theorem.

1

はじめに
本稿では筆者らが作成している連続関数全体の集合からなる関数空間の形式化表現について途中経過を報告する．周知のように連続関数全体の集合からなる関数空間 C 空間 [1]は関数空間の中で最も基本的なものである．Mizar Mathematical Library (以下 MML)には位相空間上の実数値連続関数全体の集合によるノルム環や，コンパクト空間上の実数値連続関数全体の集合による完備なノルム環の形式化が C0SP1,C0SP2 [2], [3] に収録されている．本稿ではその後続として，ノルム空間に値をとる連続関数全体の集合による関数空間の形式化について述べる．また，この空間の部分集合のコンパクト性の必要十分条
件の定理，Ascoli-Arzelà の定理の形式化を行った．

MMA-WiP (2020), vol.2, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2020.2.1 - ISSN 2434-5458 (Online)

1/16

Mechanized Mathematics and Its Applications, Works in Progress

Functional Spaces of Continuous Functions (Shidama Y.)

2

連続関数全体の集合による関数空間

2.1

Mizar による数学的構造の定義

MML では [4] と同様に集合論を基礎とする形式化を行っている．群や環，位相空間など数学的な概念は集合と写像などから構成される構造体 (struct) と，それの特定の性質を表す属性 (attribute) を定義することによって形式化される．最も原始的な構造
体は 1 − sorted である．これは STRUCT 0 で以下のように定義されている．またこの

1 − sorted の上に加法が加えられたものが addMagma であり ALGSTR 0 に収録されている．これは代数的な構造体の内，最も原始的な構造体である．

Listing 1. 1-sorted addMagmadeﬁnition
struct 1−sorted(# carrier −> set #);end;
deﬁnition
struct (1−sorted) addMagma (# carrier −> set, addF −> BinOp of the carrier
#);
end;

MML では，これらの原始的な構造体に，所要の付加を行い，線形空間 [5] や，位相空間 [6] などのより複雑な数学的構造体を定義している．本稿で扱う線形空間やノルム空間は以下のように段階的に定義されている．まず，上記の台集合 (carrier) のみからなる構造体 1 − sorted に台集合の一つの元 ZeroF を指定した構造体 ZeroStr を定義する．次にこの構造体 ZeroStr と前述の加法演算をもつ構造体 addMagma からこれらを合成して加法とゼロ元をもった構造体 addLoopStr を造る．

Listing 2. ZeroStr addLoopStr
deﬁnition
struct (1−sorted) ZeroStr (# carrier −> set, ZeroF −> Element of the carrier #);end;
deﬁnition
struct (ZeroStr,addMagma) addLoopStr (# carrier −> set, addF −> BinOp of thecarrier, ZeroF −> Element of the carrier #);end;

続いて，この構造体 addLoopStr にこれに実数係数のスカラ倍演算 Mult を加えた
実線形空間の構造体 RLSStruct [5] を定義する．

Listing 3. RLSStructdeﬁnition
struct (addLoopStr) RLSStruct (# carrier −> set, ZeroF −> Element of the carrier,addF −> BinOp of the carrier, Mult −> Function of [:REAL, the carrier :], the carrier #);end;

次にこの構造体 RLSStruct について以下のように加法の可換則，結合則，ゼロ元の存在，加法についての逆元の存在，スカラ倍についての結合則，加法とスカラ倍についての分配則などの属性を定義している．

MMA-WiP (2020), vol.2, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2020.2.1 - ISSN 2434-5458 (Online)

2/16

Mechanized Mathematics and Its Applications, Works in Progress

Functional Spaces of Continuous Functions (Shidama Y.)

Listing 4. attributedeﬁnition
let IT be addMagma;
attr IT is Abelian means:: RLVECT 1:def 2
for v,w being Element of IT holds v + w = w + v;
attr IT is add−associative means:: RLVECT 1:def 3
for u,v,w being Element of IT holds (u + v) + w = u + (v + w);
end;
deﬁnition
let IT be addLoopStr;
attr IT is right zeroed means:: RLVECT 1:def 4
for v being Element of IT holds v + 0.IT = v;
end;
deﬁnition
let IT be non empty RLSStruct;attr IT is vector−distributive means:: RLVECT 1:def 5
for a for v,w being VECTOR of IT holds a ∗ (v + w) = a ∗ v + a ∗ w;
attr IT is scalar−distributive means:: RLVECT 1:def 6
for a,b for v being VECTOR of IT holds (a + b) ∗ v = a ∗ v + b ∗ v;
attr IT is scalar−associative means:: RLVECT 1:def 7
for a,b for v being VECTOR of IT holds (a ∗ b) ∗ v = a ∗ (b ∗ v);
attr IT is scalar−unital means:: RLVECT 1:def 8
for v being VECTOR of IT holds 1 ∗ v = v;
end;

実線形空間は構造体 RLSStruct に上記の属性を付加することにより定義される．以
下の記述は RLVECT 1 に収録されている．registration 宣言に続く cluster は上記の線形空間の属性を満たす構造体 RLSStruct が存在することを宣言する．この宣言文以降
は，環境部 environ にこの RLVECT 1 を所要の記述をすれば存在の証明なしにこの実線形空間の属性をもつ構造体 RLSStruct を扱うことができる．また，mode の定義に
よって実線形空間の属性をもつ構造体 RLSStruct である変数型 RealLinearSpace を導入している．mode と cluster の違いなど詳細は以下の解説記事を参照されたい．
http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar4/printout/
mizar4ja_prn.pdf

Mizar では関数 f の変数 x に対する値は f (x) ではなく f.x で表し, ベクトル x のノル
ムは ||x|| ではなく ||.x.|| で表現している. 本稿で引用する Mizar の記述ではこれによっていることに注意されたい.

Listing 5. RealLinearSpace
registration
cluster strict Abelian add−associative non empty for addMagma;
end;registration
cluster strict Abelian add−associative right zeroed right complementable non empty for addLoopStr;
end;registration
cluster strict Abelian add−associative right zeroed right complementable scalar−distributive vector−distributive
scalar−associative scalar−unital for non empty RLSStruct;end;

MMA-WiP (2020), vol.2, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2020.2.1 - ISSN 2434-5458 (Online)

3/16

Mechanized Mathematics and Its Applications, Works in Progress

Functional Spaces of Continuous Functions (Shidama Y.)

deﬁnitionmode RealLinearSpace is Abelian add−associative right zeroed
right complementable scalar−distributive vector−distributive
scalar−associative scalar−unital non empty RLSStruct;
end;

2.2

連続写像全体の集合による実線形空間

冒頭に前述したように連続関数全体の集合からなる関数空間 C 空間 [1] は関数空間の中で最も基本的なものである．MML には位相空間上の実数値連続関数全体の集合によるノルム環や，コンパクト空間上の実数値連続関数全体の集合による完備なノルム環の形式化が C0SP1,C0SP2 [2], [3] に収録されている．本稿ではその後続として，ノルム空間に値をとる連続関数全体の集合による関数空間の形式化について述べる．関数空間の形式化には特に，有界な線形写像 [7] 全体の集合による関数空間もある．これらは MML のLOPBAN シリーズ [8] や双対空間を扱った DUALSP シリーズ [9] に収録されている．本稿ではそれらの結果の一部も利用している．ノルム空間に限らず，実線形空間に値をとる関数全体の集合による線形空間の形式化は MML の LOPBAN 1 で以下のように形式化されている．

Listing 6. LOPBAN 1:def 4
deﬁnition
let X be non empty set;let Y be RealLinearSpace;func RealVectSpace(X,Y) −> RealLinearSpace equals:: LOPBAN 1:def 4
RLSStruct(#Funcs(X,the carrier of Y), (FuncZero(X,Y)),FuncAdd(X,Y),FuncExtMult(X,Y)#);end;

X は空でない集合であり，Y は実数係数の線形空間である．Funcs(X, the carrier of Y)
は集合 X から Y の台集合への写像全体全体の集合で FUNCT 2 にある以下の定義によっている．これは上の線形空間の台集合 (carrier) になっている．

Listing 7. FUNCT 2:def 2
deﬁnition
let X,Y;func Funcs(X,Y) −> set means:: FUNCT 2:def 2
x in it iﬀ ex f being Function st x = f & dom f = X & rng f c= Y;
end;

前項で述べたように台集合 carrier は MML で，代数構造や位相構造他，数学的な構
造を形式化するための概念である．代数構造を定義する場合には carrier は演算の定義域に一致する．また位相構造を定義する場合は，carrier の部分集合の族が位相の開集合系を構成する. 前項の定義 RealVectSpace(X, Y) 中の FuncAdd(X, Y) はこの実線形空間の元である写像の加法すなわち，集合 X から Y への写像 f, g の加法

f + g : x ∈ X 7→ f (x) + g(x) ∈ Yを表している．同様に FuncExtMult(X, Y) は写像 f と実数 a の積

a · f : x ∈ X 7→ a · f (x) ∈ Y

MMA-WiP (2020), vol.2, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2020.2.1 - ISSN 2434-5458 (Online)

4/16

Mechanized Mathematics and Its Applications, Works in Progress

Functional Spaces of Continuous Functions (Shidama Y.)を表している．また FuncZero(X, Y) は X 上で恒に Y のゼロ元を値にとる写像を表しており，この実線形空間の RealVectSpace(X, Y) のゼロ元

0 : x ∈ X 7→ 0.Y ∈ Yを表している．これは LOPBAN 1 の以下の定義で形式化されている．[8]Listing 8. LOPBAN 1:def1
deﬁnition
let X be non empty set;let Y be non empty addLoopStr;
func FuncAdd(X,Y) −> BinOp of Funcs(X,the carrier of Y) means:: LOPBAN 1:def 1
for f,g being Element of Funcs(X,the carrier of Y) holds it.(f,g) = (the addF of Y).:(f,g);
end;
deﬁnition
let X be non empty set;let Y be RealLinearSpace;func FuncExtMult(X,Y) −> Function of [:REAL,Funcs(X,the carrier of Y):],
Funcs(X,the carrier of Y) means:: LOPBAN 1:def 2
for a being Real, f being Element ofFuncs(X,the carrier of Y), x being Element of X holds (it.[a,f]).x = a∗(f.x);
end;
deﬁnition
let X be set;let Y be non empty ZeroStr;
func FuncZero(X,Y) −> Element of Funcs (X,the carrier of Y) equals:: LOPBAN 1:def 3
X −−> 0.Y;
end;

S, T をそれぞれ空でない位相空間 (TopSpace)，位相線形空間 (LinearTopSpace)とするとき T に値をとる S 上の連続写像全体の集合は上で述べた

RealVectSpace(the carrier of S, T)と同様に線形空間を造るが，これは RealVectSpace(the carrier of S, T) の部分線形空間として定義できる．まず，以下のように連続写像全体の集合 ContinuousFunctions(S, T)
をこの線形空間の部分集合として定義する．

Listing 9. C0SP3:def 2
deﬁnition
let S be non empty TopSpace, T be non empty LinearTopSpace ;func ContinuousFunctions(S,T) −> Subset of RealVectSpace(the carrier of S,T)
equals:: C0SP3:def 2{ f where f is Function of the carrier of S, the carrier of T :f is continuous };end;

次にこれが線形的に閉じていることを示す．

Listing 10. C0SP3:5
theorem :: C0SP3:5
for S be non empty TopSpace, T be non empty LinearTopSpace holds ContinuousFunctions(S,T) is linearly−
closed;MMA-WiP (2020), vol.2, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2020.2.1 - ISSN 2434-5458 (Online)

5/16

Mechanized Mathematics and Its Applications, Works in Progress

Functional Spaces of Continuous Functions (Shidama Y.)

実線形空間の代数的に閉じた部分集合についてその部分集合を台集合とした実線形空間の構造が定義できることを示す以下の命題 [10] を用いる．

Listing 11. RSSPACE:11
theorem :: RSSPACE:11
for V be RealLinearSpace, V1 be Subset of V st
V1 is linearly−closed non empty holds RLSStruct (# V1,Zero (V1,V), Add (V1,V),Mult (V1,V) #) is Subspaceof V;

線形空間 V の代数的に閉じた部分集合 V1 について，上記の Add (V1, V) は V の加法から導入される V1 上の加法を表している．これは V の加法の定義域を V1 の直積

V1 × V1 上に制限して得られる．同様に Mult (V1, V) は V のそれから導入される実数係数と V1 の元とのスカラ倍演算を表している．また，Zero (V1, V) は V のゼロ元と同一だがそれを V1 の元として見なしたものを表している．これら命題を用いて以下の連続写像全体の集合による実線形空間の構造体について定理 C0SP3:6 で前項に述べた実線形空間の属性を満たすことを示す．

Listing 12. ContinuousFunctions
RLSStruct (# ContinuousFunctions(S,T),Zero (ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
Add (ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T)),Mult (ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T))#)

Listing 13. C0SP3:6
theorem :: C0SP3:6
for S be non empty TopSpace, T be non empty LinearTopSpace
holds RLSStruct(# ContinuousFunctions(S,T),Zero (ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
Add (ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),Mult (ContinuousFunctions(S,T), RealVectSpace(
the carrier of S,T))#)is Subspace of RealVectSpace(the carrier of S,T);

この定理により上記の構造体が実線形空間の属性を満たすことを registration を用いて宣言する．さらにこのような構造体を空でない位相空間，位相線形空間 S, T を引数にもち実線形空間の変数型 (mode) をもつ Functor

R VectorSpace of ContinuousFunctions(S, T)
として定義する．

Listing 14. C0SP3:def 3
registrationlet S be non empty TopSpace, T be non empty LinearTopSpace;cluster RLSStruct (# ContinuousFunctions(S,T),Zero (ContinuousFunctions(S,T),RealVectSpace(the carrier of S,
T)),
Add (ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T)),Mult (ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T))#)−> Abelian add−associative right zeroed right complementable vector−distributive scalar−distributive scalar−associative scalar−unital;end;
deﬁnition
let S be non empty TopSpace, T be non empty LinearTopSpace;func R VectorSpace of ContinuousFunctions(S,T)−> RealLinearSpace equals:: C0SP3:def 3

MMA-WiP (2020), vol.2, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2020.2.1 - ISSN 2434-5458 (Online)

6/16

Mechanized Mathematics and Its Applications, Works in Progress

Functional Spaces of Continuous Functions (Shidama Y.)

RLSStruct (# ContinuousFunctions(S,T),Zero (ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
Add (ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T)),Mult (ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T))#);
end;

この R VectorSpace of ContinuousFunctions(S, T) には

RealVectSpace(the carrier of S, T) の部分線形空間としてその加法，スカラ倍の代数
演算を ContinuousFunctions(S, T) の元に制限して導入している．

Listing 15. C0SP3:13-14
theorem :: C0SP3:13
for S,T be RealNormSpace
for f,g,h be VECTOR of R VectorSpace of ContinuousFunctions(S,T)
holds h = f+g iﬀ for x be Element of S holds h.x = f.x + g.x;
theorem :: C0SP3:14
for S,T be RealNormSpace
for f,h be VECTOR of R VectorSpace of ContinuousFunctions(S,T)
for a be Real holds h = a∗f iﬀ for x be Element of S holds h.x = a ∗ f.x;

C 空間の形式化表現

3

前項と同様にしてコンパクト空間上の連続写像全体の集合による実線形空間を構成できるが，この空間にはさらにノルムが定義でき，そのノルムによって完備であることを示すことができる．

3.1

ノルムを伴う位相線形空間

まず，ノルムを伴う位相線形空間の構成について述べる．周知のようにノルム線形空間は，そのノルムから定義される距離を経由して位相が定義でき，この空間は位相線形空間になっている．しかしながら，Mizar は厳密な形式検証を目的としたシステムであるため，一つの変数型について成立する命題や定義を，他の変数型について用いることは，それが可能であることを証明しない限りできない．これは前章で述べた構造体についても同様である．現状の MML では，ノルム線形空間 (RealNormSpace) [11] と，位相線形空間(LinearTopSpace) [12] の定義はそれぞれ MML の NOMSP 1 と RLTOPSP1 で以下のよ
うに定義されている．

Listing 16. NORMSTR
struct(RLSStruct, N−ZeroStr) NORMSTR (# carrier −> set, ZeroF −> Element of the carrier,addF −> BinOp of the carrier,Mult −> Function of [:REAL, the carrier:], the carrier, normF −> Function of the carrier, REAL #);end;registration
cluster reﬂexive discerning RealNormSpace−like vector−distributive scalar−distributive
scalar−associative scalar−unital Abelian add−associative
right zeroed right complementable strict for non empty NORMSTR;
end;
deﬁnitionmode RealNormSpace is reﬂexive discerning RealNormSpace−like vector−distributive
scalar−distributive scalar−associative scalar−unital
Abelian add−associative right zeroed right complementable non empty NORMSTR;
end;

MMA-WiP (2020), vol.2, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2020.2.1 - ISSN 2434-5458 (Online)

7/16

Mechanized Mathematics and Its Applications, Works in Progress

Functional Spaces of Continuous Functions (Shidama Y.)

Listing 17. RLTopStructdeﬁnition
struct(RLSStruct,TopStruct) RLTopStruct (# carrier −> set, ZeroF −> Element of the carrier,addF −> BinOp of the carrier,Mult −> Function of [:REAL, the carrier:],the carrier, topology −> Subset−Family of the carrier #);end;
registration
cluster strict add−continuous Mult−continuous TopSpace−like Abelian add−associative right zeroed
right complementable vector−distributive
scalar−distributive scalar−associative scalar−unital for non empty RLTopStruct;end;
deﬁnitionmode LinearTopSpace is add−continuous Mult−continuous TopSpace−like Abelian
add−associative right zeroed right complementable vector−distributive
scalar−distributive scalar−associative scalar−unital non empty RLTopStruct;end;

両者の定義を比較すると，実線形空間 (RealLinearSpace) の構造体 RLSStruct とそれに必要な Abelian など代数的属性は同一であるが，前者の構造体 NORMSTR にはノルム (normF) があり，後者の RLTopStruct には位相 (topology) が記述され，さらにはそれぞれの定義に必要な属性が記述され異なっている．結果として構造体の生成系
列は両者とも図 1 のように実線形空間 (RealLinearSpace) の構造体までは同一であるが構成の系列で同一線上 (先祖，子孫，親子関係) にはない．

N-Str

N-ZeroStr

NORMSTRZeroStr1-sorted
addMagma

TopStruct

addLoopStr

RLSStruct

RLTopStruct

RLNormTopStruct

図 1. 構造体の生成系列
このため，位相に関わるものについては意味の上では同一線上にあるべきノルム線形空間 (RealNormSpace) は位相線形空間 (LinearTopSpace) の命題や定義を流用できない．
この不便を解消するためには，一つの方法として，屋上屋根ではあるが，図 1 の白線矢印に示したように両者から新たな構造体を合成し，それをそれぞれの構成の系列の共通の「子孫」にすることが考えられる．本稿ではこれによりノルムを伴う実ノルム線形空間を以下のように構成した．RLNormTopStruct がその構造体であり，NormedLinearTopSpaceがその型変数名である．一般の位相空間については MML では TOPS 1∼TOPS 5 [6] 他，
多くの定理が収録されており，ノルム空間 [11] についても同様に「資産」がある．特にMMA-WiP (2020), vol.2, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2020.2.1 - ISSN 2434-5458 (Online)

8/16

Mechanized Mathematics and Its Applications, Works in Progress

Functional Spaces of Continuous Functions (Shidama Y.)

ノルム空間特有の命題が収録されている．これらを引用できることの利便性は大きい．

Listing 18. NormedLinearTopSpace
deﬁnition
struct(RLTopStruct,NORMSTR) RLNormTopStruct(# carrier −> set, ZeroF −> Element of the carrier, addF−> BinOp of the carrier,Mult −> Function of [:REAL, the carrier:],the carrier,topology −> Subset−Family of the carrier,normF −>Function of the carrier,REAL #);end;registration
cluster strict non empty for RLNormTopStruct;end;
deﬁnition
let X be non empty RLNormTopStruct ;attr X is norm−generated means:: C0SP3:def 7
ex RNS be RealNormSpace st RNS = the NORMSTR of X & the topology of X = the topology of (TopSpaceNorm RNS) ;end;
registration cluster strict add−continuous Mult−continuous TopSpace−like Abelian add−associative
right zeroed right complementable vector−distributive
scalar−distributive scalar−associative scalar−unital discerning reﬂexive RealNormSpace−likenorm−generated T 2 for non empty RLNormTopStruct;end;
deﬁnitionmode NormedLinearTopSpace is strict add−continuous Mult−continuous TopSpace−like Abelian add−associative
right zeroed
right complementable vector−distributive scalar−distributive scalar−associative scalar−unital
discerning reﬂexive RealNormSpace−like norm−generated T 2 non empty RLNormTopStruct;end;

上記の属性 norm − generated は空間の位相がノルムによって導入されることを意味する．この NormedLinearTopSpace の導入によって，ノルム線形空間 (NORMSP)と位相線形空間 (LinearTopSpace) 両者の命題を引用することが可能になったが，それらの一部，例えば開集合 (Openset) などが，両者それぞれに重複して定義されている．
新たに導入した NormedLinearTopSpace では位相は LinearTopSpace のものを用いるため， NORMSP 1∼NORMSP 4 の命題をそのままこの新たな構造体で流用できない．
この問題を解決するため，今回の形式化では以下のような命題を加えた．

Listing 19. C0SP3:23 etc
theorem :: C0SP3:23
for X being NormedLinearTopSpace, V being Subset of X holds
V is open iﬀ for x being Point of X st x in V holds
ex r being Real st r > 0 & { y where y is Point of X : ||.(x − y).|| < r } c= V;
theorem :: C0SP3:26
for X being NormedLinearTopSpace, RNS being RealNormSpace,t being sequence of X,s being sequence of RNS
st RNS = the NORMSTR of X & t=s & t is convergent holds s is convergent & lim s = lim t;
theorem :: C0SP3:27
for X being NormedLinearTopSpace, RNS being RealNormSpace,s being sequence of X, t being sequence of RNS
st RNS = the NORMSTR of X & s=t holds s is convergent iﬀ t is convergent;
theorem :: C0SP3:29
for X being NormedLinearTopSpace,RNS be RealNormSpace,V being Subset of X, W being Subset of RNS
st RNS = the NORMSTR of X & the topology of X = the topology of (TopSpaceNorm RNS)
& V = W holds V is closed iﬀ W is closed;

MMA-WiP (2020), vol.2, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2020.2.1 - ISSN 2434-5458 (Online)

9/16

Mechanized Mathematics and Its Applications, Works in Progress

Functional Spaces of Continuous Functions (Shidama Y.)

theorem :: C0SP3:32
for X being NormedLinearTopSpace, RNS be RealNormSpace,V being Subset of X,W being Subset of RNS
st RNS = the NORMSTR of X & the topology of X = the topology of (TopSpaceNorm RNS)
& V = W holds V is compact iﬀ W is compact;3.2

実ノルム線形空間

コンパクトな位相空間上の連続関数は有界関数でもある．有界関数全体の集合からなる完備なノルム線形空間は RSSPACE4 で形式化されている．空でない集合 X からノル
ム空間 Y への有界な写像全体の集合を BoundedFunctions(X, Y) で表し，それを台集
合 (carrier) とするノルム空間を R NormSpace of BoundedFunctions(X, Y) で定義している．

Listing 20. RSSPACE4:def 10
deﬁnition
let X be non empty set;let Y be RealNormSpace;func R NormSpace of BoundedFunctions(X,Y) −> non empty NORMSTR equals:: RSSPACE4:def 10
NORMSTR (# BoundedFunctions(X,Y), Zero (BoundedFunctions(X,Y), RealVectSpace(X,Y)), Add (BoundedFunctions(X,Y), RealVectSpace(X,Y)),Mult (BoundedFunctions(X,Y), RealVectSpace(X,Y)), BoundedFunctionsNorm(X,Y) #);end;

特に値域のノルム空間が完備な場合 (RealBanachSpace) はそのノルム空間も完備であることも示されている．

Listing 21. RSSPACE4:26
theorem :: RSSPACE4:26
for X be non empty set for Y be RealBanachSpace holds
R NormSpace of BoundedFunctions(X,Y) is RealBanachSpace;

本稿での形式化はコンパクトな位相空間 S 上の連続でノルムを伴う位相線形空間 T に値を取る関数の集合 ContinuousFunctions(S, T) を S の台集合上の有界写像で T に値を取る関数全体の集合 BoundedFunctions(the carrier of S, T) の部分集合として扱
い,ContinuousFunctions(S, T) を台集合 (carrier) とするノルム線形空間

R NormSpace of ContinuousFunctions(S, T)
を以下のような命題と定義で導入した．

Listing 22. C0SP3:34-def9
theorem :: C0SP3:34
for S be non empty compact TopSpace ,T be NormedLinearTopSpace
holds for x being set st x in ContinuousFunctions(S,T) holds x in BoundedFunctions (the carrier of S,T);
theorem :: C0SP3:35
for S be non empty compact TopSpace ,T be NormedLinearTopSpace holds(R VectorSpace of ContinuousFunctions(S,T) is Subspace of R VectorSpace of BoundedFunctions(the carrier of S,T));

MMA-WiP (2020), vol.2, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2020.2.1 - ISSN 2434-5458 (Online)

10/16

Mechanized Mathematics and Its Applications, Works in Progress

Functional Spaces of Continuous Functions (Shidama Y.)

deﬁnition
let S be non empty compact TopSpace ,T be NormedLinearTopSpace ;func ContinuousFunctionsNorm(S,T) −> Function of (ContinuousFunctions(S,T)),REAL equals:: C0SP3:def 8(BoundedFunctionsNorm(the carrier of S,T)) | (ContinuousFunctions(S,T));end;
deﬁnition
let S be non empty compact TopSpace ,T be NormedLinearTopSpace ;func R NormSpace of ContinuousFunctions(S,T) −> NORMSTR equals:: C0SP3:def 9
NORMSTR (# ContinuousFunctions(S,T), Zero (ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
Add (ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)), Mult (ContinuousFunctions(S,T),
RealVectSpace(the carrier of S,T)),
ContinuousFunctionsNorm(S,T) #);end;

この空間のノルムは S から T への有界な写像全体の集合から構成されるノルム線形空
間 R NormSpace of BoundedFunctions(S, T) のノルム||f || = sup{||f (x)|| : x ∈ S} f ∈ BoundedFunctions(the carrier of S, T)の定義域を C 0 Functions(S, T) に制限したものとして導入している．

C0SP3:def 9 に記述したように実線形空間としての構造は加法，スカラ倍演算の定義
域を集合 ContinuousFunctions(S, T) に制限することにより実線形空間
R VectorSpace of BoundedFunctions(the carrier of S, T)の部分空間として構成している．部分空間の構成方法は前章の連続関数全体の集合による実線形空間の構成と同様に ContinuousFunctions(S, T) が代数的に閉じていることを示した上で RSSPACE:11 を用いている．ノルムについては C0SP3:def 8 に示したように有界関数全体の集合によるノルム空間のそれを定義域を集合 ContinuousFunctions(S, T)に制限することにより定義している．
加法やスカラ倍等の演算は前章と同様に RealVectSpace(the carrier of S, T) の部
分空間として，以下のように演算を ContinuousFunctions(S, T) に制限して踏襲している．

Listing 23. C0SP3:44-45
theorem :: C0SP3:44
for S be non empty compact TopSpace ,T be NormedLinearTopSpace
for F,G,H being Point of R NormSpace of ContinuousFunctions(S,T)
for f,g,h be Function of S,T holds(f=F & g=G & h=H implies (H = F+G iﬀ for x be Element of S holds h.x = f.x + g.x));
theorem :: C0SP3:45
for a be Realfor S be non empty compact TopSpace ,T be NormedLinearTopSpace
for F,G being Point of R NormSpace of ContinuousFunctions(S,T)
for f,g being Function of S,T holds(f=F & g=G implies ( G = a∗F iﬀ for x be Element of S holds g.x = a∗f.x ));T が完備な場合はこの R NormSpace of ContinuousFunctions(S, T) も完備になるが，これについては前項と同様に以下の定理によって有界関数全体の集合によるノルム
空間 R NormSpace of BoundedFunctions(X, Y) が完備 (RealBanachSpace) になることを用いた．

MMA-WiP (2020), vol.2, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2020.2.1 - ISSN 2434-5458 (Online)

11/16

Mechanized Mathematics and Its Applications, Works in Progress

Functional Spaces of Continuous Functions (Shidama Y.)

Listing 24. RealBanachSpace
theorem :: RSSPACE4:26
for X be non empty set for Y be RealBanachSpace holds R NormSpace of BoundedFunctions(X,Y) is
RealBanachSpace;

そのためにコンパクト位相空間上の連続関数列の一様収束した関数が連続関数になることを示す以下の定理を形式化した．

Listing 25. C0SP3:49
theorem :: C0SP3:49
for S be non empty TopSpace ,T be NormedLinearTopSpace,
H be Functional Sequence of the carrier of S,the carrier of T,
LimH be Function of S,Tst H is unif conv on the carrier of S
& ( for n be Nat holds ex Hn be Function of S,T st Hn = H.n & Hn is continuous )& LimH = lim(H,the carrier of S) holds LimH is continuous;

これを用いて ContinuousFunctions(S, T) がこの完備なノルム空間の部分集合として位相的に閉じている (閉集合である) ことを以下の定理 C0SP3:50 で示し，C0SP3:52
によって R NormSpace of ContinuousFunctions(S, T) が完備になることを示している．

Listing 26. C0SP3:50-52
theorem :: C0SP3:50
for S be non empty compact TopSpace ,T be NormedLinearTopSpace holds
for Y be Subset of the carrier of
R NormSpace of BoundedFunctions(the carrier of S,T) st
Y = ContinuousFunctions(S,T) holds Y is closed;
theorem :: C0SP3:51
for S be non empty compact TopSpace ,T be NormedLinearTopSpace st T is complete holds
for seq be sequence of R NormSpace of ContinuousFunctions(S,T)
st seq is Cauchy sequence by Norm holds seq is convergent;
theorem :: C0SP3:52
for S be non empty compact TopSpace ,T be NormedLinearTopSpace st T is complete
holds R NormSpace of ContinuousFunctions(S,T) is complete;

4

C0 空間の形式化表現
筆者らはコンパクト集合内に台をもつ連続関数全体の集合によるノルム空間 (C0 空間) も形式化している．X を位相空間，T をノルムを伴う位相線形空間とするとき，X のコンパク
トな部分集合内に台をもつ X から T への連続関数全体の集合 C 0 Functions(X, T) を X
から T への関数全体の集合で構成される実線形空間 RealVectSpace(the carrier of X, T)[13] の部分集合として以下のように定義し，これが RealVectSpace(the carrier of X, T)
で代数的に閉じていることを示した．

Listing 27. C0SP3:def 11
deﬁnition
let X be non empty TopSpace ,T be NormedLinearTopSpace;func C 0 Functions(X,T) −> non empty

MMA-WiP (2020), vol.2, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2020.2.1 - ISSN 2434-5458 (Online)

12/16

Mechanized Mathematics and Its Applications, Works in Progress

Functional Spaces of Continuous Functions (Shidama Y.)

Subset of RealVectSpace(the carrier of X,T) equals:: C0SP3:def 11{ f where f is Function of the carrier of X, the carrier of T :f is continuous & ex Y be non empty Subset of X st
Y is compact & Cl ( support f ) c= Y };end;

Listing 28. C0SP3:56-theorem 58
theorem :: C0SP3:56
for X be non empty TopSpace ,T be NormedLinearTopSpacefor v,u be Element of RealVectSpace(the carrier of X,T)
st v in C 0 Functions(X,T) & u in C 0 Functions(X,T) holds v + u in C 0 Functions(X,T);
theorem :: C0SP3:57
for X be non empty TopSpace ,T be NormedLinearTopSpace
for a be Real,u be Element of RealVectSpace(the carrier of X,T)
st u in C 0 Functions(X,T) holds a ∗ u in C 0 Functions(X,T);
theorem :: C0SP3:58
for X be non empty TopSpace ,T be NormedLinearTopSpace holds
C 0 Functions(X,T) is linearly−closed;

さらに前章の C 空間と同様にノルムを X から T への有界な関数全体の集合で構成されるノルム線形空間のノルム||f || = sup{||f (x)|| : x ∈ S}, f ∈ BoundedFunctions(the carrier of S, T)
を以下のように C 0 Functions(X, T) に定義域に制限することによって導入した．

Listing 29. C0SP3:def 13 - theorem 68
deﬁnition
let X be non empty TopSpace ,T be NormedLinearTopSpace;func C 0 FunctionsNorm(X,T) −> Function of (C 0 Functions(X,T)),REAL equals:: C0SP3:def 13(BoundedFunctionsNorm(the carrier of X,T)) | (C 0 Functions(X,T));end;
deﬁnition
let X be non empty TopSpace ,T be NormedLinearTopSpace;func R Normed Space of C 0 Functions (X,T) −> non empty NORMSTR equals:: C0SP3:def 14
NORMSTR (# C 0 Functions(X,T), Zero (C 0 Functions(X,T), RealVectSpace(the carrier of X,T)),
Add (C 0 Functions(X,T), RealVectSpace(the carrier of X,T)),Mult (C 0 Functions(X,T), RealVectSpace(the carrier of X,T)),C 0 FunctionsNorm(X,T) #);theorem :: C0SP3:68
for X be non empty TopSpace ,T be NormedLinearTopSpace holds R Normed Space of C 0 Functions (X,T) is
RealNormSpace;end;5

Ascoli-Arzelà の定理
筆者らはさらに，Ascoli-Arzelà の定理 [14] として知られる関数の族についてのコン

パクト性の必要十分条件，すなわち前章までに述べた空間の部分集合のコンパクト性についての定理の形式化を行っている．先ず同程度連続性と同程度有界性の定義を以下のように形式化した．

MMA-WiP (2020), vol.2, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2020.2.1 - ISSN 2434-5458 (Online)

13/16

Mechanized Mathematics and Its Applications, Works in Progress

Functional Spaces of Continuous Functions (Shidama Y.)

Listing 30. ASCORI:def 2 def 4
deﬁnition
let S be non empty MetrSpace ,T be RealNormSpace;
let F be Subset of Funcs(the carrier of S,the carrier of T);
attr F is equibounded means:: ASCORI:def 2
ex K be Real st for f be Function of the carrier of S,the carrier of T
st f in F holds for x be Element of S holds ||.f.x.|| <= K ;end;
deﬁnition
let S be non empty MetrSpace,T be RealNormSpace;
let F be Subset of Funcs(the carrier of S,the carrier of T);
pred F is equicontinuous means:: ASCORI:def 4
for e be Real st 0 < e ex d be Real st 0 < d&for f be Function of the carrier of S,the carrier of T
st f in F holds for x1,x2 be Point of S st dist(x1,x2) < d holds ||.f.x1−f.x2.|| < e;end;

これらの定義と MML の TOPMETR4 に収録されている距離空間に関する定理及び補題により以下のように Ascoli-Arzelà の定理の形式化を行った．

Listing 31. ASCORI:18
theorem :: ASCORI:18
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace,
F be non empty Subset of R NormSpace of ContinuousFunctions(S,T),
G be Subset of Funcs(the carrier of M, the carrier of T)
st S = TopSpaceMetr(M) & T is complete & G = F
holds
Cl(F) is compactiﬀ
G is equicontinuous& for x be Point of S, Fx be non empty Subset of (MetricSpaceNorm T)
st Fx = {f.x where f is Function of S,T :f in F }holds (MetricSpaceNorm T) | Cl(Fx) is compact;

特にこの定理の系として，S から T の compact な部分集合 U の中への写像の集合については，以下の定理が得られる．

Listing 32. ASCORI:23
theorem :: ASCORI:23
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace,
U be compact Subset of T,
F be non empty Subset of
R NormSpace of ContinuousFunctions(S,T),
G be Subset of Funcs(the carrier of M, the carrier of T)
st S = TopSpaceMetr(M) & T is complete& G = F & for f be Function st f in F holds rng f c= U
holds
( Cl(F) is compact implies G is equibounded & G is equicontinuous )&( G is equicontinuous implies Cl(F) is compact )MMA-WiP (2020), vol.2, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2020.2.1 - ISSN 2434-5458 (Online)

14/16

Mechanized Mathematics and Its Applications, Works in Progress6Functional Spaces of Continuous Functions (Shidama Y.)

まとめ
位相線形空間に値をとる連続関数全体の集合による関数空間 C 空間(ノルム線形空間)の形式化について報告した．コンパクト空間上の連続関数，コンパクト集合内に台をもつ連続関数の集合全体により構成されるノルム線形空間 C, C0 についての形式化である．その過程でノルム線形空間 (RealNormSpace) と位相線形空間 (LinearTopSpace) の構
造体から新たな構造体を合成した．これは位相がノルムによって定義される位相線形空間である．これによって従来は別々に引用されてきたノルム線形空間 (RealNormSpace)と位相空間 (TopSpace) の定理群を統一的に扱う一つの形式化方法を提示した．またこれらの空間の部分集合のコンパクト性についての定理，すなわち Ascoli-Arzelà の定理として知られる関数の族についてのコンパクト性の必要十分条件についての定理の形式化を行った．筆者らはさらに階層型ニューラルネットワークを入力データと出力データの関係を表す関数と見なし，そのような関数の集合を上記の空間の部分集合として扱い，そのコ
ンパクト性についての定理の形式化を行っているがこれについては次回以降に報告する．

参考文献[1] Yoshida K. Functional Analysis. Springer; 1980.
[2] Shidama Y, Suzuki H, Endou N. Banach Algebra of Bounded Functionals. Formalized Mathematics. 2008;16(2):115–122. Available from: https://content.
sciendo.com/downloadpdf/journals/forma/16/2/article-p115.xml.
[3] Kanazashi K, Endou N, Shidama Y. Banach Algebra of Continuous Functionals and the Space of Real-Valued Continuous Functionals with Bounded Support.
Formalized Mathematics. 2010;18(1):11–16. Available from: https://content.
sciendo.com/downloadpdf/journals/forma/18/1/article-p11.xml.
[4] Bourbaki N. Elements de Mathematique. vol. Topologie Generale. troisieme ed.
HERMANN; 1960.
[5] Trybulec WA.
1990;1(2):291–296.

Vectors in Real Linear Space.
Available from:

Formalized Mathematics.

http://fm.mizar.org/1990-1/pdf1-2/

rlvect_1.pdf.
[6] Wysocki M, Darmochwal A. Subsets of Topological Spaces. Formalized Mathematics. 1990;1(1):231–237. Available from: http://fm.mizar.org/1990-1/pdf1-1/
tops_1.pdf.
[7] Dunford N, Schwartz JT. Linear operators I. Interscience Publ.; 1958.
[8] Shidama Y. Banach Space of Bounded Linear Operators. Formalized Mathematics. 2004;12(1):39–48. Available from: http://fm.mizar.org/2004-12/pdf12-1/
lopban_1.pdf.

MMA-WiP (2020), vol.2, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2020.2.1 - ISSN 2434-5458 (Online)

15/16

Mechanized Mathematics and Its Applications, Works in Progress

Functional Spaces of Continuous Functions (Shidama Y.)[9] Narita K, Endou N, Shidama Y. Dual Spaces and Hahn-Banach Theorem. Formalized Mathematics. 2014;22(1):69–77. Available from: https://content.sciendo.
com/downloadpdf/journals/forma/22/1/article-p69.xml.
[10] Endou N, Suzuki Y, Shidama Y. Real Linear Space of Real Sequences. Formalized Mathematics. 2003;11(3):249–253. Available from: http://fm.mizar.org/
2003-11/pdf11-3/rsspace.pdf.
[11] Popiolek J. Real Normed Space. Formalized Mathematics. 1991;2(1):111–115.
Available from: http://fm.mizar.org/1991-2/pdf2-1/normsp_1.pdf.
[12] Byliński C. Introduction to Real Linear Topological Spaces. Formalized Mathematics. 2005;13(1):99–107.

Available from: http://fm.mizar.org/2005-13/

pdf13-1/rltopsp1.pdf.
[13] Suzuki Y. Banach Space of Bounded Real Sequences. Formalized Mathematics. 2004;12(2):77–83. Available from: http://fm.mizar.org/2004-12/pdf12-2/
rsspace4.pdf.
[14] Ozawa T. Ascoli-Arzelà theorem. 2012;Available from: http://www.ozawa.phys.
waseda.ac.jp/pdf/Ascoli.pdf.

Mizar article information
Works in Progress
SEQFUNC2 Functional Sequence from a Domain to a Normed Vector Space
by Hiroshi Yamazaki
Summary: Deﬁnitions of functional sequences and basic operations on functional sequencesfrom a non empty set to a normed vector space, point and uniform convergence, limit offunctional sequence from a non empty set to the normed vector space, and facts about propertiesof the limit of functional sequences are proved.

COSP3 C(Ω) space and C0 (Ω) space
by Hiroshi Yamazaki and Yasunari Shidama
Summary: In this article, ﬁrst we give a deﬁnition of a functional space which is constructedfrom all continuous functions deﬁned on a compact topological space. We prove that thisfunctional space is a Banach spacea. Next, we give a deﬁnition of a function space whichis constructed from all continuous functions with bounded support. We also prove that thisfunction space is a normed space.

ASCORI Ascoli − Arzela′ s theorem
by Hiroshi Yamazaki and Yasunari Shidama
Summary: In this article, the Ascoli-Arzela’s theorem is formalized. First, we gave deﬁnitionsof equicontinuousness and equiboundedness of a set of continuous functions. Next,we formalized
the Ascoli-Arzela’s theorem by those deﬁntions , and proved this theorem.

MMA-WiP (2020), vol.2, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2020.2.1 - ISSN 2434-5458 (Online)

16/16