リニアリーオーダードセット（線形順序集合）およびサブセット（部分集合）に対して、セット（集合）の要素はサブセット（部分集合）のサプリマム（上限）である、もしも、要素がサブセット（部分集合）の各要素に等しいかそれより大きく、要素より小さいセット（集合）の各要素に対して、より大きいサブセット（部分集合）の要素がある場合、そしてその場合に限って、ことの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、リニアリーオーダードセット（線形順序集合）の定義を知っている。
- 読者は、パーシャリーオーダードセット（半順序集合）のサブセット（部分集合）のサプリマム（上限）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のリニアリーオーダードセット（線形順序集合）および任意のサブセット（部分集合）に対して、当該セット（集合）の任意の要素は当該サブセット（部分集合）のサプリマム（上限）である、もしも、当該要素が当該サブセット（部分集合）の各要素に等しいかそれより大きく、当該要素より小さい当該セット（集合）の各要素に対して、より大きい当該サブセット（部分集合）のある要素がある場合、そしてその場合に限って、という命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(S'\): \(\in \{\text{ 全てのリニアリーオーダードセット（線形順序集合）たち }\}\)で、任意のリニアオーダリング（線形順序）\(\lt'\)を持つもの
\(S\): \(\subseteq S'\)
\(s'\): \(\in S'\)
//
ステートメント（言明）たち:
\(s' = Sup (S)\)
\(\iff\)
\((\forall s \in S (s \le s')) \land (\forall s'' \in S' \text{ で、以下を満たすもの、つまり、 } s'' \lt' s' (\exists s \in S (s'' \lt' s)))\)
//
2: 注
本命題は、\(S = \emptyset\)である時も成立する（空虚に）。
3: 証明
全体戦略: ステップ1: \(s' = Sup (S)\)であると仮定する; ステップ2: \((\forall s \in S (s \le s')) \land (\forall s'' \in S' \text{ で、以下を満たすもの、つまり、 } s'' \lt' s' (\exists s \in S (s'' \lt' s)))\)であることを見る; ステップ3: \((\forall s \in S (s \le s')) \land (\forall s'' \in S' \text{ で、以下を満たすもの、つまり、 } s'' \lt' s' (\exists s \in S (s'' \lt' s)))\)であると仮定する; ステップ4: \(s' = Sup (S)\)であることを見る; ステップ5: 本命題は、\(S = \emptyset\)である時も成立することをチェックする。
ステップ1:
\(s' = Sup (S)\)であると仮定しよう。
ステップ2:
\(s \in S\)を任意のものとしよう。
\(Sup (S) \in Ub (S)\)であるから、\(s \le s'\)、アッパーバウンド（上限）たちのセット（集合）の定義によって。
したがって、\(\forall s \in S (s \le s')\)。
\(s'' \in S'\)を、\(s'' \lt' s'\)を満たす任意のものとしよう。
\(s'' \lt' s\)を満たす\(s \in S\)は無かったと仮定しよう。
それが意味することになるのは、各\(s \in S\)に対して、\(s \le' s''\)、なぜなら、\(S'\)はリニアリーオーダード（線形順序付き）であった。
それが意味することになるのは、\(s'' \in Ub (S)\)。
しかし、\(s'' \lt' s'\)であったから、\(s'\)は\(Ub (S)\)のミニマム（最小）ではなかった、\(s' = Sup (S)\)に反する矛盾。
したがって、\(s'' \lt' s\)を満たすある\(s \in S\)がある。
ステップ3:
\((\forall s \in S (s \le s')) \land (\forall s'' \in S' \text{ で、以下を満たすもの、つまり、 } s'' \lt' s' (\exists s \in S (s'' \lt' s)))\)であると仮定しよう。
ステップ4:
\(s' \in Ub (S)\)、アッパーバウンド（上限）たちのセット（集合）の定義によって。
\(s'\)は\(Ub (S)\)のミニマム（最小）でなかったと仮定しよう。
それが意味することになるのは、\(s' \le' s''\)が成立しないある\(s'' \in Ub (S)\)があったということ。
\(S'\)はリニアリーオーダード（線形順序付き）であったから、\(s'' \lt' s'\)。
仮定によって、\(s'' \lt' s\)を満たすある\(s \in S\)があることになる、それが意味することになるのは、\(s \le' s''\)は成立しないということ。
それが意味することになるのは、\(s'' \notin Ub (S)\)、\(s'' \in Ub (S)\)に反する矛盾。
したがって、\(s'\)は\(Ub (S)\)のミニマム（最小）である。
したがって、\(s' = Sup (S)\)。
ステップ5:
本命題は、\(S = \emptyset\)である時も成立することをチェックしよう。
\(Ub (S) = S'\)。
\(Sup (S) = Min (Ub (S)) = Min (S')\)。
したがって、もしも、\(s' = Sup (S)\)である場合、\(\forall s \in S (s \le s')\)は空虚に成立する、そして、\(\forall s'' \in S' \text{ で、以下を満たすもの、つまり、 } s'' \lt' s' (\exists s \in S (s'' \lt' s))\)は空虚に成立する: そうした\(s''\)は無い。
もしも、\((\forall s \in S (s \le s')) \land (\forall s'' \in S' \text{ で、以下を満たすもの、つまり、 } s'' \lt' s' (\exists s \in S (s'' \lt' s)))\)が成立する場合、そうした\(s''\)は無い、なぜなら、そうでなければ、\(\exists s \in S (s'' \lt' s)\)は成立しないことになる、したがって、\(s' = Min (S') = Sup (S)\)。
