トポロジカルスペース（空間）マイナス任意のポイントからファイナイト（有限）-ディメンショナル（次元）リアル（実）ベクトルたちスペース（空間）でカノニカル（正典）トポロジーを持つものの中へのマップ（写像）に対して、マップ（写像）の、ポイントに関するコンバージェンス（収束ポイント）は存在する、もしも、コンポーネントマップ（写像）たちのポイントに関するコンバージェンス（収束ポイント）たちが存在する場合、そしてその場合に限って、そして、その場合、コンバージェンス（収束ポイント）はコンバージェンス（収束ポイント）たちで表わされることの記述/証明
話題
About: トポロジカルスペース（空間）
この記事の目次
開始コンテキスト
ターゲットコンテキスト
- 読者は、任意のトポロジカルスペース（空間）マイナス任意のポイントから任意のファイナイト（有限）-ディメンショナル（次元）リアル（実）ベクトルたちスペース（空間）でカノニカル（正典）トポロジーを持つものの中への任意のマップ（写像）に対して、当該マップ（写像）の、当該ポイントに関するコンバージェンス（収束ポイント）は存在する、もしも、当該コンポーネントマップ（写像）たち（任意のベーシス（基底）に関して）の当該ポイントに関するコンバージェンス（収束ポイント）たちが存在する場合、そしてその場合に限って、そして、その場合、当該コンバージェンス（収束ポイント）は当該コンバージェンス（収束ポイント）たちで表わされるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(T\): \(\in \{\text{ 全てのトポロジカルスペース（空間）たち }\}\)
\(V\): \(\in \{\text{ 全ての } d \text{ -ディメンショナル（次元） } \mathbb{R} \text{ ベクトルたちスペース（空間）たち }\}\)で、カノニカル（正典）トポロジーを持つもの
\(B\): \(\in \{V \text{ に対する全てのベーシス（基底）たち }\}\), \(= \{b_1, .., b_d\}\)
\(t\): \(\in T\)
\(f\): \(: T \setminus \{t\} \to V, t' \mapsto f^j (t') b_j\)
//
ステートメント（言明）たち:
(
\(\exists lim_{t' \to t} f (t')\)
\(\iff\)
\(\forall j \in \{1, ..., d\} (\exists lim_{t' \to t} f^j (t'))\)
)
\(\implies\)
\(lim_{t' \to t} f (t') = lim_{t' \to t} f^j (t') b_j\)
//
2: 証明
全体戦略: ステップ1: \(lim_{t' \to t} f (t')\)が存在すると仮定し、それを\(v = v^j b_j\)と表わす; ステップ2: \(lim_{t' \to t} f^j (t')\)が存在し\(v^j\)に等しいことを見る; ステップ3: \(lim_{t' \to t} f^j (t')\)が存在すると仮定し、それを\(v^j\)と表わす; ステップ4: \(lim_{t' \to t} f (t')\)が存在し\(v^j b_j\)に等しいことを見る。
ステップ0:
\(V\)はハウスドルフであることに留意する。
\(lim_{t' \to t} f (t')\)の存在を仮定することも\(lim_{t' \to t} f^j (t')\)の存在を仮定することも、\(\{t\} \subseteq T\)はオープン（開）でないことを含意する、なぜなら、そうでなければ、コンバージェンス（収束ポイント）たちはユニークでないことになる: トポロジカルスペース（空間）マイナスポイントからトポロジカルスペース（空間）の中へのマップ（写像）のポイントに関するコンバージェンス（収束ポイント）の定義に対する"注"を参照のこと。
したがって、コンバージェンス（収束ポイント）たちのユニーク性について心配する必要はない。
ステップ1:
\(lim_{t' \to t} f (t')\)は存在すると仮定し、それを\(v = v^j b_j\)と表わそう。
ステップ2:
\(lim_{t' \to t} f^j (t')\)は存在し\(v^j\)に等しいことを見よう。
\(v\)の各ネイバーフッド（近傍）\(N_v \subseteq V\)に対して、以下を満たすオープンネイバーフッド（開近傍）\(B_{v, \epsilon} \subseteq V\)、つまり、\(B_{v, \epsilon} \subseteq N_v\)、がある、カノニカル（正典）トポロジーの定義によって: \(B_{v, \epsilon}\)が意味するのは、\(\mathbb{R}^d\)の対応するサブセット（部分集合）が\(\epsilon\)-'オープンボール（開球）'であること。
\(t\)の以下を満たすあるネイバーフッド（近傍）\(U_t \subseteq T\)、つまり、\(f (U_t \setminus \{t\}) \subseteq B_{v, \epsilon} \subseteq N_v\)、がある、なぜなら、\(f\)は\(t\)に関してコンバージ（収束）する。
それが意味するのは、各\(t' \in U_t \setminus \{t\}\)に対して、\(f (t') = f^j (t') b_j \in B_{v, \epsilon}\)、それが意味するのは、\(\sum_{j \in \{1, ..., d\}} (f^j (t') - v^j)^2 \lt \epsilon^2\)。
したがって、各\(j\)に対して、\((f^j (t') - v^j)^2 \lt \epsilon^2\)。
それが意味するのは、マップ（写像）\(f^j: T_1 \setminus \{t\} \to \mathbb{R}\)は\(t\)に関してコンバージェンス（収束ポイント）を持つ、\(lim_{t' \to t} f^j (t') = v^j\)として、ということ。
したがって、\(lim_{t' \to t} f (t') = v = v^j b_j = lim_{t' \to t} f^j (t') b_j\)。
ステップ3:
各\(j \in \{1, ..., d\}\)に対して、\(lim_{t' \to t} f^j (t')\)が存在すると仮定し、それを\(v^j\)と表わそう。
ステップ4:
\(lim_{t' \to t} f (t')\)が存在し\(v^j b_j\)に等しいことを見よう。
\(v := v^j b_j\)と定義しよう。
\(v\)の各ネイバーフッド（近傍）\(N_v \subseteq V\)に対して、以下を満たすあるオープンボール（開球）\(B_{v, \epsilon} \subseteq V\)、つまり、\(B_{v, \epsilon} \subseteq N_v\)、がある。
各\(j\)に対して、\(B_{v^j, \epsilon / \sqrt{d}} \subseteq \mathbb{R}\)を\(v^j\)の周りのオープンボール（開球）としよう。
各\(j\)に対して、\(t\)の以下を満たすあるネイバーフッド（近傍）\(U_{j, t} \subseteq T\)、つまり、\(f^j (U_{j, t} \setminus \{t\}) \subseteq B_{v^j, \epsilon / \sqrt{d}}\)、がある、なぜなら、\(f^j\)は\(t\)に関してコンバージ（収束）する。
\(U_t := \cap_{j \in \{1, ..., d\}} U_{j, t} \subseteq T\)としよう、それは\(t\)のネイバーフッド（近傍）である。
各\(j\)に対して、\(f^j (U_t \setminus \{t\}) \subseteq B_{v^j, \epsilon / \sqrt{d}}\)、それが意味するのは、各\(t' \in U_t \setminus \{t\}\)に対して、\((f^j (t') - v^j)^2 \lt \epsilon^2 / d\)であること。
すると、各\(t' \in U_t \setminus \{t\}\)に対して、\(f (t') = f^j (t') b_j \in B_{v, \epsilon}\)、なぜなら、\(\sum_{j \in \{1, ..., d\}} (f^j (t') - v^j)^2 \lt \sum_{j \in \{1, ..., d\}} \epsilon^2 / d = \epsilon^2\)。
それが意味するのは、\(f (U_t \setminus \{t\}) \subseteq B_{v, \epsilon} \subseteq N_v\)。
それが意味するのは、\(f\)は\(t\)に関するコンバージェンス（収束ポイント）を持ち、\(lim_{t' \to t} f (t') = v\)であること。
したがって、\(lim_{t' \to t} f (t') = v = v^j b_j = lim_{t' \to t} f^j (t') b_j\)。
