上限
supermum
常に存在するとは限らない
存在するなら唯一に決まる
定義
$ dが$ Xの上界のうち最小の元であるとき、$ dを$ Xの上限と呼ぶ 前提
$ Dは半順序集合
$ Xは、$ Dの部分集合
$ d\in D
$ X \sqsubseteq dである
つまり、以下2つの条件を満たす元$ d\in Dのこと
$ X \sqsubseteq d
$ ^\forall a\in D\; [X\sqsubseteq a \Rightarrow d \sqsubseteq a]
いろいろな表記
$ Xの上限をどう表記するか
順序を$ \leで表す時は、以下のように書くことが多い
$ \sup X
$ \sup_{\le} X
$ \lor X
順序を$ \sqsubseteqで表す時は、同じノリで以下のように書く
$ \sup_\sqsubseteq
$ \sqcup X
ref 横内『プログラム意味論』.icon
$ \lor Xとか$ \sqcup Xってイメージと逆だなmrsekut.icon
上に突き抜けるイメージをすればいいのか
上限は極限のイメージ
$ \mathbb{R}の部分集合$ P=\{3,3.1,3.14,3.141,\cdots\}を考えた時、
$ \sqcup P = \piになる
定理
参考