かじもとにっき

ゆるふわなおはなしをかきます

2項関係(15)

定義 univalent relation*1

\begin{array}{l}R:{\mathop{\rm univalent}\nolimits} \\\mathop  \equiv \limits^{def} \forall x \in X.\forall y,z \in Y.xRy \wedge xRz \Rightarrow y = z\\ \equiv {R^T} \circ R \subseteq {\rm I}\\ \equiv R \circ \overline {\rm I}  \subseteq \overline R \end{array}

定理

R:{\mathop{\rm univalent}\nolimits}  \wedge S:{\mathop{\rm univalent}\nolimits}  \Rightarrow (R \circ S):{\mathop{\rm univalent}\nolimits}

証明

{R^T} \circ R \subseteq {\rm I}{S^T} \circ S \subseteq {\rm I}を仮定すると、
{(R \circ S)^T} \circ (R \circ S) = {S^T} \circ {R^T} \circ R \circ S \subseteq {S^T} \circ S \subseteq {\rm I}

定理

R \subseteq S \wedge S:{\mathop{\rm univalent}\nolimits}  \wedge R \circ \Omega  \supseteq S \circ \Omega  \Rightarrow R = S*2

証明

R \subseteq S{S^T} \circ S \subseteq {\rm I}S \circ \Omega  \subseteq R \circ \Omegaを仮定すると、
\begin{array}{l}S\\ = S \circ \Omega  \cap S\\ \subseteq R \circ \Omega  \cap S\\ \subseteq (R \cap S \circ \Omega ) \circ (\Omega  \cap {R^T} \circ S)\\ \subseteq R \circ {R^T} \circ S\\ \subseteq R \circ {S^T} \circ S\\ \subseteq R\end{array}

定理 分配律

R:{\mathop{\rm univalent}\nolimits}  \Rightarrow R \circ (P \cap Q) = R \circ P \cap R \circ Q

証明

{R^T} \circ R \subseteq {\rm I}と仮定すると、
\begin{array}{l}R \circ P \cap R \circ Q\\ \subseteq (R \cap R \circ Q \circ {P^T}) \circ (P \cap {R^T} \circ R \circ Q)\\ \subseteq R \circ (P \cap Q)\end{array}

定理

R \circ P \cap Q \subseteq (R \cap Q \circ {P^T}) \circ P
R \circ P \cap Q \subseteq R \circ (P \cap {R^T} \circ Q)

証明

どちらもDedekind律から直ちに出る。

定理

P:{\mathop{\rm univalent}\nolimits}  \Rightarrow R \circ P \cap Q = (R \cap Q \circ {P^T}) \circ P

定理

R:{\mathop{\rm univalent}\nolimits}  \Rightarrow R \circ \overline S  = R \circ \Omega  \cap \overline {R \circ S}

証明

{R^T} \circ R \subseteq {\rm I}と仮定。

\overline S  \subseteq \OmegaよりR \circ \overline S  \subseteq R \circ \Omega

\begin{array}{l}R \circ \overline S  \subseteq \overline {R \circ S} \\ \equiv {R^T} \circ R \circ S \subseteq S\\ \Leftarrow {R^T} \circ R \subseteq {\rm I} \wedge S \subseteq S\\ \equiv {\mathop{\rm true}\nolimits} \end{array}

よってR \circ \overline S  \subseteq R \circ \Omega  \cap \overline {R \circ S}

また、
\begin{array}{l}R \circ \Omega  \cap \overline {R \circ S}  \subseteq R \circ \overline S \\ \equiv \Omega  \subseteq \overline {R \circ \Omega }  \cup R \circ S \cup R \circ \overline S \\ \equiv \Omega  \subseteq \overline {R \circ \Omega }  \cup R \circ (S \cup \overline S )\\ \equiv \Omega  \subseteq \overline {R \circ \Omega }  \cup R \circ \Omega \\ \equiv \Omega  \subseteq \Omega \\ \equiv {\mathop{\rm true}\nolimits} \end{array}

定理

R:{\mathop{\rm univalent}\nolimits}  \Rightarrow \overline {R \circ S}  = \overline {R \circ \Omega }  \cup R \circ \overline S

*1:partial function

*2:R \circ \Omega  \supseteq S \circ \Omega  \equiv {\mathop{\rm def}\nolimits} R \supseteq {\mathop{\rm def}\nolimits} S