有限集合

$n$ に関する数学的帰納法で、「すべての $m\in\mathbb{N}$ について、単射 $I_m\to I_n$ があれば $m\le n$」を示す。
$n=0$ のとき：$I_0=\emptyset$ への写像があるのは始域が空のときだけなので、$I_m=\emptyset$、すなわち $m=0\le0$ である。
$n$ で成り立つとし、単射 $f\colon I_m\to I_{n+1}$ があるとする。$m=0$ なら $m\le n+1$ である。$m\ge1$ とする。$I_{n+1}$ の 2 元 $f(m)$ と $n+1$ を入れ替え、他の元を動かさない写像を $\tau\colon I_{n+1}\to I_{n+1}$ とする（$f(m)=n+1$ なら $\tau$ は恒等写像）。$\tau$ は全単射なので $\tau\circ f$ は単射であり、$\tau(f(m))=n+1$ である。$1\le k\le m-1$ なら $k\ne m$ なので単射性から $\tau(f(k))\ne n+1$、すなわち $\tau(f(k))\in I_n$ である。したがって $g(k):=\tau(f(k))$ は単射 $g\colon I_{m-1}\to I_n$ を定める。帰納法の仮定により $m-1\le n$、すなわち $m\le n+1$ である。$\square$

1. 全単射 $h\colon I_m\to I_n$ があれば、$h$ と逆写像 $h^{-1}$ はどちらも単射なので、lem-finset-injection により $m\le n$ かつ $n\le m$、よって $m=n$ である。逆に $m=n$ なら恒等写像がある。
2. 全単射 $\varphi\colon I_m\to X$、$\psi\colon I_n\to X$ があれば、$\psi^{-1}\circ\varphi\colon I_m\to I_n$ は全単射なので、1 により $m=n$ である。
3. $\varphi\colon I_n\to X$ と $h\colon X\to Y$ が全単射なら、$h\circ\varphi\colon I_n\to Y$ は全単射なので $Y$ は有限で $|Y|=n=|X|$ である。$X,Y$ が有限で $|X|=|Y|=n$ なら、全単射 $\varphi\colon I_n\to X$、$\psi\colon I_n\to Y$ から全単射 $\psi\circ\varphi^{-1}\colon X\to Y$ が得られる。$\square$

まず $X=I_n$ の場合を $n$ に関する帰納法で示す。$n=0$ なら $A=\emptyset=I_0$ で主張は成り立つ。
$n$ で成り立つとし、$A\subset I_{n+1}$ とする。$A':=A\setminus\{n+1\}$ は $I_n$ の部分集合なので、帰納法の仮定により有限で、$k:=|A'|\le n$、全単射 $h\colon I_k\to A'$ がある。

• $n+1\notin A$ のとき：$A=A'$ なので $A$ は有限で $|A|=k\le n< n+1$ である。特に $|A|\ne n+1$ であり、$A\ne I_{n+1}$ とも整合する。
• $n+1\in A$ のとき：$h$ を $k+1\mapsto n+1$ で延長した写像 $I_{k+1}\to A$ は全単射なので（$n+1\notin A'$ に注意）、$A$ は有限で $|A|=k+1\le n+1$ である。$|A|=n+1$ なら $k=n$ なので、帰納法の仮定により $A'=I_n$、したがって $A=I_n\cup\{n+1\}=I_{n+1}$ である。
  一般の場合、全単射 $\varphi\colon I_n\to X$ をとり、$B:=\varphi^{-1}(A)\subset I_n$ とおく。$\varphi$ を $B$ に制限すると全単射 $B\to A$ になる。今示したことから $B$ は有限で $|B|\le n$ であり、cor-finset-well-defined の 3 により $A$ も有限で $|A|=|B|\le n=|X|$ である。$|A|=n$ なら $|B|=n$ なので $B=I_n$、よって $A=\varphi(I_n)=X$ である。$\square$

1. $f$ は $X$ から像 $f(X)\subset Y$ への全単射を与える。prop-finset-subset により $f(X)$ は有限で $|f(X)|\le|Y|$ であり、cor-finset-well-defined の 3 により $X$ は有限で $|X|=|f(X)|$ である。
2. 全単射 $\varphi\colon I_n\to X$ をとる。$y\in f(X)$ に対し、$\{k\in I_n\mid f(\varphi(k))=y\}$ は空でないので最小元 $k_y$ をもつ（数学的帰納法 の記事の定理「自然数の整列原理」）。$s(y):=\varphi(k_y)$ とおくと $f(s(y))=y$ なので、$s\colon f(X)\to X$ は単射である。1 により $f(X)$ は有限で $|f(X)|\le|X|$ である。$f$ が全射なら $f(X)=Y$ である。
3. $|X|=|Y|=n$ とする。$f$ が単射なら、1 の証明のとおり $|f(X)|=|X|=|Y|$ なので、prop-finset-subset により $f(X)=Y$、すなわち $f$ は全射である。$f$ が全射で単射でないとし、$x\ne x'$、$f(x)=f(x')$ とする。$X':=X\setminus\{x'\}$ への $f$ の制限も全射なので、2 により $n=|Y|\le|X'|$ であるが、$X'$ は $X$ の真部分集合なので prop-finset-subset により $|X'|< n$ となり矛盾する。$\square$

1. $a:=|A|$、$b:=|B|$ とし、全単射 $\alpha\colon I_a\to A$、$\beta\colon I_b\to B$ をとる。$\gamma\colon I_{a+b}\to A\cup B$ を、$1\le k\le a$ なら $\gamma(k)=\alpha(k)$、$a< k\le a+b$ なら $\gamma(k)=\beta(k-a)$ と定める。$\gamma$ は $A$ と $B$ の元をすべて値にとるので全射である。前半どうし・後半どうしでは $\alpha,\beta$ の単射性から値が異なり、前半の値は $A$、後半の値は $B$ に属して $A\cap B=\emptyset$ なので、前半と後半でも値が異なる。よって $\gamma$ は全単射であり、$|A\cup B|=a+b$ である。
2. $B\setminus A\subset B$ と $A\cap B\subset A$ は prop-finset-subset により有限である。$A\cup B$ は交わらない $A$ と $B\setminus A$ の和集合であり、$B$ は交わらない $B\setminus A$ と $A\cap B$ の和集合である。1 を 2 回使うと
   $$ |A\cup B|=|A|+|B\setminus A|,\qquad |B|=|B\setminus A|+|A\cap B| $$
   となり、2 式から $|B\setminus A|$ を消去すれば主張を得る。$\square$

1. $|B|=n$ に関する帰納法で示す。$n=0$ なら $B=\emptyset$ なので $A\times B=\emptyset$（集合 の記事の命題「直積の空性」）で、$|A\times B|=0=|A|\cdot0$ である。$|B|=n+1$ とし、全単射 $\psi\colon I_{n+1}\to B$ をとって $b:=\psi(n+1)$、$B':=\psi(I_n)$ とおく。$|B'|=n$ であり、$B$ は交わらない $B'$ と $\{b\}$ の和集合である。したがって $A\times B$ は交わらない $A\times B'$ と $A\times\{b\}$ の和集合である。帰納法の仮定により $|A\times B'|=|A|\cdot n$ であり、$(x,b)\mapsto x$ は $A\times\{b\}$ から $A$ への全単射なので $|A\times\{b\}|=|A|$ である。prop-finset-union の 1 により $|A\times B|=|A|\cdot n+|A|=|A|\cdot(n+1)$ である。
2. $|A|=n$ に関する帰納法で示す。$n=0$ なら $\mathcal{P}(\emptyset)=\{\emptyset\}$ で元の個数は $1=2^0$ である。$|A|=n+1$ とし、1 と同様に $A$ を $|A'|=n$ の $A'$ と $A'$ に属さない 1 元 $a$ の和集合に分ける。$A$ の部分集合 $T$ は、$a\notin T$ なら $T\subset A'$ であり、$a\in T$ なら $T=S\cup\{a\}$、$S:=T\setminus\{a\}\subset A'$ と書ける。写像 $\mathcal{P}(A')\to\{T\subset A\mid a\in T\}$、$S\mapsto S\cup\{a\}$ は、$a\notin S$ なので $S=(S\cup\{a\})\setminus\{a\}$ と復元でき、全単射である。よって $\mathcal{P}(A)$ は交わらない $\mathcal{P}(A')$ と $\{T\subset A\mid a\in T\}$ の和集合で、帰納法の仮定と prop-finset-union の 1 により $|\mathcal{P}(A)|=2^n+2^n=2^{n+1}$ である。$\square$