\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、エンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対して、サブマニフォールド（部分多様体）、バウンダリー（境界）付き、の各ポイントの周りに、マニフォールド（多様体）、バウンダリー（境界）付き、に対するトリビアライジングオープンサブセット（開部分集合）でサブマニフォールド（部分多様体）、バウンダリー（境界）付き、とのインターセクション（共通集合）がチャートドメイン（定義域）であるものがあることの記述/証明
話題
About: \(C^\infty\)マニフォールド（多様体）
この記事の目次
開始コンテキスト
- 読者は、\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、のエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付きの定義を知っている。
- 読者は、\(C^\infty\)トリビアライジングオープンサブセット（開部分集合）および\(C^\infty\)ローカルトリビアライゼーションの定義を知っている。
- 読者は、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、その任意のチャートに対して、当該チャートの、任意のオープンサブセット（開部分集合）ドメイン（定義域）についてのリストリクション（制限）はチャートであるという命題を認めている。
- 読者は、任意の\(C^\infty\)トリビアライジングオープンサブセット（開部分集合）の任意のオープンサブセット（開部分集合）は\(C^\infty\)トリビアライジングオープンサブセット（開部分集合）であるという命題を認めている。
ターゲットコンテキスト
- 読者は、任意の\(C^\infty\)マニフォールド（多様体）、その任意のバウンダリー（境界）付き、エンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対して、当該サブマニフォールド（部分多様体）、バウンダリー（境界）付き、上の各ポイントの周りに、当該マニフォールド（多様体）、バウンダリー（境界）付き、に対するあるトリビアライジングオープンサブセット（開部分集合）で当該サブマニフォールド（部分多様体）、バウンダリー（境界）付き、とのインターセクション（共通集合）が当該サブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するチャートドメイン（定義域）であるものがあるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(M'\): \(\in \{\text{ 全ての } C^\infty \text{ マニフォールド（多様体）、バウンダリー（境界）付き、たち }\}\)
\(M\): \(\in \{M' \text{ の全てのエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、たち }\}\)
\(m\): \(\in M\)
//
ステートメント（言明）たち:
\(\exists U'_m \in \{M' \text{ の } m \text{ の周りの全てのトリビアライジングオープンサブセット（開部分集合）たち }\} (U'_m \cap M \in \{M \text{ に対する全てのチャートドメイン（定義域）たち }\})\)
//
2: 注
要点は、\(M'\)は非空バウンダリー（境界）を持っていてもよいということである: \(M'\)がバウンダリー（境界）なしの時は、スライスチャートたち定理が使えて、\(U'_m\)をアダプテッドチャートドメイン（定義域）として持てる; 本命題が言っているのは、\(M'\)が非空バウンダリー（境界）を持っている時でも、ある\(U'_m\)、それは必ずしもチャートドメイン（定義域）ではない、が選べる、ということ。
3: 証明
全体戦略: ステップ1: \(m\)の周りの\(M'\)に対する任意のトリビアライジングオープンサブセット（開部分集合）\(V'_m\)を取る; ステップ2: \(m\)の\(M\)上における任意のオープンネイバーフッド（開近傍）\(V_m\)でそのインクルージョン（封入）が\(V'_m\)内に包含されているものを取り、\(V_m\)内に包含されている任意のチャートドメイン（定義域）\(W_m\)を取る; ステップ3: \(W_m = W'_m \cap M\)とし、\(U'_m := V'_m \cap W'_m\)および\(U_m := U'_m \cap M\)を取り、\(U'_m\)は\(M'\)に対するトリビアライジングオープンサブセット（開部分集合）であり\(U_m\)は\(M\)に対するチャートドメイン（定義域）であることを見る。
ステップ1:
\(m\)の周りの\(M'\)のための任意のトリビアライジングオープンサブセット（開部分集合）\(V'_m \subseteq M'\)を取ろう。
ステップ2:
\(\iota: M \to M'\)をインクルージョン（封入）としよう。
\(\iota\)はコンティニュアス（連続）であるから、\(m\)の\(M\)上における以下を満たすあるオープンネイバーフッド（開近傍）\(V_m \subseteq M\)、つまり、\(\iota (V_m) \subseteq V'_m\)、がある。
\(V_m\)内に包含されている以下を満たすあるチャートドメイン（定義域）\(W_m \subseteq M\)、つまり、\(W_m \subseteq V_m\)、がある、なぜなら、\(m\)の周りのあるチャートドメイン（定義域）があるが、当該チャートドメイン（定義域）と\(V_m\)のインターセクション（共通集合）はチャートドメイン（定義域）である、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、その任意のチャートに対して、当該チャートの、任意のオープンサブセット（開部分集合）ドメイン（定義域）についてのリストリクション（制限）はチャートであるという命題によって、そして、当該インターセクション（共通集合）を\(W_m\)にできる。
ステップ3:
\(M\)は\(M'\)のサブスペース（部分空間）トポロジーを持つので、\(W_m = W'_m \cap M\)である、ここで、\(W'_m \subseteq M'\)は\(m\)の\(M'\)上におけるオープンサブセット（開部分集合）。
\(U'_m := V'_m \cap W'_m\)および\(U_m := U'_m \cap M\)を取ろう。
\(U'_m\)は\(V'_m\)のオープンサブセット（開部分集合）であるから、\(U'_m\)は\(M'\)に対するトリビアライジングオープンサブセット（開部分集合）である、任意の\(C^\infty\)トリビアライジングオープンサブセット（開部分集合）の任意のオープンサブセット（開部分集合）は\(C^\infty\)トリビアライジングオープンサブセット（開部分集合）であるという命題によって。
\(U_m = U'_m \cap M = V'_m \cap W'_m \cap M = V'_m \cap M \cap W'_m \cap M = V'_m \cap M \cap W_m\)は\(W_m\)のオープンサブセット（開部分集合）である（\(W_m\)は\(M\)のトポロジカルサブスペース（部分空間）であり\(V'_m \cap M\)は\(M\)上でオープン（開）である）ので、\(U_m\)はチャートドメイン（定義域）である、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、その任意のチャートに対して、当該チャートの、任意のオープンサブセット（開部分集合）ドメイン（定義域）についてのリストリクション（制限）はチャートであるという命題によって。
