783: $C^\infty$マニフォールド（多様体）、サブセット（部分集合）、サブセット（部分集合）上のポイントに対して、もしも、チャートがエンベッデッドサブマニフォールド（部分多様体）のためのローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、のためのローカルスライスコンディションを満たす場合、そのサブオープンネイバーフッド（開近傍）もそうする|T.B.P.日本語版

<このシリーズの前の記事 | このシリーズの目次 | このシリーズの次の記事>

C^{\infty}

マニフォールド（多様体）、サブセット（部分集合）、サブセット（部分集合）上のポイントに対して、もしも、チャートがエンベッデッドサブマニフォールド（部分多様体）のためのローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、のためのローカルスライスコンディションを満たす場合、そのサブオープンネイバーフッド（開近傍）もそうすることの記述/証明

話題

About: $C^{\infty}$ マニフォールド（多様体）

開始コンテキスト

ターゲットコンテキスト

読者は、任意の $C^{\infty}$ マニフォールド（多様体）、任意のサブセット（部分集合）、当該サブセット（部分集合）上の任意のポイントに対して、もしも、あるチャートがエンベッデッドサブマニフォールド（部分多様体）のためのローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、のためのローカルスライスコンディションを満たす場合、その任意のサブオープンネイバーフッド（開近傍）もそうするという命題の記述および証明を得る。

オリエンテーション

本サイトにてこれまで議論された定義たちの一覧があります。

本サイトにてこれまで議論された命題たちの一覧があります。

本体

1: 構造化された記述

ここに'構造化された記述'のルールたちがある。

エンティティ（実体）たち:

M^{'}

\in {全ての d^{'} ディメンショナル（次元） C^{\infty} マニフォールド（多様体）たち}

S

\subseteq M^{'}

J

\subseteq {1, . . ., d^{'}}

such that

| J | = d

k

\in J

s

\in S

λ_{J, r}

: P o w (R^{d^{'}}) \to P o w (R^{d^{'}})

= 当該スライスマップ（写像）

、ここで、

r \in R^{d^{'}}

は任意のもの

λ_{J, r, k}

: P o w (R^{d^{'}}) \to P o w (R^{d^{'}})

= 当該スライシングアンドハーフ化マップ（写像）

、ここで、

r \in R^{d^{'}}

は任意のもの

π_{J}

: R^{d^{'}} \to R^{d}

= 当該プロジェクション（射影）

(U_{s}^{'} \subseteq M^{'}, ϕ_{s}^{'})

\in {s の周りの M^{'} の全てのチャートたち}

V_{s}^{'}

\in {s の M^{'} 上の全てのオープンネイバーフッド（開近傍）たち}

で、

V_{s}^{'} \subseteq U_{s}^{'}

を満たすもの
//

ステートメント（言明）たち:

(U_{s}^{'} \subseteq M^{'}, ϕ_{s}^{'})

はエンベッデッドサブマニフォールド（部分多様体）のためのローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、のためのローカルスライスコンディションを満たす

⟹

(V_{s}^{'} \subseteq M^{'}, ϕ_{s}^{'} |_{V_{s}^{'}})

はエンベッデッドサブマニフォールド（部分多様体）のためのローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、のためのローカルスライスコンディションを満たす
//

2: 自然言語記述

任意の

d^{'}

ディメンショナル（次元）

C^{\infty}

マニフォールド（多様体）

M^{'}

、任意のサブセット（部分集合）

S \subseteq M^{'}

、以下を満たす任意のサブセット（部分集合）

J \subseteq {1, . . ., d^{'}}

、つまり、

| J | = d

、任意の

k \in J

、任意のポイント

s \in S

、スライスマップ（写像）

λ_{J, r} : P o w (R^{d^{'}}) \to P o w (R^{d^{'}})

、ここで、

r \in R^{d^{'}}

は任意のもの、スライシングアンドハーフ化マップ（写像）

λ_{J, r, k} : P o w (R^{d^{'}}) \to P o w (R^{d^{'}})

、ここで、

r \in R^{d^{'}}

は任意のもの、プロジェクション（射影）

π_{J} : R^{d^{'}} \to R^{d}

、

s

の周りの任意のチャート

(U_{s}^{'} \subseteq M^{'}, ϕ_{s}^{'})

、

s

の以下を満たす任意のオープンネイバーフッド（開近傍）

V_{s}^{'} \subseteq M^{'}

、つまり、

V_{s}^{'} \subseteq U_{s}^{'}

、に対して、もしも、

(U_{s}^{'} \subseteq M^{'}, ϕ_{s}^{'})

がエンベッデッドサブマニフォールド（部分多様体）のためのローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、のためのローカルスライスコンディションを満たす場合、

(V_{s}^{'} \subseteq M^{'}, ϕ_{s}^{'} |_{V_{s}^{'}})

エンベッデッドサブマニフォールド（部分多様体）のためのローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、のためのローカルスライスコンディションを満たす。

3: 証明

全体戦略: ステップ1:

(U_{s}^{'} \subseteq M^{'}, ϕ_{s}^{'})

はエンベッデッドサブマニフォールド（部分多様体）のためのローカルスライスコンディションを満たすと仮定し、フォーマライゼーション

ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'}))

を得る; ステップ2:

ϕ_{s}^{'} (V_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (V_{s}^{'}))

が満たされていることを見る; ステップ3:

(U_{s}^{'} \subseteq M^{'}, ϕ_{s}^{'})

はエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、のためのローカルスライスコンディションを満たすと仮定し、フォーマライゼーション

ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'})) \lor (ϕ_{s}^{'} (s)^{k} = 0 \land ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (U_{s}^{'})))

を得る; ステップ4:

ϕ_{s}^{'} (V_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (V_{s}^{'})) \lor (ϕ_{s}^{'} (s)^{k} = 0 \land ϕ_{s}^{'} (V_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (V_{s}^{'})))

が満たされていることを見る。

ステップ1:

(U_{s}^{'} \subseteq M^{'}, ϕ_{s}^{'})

はエンベッデッドサブマニフォールド（部分多様体）のためのローカルスライスコンディションを満たすと仮定しよう。

エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションのフォーマライゼーション（定式化）は妥当であるという命題によって、

ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'}))

。

ステップ2:

エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションのフォーマライゼーション（定式化）は妥当であるという命題によって、見る必要のあることは、

ϕ_{s}^{'} (V_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (V_{s}^{'}))

が満たされるということだけ。

p \in ϕ_{s}^{'} (V_{s}^{'} \cap S)

は任意のものであるとし、

p \in λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (V_{s}^{'}))

であることを見よう。

p \in ϕ_{s}^{'} (V_{s}^{'})

、なぜなら、

p \in ϕ_{s}^{'} (V_{s}^{'} \cap S) \subseteq ϕ_{s}^{'} (V_{s}^{'})

。

p \in ϕ_{s}^{'} (V_{s}^{'} \cap S) \subseteq ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'}))

、それが含意するのは、各

j \in {1, . . ., d^{'}} ∖ J

に対して、

p^{j} = ϕ_{s}^{'} (s)^{j}

であること。しかし、それが含意するのは、

p \in λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (V_{s}^{'}))

。

p \in λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (V_{s}^{'}))

は任意のものであるとし、

p \in ϕ_{s}^{'} (V_{s}^{'} \cap S)

であることを見よう。

以下を満たすある

p^{'} \in V_{s}^{'}

、つまり、

p = ϕ_{s}^{'} (p^{'})

、がある。

p \in λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (V_{s}^{'})) \subseteq λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'})) = ϕ_{s}^{'} (U_{s}^{'} \cap S)

。したがって、以下を満たすある

p^{″} \in U_{s}^{'} \cap S

、つまり、

p = ϕ_{s}^{'} (p^{″})

、がある。

ϕ_{s}^{'}

はインジェクティブ（単射）であるから、

p^{'} = p^{″} \in V_{s}^{'} \cap U_{s}^{'} \cap S = V_{s}^{'} \cap S

。したがって、

p = ϕ_{s}^{'} (p^{'}) \in ϕ_{s}^{'} (V_{s}^{'} \cap S)

。

したがって、

ϕ_{s}^{'} (V_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (V_{s}^{'}))

。

ステップ3:

(U_{s}^{'} \subseteq M^{'}, ϕ_{s}^{'})

はエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、のためのローカルスライスコンディションを満たすと仮定しよう。

エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションのフォーマライゼーション（定式化）は妥当であるという命題によって、

ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'})) \lor (ϕ_{s}^{'} (s)^{k} = 0 \land ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (U_{s}^{'})))

。

ステップ4:

エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションのフォーマライゼーション（定式化）は妥当であるという命題によって、見る必要のあることは、

ϕ_{s}^{'} (V_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (V_{s}^{'})) \lor (ϕ_{s}^{'} (s)^{k} = 0 \land ϕ_{s}^{'} (V_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (V_{s}^{'})))

が満たされるということだけである。

ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'}))

である時、

ϕ_{s}^{'} (V_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (V_{s}^{'}))

である、前と同様に。

ϕ_{s}^{'} (s)^{k} = 0 \land ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (U_{s}^{'}))

であると仮定し、

ϕ_{s}^{'} (s)^{k} = 0 \land ϕ_{s}^{'} (V_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (V_{s}^{'}))

であることを見よう。

ϕ_{s}^{'} (s)^{k} = 0

、明らかに。

p \in ϕ_{s}^{'} (V_{s}^{'} \cap S)

は任意のものであるとし、

p \in λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (V_{s}^{'}))

であることを見よう。

p \in ϕ_{s}^{'} (V_{s}^{'})

、なぜなら、

p \in ϕ_{s}^{'} (V_{s}^{'} \cap S) \subseteq ϕ_{s}^{'} (V_{s}^{'})

。

p \in ϕ_{s}^{'} (V_{s}^{'} \cap S) \subseteq ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (U_{s}^{'}))

、それが含意するのは、各

j \in {1, . . ., d^{'}} ∖ J

に対して、

p^{j} = ϕ_{s}^{'} (s)^{j}

および

ϕ_{s}^{'} (s)^{k} \leq p^{k}

。しかし、それが含意するのは、

p \in λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (V_{s}^{'}))

。

p \in λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (V_{s}^{'}))

は任意のものであるとし、

p \in ϕ_{s}^{'} (V_{s}^{'} \cap S)

であることを見よう。

以下を満たすある

p^{'} \in V_{s}^{'}

、つまり、

p = ϕ_{s}^{'} (p^{'})

、がある。

p \in λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (V_{s}^{'})) \subseteq λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (U_{s}^{'})) = ϕ_{s}^{'} (U_{s}^{'} \cap S)

。したがって、以下を満たすある

p^{″} \in U_{s}^{'} \cap S

、つまり、

p = ϕ_{s}^{'} (p^{″})

、がある。

ϕ_{s}^{'}

はインジェクティブ（単射）であるから、

p^{'} = p^{″} \in V_{s}^{'} \cap U_{s}^{'} \cap S = V_{s}^{'} \cap S

。したがって、

p = ϕ_{s}^{'} (p^{'}) \in ϕ_{s}^{'} (V_{s}^{'} \cap S)

。

したがって、

ϕ_{s}^{'} (s)^{k} = 0 \land ϕ_{s}^{'} (V_{s}^{'} \cap S) = ϕ_{s}^{'} (V_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (V_{s}^{'}))

。

参考資料

<このシリーズの前の記事 | このシリーズの目次 | このシリーズの次の記事>

バイアス惑星
定義たちと命題たち
学校数学をより高い視点から
わかりにくい用語や説明をひもとく
情報テーブル群
LibreOfficeまたはOpenOfficeを活用する
Javaプログラミング言語を暴く
C++を暴く
Pythonを暴く
C#を暴く
Gradleを暴く
Gitを暴く
UNOディスパッチコマンドたち

2024年9月22日日曜日

話題

この記事の目次

開始コンテキスト

ターゲットコンテキスト

オリエンテーション

本体

1: 構造化された記述

2: 自然言語記述

3: 証明

参考資料