グループ（群）からリニアリーオーダードセット（線形順序集合）の中への\(2\)個のマップ（写像）たちに対して、前者は後者以下またはそれより小さい、もしも、要素によるそれらの左または右トランスレーション（平行移動）たちが同じ関係を満たす場合、そしてその場合に限って、ことの記述/証明
話題
About: グループ（群）
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、グループ（群）からのマップ（写像）の要素による左または右トランスレーション（平行移動）の定義を知っている。
- 読者は、リニアリーオーダードセット（線形順序集合）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のグループ（群）から任意のリニアリーオーダードセット（線形順序集合）の中への任意の\(2\)個のマップ（写像）たちに対して、前者は後者以下またはそれより小さい、もしも、任意の要素によるそれらの左または右トランスレーション（平行移動）たちが同じ関係を満たす場合、そしてその場合に限って、という命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(G\): \(\in \{\text{ 全てのグループ（群）たち }\}\)
\(S\): \(\in \{\text{ 全てのリニアリーオーダードセット（線形順序集合）たち }\}\)
\(f_1\): \(: G \to S\)
\(f_2\): \(: G \to S\)
\(g\): \(\in G\)
\(_gf_1\): \(= \text{ 当該左トランスレーション（平行移動） }\)
\(_gf_2\): \(= \text{ 当該左トランスレーション（平行移動） }\)
\({f_1}_g\): \(= \text{ 当該右トランスレーション }\)
\({f_2}_g\): \(= \text{ 当該右トランスレーション }\)
//
ステートメント（言明）たち:
(
\(f_1 \le f_2\)
\(\iff\)
\(_gf_1 \le _gf_2\)
)
\(\land\)
(
\(f_1 \le f_2\)
\(\iff\)
\({f_1}_g \le {f_2}_g\)
)
\(\land\)
(
\(f_1 \lt f_2\)
\(\iff\)
\(_gf_1 \lt _gf_2\)
)
\(\land\)
(
\(f_1 \lt f_2\)
\(\iff\)
\({f_1}_g \lt {f_2}_g\)
)
//
2: 証明
全体戦略: ステップ1: \(f_1 \le f_2\)であると仮定する; ステップ2: \(_gf_1 \le _gf_2\)および\({f_1}_g \le {f_2}_g\)であることを見る; ステップ3: \(f_1 \lt f_2\)であると仮定する; ステップ4: \(_gf_1 \lt _gf_2\)および\({f_1}_g \lt {f_2}_g\)であることを見る; ステップ5: \(_{g^{-1}}(_gf_j) = f_j\)および\(({f_j}_g)_{g^{-1}} = f_j\)であることを見る; ステップ6: 本命題を結論する。
ステップ1:
\(f_1 \le f_2\)であると仮定しよう。
ステップ2:
各\(g' \in G\)に対して、\(_gf_1 (g') = f_1 (g^{-1} g') \le f_2 (g^{-1} g') = _gf_2 (g')\)。
したがって、\(_gf_1 \le _gf_2\)。
各\(g' \in G\)に対して、\({f_1}_g (g') = f_1 (g' g^{-1}) \le f_2 (g' g^{-1}) = {f_2}_g (g')\)。
したがって、\({f_1}_g \le {f_2}_g\)。
ステップ3:
\(f_1 \lt f_2\)であると仮定しよう。
ステップ4:
各\(g' \in G\)に対して、\(_gf_1 (g') = f_1 (g^{-1} g') \lt f_2 (g^{-1} g') = _gf_2 (g')\)。
したがって、\(_gf_1 \lt _gf_2\)。
各\(g' \in G\)に対して、\({f_1}_g (g') = f_1 (g' g^{-1}) \lt f_2 (g' g^{-1}) = {f_2}_g (g')\)。
したがって、\({f_1}_g \lt {f_2}_g\)。
ステップ5:
各\(g' \in G\)に対して、\(_{g^{-1}}(_gf_j) (g') = _gf_j (g g') = f_j (g^{-1} g g') = f_j (g')\)。
したがって、\(_{g^{-1}}(_gf_j) = f_j\)。
各\(g' \in G\)に対して、\(({f_j}_g)_{g^{-1}} (g') = {f_j}_g (g' g) = f_j (g' g g^{-1}) = f_j (g')\)。
したがって、\(({f_j}_g)_{g^{-1}} = f_j\)。
ステップ6:
\(_gf_1 \le _gf_2\)が含意するのは、\(_{g^{-1}}(_gf_1) \le _{g^{-1}}(_gf_2)\)、ステップ2によって、それが含意するのは、\(f_1 \le f_2\)、ステップ5によって。
\({f_1}_g \le {f_2}_g\)が含意するのは、\(({f_1}_g)_{g^{-1}} \le ({f_2}_g)_{g^{-1}}\)、ステップ2によって、それが含意するのは、\(f_1 \le f_2\)、ステップ5によって。
\(_gf_1 \lt _gf_2\)が含意するのは、\(_{g^{-1}}(_gf_1) \lt _{g^{-1}}(_gf_2)\)、ステップ4によって、それが含意するのは、\(f_1 \lt f_2\)、ステップ5によって。
\({f_1}_g \lt {f_2}_g\)が含意するのは、\(({f_1}_g)_{g^{-1}} \lt ({f_2}_g)_{g^{-1}}\)、ステップ4によって、それが含意するのは、\(f_1 \lt f_2\)、ステップ5によって。
したがって、本命題は成立する。
