トポロジカルスペース(空間)マイナス任意のポイントからファイナイト(有限)-ディメンショナル(次元)リアル(実)ベクトルたちスペース(空間)でカノニカル(正典)トポロジーを持つものの中へのマップ(写像)に対して、マップ(写像)の、ポイントに関するコンバージェンス(収束ポイント)は存在する、もしも、コンポーネントマップ(写像)たちのポイントに関するコンバージェンス(収束ポイント)たちが存在する場合、そしてその場合に限って、そして、その場合、コンバージェンス(収束ポイント)はコンバージェンス(収束ポイント)たちで表わされることの記述/証明
話題
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\)。