集合の等濃度の定義

以下は,二つの集合$X,Y$の間に,双射(一対一,かつ,上への写像）が存在するとき, 「$X,Y$の濃度が等しい」$equipotent$と定義すること表しています。

 definition let X,Y;
  pred X,Y are_equipotent means
    ex Z st
       (for x st x in X ex y st y in Y & [x,y] in Z) &
       (for y st y in Y ex x st x in X & [x,y] in Z) &
        for x,y,z,u st [x,y] in Z & [z,u] in Z holds x = z iff y = u;
 end;

すなわち, 任意の$X,Y$に対して, これらが,等濃度である（$equipotent$である） とは

$$\begin{eqnarray*} &&(\exists Z) \\ &&\{ (\forall x :x \in X)(\exists y )(y \i... ...n Z \ and \ [z,u] \in Z) ( x = z \Leftrightarrow y = u) \} \end{eqnarray*}$$

が成り立つことを言います。