有向集合の同値な言い換え
順序集合における有向性、任意の２元は必ず何かの元に同時に抑えられるという定義だが、これはしばしば「向きつけられている」と表現される。
非空集合$I$上の二項関係$\lesssim_I\subseteq I\times I$が有向前順序であるとは
を満たすこと。非空集合と有向前順序の組$(I,\lesssim_I)$を非空有向前順序集合（または有向集合）という。
これがどういうことかは この記事 の冒頭に書いた。適当に言うと十分先が２通り以上解釈できるケースを排除するという制約だ。だけどなんだか釈然としない。。そんな人のために、以下の変形ができるという規約だと思ってしまおう！という方法があるのでメモ。
前順序集合$(I,\lesssim_I)$が上に有向であることは以下と同値：
一つずつ順番に見ていこう。
十分先で全部$P$が成り立つとは、
\begin{equation} (\exists i_0\in I)(\forall i\in I)[i\gtrsim_I i_0\Longrightarrow P(i)]
\end{equation}
何か以上が全部$P$を満たすということ。さらに、$P(i)\Longleftrightarrow i\in P$と同一視して集合論表記にしよう。すると、さっきの条件はこのように言い換えられる
$(\Longleftarrow)$は必ず成り立つので、$(\Longrightarrow)$だけにしても同値。
ということで、定理１を証明してみよう！
\begin{eqnarray} &(\exists i_0\in I)(\forall i\gtrsim_I i_0)[i\in P\cap Q]\\ \Longleftrightarrow&(\exists i_0\in I)(\forall i\gtrsim_I i_0)[i\gtrsim_I i_1,i_2]& \end{eqnarray}を得る。
*1 十分先で全部$P$に入るとは、$\text{id}:I\rightarrow I$というネットのeventuallyフィルターを用いて$P\in\mathcal{E}_\text{id}$と書ける。ということは、上に有向'は「$\mathcal{E}_\text{id}$が共通部分について閉じている」ことと同値になる。eventuallyフィルターはフィルターなんだから当たり前なんじゃないか？と思うかもしれないが、それは添字が上に有向だから。添字の有向性を排せばeventuallyフィルターはフィルターになるとは限らない。
