\(C^\infty\)ベクトルたちバンドル（束）およびオープン（開）ドメイン（定義域）上方のローカル\(C^\infty\)セクションたちのセット（集合）でリニアにインディペンデント（線形独立）であるものに対して、ドメイン（定義域）の各ポイントの、より小さいかもしれないオープンネイバーフッド（開近傍）でその上方にあるローカル\(C^\infty\)フレームでリストリクテッド（制限された）セクションたちセット（集合）を含むものがあるものがあることの記述/証明
話題
About: \(C^\infty\)マニフォールド（多様体）
この記事の目次
開始コンテキスト
- 読者は、\(C^\infty\)ベクトルたちバンドル（束）上のローカル\(C^\infty\)フレームの定義を知っている。
- 読者は、任意の\(C^\infty\)ベクトルたちバンドル（束）に対して、当該ベーススペース（空間）の任意のクローズドサブセット（閉部分集合）に沿った任意の\(C^\infty\)セクション（断面）は、当該ベーススペース（空間）全体上方へ拡張し、サポートが当該サブセット（部分集合）の任意のオープンネイバーフッド（開近傍）内に包含されるようにできるという命題を認めている。
- 読者は、任意の\(C^\infty\)ベクトルたちバンドル（束）の任意の\(C^\infty\)セクション（断面）たちのセット（集合）であるポイントにおいてリニア（線形）にインディペンデント（独立）であるものは、当該ポイントのあるオープンネイバーフッド（開近傍）上でリニア（線形）にインディペンデント（独立）であるという命題を認めている。
ターゲットコンテキスト
- 読者は、任意の\(C^\infty\)ベクトルたちバンドル（束）および任意のオープン（開）ドメイン（定義域）上方のローカル\(C^\infty\)セクションたちの任意のセット（集合）でリニアにインディペンデント（線形独立）であるものに対して、当該ドメイン（定義域）の各ポイントの、より小さいかもしれないオープンネイバーフッド（開近傍）でその上方にあるローカル\(C^\infty\)フレームでリストリクテッド（制限された）セクションたちセット（集合）を含むものがあるものがあるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\((E, M, \pi)\): \(\in \{\text{ ランク } k \text{ の全ての } C^\infty \text{ ベクトルたちバンドル（束）たち }\}\)
\(U\): \(\in \{M \text{ の全てのオープンサブセット（開部分集合）たち }\}\)
\(\{s_1, ..., s_n\}\): \(s_j: U \to E \in \{\pi \text{ の全てののローカル } C^\infty \text{ セクションたち }\}\)で、\(\forall u \in U (\{s_1 (u), ..., s_n (u)\} \in \{\pi^{-1} (u) \text{ の全てのリニアにインディペンデント（線形独立）なサブセット（部分集合）たち }\})\)
//
ステートメント（言明）たち:
\(\forall u \in U (\exists U_u \subseteq M \in \{u \text{ の全てのオープンネイバーフッド（開近傍）たち }\} \text{ で } U_u \subseteq U \text{ を満たすもの }, \exists \{s_{n + 1}, ..., s_k\} \text{ ここで、 } s_{n + j}: M \to E \in \{\pi \text{ の全ての } C^\infty \text{ セクションたち }\} (\{s_1 \vert_{U_u}, ..., s_k \vert_{U_u}\} \in \{\text{ 全てのローカル } C^\infty \text{ フレームたち }\}))\)
//
2: 証明
全体戦略: ステップ1: \(\pi^{-1} (u)\)に対する任意のベーシス（基底）\(\{s_1 (u), ..., s_n (u), v_{n + 1}, ..., v_k\}\)を取る; ステップ2: 各\(j \in \{1, ..., k - n\}\)に対して、\(\pi\)の以下を満たすある\(C^\infty\)セクション\(s_{n + j}: M \to E\)、つまり、\(s_{n + j} (u) = v_{n + j}\)、を取る; ステップ3: \(u\)の以下を満たすあるオープンネイバーフッド（開近傍）\(U_u \subseteq M\)、つまり、\(U_u \subseteq U\)、でその上方で\(\{s_1, ..., s_n, s_{n + 1}, ..., s_k\}\)はリニアにインディペンデント（線形独立）なものがあることを見る。
ステップ1:
\(\pi^{-1} (u)\)に対するあるベーシス（基底）\(\{s_1 (u), ..., s_n (u), v_{n + 1}, ..., v_k\}\)がある。
ステップ2:
\(j \in \{1, ..., k - n\}\)を任意のものとする。
\(\{u\} \subseteq M\)は\(M\)のクローズドサブセット（閉部分集合）である。
\(s_{n + j}: \{u\} \to E, u \mapsto v_{n + j}\)は、\(\{u\}\)に沿った\(C^\infty\)セクションである: \(u\)の周りのあるトリビアライジングチャートおよび\(E\)に対する対応するチャートを取る、すると、\(s_{n + j}\)の当該コンポーネントたちファンクション（関数）は当該トリビアライジングチャート上方の明らかな\(C^\infty\)エクステンション（拡張）\(: x \mapsto (v_{n + j}^1, ..., v_{n + j}^k, x)\)を持つ。
\(\pi\)の以下を満たすある\(C^\infty\)セクション\(s_{n + j}: M \to E\)、つまり、\(s_{n + j} (u) = v_{n + j}\)、がある、任意の\(C^\infty\)ベクトルたちバンドル（束）に対して、当該ベーススペース（空間）の任意のクローズドサブセット（閉部分集合）に沿った任意の\(C^\infty\)セクション（断面）は、当該ベーススペース（空間）全体上方へ拡張し、サポートが当該サブセット（部分集合）の任意のオープンネイバーフッド（開近傍）内に包含されるようにできるという命題によって。
ステップ3:
今や、私たちは、\(U\)上方のローカル\(C^\infty\)セクションたちの以下を満たすあるセット（集合）\(\{s_1, ..., s_n, s_{n + 1} \vert_U, ..., s_k \vert_U\}\)、つまり、\(\{s_1 (u), ..., s_k (u)\}\)はリニアにインディペンデント（線形独立）である、を持っている。
\(u\)の以下を満たすあるオープンネイバーフッド（開近傍）\(U_u \subseteq M\)、つまり、\(U_u \subseteq U\)、でその上方で\(\{s_1, ..., s_k\}\)はリニアにインディペンデント（線形独立）であるものがある、任意の\(C^\infty\)ベクトルたちバンドル（束）の任意の\(C^\infty\)セクション（断面）たちのセット（集合）であるポイントにおいてリニア（線形）にインディペンデント（独立）であるものは、当該ポイントのあるオープンネイバーフッド（開近傍）上でリニア（線形）にインディペンデント（独立）であるという命題によって: 当該命題は字面上は当該セクションたちが\(M\)全体上方にあることを要求しているが、当該命題は、ローカルセクションたちを持つ本ケースにも適用できる、その"証明"から明らかであるとおり。
したがって、\(\{s_1 \vert_{U_u}, ..., s_k \vert_{U_u}\}\)は、\(U_u\)上方のローカル\(C^\infty\)フレームである。
