距離空間の完備化（２）

C(X)/～ の距離をどう定義するか

C(X)とは、距離空間Xの基本列全体の集合のことで、
この記事は、 http://blogs.yahoo.co.jp/kafukanoochan/62700932.html 　Murakuさんの
問３：このときXの距離ρによりC(X)/～にも自然に距離が定義されることを示せ。
の答え？です。

内田伏一「集合と位相」ｐ150より、

C(X)/～ の距離の定義のストーリ：
C(X)は、距離空間Xの基本列全体の集合とする
１．まず、C(X)上の２つの元　点列（ｘn|n∈N）と（ｙn|n∈N）に対して、実数列（ρ(xn,yn)|n∈N）がｎ→∞で
　　収束すること　を示す。
２．よって、d(（ｘn|n∈N),（ｙn|n∈N）)＝Lim[n→∞]ρ(xn,yn)　として関数d：C(X)×C(X)→R　が定義できる。
３．二項関係を、C(X)上の２つの元（xn|n∈N）と（x'n|n∈N）に対して、d(（xn|n∈N),（x'n|n∈N）)＝０ 　　となる時、
　　（その時に限って）、（ｘn|n∈N）～（x'n|n∈N）という同値関係を定義する。
４．で、C(X)の元（ｘn|n∈N）を、C(X)/～ の１つの代表元[（ｘn|n∈N）]とし、
　　C(X)の元（ｙn|n∈N）を、C(X)/～ のもう１つの代表元[（ｙn|n∈N）]とする。
５．C(X)/～ をX~とし、関数d~ ：X~×X~→R　を、上記２つの代表元に対し、
　　d~([（ｘn|n∈N）],　[（ｙn|n∈N）])＝d(（ｘn|n∈N),（ｙn|n∈N）)　によって定義する。
したがって、
　　d~([（ｘn|n∈N）],　[（ｙn|n∈N）])＝Lim[n→∞]ρ(xn,yn)　
つまり、C(X)での距離ρは点列の関数で、商空間C(X)/～ の距離d~は代表元[点列]の関数という自然な関係
になっています。