パーシャリーオーダードセット（半順序集合）およびサブセット（部分集合）に対して、もしも、サブセット（部分集合）のミニマム（最小）が存在する場合、ミニマム（最小）はインフィマム（下限）であり、もしも、サブセット（部分集合）のマキシマム（最大）が存在する場合、マキシマム（最大）はサプリマム（上限）であることの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、パーシャリーオーダードセット（半順序集合）のサブセット（部分集合）でインデュースト（誘導された）パーシャルオーダリング（半順序）を持つものの定義を知っている。
- 読者は、パーシャリーオーダードセット（半順序集合）のミニマム（最小）の定義を知っている。
- 読者は、パーシャリーオーダードセット（半順序集合）のサブセット（部分集合）のインフィマム（下限）の定義を知っている。
- 読者は、パーシャリーオーダードセット（半順序集合）のマキシマム（最大）の定義を知っている。
- 読者は、パーシャリーオーダードセット（半順序集合）のサブセット（部分集合）のサプリマム（上限）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のパーシャリーオーダードセット（半順序集合）および任意のサブセット（部分集合）に対して、もしも、当該サブセット（部分集合）のミニマム（最小）が存在する場合、当該ミニマム（最小）はインフィマム（下限）であり、もしも、当該サブセット（部分集合）のマキシマム（最大）が存在する場合、当該マキシマム（最大）はサプリマム（上限）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(S'\): \(\in \{\text{ 全てのパーシャリーオーダードセット（半順序集合）たち }\}\)で、任意のパーシャルオーダリング（半順序）\(\lt'\)を持つもの
\(S\): \(\subseteq S'\)で、インデュースト（誘導された）パーシャルオーダリング（半順序）\(\lt\)を持つもの
//
ステートメント（言明）たち:
(
\(\exists Min (S)\)
\(\implies\)
\(Min (S) = Inf (S)\)
)
\(\land\)
(
\(\exists Max (S)\)
\(\implies\)
\(Max (S) = Sup (S)\)
)
//
2: 証明
全体戦略: ステップ1: \(Min (S)\)が存在すると仮定する; ステップ2: \(Min (S) = Inf (S)\)であることを見る; ステップ3: \(Max (S)\)が存在すると仮定する; ステップ4: \(Max (S) = Sup (S)\)であることを見る。
ステップ1:
\(Min (S)\)が存在すると仮定しよう。
ステップ2:
各\(s \in S\)に対して、\(Min (S) \le s\)（それが意味するのは、\(Min (S) = s \text{ または } Min (S) \lt s\)）。
それが含意するのは、\(Min (S) \le' s\)、各\(s \in S\)に対して（それが意味するのは、\(Min (S) = s \text{ または } Min (S) \lt' s\)）。
したがって、\(Min (S) \in Lb (S)\)。
各\(s' \in Lb (S)\)に対して、\(s' \le' Min (S)\)、なぜなら、\(Min (S) \in S\)、それが意味するのは、\(Min (S) = Max (Lb (S)) = Inf (S)\)。
ステップ3:
\(Max (S)\)が存在すると仮定しよう。
ステップ4:
各\(s \in S\)に対して、\(s \le Max (S)\)（それが意味するのは、\(s = Max (S)\text{ or } s \lt Max (S)\)）。
それが含意するのは、\(s \le' Max (S)\)、各\(s \in S\)に対して（それが意味するのは、\(s = Max (S) \text{ または } s \lt' Max (S)\)）。
したがって、\(Max (S) \in Ub (S)\)。
各\(s' \in Ub (S)\)に対して、\(Max (S) \le' s'\)、なぜなら、\(Max (S) \in S\)、それが意味するのは、\(Max (S) = Min (Ub (S)) = Sup (S)\)。
