\(C^\infty\)マニフォールド（多様体）、サブセット（部分集合）、サブセット（部分集合）上のポイントに対して、もしも、チャートがエンベッデッドサブマニフォールド（部分多様体）のためのローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、のためのローカルスライスコンディションを満たす場合、そのサブオープンネイバーフッド（開近傍）もそうすることの記述/証明
話題
About: \(C^\infty\)マニフォールド（多様体）
この記事の目次
開始コンテキスト
ターゲットコンテキスト
- 読者は、任意の\(C^\infty\)マニフォールド（多様体）、任意のサブセット（部分集合）、当該サブセット（部分集合）上の任意のポイントに対して、もしも、あるチャートがエンベッデッドサブマニフォールド（部分多様体）のためのローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、のためのローカルスライスコンディションを満たす場合、その任意のサブオープンネイバーフッド（開近傍）もそうするという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(M'\): \(\in \{ \text{ 全ての } d' \text{ ディメンショナル（次元） } C^\infty \text{ マニフォールド（多様体）たち } \}\)
\(S\): \(\subseteq M'\)
\(J\): \(\subseteq \{1, ..., d'\}\) such that \(\vert J \vert = d\)
\(k\): \(\in J\)
\(s\): \(\in S\)
\(\lambda_{J, r}\): \(: Pow (\mathbb{R}^{d'}) \to Pow (\mathbb{R}^{d'})\), \(= \text{ 当該スライスマップ（写像） }\)、ここで、\(r \in \mathbb{R}^{d'}\)は任意のもの
\(\lambda_{J, r, k}\): \(: Pow (\mathbb{R}^{d'}) \to Pow (\mathbb{R}^{d'})\), \(= \text{ 当該スライシングアンドハーフ化マップ（写像） }\)、ここで、\(r \in \mathbb{R}^{d'}\)は任意のもの
\(\pi_J\): \(: \mathbb{R}^{d'} \to \mathbb{R}^d\), \(= \text{ 当該プロジェクション（射影） }\)
\((U'_s \subseteq M', \phi'_s)\): \(\in \{s \text{ の周りの } M' \text{ の全てのチャートたち }\}\)
\(V'_s\): \(\in \{s \text{ の } M' \text{ 上の全てのオープンネイバーフッド（開近傍）たち } \}\)で、\(V'_s \subseteq U'_s\)を満たすもの
//
ステートメント（言明）たち:
\((U'_s \subseteq M', \phi'_s)\)はエンベッデッドサブマニフォールド（部分多様体）のためのローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、のためのローカルスライスコンディションを満たす
\(\implies\)
\((V'_s \subseteq M', \phi'_s \vert_{V'_s})\)はエンベッデッドサブマニフォールド（部分多様体）のためのローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、のためのローカルスライスコンディションを満たす
//
2: 自然言語記述
任意の\(d'\)ディメンショナル（次元）\(C^\infty\)マニフォールド（多様体）\(M'\)、任意のサブセット（部分集合）\(S \subseteq M'\)、以下を満たす任意のサブセット（部分集合）\(J \subseteq \{1, ..., d'\}\)、つまり、\(\vert J \vert = d\)、任意の\(k \in J\)、任意のポイント\(s \in S\)、スライスマップ（写像）\(\lambda_{J, r}: Pow (\mathbb{R}^{d'}) \to Pow (\mathbb{R}^{d'})\)、ここで、\(r \in \mathbb{R}^{d'}\)は任意のもの、スライシングアンドハーフ化マップ（写像）\(\lambda_{J, r, k}: Pow (\mathbb{R}^{d'}) \to Pow (\mathbb{R}^{d'})\)、ここで、\(r \in \mathbb{R}^{d'}\)は任意のもの、プロジェクション（射影）\(\pi_J: \mathbb{R}^{d'} \to \mathbb{R}^d\)、\(s\)の周りの任意のチャート\((U'_s \subseteq M', \phi'_s)\)、\(s\)の以下を満たす任意のオープンネイバーフッド（開近傍）\(V'_s \subseteq M'\)、つまり、\(V'_s \subseteq U'_s\)、に対して、もしも、\((U'_s \subseteq M', \phi'_s)\)がエンベッデッドサブマニフォールド（部分多様体）のためのローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、のためのローカルスライスコンディションを満たす場合、\((V'_s \subseteq M', \phi'_s \vert_{V'_s})\)エンベッデッドサブマニフォールド（部分多様体）のためのローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、のためのローカルスライスコンディションを満たす。
3: 証明
全体戦略: ステップ1: \((U'_s \subseteq M', \phi'_s)\)はエンベッデッドサブマニフォールド（部分多様体）のためのローカルスライスコンディションを満たすと仮定し、フォーマライゼーション\(\phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s))\)を得る; ステップ2: \(\phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s))\)が満たされていることを見る; ステップ3: \((U'_s \subseteq M', \phi'_s)\)はエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、のためのローカルスライスコンディションを満たすと仮定し、フォーマライゼーション\(\phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s)) \lor (\phi'_s (s)^k = 0 \land \phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s), k} (\phi'_s (U'_s)))\)を得る; ステップ4: \(\phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s)) \lor (\phi'_s (s)^k = 0 \land \phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s), k} (\phi'_s (V'_s)))\)が満たされていることを見る。
ステップ1:
\((U'_s \subseteq M', \phi'_s)\)はエンベッデッドサブマニフォールド（部分多様体）のためのローカルスライスコンディションを満たすと仮定しよう。
エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションのフォーマライゼーション（定式化）は妥当であるという命題によって、\(\phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s))\)。
ステップ2:
エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションのフォーマライゼーション（定式化）は妥当であるという命題によって、見る必要のあることは、\(\phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s))\)が満たされるということだけ。
\(p \in \phi'_s (V'_s \cap S)\)は任意のものであるとし、\(p \in \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s))\)であることを見よう。
\(p \in \phi'_s (V'_s)\)、なぜなら、\(p \in \phi'_s (V'_s \cap S) \subseteq \phi'_s (V'_s)\)。
\(p \in \phi'_s (V'_s \cap S) \subseteq \phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s))\)、それが含意するのは、各\(j \in \{1, ..., d'\} \setminus J\)に対して、\(p^j = \phi'_s (s)^j\)であること。しかし、それが含意するのは、\(p \in \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s))\)。
\(p \in \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s))\)は任意のものであるとし、\(p \in \phi'_s (V'_s \cap S)\)であることを見よう。
以下を満たすある\(p' \in V'_s\)、つまり、\(p = \phi'_s (p')\)、がある。
\(p \in \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s)) \subseteq \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s)) = \phi'_s (U'_s \cap S)\)。したがって、以下を満たすある\(p'' \in U'_s \cap S\)、つまり、\(p = \phi'_s (p'')\)、がある。
\(\phi'_s\)はインジェクティブ（単射）であるから、\(p' = p'' \in V'_s \cap U'_s \cap S = V'_s \cap S\)。したがって、\(p = \phi'_s (p') \in \phi'_s (V'_s \cap S)\)。
したがって、\(\phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s))\)。
ステップ3:
\((U'_s \subseteq M', \phi'_s)\)はエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、のためのローカルスライスコンディションを満たすと仮定しよう。
エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションのフォーマライゼーション（定式化）は妥当であるという命題によって、\(\phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s)) \lor (\phi'_s (s)^k = 0 \land \phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s), k} (\phi'_s (U'_s)))\)。
ステップ4:
エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションのフォーマライゼーション（定式化）は妥当であるという命題によって、見る必要のあることは、\(\phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s)) \lor (\phi'_s (s)^k = 0 \land \phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s), k} (\phi'_s (V'_s)))\)が満たされるということだけである。
\(\phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s))\)である時、\(\phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s))\)である、前と同様に。
\(\phi'_s (s)^k = 0 \land \phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s), k} (\phi'_s (U'_s))\)であると仮定し、\(\phi'_s (s)^k = 0 \land \phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s), k} (\phi'_s (V'_s))\)であることを見よう。
\(\phi'_s (s)^k = 0\)、明らかに。
\(p \in \phi'_s (V'_s \cap S)\)は任意のものであるとし、\(p \in \lambda_{J, \phi'_s (s), k} (\phi'_s (V'_s))\)であることを見よう。
\(p \in \phi'_s (V'_s)\)、なぜなら、\(p \in \phi'_s (V'_s \cap S) \subseteq \phi'_s (V'_s)\)。
\(p \in \phi'_s (V'_s \cap S) \subseteq \phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s), k} (\phi'_s (U'_s))\)、それが含意するのは、各\(j \in \{1, ..., d'\} \setminus J\)に対して、\(p^j = \phi'_s (s)^j\)および\(\phi'_s (s)^k \le p^k\)。しかし、それが含意するのは、\(p \in \lambda_{J, \phi'_s (s), k} (\phi'_s (V'_s))\)。
\(p \in \lambda_{J, \phi'_s (s), k} (\phi'_s (V'_s))\)は任意のものであるとし、\(p \in \phi'_s (V'_s \cap S)\)であることを見よう。
以下を満たすある\(p' \in V'_s\)、つまり、\(p = \phi'_s (p')\)、がある。
\(p \in \lambda_{J, \phi'_s (s), k} (\phi'_s (V'_s)) \subseteq \lambda_{J, \phi'_s (s), k} (\phi'_s (U'_s)) = \phi'_s (U'_s \cap S)\)。したがって、以下を満たすある\(p'' \in U'_s \cap S\)、つまり、\(p = \phi'_s (p'')\)、がある。
\(\phi'_s\)はインジェクティブ（単射）であるから、\(p' = p'' \in V'_s \cap U'_s \cap S = V'_s \cap S\)。したがって、\(p = \phi'_s (p') \in \phi'_s (V'_s \cap S)\)。
したがって、\(\phi'_s (s)^k = 0 \land \phi'_s (V'_s \cap S) = \phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s), k} (\phi'_s (V'_s))\)。
