ファイナイト（有限）プロダクトメトリックスペース（計量付き空間）に対して、プロダクトメトリック（計量）によってインデュースト（誘導された）トポロジーは、構成要素メトリック（計量）たちによってインデュースト（誘導された）トポロジーたちのプロダクトトポロジーであることの記述/証明
話題
About: メトリックスペース（計量付き空間）
About: トポロジカルスペース（空間）
この記事の目次
開始コンテキスト
- 読者は、ファイナイト（有限）プロダクトメトリックスペース（計量付き空間）の定義を知っている。
- 読者は、メトリック（計量）によってインデュースト（誘導された）トポロジーの定義を知っている。
- 読者は、プロダクトトポロジーの定義を知っている。
- 読者は、任意のファイナイト（有限）プロダクトメトリックスペース（計量付き空間）および任意のオープンボール（開球）に対して、当該オープンボール（開球）内に包含されている何らかのオープンボール（開球）たちのプロダクトがあり、その（プロダクト）中にあるオープンボール（開球）が包含されているという命題を認めている。
- 読者は、オープン（開）であることのローカル基準を認めている。
ターゲットコンテキスト
- 読者は、任意のファイナイト（有限）プロダクトメトリックスペース（計量付き空間）に対して、当該プロダクトメトリック（計量）によってインデュースト（誘導された）トポロジーは、当該構成要素メトリック（計量）たちによってインデュースト（誘導された）トポロジーたちのプロダクトトポロジーであるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(J\): \(\in \{\text{ 全てのファイナイト（有限）インデックスセット（集合）たち }\}\)
\(\{M_j \vert j \in J\}\): \(M_j \in \{\text{ 全てのメトリックスペース（計量付き空間）たち }\}\)で、任意のメトリック（計量）\(dist_j\)を持つもの
\(\times_{j \in J} M_j\): \(= \text{ 当該ファイナイト（有限）プロダクトメトリックスペース（計量付き空間） }\)で、当該ファイナイト（有限）プロダクトメトリック（計量）\(dist\)を持つもの
\(O'\): \(= dist \text{ によってインデュースト（誘導された）トポロジー }\)
\(O\): \(= dist_j \text{ たちによってインデュースト（誘導された）トポロジーたち }\{O_j \vert j \in J\} \text{ のプロダクトトポロジー }\)
//
ステートメント（言明）たち:
\(O' = O\)
//
2: 証明
全体戦略: ステップ1: 任意の\(U' \in O'\)を取り、\(U' \in O\)であることを見る; ステップ2: 任意の\(U \in O\)を取り、\(U \in O'\)であることを見る。
ステップ1:
\(U' \in O'\)を任意のものとしよう。
\(u' \in U'\)を任意のものとしよう。
以下を満たすあるオープンボール（開球）\(B_{u', \epsilon} \subseteq \times_{j \in J} M_j\)、つまり、\(B_{u', \epsilon} \subseteq U'\)、がある、メトリック（計量）によってインデュースト（誘導された）トポロジーの定義によって。
\(\beta := \epsilon / \sqrt{\vert J \vert}\)に対して、\(\times_{j \in J} B_{u'^j, \beta} \subseteq B_{u', \epsilon}\)、任意のファイナイト（有限）プロダクトメトリックスペース（計量付き空間）および任意のオープンボール（開球）に対して、当該オープンボール（開球）内に包含されている何らかのオープンボール（開球）たちのプロダクトがあり、その（プロダクト）中にあるオープンボール（開球）が包含されているという命題によって。
しかし、各\(B_{u'^j, \beta} \subseteq M_j\)は、\(M_j\)に対する、\(dist_j\)によってインデュースト（誘導された）トポロジーにおいて、\(u'^j\)のあるオープンネイバーフッド（開近傍）である、そして、\(\times_{j \in J} B_{u'^j, \beta} \subseteq \times_{j \in J} M_j\)は、当該プロダクトトポロジーにおいて、\(u'\)のあるオープンネイバーフッド（開近傍）である。
\(\times_{j \in J} B_{u'^j, \beta} \subseteq B_{u', \epsilon} \subseteq U'\)であるから、\(U' \in O\)、オープン（開）であることのローカル基準によって。
ステップ2:
\(U \in O\)を任意のものとしよう。
\(u \in U\)を任意のものとしよう。
\(U = \cup_{j' \in J'} \times_{j \in J} U_{j, j'}\)、ここで、\(J'\)はアンカウンタブル（不可算）かもしれないインデックスセット（集合）であり、\(U_{j, j'} \subseteq M_j\)は\(dist_j\)によってインデュースト（誘導された）トポロジーにおいてオープン（開）である: プロダクトトポロジーの定義に対する"注"を参照のこと。
\(u \in \times_{j \in J} U_{j, j'}\)、ある\(j' \in J'\)に対して。
\(u^j \in U_{j, j'}\)、したがって、以下を満たすあるオープンボール（開球）\(B_{u^j, \epsilon_j} \subseteq M_j\)、つまり、\(B_{u^j, \epsilon_j} \subseteq U_{j, j'}\)、がある、メトリック（計量）によってインデュースト（誘導された）トポロジーの定義によって。
\(\epsilon = Min \{\epsilon_j \vert j \in J\}\)としよう。
\(B_{u^j, \epsilon} \subseteq U_{j, j'}\)および\(\times_{j \in J} B_{u^j, \epsilon} \subseteq \times_{j \in J} U_{j, j'}\)。
\(B_{u, \epsilon} \subseteq \times_{j \in J} B_{u^j, \epsilon}\)、任意のファイナイト（有限）プロダクトメトリックスペース（計量付き空間）および任意のオープンボール（開球）に対して、当該オープンボール（開球）内に包含されている何らかのオープンボール（開球）たちのプロダクトがあり、その（プロダクト）中にあるオープンボール（開球）が包含されているという命題によって。
したがって、\(B_{u, \epsilon} \subseteq \times_{j \in J} B_{u^j, \epsilon} \subseteq \times_{j \in J} U_{j, j'} \subseteq \cup_{j' \in J'} \times_{j \in J} U_{j, j'} = U\)。
したがって、\(U \in O'\)、メトリック（計量）によってインデュースト（誘導された）トポロジーの定義によって。
