パーシャリーオーダードセット（半順序集合）およびサブセット（部分集合）に対して、もしも、サブセット（部分集合）のインフィマム（下限）がサブセット（部分集合）内に存在する場合、インフィマム（下限）はサブセット（部分集合）のミニマム（最小）であり、もしも、サブセット（部分集合）のサプリマム（上限）がサブセット（部分集合）内に存在する場合、サプリマム（上限）はサブセット（部分集合）のマキシマム（最大）であることの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、パーシャリーオーダードセット（半順序集合）のサブセット（部分集合）のインフィマム（下限）の定義を知っている。
- 読者は、パーシャリーオーダードセット（半順序集合）のサブセット（部分集合）でインデュースト（誘導された）パーシャルオーダリング（半順序）を持つものの定義を知っている。
- 読者は、パーシャリーオーダードセット（半順序集合）のミニマム（最小）の定義を知っている。
- 読者は、パーシャリーオーダードセット（半順序集合）のサブセット（部分集合）のサプリマム（上限）の定義を知っている。
- 読者は、パーシャリーオーダードセット（半順序集合）のマキシマム（最大）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のパーシャリーオーダードセット（半順序集合）および任意のサブセット（部分集合）に対して、もしも、当該サブセット（部分集合）のインフィマム（下限）が当該サブセット（部分集合）内に存在する場合、インフィマム（下限）は当該サブセット（部分集合）のミニマム（最小）であり、もしも、当該サブセット（部分集合）のサプリマム（上限）が当該サブセット（部分集合）内に存在する場合、サプリマム（上限）は当該サブセット（部分集合）のマキシマム（最大）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(S'\): \(\in \{\text{ 全てのパーシャリーオーダードセット（半順序集合）たち }\}\)で、任意のパーシャルオーダリング（半順序）\(\lt'\)を持つもの
\(S\): \(\subseteq S'\)で、インデュースト（誘導された）パーシャルオーダリング（半順序）\(\lt\)を持つもの
//
ステートメント（言明）たち:
(
\(\exists Inf (S) \in S\)
\(\implies\)
\(Inf (S) = Min (S)\)
)
\(\land\)
(
\(\exists Sup (S) \in S\)
\(\implies\)
\(Sup (S) = Max (S)\)
)
//
2: Proof
Whole Strategy: Step 1: suppose that \(Inf (S)\) exists in \(S\); Step 2: see that \(Inf (S) = Min (S)\); Step 3: suppose that \(Sup (S)\) exists in \(S\); Step 4: see that \(Sup (S) = Max (S)\).
Step 1:
Let us suppose that \(Inf (S)\) exists in \(S\).
Step 2:
\(Inf (S) \in S\), by the supposition.
Let \(s \in S \setminus \{Inf (S)\}\) be any.
\(Inf (S) \lt' s\), because \(Inf (S) \in Lb (S)\).
\(Inf (S) \lt s\), by the definition of subset of partially-ordered set with induced partial ordering.
So, \(Inf (S) = Min (S)\)
Step 3:
Let us suppose that \(Sup (S)\) exists in \(S\).
Step 4:
\(Sup (S) \in S\), by the supposition.
Let \(s \in S \setminus \{Sup (S)\}\) be any.
\(s \lt' Sup (S)\), because \(Sup (S) \in Ub (S)\).
\(s \lt Sup (S)\), by the definition of subset of partially-ordered set with induced partial ordering.
So, \(Sup (S) = Max (S)\)
