1 順序対

1.1 順序対

word(ss,s)F … \(\mathsf{pr}\)
abbr … \(\langle X , Y \rangle\) ≈ \(\mathsf{pr} ( X , Y )\)

word(s,s) … \(\triangleleft\)  \(\triangleright\)
◁. … \(\triangleleft \langle x , y \rangle = x\)
▷. … \(\triangleright \langle x , y \rangle = y\)
pr:0 … \(\langle x_{0} , y_{0} \rangle = \langle x_{1} , y_{1} \rangle \Longleftrightarrow x_{0} = x_{1} , y_{0} = y_{1}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

次のwordは一般的には \({\rm dom}\) \({\rm im}\)
word(s,s)F … \({\hat\triangleleft}\)  \({\hat\triangleright}\)
^◁. … \({\hat\triangleleft} ( R ) = \{ x \mid \exists y \, \langle x , y \rangle \in R \}\)
^▷. … \({\hat\triangleright} ( R ) = \{ y \mid \exists x \, \langle x , y \rangle \in R \}\)

1.2 直積、関係

word(cc,c) … \(\times\)
^^pr_. … \(X \times Y = \{ \langle x , y \rangle \mid x \in X , y \in Y \}\)
word(ss,s) … \(\times\)
^^pr. … \([\times] \stackrel{\star\!\star}{=} [\times]\)
\([\times] \stackrel{\star\!\star}{=} [\stackrel{\text{^^}}{\mathsf{pr}}]\) \(\blacktriangleleft\) \(\mathbb{W}.\)

word(,c) … \(\text{Rel}\)
Rel. … \(\text{Rel} = \{ R \mid R \subset \mathbb{V} \times \mathbb{V} \}\)
Rel.' … \(\text{Rel} = \{ R \mid R \subset {\hat\triangleleft} ( R ) \times {\hat\triangleright} ( R ) \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
Rel.. … \(\text{Rel} = \{ R \mid \forall x \in R . x = \langle \triangleleft x , \triangleright x \rangle \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(R \in \text{Rel} \Longrightarrow {\hat\triangleleft} ( R ) = \; \stackrel{\text{^}}{\triangleleft} \! ( R ) , {\hat\triangleright} ( R ) = \; \stackrel{\text{^}}{\triangleright} \! ( R )\) \(\blacktriangleleft\) \(\mathbb{W}.\)

1.3 代入

word(s,s)F … \({\hat\triangleleft!}\)
^◁!. … \({\hat\triangleleft!} ( R ) = \{ x \mid \exists! y \langle x , y \rangle \in R \}\)

word(ss,s) … ap
ap. … \(x \in {\hat\triangleleft!} ( f ) \Longrightarrow y = f ( x ) \Leftrightarrow \langle x , y \rangle \in f\)
ap:0 … \(x \in {\hat\triangleleft!} ( f ) \Longrightarrow \langle x , f ( x ) \rangle \in f\) \(\blacktriangleleft\) \(\mathbb{W}.\)

word(ss,s) … *^ap
*^ap. … \(R ( A ) = \{ y \mid \exists x \in A . \langle x , y \rangle \in R \}\)
*^ap:0 … \(A \subset {\hat\triangleleft!} ( f ) \Longrightarrow f ( A ) = \{ f ( a ) \mid a \in A \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

1.4 対の入れ替え、逆関係

word(s,s) … \(^\leftrightarrow\)
sw. … \(\langle x , y \rangle ^\leftrightarrow = \langle y , x \rangle\)
sw:I … \(\langle x , y \rangle ^\leftrightarrow \, \! ^\leftrightarrow = \langle x , y \rangle\) \(\blacktriangleleft\) \(\mathbb{W}.\)

次のwordは一般的には \(^{-1}\)
word(s,s) … \(^{\hat\leftrightarrow}\)
^sw. … \([^{\hat\leftrightarrow}] \stackrel{\star}{=} \; [\stackrel{\text{^}}{^\leftrightarrow}]\)
^sw:0 … \(R \subset X \times Y \Longrightarrow R ^{\hat\leftrightarrow} \subset Y \times X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
^sw:I … \(R \in \text{Rel} \Longrightarrow R ^{\hat\leftrightarrow} \, \! ^{\hat\leftrightarrow} = R\) \(\blacktriangleleft\) \(\mathbb{W}.\)

1.5 関係の合成

word(ss,s) … \(\circ\)
∘. … \(S \circ R = \{ \langle x , z \rangle \mid \exists y \, ( \langle x , y \rangle \in R , \langle y , z \rangle \in S ) \}\)
∘:0 … \(R \subset X \times Y , S \subset Y \times Z \Longrightarrow S \circ R \subset X \times Z\) \(\blacktriangleleft\) \(\mathbb{W}.\)
∘:A … \(R , S , T \in \text{Rel} \Longrightarrow ( T \circ S ) \circ R = T \circ ( S \circ R )\) \(\blacktriangleleft\) \(\mathbb{W}.\)
∘:X … \(R , S \in \text{Rel} \Longrightarrow ( R \circ S ) ^{\hat\leftrightarrow} = S ^{\hat\leftrightarrow} \circ R ^{\hat\leftrightarrow}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
∘ap … \(x \in {\hat\triangleleft!} ( f ) , f ( x ) \in {\hat\triangleleft!} ( g ) \Longrightarrow ( g \circ f ) ( x ) = g ( f ( x ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(( \wp ( X \times X ) , [\circ] ) :\underline{2}\mathsf{A}\) \(\blacktriangleleft\) \(\mathbb{W}.\)