半順序と狭義半順序の相互変換式

$ \begin{dcases}\forall a,b\in X:a\le b\iff a<b\lor a=b\\<\text{は狭義半順序}\end{dcases}\iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\le\text{は半順序}\end{dcases}

証明

各論理式の同値関係がわかるよう、いくつかの補題に分けて示す

補題①

$ \begin{dcases}\forall a,b\in X:a\le b\iff a<b\lor a=b\\\forall a\in X:\lnot(a<a)\end{dcases}\iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\forall a\in X:a\le a\end{dcases}

証明

$ \begin{dcases}\forall a,b\in X:a\le b\iff a<b\lor a=b\\\forall a\in X:\lnot(a<a)\end{dcases}

$ \iff\begin{dcases}\forall a,b\in X:a\le b\implies a<b\lor a=b\\\forall a,b\in X:a<b\lor a=b\implies a\le b\\\forall a,b\in X:a<b\implies a\neq b\end{dcases}

$ \iff\begin{dcases}\forall a,b\in X:a\le b\land a\neq b\implies a<b\\\forall a,b\in X:a<b\implies a\le b\\\forall a,b\in X:a=b\implies a\le b\\\forall a,b\in X:a<b\implies a\neq b\end{dcases}

$ \iff\begin{dcases}\forall a,b\in X:a\le b\land a\neq b\implies a<b\\\forall a,b\in X:a<b\implies a\le b\land a\neq b\\\forall a,b\in X:a=b\implies a\le b\end{dcases}

$ \iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\forall a,b\in X:a=b\implies a\le b\end{dcases}

$ \underline{\iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\forall a\in X:a\le a\end{dcases}\quad}_\blacksquare

補題②

$ \begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\forall a,b,c\in X:a<b<c\implies a<c\end{dcases}\iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\forall a,b,c\in X:a\le b\le c\implies a\le c\\\forall a,b\in X:a\le b\le a\implies a=b\end{dcases}

証明

$ \begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\forall a,b,c\in X:a<b<c\implies a<c\end{dcases}

$ \iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\forall a,b,c\in X:\begin{dcases}a\le b\le c\\a\neq b\neq c\end{dcases}\implies a\le c\\\forall a,b,c\in X:\begin{dcases}a\le b\le c\\a\neq b\neq c\end{dcases}\implies a\neq c\end{dcases}

$ \iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\forall a,b,c\in X:\begin{dcases}a\le b\le c\\a\neq b\neq c\end{dcases}\implies a\le c\\\forall a,b,c\in X:\begin{dcases}a\le b\le c\\a=b\lor b=c\end{dcases}\implies a\le c\\\forall a,b,c\in X:a\le b\le c\implies(a\neq b\neq c\implies a\neq c)\end{dcases}

$ \because a\le b=c\implies a\le c

$ \because a=b\le c\implies a\le c

$ \iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\forall a,b,c\in X:a\le b\le c\implies a\le c\\\forall a,b,c\in X:a\le b\le c\implies(a=c\implies a=b\lor b=c)\end{dcases}

$ \underline{\iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\forall a,b,c\in X:a\le b\le c\implies a\le c\\\forall a,b\in X:a\le b\le a\implies a=b\end{dcases}\quad}_\blacksquare

①、②より題意を示す

$ \begin{dcases}\forall a,b\in X:a\le b\iff a<b\lor a=b\\<\text{は狭義半順序}\end{dcases}

$ \iff\begin{dcases}\forall a,b\in X:a<b\implies a\le b\land a\neq b\\\forall a\in X:a\le a\\\forall a,b,c\in X:a<b<c\implies a<c\end{dcases}

$ \iff\begin{dcases}\forall a,b\in X:a<b\implies a\le b\land a\neq b\\\forall a\in X:a\le a\\\forall a,b,c\in X:a\le b\le c\implies a\le c\\\forall a,b\in X:a\le b\le a\implies a=b\end{dcases}

$ \underline{\iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\le\text{は半順序}\end{dcases}\quad}