a3
Proverバグ？解消のため次を準備しておきます。set\({\tt n}\).x … \(v \in \{ x_{1} , \cdots , x_{\tt n} \} \Rightarrow \mathrm{P} \Longleftrightarrow ( v = x_{1} \Rightarrow \mathrm{P} ) , \cdots , ( v = x_{\tt n} \Rightarrow \mathrm{P} )\)
a4
Cap. … \(x \in \bigcap \mathcal{X} \Longleftrightarrow \begin{cases} \exists X \, X \in \mathcal{X} \Rightarrow x \in \bigcap \mathcal{X} \\ \not\exists X \, X \in \mathcal{X} \Rightarrow x \in \bigcap \mathcal{X} \end{cases}\)b2
Rel. … \(\text{Rel} = \{ R \mid \forall p \in R . \exists x , y . p = \langle x , y \rangle \}\)ap. … \(y = f ( x ) \Longleftrightarrow \begin{cases} x \in \triangleleft! ( f ) \Rightarrow \langle x , y \rangle \in f \\ x \notin \triangleleft! ( f ) \Rightarrow y = f ( x ) \end{cases}\)
b3
->.. … \(X \to Y = \{ f \in \text{mapon} ( X ) \mid \forall x \in X . f ( x ) \in Y \}\) \(\blacktriangleleft\)mto. … \(p \in x \mathop{{\cdot}{\to}} y \Longleftrightarrow p = \langle x , y \rangle\) \(\blacktriangleleft\)
->I. … \(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid \forall y \, ! x \, \langle x , y \rangle \in f \}\) \(\blacktriangleleft\)
->S. … \(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \forall y \in Y . \exists x \, \langle x , y \rangle \in f \}\) \(\blacktriangleleft\)
->S.'' … \(X \stackrel{\rm S}\to Y = \{ f \in \text{mapon} ( X ) \mid \triangleright ( f ) = Y \}\) \(\blacktriangleleft\)
b4
=#. … \(X \stackrel{\#}= Y \Longleftrightarrow \exists f \, f \in X \stackrel{\rm IS}\to Y\) \(\blacktriangleleft\)le#. … \(X \stackrel{\#}\le Y \Longleftrightarrow \exists f \, f \in X \stackrel{\rm I}\to Y\) \(\blacktriangleleft\)
c1
0. … \(x \in 0 \Longleftrightarrow {\perp}\) \(\blacktriangleleft\)suc. … \(x \in n \textit{+1} \Longleftrightarrow x \in n \mathbin{\rm o\!r} x = n\) \(\blacktriangleleft\)
Ind. … \(\text{Ind} = \{ M \mid 0 \in M , \forall m \in M . m \textit{+1} \in M \}\) \(\blacktriangleleft\)
\Mi1 … \(\forall n \in \mathbb{M} . n \textit{+1} \in \mathbb{M}\) \(\blacktriangleleft\)
<\Mi … \(n \in \mathbb{M} \Longrightarrow n \subset \mathbb{M}\) \(\blacktriangleleft\)
\(\mathbb{M}\)が推移的であることを示します。機械は細い論理も平気で通します！
<\Ml … \(m \in n \in \mathbb{M} \Longrightarrow m \subsetneq n\) \(\blacktriangleleft\)
<\Mr … \( m , n \in \mathbb{M} , m \subsetneq n \Longrightarrow m \in n\) \(\blacktriangleleft\)
\({\tt n}\). … \(x \in {\tt n} \Longleftrightarrow x = 0 \mathbin{\rm o\!r} x = 1 \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} x = {\tt n\,{\text -}\,1}\) \(\blacktriangleleft\)
c2
+\M:0 … \(m \in \mathbb{M} , n \in \mathbb{M} \Longrightarrow m + n \in \mathbb{M}\) \(\blacktriangleleft\)*\M:0 … \(m \in \mathbb{M} , n \in \mathbb{M} \Longrightarrow m \cdot n \in \mathbb{M}\) \(\blacktriangleleft\)
b4
mapon/c. … \(\text{mapon:c} ( \mathcal{X} ) = \{ f \in \mathcal{X} \to \bigcup \mathcal{X} \mid \forall X , x \, ( \langle X , x \rangle \in f \Rightarrow x \in X ) \}\) \(\blacktriangleleft\)dp. … \(x \in \Pi X \Longleftrightarrow \begin{cases} X \in \text{Map} \Longrightarrow x \in \text{mapon} ( \triangleleft ( X ) ) , \forall \lambda \in \triangleleft ( X ) . x _ \lambda \in X _ \lambda X \notin \text{Map} \Longrightarrow x \in X \end{cases}\) \(\blacktriangleleft\)