Mechanized Mathematics and Its Applications, Works in Progress

Ascoli-Arzelà’s Theorem (Miyajima and Yamazaki)

Regular Paper

Ascoli-Arzelà の定理の形式化について
On the Formalization of Ascoli-Arzelà’s Theorem
宮島 啓一 1,* 山崎 浩 2
Keiichi Miyajima1 , Hiroshi Yamazaki2
1 茨城大学工学部, 日立市
1 Ibaraki University College of Engineering, Hitachi, Ibaraki, Japan
2 長野県工科短期大学校, 上田市
2 Nagano Prefectural Institute of Technology, Ueda, Nagano, Japan* keiichi.miyajima.fmath@vc.ibaraki.ac.jp
Proof checked by Mizar Version: 8.1.11 and MML Version: 5.68.1412
Received: December 21, 2021, Accepted: May 16, 2022.

Abstract
In this article we formalize the Ascoli-Arzelà’s theorem in Mizar. First, we gave
definitions of equicontinuousness and equiboundedness of a set of continuous functions.
Next, we formalized the Ascoli-Arzelà’s theorem using those definitions, and proved thistheorem.

1

はじめにAscoli–Arzelà の定理は, 連続関数の族の一様位相に関する相対コンパクト性の必要十分条件を与える定理である [1] [2] [3] [4] [5]．有界閉区間上の実数値連続関数の集合の元の任意の列が一様収束する部分列を持つ (点列コンパクト sequentially compact である) ための必要十分条件が同程度連続性の概念を用いて Ascoli と Arzelà によって証明された. この定理は常微分方程式論におけるペアノの存在定理など多くの定理の証明に用いられてきた. Fréchet により定義域のコンパクト距離空間である実数値連続関数の族への一般化がなされた後, 現在は定義域はコンパクトなハウスドルフ空間, 値域は任意の距離空間にまで拡張されている.
筆者らは距離空間から生成されるコンパクトな位相空間からノルム空間から生成される位相線形空間への連続関数の集合についての一様位相に関する相対コンパクト性の必要十分条件に関しての Ascoli–Arzelà の定理とその証明を形式化した. 値域を一般的な距

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

1/15

Mechanized Mathematics and Its Applications, Works in Progress

Ascoli-Arzelà’s Theorem (Miyajima and Yamazaki)

離空間ではなく, ノルム空間から生成される位相線形空間としたのは筆者らのニューラル
ネットの形式化についての報告 [6] で述べたように, 相対コンパクト空間に含まれる関数の値の代数的演算やノルムを扱う場合の利便性を考慮したためである．本稿ではこれについて報告する. その形式化は Mizar Mathematical Library (以下 MML) に ASCOLI [7]として収録されている. 前回の報告 [8] で, 一部その概要に言及したが, その後, 内容の修正その他を行ったので今回, 改めてその詳細を報告する.

2

形式化の概要筆者らの形式化の最終的な結果は以下の通りである.

Listing 1. ASCOLI:23
theorem :: ASCOLI: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 );S は距離空間 M から生成されるコンパクトな位相空間であり, T はノルム空間から生成される位相線形空間である. この位相線形空間については [8] で解説したので, 詳しくはこれを参照されたい. T はノルム空間であると同時に位相空間である.

T には完備性を仮定する.
R NormSpace of ContinuousFunctions(S, T)
は S から T への連続写像全体の集合が造るノルム空間であり,T の完備性からこの空間も完備である. 以後, このノルム空間を MML の記述を引用する場合を除き L(S, T) で表す.

Funcs(the carrier of M, the carrier of T)
は M の元の集合から T の元の集合への写像全部の集合を表す. MML では [9] と同様に集合論を基礎とする形式化を行っている．群や環，位相空間など数学的な概念は集合と写像などから構成される構造体 (struct) と，それの特定の性質を表す属性 (attribute) を定義することによって形式化される．
距離空間の構造体は METRIC 1 [10] で以下のように形式化されている．

Listing 2. METRIC 1
deﬁnition
struct(1−sorted) MetrStruct(# carrier −> set, distance −>Function of [:the carrier,the carrier:],REAL #);end;

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

2/15

Mechanized Mathematics and Its Applications, Works in Progress

Ascoli-Arzelà’s Theorem (Miyajima and Yamazaki)

carrier は M の点全ての集合を表し, distance は M の任意の 2 点間の距離を与える[: the carrier, the carrier :] から R への写像である. [: the carrier, the carrier :] はcarrier の 2 重直積である.
この構造体に距離 distance についての以下の対称性や三角不等式などの属性が定義される.

Listing 3. METRIC 1:def 2 ∼ def 5
deﬁnition
let A be set;let f be PartFunc of [:A,A:], REAL;
attr f is Reﬂexive means :: METRIC 1:def 2
for a being Element of A holds f.(a,a) = 0;
attr f is discerning means :: METRIC 1:def 3
for a, b being Element of A st f.(a,b) = 0 holds a = b;
attr f is symmetric means :: METRIC 1:def 4
for a, b being Element of A holds f.(a,b) = f.(b,a);
attr f is triangle means :: METRIC 1:def 5
for a, b, c being Element of A holds f.(a,c) <= f.(a,b) + f.(b,c);end;

距離空間は構造体 METRIC 1 で上記の属性を持った変数型 MetrSpace として以下のように導入されている.

Listing 4. METRIC 1
deﬁnitionmode MetrSpace is Reﬂexive discerning symmetric triangle MetrStruct;end;

位相空間 TopSpace や位相線形空間 NormedLinearTopSpace も同様に構造体 (struct)と，それの特定の性質を表す属性 (attribute) を定義することによって形式化されている.

Cl(F) は位相空間 S の部分集合 F の閉包である．PRE TOPC [11] で以下のように定義されている.

Listing 5. PRE TOPC:def 7
deﬁnition
let S be TopStruct, F be Subset of S;
func Cl F −> Subset of S means :: PRE TOPC:def 7
for p being set st p in the carrier of S holds p in it
iﬀ for G being Subset of S st G is open holds p in G implies F meets G;
projectivity;end;

構造体とその構成要素である carrier は厳密に区別される.
以後, 表現の煩さを避けるため距離空間 M の点の集合 the carrier of M から位相空間 T の点の集合 the carrier of M への写像 を距離空間 M から位相空間 T への写像と表現する.

G が距離空間 M からノルム空間 T への写像全部の集合
Funcs(the carrier of M, the carrier of T)の部分集合とするとき, 同程度有界性 equibounded と同程度連続性 equicontinuous [1][2] [4] [5] を以下のように定義する.

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

3/15

Mechanized Mathematics and Its Applications, Works in Progress

Ascoli-Arzelà’s Theorem (Miyajima and Yamazaki)

Listing 6. ASCORI:def 2 def 4
deﬁnition
let M be non empty MetrSpace ,T be RealNormSpace;
let G be Subset of Funcs(the carrier of M,the carrier of T);
attr G is equibounded means :: ASCORI:def 2
ex K be Real st for f be Function of the carrier of M,the carrier of T
st f in G holds for x be Element of M holds ||.f.x.|| <= K ;end;
deﬁnition
let M be non empty MetrSpace,T be RealNormSpace;
let G be Subset of Funcs(the carrier of S,the carrier of T);
pred G 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 M,the carrier of T
st f in G holds for x1,x2 be Point of M st dist(x1,x2) < d holds ||.f.x1−f.x2.|| < e;end;

冒頭に示した 定理 ASCOLI:23 は同程度有界性 equibounded と同程度連続性

equicontinuous がノルム空間から生成される位相線形空間への連続関数の集合 G が一様位相に関する相対コンパクトであることの必要十分条件であることを表している. 次章
以降, これについて解説する.

3

補題と定義
前章で述べたように MML では位相空間など数学的な概念は集合と写像などから構成される構造体 (struct) と，それの特定の性質を表す属性 (attribute) を定義することによって形式化される．構造体には基となる構造を拡張した構造など上位，下位の階層関係をもつものもあるが，数学的には上位, 下位の階層関係にあっても開発段階にある現状のMML ではそのように関係付けられていないものがある. その場合, 一方の構造体に関して形式化され MML に収録されているものであっても, 数学的には階層関係があるのにも関わらず, そのまま引用できないものがある.

Mizar は変数の型や構造の違いを厳密に区別する. これは, 人手に依らず, 計算機の記号列の処理によって機械的, かつ厳密に定理証明の検証を行うシステムの目的から止むを得ないことでもある.
例えば, 計算機による数値計算のプログラムで, 同じ演算子であっても変数型が実数と整数で, 小数点以下を扱うか扱わないかで, 結果が異なる場合があり, 関数など使用する引数の型が異なれば, エラーメッセージを出力するなどと同じである.
閉包は位相空間で定義され, 距離空間で未定義であるため, 利便性のため以下のように距離空間での閉包を定義した.

Listing 7. ASCOLI:def 1
deﬁnition
let X be non empty MetrSpace, Y be Subset of X;
func Cl Y −> Subset of X means :: ASCOLI:def 1
ex Z be Subset of TopSpaceMetr X st Z = Y & it = Cl Z;
end;theorem :: ASCOLI:1
for X be RealNormSpace, Y be Subset of X, Z be Subset of MetricSpaceNorm X

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

4/15

Mechanized Mathematics and Its Applications, Works in Progress

Ascoli-Arzelà’s Theorem (Miyajima and Yamazaki)

st Y = Z holds Cl(Y) = Cl(Z);registration
let X be non empty MetrSpace;let H be non empty Subset of X;
cluster Cl(H) −> non empty;
end;

また, 数学的にはノルム空間は, 距離空間であり, 距離空間は位相空間である．一方, ノ
ルム空間は線形空間であり, 位相線形空間でもある．報告で解説したように C0SP3 [12]にはこのノルム空間を基にし位相線形空間の構造を併せ持つ NormedLinearTopSpaceを導入したが, さらに利便性を高めるため関数の連続性に関しての以下の補題を用意した.

Listing 8. ASCOLI:3
theorem :: ASCOLI:3
for S be non empty TopSpace,T be NormedLinearTopSpace,f be Function of S,T, x be Point of S holds( f is continuous at x iﬀ for e be Real st 0 < e holds ex H being Subset of S st
( H is open & x in H & for y be Point of S st y in H holds ||.f.x−f.y.|| < e ) );theorem :: ASCOLI:4
for S be non empty MetrSpace, V be non empty compact TopSpace,
T be NormedLinearTopSpace, f be Function of V,Tst V = TopSpaceMetr(S)holds
f is continuous
iﬀ for e be Real st 0 < e holds ex d be Real st 0 < d& for x1,x2 be Point of S st dist(x1,x2) < d holds ||.f/.x1−f/.x2.|| < e;

距離空間には TBSP 1 [13] で点列の収束 convergence, 全有界性 totally boundedや完備性 complete などの概念が定義されている．

Listing 9. TBSP 1
deﬁnition
let N;
attr N is totally bounded means :: TBSP 1:def 1
for r st r>0 ex G st G is ﬁnite & the carrier of N = union G & for C st C in G ex w st C = Ball(w,r);
end;
reserve S1 for sequence of M,
S2 for sequence of N;
theorem :: TBSP 1:4
f is sequence of N iﬀ dom f = NAT & for n holds f.n is Element of N;
deﬁnition
let N,S2;
attr S2 is convergent means :: TBSP 1:def 2
ex x being Element of N st for r st r>0
ex n st for m st n<=m holds dist(S2.m,x)<r;
end;
deﬁnition
let M,S1;
assumeS1 is convergent;func lim S1 −> Element of M means :: TBSP 1:def 3
for r st r>0 ex n st for m st m>=n holds dist(S1.m,it)<r;
end;
deﬁnition
let N,S2;
attr S2 is Cauchy means :: TBSP 1:def 4

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

5/15

Mechanized Mathematics and Its Applications, Works in Progress

Ascoli-Arzelà’s Theorem (Miyajima and Yamazaki)

for r st r>0 ex p st for n,m st p<=n & p<=m holds dist(S2.n,S2.m)<r;
end;
deﬁnition
let N;
attr N is complete means :: TBSP 1:def 5
for S2 st S2 is Cauchy holds S2 is convergent;end;

ノルム空間 T は 周知のように距離 distance を

distance.(x, y) = ||.x − y.||で定義すれば距離空間にもなる.NORMSP 2 [14] でこれを MetricSpaceNorm T で表し定義している.

MetricSpaceNorm T の距離の作り方から T の完備性は T から生成される距離空間 MetricSpaceNorm T が完備であることと同値であり, 以下の命題が成り立つ.

Listing 10. ASCOLI:7
theorem :: ASCOLI:7
for T be RealNormSpace, H be non empty Subset of MetricSpaceNorm T
st T is complete holds (MetricSpaceNorm T) | Cl(H) is complete;

また全有界性 totally bounded と閉包の定義から以下も成り立っている.

Listing 11. ASCOLI:8
theorem :: ASCOLI:8
for T be RealNormSpace,
H be non empty Subset of MetricSpaceNorm T
holds(MetricSpaceNorm T) | H is totally bounded
iﬀ (MetricSpaceNorm T) | Cl(H) is totally bounded;

以上の準備のもとに, 完備なノルム空間 T から生成される完備距離空間

MetricSpaceNorm T について, その部分集合 H の全有界性 totally bounded, 閉包
Cl(H) の点列コンパクト性 sequentially compact, 相対コンパクト性が何れも同値であること示す以下の命題を形式化した.

Listing 12. ASCOLI:10
theorem :: ASCOLI:10
for Z be RealNormSpace, F be non empty Subset of Z,
H be non empty Subset of MetricSpaceNorm Z,
T being Subset of TopSpaceNorm Z st Z is complete & H = F & H = T
holds( (MetricSpaceNorm Z) | H is
totally boundediﬀ Cl(H) is sequentially compact) &( (MetricSpaceNorm Z) | H is
totally boundediﬀ (MetricSpaceNorm Z) | Cl(H) is compact) &( (MetricSpaceNorm Z) | H is
totally boundediﬀ Cl(F) is compact) &( (MetricSpaceNorm Z) | H is
totally boundediﬀ Cl(T) is compact);

4

Ascoli–Arzelà の定理
周知のように距離空間 M は開球 Ball を用いて開集合の族を定義でき, 位相空間を構成できる． PCOMPS 1 [15] にはこれを以下のように形式化している.

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

6/15

Mechanized Mathematics and Its Applications, Works in Progress

Ascoli-Arzelà’s Theorem (Miyajima and Yamazaki)

Listing 13. PCOMPS 1
deﬁnition
let M be MetrStruct;
func Family open set(M) −> Subset−Family of M means :: PCOMPS 1:def 4
for V holds V in it iﬀ for x st x in V holds ex r st r>0 & Ball(x,r) c= V;
end;theorem :: PCOMPS 1:33
TopStruct (#the carrier of M,Family open set(M)#) is TopSpace;deﬁnition
let M be MetrStruct;
func TopSpaceMetr M −> TopStruct equals :: PCOMPS 1:def 5
TopStruct (#the carrier of M, Family open set(M)#);
end;

Family open set(M) が開球による開集合の属であり, TopSpaceMetr M がそれによって構成される位相空間である.
さらに本稿の形式化では以下の命題を用いている.

Listing 14. TBSP 1:8，TBSP 1:9
theorem :: TBSP 1:8
TopSpaceMetr(T) is compact implies T is complete;theorem :: TBSP 1:9
N is Reﬂexive triangle & TopSpaceMetr(N)is compact implies N is totally bounded;

これにより, 距離空間 M が完備 complete ならば M から構成される．
位相空間 TopSpaceMetr M も完備であり, TopSpaceMetr M が compact であれば,M は全有界 totally bounded である.
これと, 前章で述べた補題を用いて Ascoli–Arzelà の定理の形式化を以下の順に行った.
以下,T の完備性を仮定する.

T の完備性により,S から T への連続写像全体の集合が造るノルム空間 L(S, T) は完備である. このノルム空間から構成される距離空間

MetricSpaceNorm L(S, T) も完備である. H がこの空間の部分集合のとき,H の閉包Cl(H) の列コンパクト性 sequentially compact と全有界性 totally bounded の同値性についての以下の命題とその証明を形式化した.

Listing 15. ASCOLI:11，ASCOLI:12
theorem :: ASCOLI:11
for S be non empty compact TopSpace,T be NormedLinearTopSpacest T is complete holds
for H be non empty Subset of(MetricSpaceNorm R NormSpace of ContinuousFunctions(S,T))
holds
Cl(H) is sequentially compact iﬀ(MetricSpaceNorm R NormSpace of ContinuousFunctions(S,T) )| H is totally bounded;theorem :: ASCOLI:12
for S be non empty compact TopSpace,T be NormedLinearTopSpacest T is complete holds
for F be non empty Subset of
R NormSpace of ContinuousFunctions(S,T),
H be non empty Subset of
MetricSpaceNorm R NormSpace of ContinuousFunctions(S,T) st
H = F holds Cl(F) is compact iﬀ(MetricSpaceNorm R NormSpace of ContinuousFunctions(S,T) )| H is totally bounded;

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

7/15

Mechanized Mathematics and Its Applications, Works in Progress

Ascoli-Arzelà’s Theorem (Miyajima and Yamazaki)

MetricSpaceNorm L(S, T) の部分集合 G が全有界 totally bounded なら G の元の有限集合 L と半径 1 の開球の有限集合 {B(h, 1) : h ∈ L} が存在して∪G⊆

B(h, 1)h∈Lとなる. ここで

d = max{||h|| : h ∈ L}とおくと任意の f ∈ G, x ∈ S について,

∪

f ∈G⊆

B(h, 1)h∈Lから||h − f || ≤ 1となる h ∈ L が存在する．

||h − f || ≤ 1 から任意の x ∈ S について,||f (x) − h(x)|| ≤ 1
であり,||f (x)|| ≤ ||h(x)|| + ||f (x) − h(x)|| ≤ d + 1が成り立つことから，前章の定義により G は同程度有界 equibounded である.
次に, 任意の正の実数 0 < ϵ について上と同様に G の元の有限集合 L と半径 ϵ/3 の開球の有限集合 {B(h, ϵ/3) : h ∈ L} をG⊆∪

B(h, ϵ/3)h∈Lとなるように選ぶ.
各 h ∈ L ⊆ G は MetricSpaceNorm L(S, T) に属する連続写像であり, 特に S のcompact 性から一様連続であるから 0 < dh が存在して, S の任意の 2 つの元 x, y ∈ S について dist(x, y) < dh なら||h(x) − h(y)|| < ϵ/3が成り立っている.(前章の命題 ASCOLI:4 そのものである)
そこで

d = min{dh : h ∈ L}とおけば, G の任意の元 f ∈ G について

f ∈G⊆

∪

B(h, ϵ/3)h∈Lから||h − f || < ϵ/3となる h ∈ L が存在し

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

8/15

Mechanized Mathematics and Its Applications, Works in Progress

Ascoli-Arzelà’s Theorem (Miyajima and Yamazaki)

S の任意の 2 つの元 x, y ∈ S について dist(x, y) < d なら dist(x, y) < dh でもあるから||f (x) − f (y)|| ≤ ||f (x) − h(x)|| + ||h(x) − h(y)|| + ||h(y) − f (y)|| < ϵ/3 + ϵ/3 + ϵ/3 = ϵが成り立つことから前章の定義により G は同程度連続 equicontinuous である. 以上を形式化したのが次の命題である.

Listing 16. ASCOLI:13
theorem :: ASCOLI:13
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace
st S = TopSpaceMetr(M) & T is complete holds
for G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of
MetricSpaceNorm R NormSpace of ContinuousFunctions(S,T) st
G = H & (MetricSpaceNorm R NormSpace of ContinuousFunctions(S,T))| H is totally bounded holds
G is equibounded & G is equicontinuous;

特に, 上記の命題で,T が有限次元空間ならば下に述べる命題 ASCOLI:16 の系として,同程度有界性 equibounded , 連続性 equicontinuous は全有界性 totally bounded の必要十分条件になり以下の命題が成り立つ. [6]Listing 17. NEURONS1:26
theorem :: NEURONS1:26
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace
st S = TopSpaceMetr(M) & T is complete & T is ﬁnite−dimensional& dim (T) <> 0 holds
for G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of(MetricSpaceNorm R NormSpace of ContinuousFunctions(S,T))
st G = H
holds(MetricSpaceNorm R NormSpace of ContinuousFunctions(S,T))| H is totally bounded iﬀ G is equibounded & G is equicontinuous;

また, 完備な距離空間 MetricSpaceNorm L(S, T) の部分集合の全有界性 totally boundedと相対 compact 性は同値なので以下の命題が成り立つ

Listing 18. NEURONS1:28
theorem :: NEURONS1:28
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace
st S = TopSpaceMetr(M) & T is complete & T is ﬁnite−dimensional& dim (T) <> 0 holds
for G be Subset of Funcs(the carrier of M, the carrier of T),
F be non empty Subset of R NormSpace of ContinuousFunctions(S,T)
st G = Fholds Cl(F) is compact iﬀ G is equibounded & G is equicontinuous;

しかしながら, 本稿では T が有限次元空間という制約を課していない. 代わりに以下の必要十分条件 ASCOLI:16 の命題が成り立つ. この命題が本稿報告の形式化の中心的命題である. 以下のその証明の概略を述べる.

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

9/15

Mechanized Mathematics and Its Applications, Works in Progress

Ascoli-Arzelà’s Theorem (Miyajima and Yamazaki)

MetricSpaceNorm L(S, T) の部分集合 G が全有界 totally bounded なら ASCOLI:13 から G は同程度連続 equicontinuous である.
次に x ∈ S を S の任意元 とする. 任意の正の実数 0 < ϵ について上と同様に G の元の有限集合 L と半径 ϵ の開球の有限集合 {B(h, ϵ) : h ∈ L} をG⊆∪

B(h, ϵ)h∈Lとなるように選ぶ.
これを用いて T の開球の有限集合{B(h(x), ϵ) : h ∈ L}をつくると,{f (x) : f ∈ G} ⊆∪∪B(h.x, ϵ)h∈Lが成り立っている. T の部分集合 {f (x) : f ∈ G} は全有界 totally bounded であり, その閉包は compact である.
逆に G が同程度連続 equicontinuous であり,S の任意の元 x について {f (x) : f ∈ G}の閉包が compact であるとする.
任意の正の実数 0 < ϵ について, G の同程度連続性から正の実数 0 < d が存在し, S の
任意の 2 元 x, y ∈ S についてdist(x, y) < d ならば ||f (x) − f (y)|| < ϵ/8(∀f ∈ G)

(1)が成り立っている
そこで S の開球の集合 {Ball(x, d) : x ∈ S} をつくると∪S⊆

Ball(x, d)x∈Sであるから S の開被覆である.

S は compact であるから S の元の有限列 {xi }1≤i≤n が存在して∪S⊆

Ball(xi , d)1≤i≤nが成り立つ.
この {xi }1≤i≤n を用いて各 i について {f (xi ) : f ∈ G} の閉包 Cl{f (xi ) : f ∈ G} をその要素とする T の部分集合の有限列{Cl{f (xi ) : f ∈ G}}1≤i≤nをつくる. 各 Cl{f (xi ) : f ∈ G} は仮定により compact であるからこの部分集合列の和B=∪

Cl{f (xi ) : f ∈ G}

1≤i≤n

も compact 集合である.

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

10/15

Mechanized Mathematics and Its Applications, Works in Progress

Ascoli-Arzelà’s Theorem (Miyajima and Yamazaki)

この T の compact 部分集合 B を覆う B の元の有限列とその各点を中心とする半径ϵ/8 開球の有限列{wj } 1≤j≤m , {Ball(wj , ϵ/8)} 1≤j≤m ,∪Ball(wj , ϵ/8)
B⊆

(2)

1≤j≤m

を構成する. この開球の有限列を用いて以下のようにして mn 個の G を覆う開球を構成す
る. 自然数の集合 {i ∈ N : 1 ≤ i ≤ n} から集合 {j ∈ N : 1 ≤ j ≤ m} への写像全体の集合{σ : {i ∈ N : 1 ≤ i ≤ n} → {j ∈ N : 1 ≤ j ≤ m}}
を P で表すと, この有限集合の要素の数は mn 個である. σ ∈ P に対して G の部分集合を対応させる写像 K

K(σ) = {f ∈ G : (∀i : 1 ≤ i ≤ n)(f (xi ) ∈ Ball(wσi , ϵ/8)}を導入する.
任意の σ ∈ P に対して G の任意の 2 元 f, g について f, g ∈ K(σ) ならば

f (xi ), g(xi ) ∈ Ball(wσi , ϵ/8)(∀i : 1 ≤ i ≤ n)から||f (xi ) − g(xi )|| ≤ ||f (xi ) − wσi || + ||wσi − g(xi )|| < ϵ/8 + ϵ/8 = ϵ/2(∀i : 1 ≤ i ≤ n)を得る.
そこで x ∈ S を任意に選ぶと,S⊆∪

Ball(xi , d)1≤i≤nから 1 ≤ i ≤ n が存在して x ∈ Ball(xi , d) となり, これから dist(xi , x) < d である. (1)式から||f (xi ) − f (x)|| < ϵ/8, ||g(xi ) − g(x)|| < ϵ/8であり,||f (x) − g(x)|| ≤ ||f (x) − f (xi )|| + ||f (xi ) − g(xi )|| + ||g(xi ) − g(x)||< ϵ/8 + ϵ/8 + ϵ/8
< ϵ/2
結局

||f − g|| < ϵ/2(∀f, g ∈ K(σ))(3)

G の任意の元 f について (2) 式 から任意の 1 ≤ i ≤ n に対して 1 ≤ j ≤ m が存在して
f (xi ) ∈ Ball(wj , ϵ/8)

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

11/15

Mechanized Mathematics and Its Applications, Works in Progress

Ascoli-Arzelà’s Theorem (Miyajima and Yamazaki)

従って,G の任意の元 f について σ ∈ P が存在してf ∈ K(σ)(4)

ここで, 任意の σ ∈ P について, K(σ) ̸= ϕ ならば Fσ ∈ K(σ) である Fσ ∈ G が存在する.

g ∈ K(σ) である任意の g ∈ G については (3) 式 から||Fσ − g|| < ϵ/2が得られ

g ∈ Ball(Fσ , ϵ)
従ってK(σ) ⊆ Ball(Fσ , ϵ)(5)

G の開球の有限列 {Ball(Fσ , ϵ)}σ∈P は (5) 式 から∪G⊆

Ball(Fσ , ϵ)σ∈P

よって G は全有界 totally bounded である.
以上から次の命題の形式証明を得た.

Listing 19. ASCOLI:16
theorem :: ASCOLI:16
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace,
G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of
MetricSpaceNorm R NormSpace of ContinuousFunctions(S,T)
st S = TopSpaceMetr(M) & T is complete & G = H holds(MetricSpaceNorm R NormSpace of ContinuousFunctions(S,T))| H is totally boundediﬀ
G is equicontinuous &for x be Point of S,
Hx be non empty Subset of MetricSpaceNorm T
st Hx = {f.x where f is Function of S,T :f in H }holds (MetricSpaceNorm T) | Cl(Hx) is compact;

これは完備ノルム空間 L(S, T) から生成される完備距離空間 MetricSpaceNorm L(S, T)の部分集合の全有界性 totally bounded と同程度連続性 equicontinuous,

MetricSpaceNorm L(S, T) に属する関数の各 S の点 x に対する値の集合の閉包の
compact 性が同値であること示している.
さらに完備距離空間の部分集合の全有界性 totally bounded と閉包の点列コンパク
ト性，相対コンパクト性は何れも同値であるから以下の命題が成り立つ.

Listing 20. ASCOLI:17，ASCOLI:18
theorem :: ASCOLI:17
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace,
G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of(MetricSpaceNorm R NormSpace of ContinuousFunctions(S,T))
st S = TopSpaceMetr(M) & T is complete & G = H
holds

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

12/15

Mechanized Mathematics and Its Applications, Works in Progress

Ascoli-Arzelà’s Theorem (Miyajima and Yamazaki)

Cl(H) is sequentially compact
iﬀ G is equicontinuous&
for x be Point of S, Hx be non empty Subset of MetricSpaceNorm T
st Hx = {f.x where f is Function of S,T :f in H }holds (MetricSpaceNorm T) | Cl(Hx) is compact;
theorem :: ASCOLI: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;

また, 証明の簡潔化に必要な補助的な命題として T の compact 性 が TopSpaceNorm Tの compact 性 と同値であること, T の compact 性 から TopSpaceNorm T の完備性

complete が従うことを表す以下の命題とその証明を形式化した.
Listing 21. ASCOLI:20 ∼ ASCOLI:22
theorem :: ASCOLI:20
for T be NormedLinearTopSpace holds
T is compact iﬀ TopSpaceNorm T is compact;
theorem :: ASCOLI:21
for T be NormedLinearTopSpace, X be set holds
X is compact Subset of T iﬀ X is compact Subset of TopSpaceNorm T;
theorem :: ASCOLI:22
for T be NormedLinearTopSpace st T is compact holds T is complete;

以上の準備のもとに最後に本稿の目的である定理 ASCOLI:23 の証明を形式化した.

Listing 22. ASCOLI:23
theorem :: ASCOLI: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 );5

まとめ
本稿では距離空間から生成されるコンパクトな位相空間からノルム空間から生成される位相線形空間への連続関数の集合についての一様位相に関する相対コンパクト性の必MMA-WiP (2022), vol.4, no.4 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.4 - ISSN 2434-5458 (Online)

13/15

Mechanized Mathematics and Its Applications, Works in Progress

Ascoli-Arzelà’s Theorem (Miyajima and Yamazaki)

要十分条件に関しての Ascoli–Arzelà の定理とその証明の形式化を報告した. 関数の値域を一般的な距離空間ではなく, ノルム空間から生成される位相線形空間としたのは筆者らのニューラルネットの形式化についての報告 [6] で述べたように, 相対コンパクト空間に含まれる関数の値の代数的演算やノルムを扱うためである．今後, この形式化を用いて,ニューラルネットによる非線形関数の近似定理の形式化を行う.

参考文献[1] Yoshida K. Functional Analysis. Springer-Verlag; 1980.
[2] Read M, Simon B.

Functional Analysis (Methods of Modern Mathematical

Physics). Academic Press; 1980.
[3] Lang S. Real and Functional Analysis (Texts in Mathematics). Springer-Verlag;
1993.
[4] Matsuzaka K. Sets and Topology (Introduction to Mathematics). IwanamiShoten;
2000.
[5] Ozawa T. Ascoli-Arzelà theorem. 2012;Available from: http://www.ozawa.phys.
waseda.ac.jp/pdf/Ascoli.pdf.
[6] Yamazaki H, Shidama Y. On the Formalizations for Multilayer Perceptron. MMAWiP (2021). 2021;3:1–12.
[7] Yamazaki H, Miyajima K, Shidama Y. Ascoli-Arzela’s Theorem. Formalized Mathematics. 2021;29(2):83–91.
[8] Shidama Y. On the Formalizations for Functional Spaces of Continuous Functions.
MMA-WiP (2020). 2020;1:1–16.
[9] Bourbaki N. Elements de Mathematique. vol. Topologie Generale. troisieme ed.
HERMANN; 1960.
[10] Kanas S, Lecko A, Startek M.
1990;1(3):607–610.

Metric Spaces.

Available from:

Formalized Mathematics.

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

metric_1.pdf.
[11] Padlewska B, Darmochwal A. Topological Spaces and Continuous Functions. Formalized Mathematics. 1990;1(1):223–230. Available from: http://fm.mizar.org/
1990-1/pdf1-1/pre_topc.pdf.
[12] Yamazaki H, Miyajima K, Shidama Y. Functional Space Consisted by Continuous
Functions on Topological Space. Formalized Mathematics. 2021;29(1):49–62.
[13] de la Cruz A. Totally Bounded Metric Spaces. Formalized Mathematics.
1991;2(4):559–562.
Available from: http://fm.mizar.org/1991-2/pdf2-4/
tbsp_1.pdf.

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

14/15

Mechanized Mathematics and Its Applications, Works in Progress

Ascoli-Arzelà’s Theorem (Miyajima and Yamazaki)[14] Endou N, Shidama Y, Okamura K. Baire’s Category Theorem and Some Spaces
Generated from Real Normed Space. Formalized Mathematics. 2006;14(4):213–219.
[15] Borys L.

Paracompact and Metrizable Spaces.

1991;2(4):481–485.

Available from:

Formalized Mathematics.

http://fm.mizar.org/1991-2/pdf2-4/

pcomps_1.pdf.

Mizar article information
Works in Progress
ASCOLI

Ascoli-Arzelà s Theorem
by Hiroshi Yamazaki,Keiichi Miyajima and Yasunari Shidama
Summary: . In this article we formalize the Ascoli-Arzelà s theorem in Mizar . First, we gave
deﬁnitions of equicontinuousness and equiboundedness of a set of continuous functions. Next,
we formalized the Ascoli-Arzelà s theorem using those deﬁnitions, and proved this theorem.

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

15/15