グループ（群）およびサブグループ（部分群）に対して、サブグループ（部分群）のコンプリメント（補集合）内の要素によるサブグループ（部分群）の左および右コセット（剰余類）たちはサブグループ（部分群）のコンプリメント（補集合）内に包含されることの記述/証明
話題
About: グループ（群）
この記事の目次
開始コンテキスト
- 読者は、グループ（群）の要素によるサブグループ（部分群）の左または右コセット（剰余類）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のグループ（群）および任意のサブグループ（部分群）に対して、当該サブグループ（部分群）のコンプリメント（補集合）内の任意の要素による当該サブグループ（部分群）の左および右コセット（剰余類）たちは当該サブグループ（部分群）のコンプリメント（補集合）内に包含されるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(G'\): \(\in \{\text{ 全てのグループ（群）たち }\}\)
\(G\): \(\in \{G' \text{ の全てのサブグループ（部分群）たち }\}\)
\(g'\): \(\in G' \setminus G\)
//
ステートメント（言明）たち:
\(g' G \subseteq G' \setminus G\)
\(\land\)
\(G g' \subseteq G' \setminus G\)
//
2: 証明
全体戦略: ステップ1: ある\(g' g \in G\)があったと仮定し、ある矛盾を見つける; ステップ2: ある\(g g' \in G\)があったと仮定し、ある矛盾を見つける。
ステップ1:
\(g' G \subseteq G' \setminus G\)であることを見よう。
以下を満たすある\(g \in G\)、つまり、\(g' g \in G\)、があったと仮定しよう。
\(\widetilde{g} := g' g \in G\)。
\(g' = \widetilde{g} g^{-1} \in G\)、なぜなら、\(G\)はあるグループ（群）であった、\(g' \in G' \setminus G\)に反する矛盾。
したがって、そうした\(g\)は無い。
それが意味するのは、\(g' G \subseteq G' \setminus G\)。
ステップ2:
\(G g' \subseteq G' \setminus G\)であることを見よう。
以下を満たすある\(g \in G\)、つまり、\(g g' \in G\)、があったと仮定しよう。
\(\widetilde{g} := g g' \in G\)。
\(g' = g^{-1} \widetilde{g} \in G\)、なぜなら、\(G\)はあるグループ（群）であった、\(g' \in G' \setminus G\)に反する矛盾。
したがって、そうした\(g\)はない。
それが意味するのは、\(G g' \subseteq G' \setminus G\)。
