全単射

第4章「集合と関数」の最後のセクションはシュレーダー＝ベルンシュタインの定理のLean4による証明です。 初めてこの定理をきちんとした形で知りました。集合論の濃度に関する基本的な定理です。 定理：$\alpha, \beta$を集合、$f:\alpha \rightarrow\beta, g:\beta\rightarrow\alpha$が両方とも単射である時、$\alpha$から$\beta$への全単射がある。 集合の濃度に関して$|\alpha| \ge |\beta|, |\beta|\ge|\alpha|$のとき$|\alpha|=|\beta|$が成り立つということで確かに基本的です…