Maxima で綴る数学の旅

紙と鉛筆の代わりに、数式処理システムMaxima / Macsyma を使って、数学を楽しみましょう

-数学- Lean4のお勉強 シュレーダー=ベルンシュタインの定理

第4章「集合と関数」の最後のセクションシュレーダー=ベルンシュタインの定理のLean4による証明です。

初めてこの定理をきちんとした形で知りました。集合論の濃度に関する基本的な定理です。

定理:$\alpha, \beta$を集合、$f:\alpha \rightarrow\beta, g:\beta\rightarrow\alpha$が両方とも単射である時、$\alpha$から$\beta$への全単射がある。

集合の濃度に関して$|\alpha| \ge |\beta|, |\beta|\ge|\alpha|$のとき$|\alpha|=|\beta|$が成り立つということで確かに基本的です。

 

$A\subseteq \alpha$をうまく構成して$h$を、

$h(x)=\begin{cases}
f(x) & (x\in A)\\
g^{-1}(x) & (x \notin A)
\end{cases}$

と定義しこの$h:\alpha\rightarrow\beta$が全単射になることを示します。

 

$A$の定義は次のとおりです。

$A_0=\alpha \backslash g(\beta)$
$A_{n+1}=g(f(A_n))$
$A=\bigcup_{n}A_{n}$

 

証明を形式化するためにはまず証明を理解する必要があります。この章ではまず定理の説明と上記$A$の構成、それを使った言葉による証明が紹介されます。$A$及び$h$の定義をから以下のことがわかります。

$\alpha\rightarrow\beta$の全射を構成するにあたりまず$g^{-1}$が使えない$\alpha$の部分集合$A_0=\alpha\backslash g(\beta)$では$f$を使います。$A_0$を起点として$A_{n+1}=g(f(A_n))$で$f$を使う領域を広げていきます。いっぱいまで広げた$A=\bigcup_{n}A_{n}$では$f$が使えるので$f$を使い、それ以外の領域$\alpha\backslash A$では$g^{-1}$を使うと、望むような全単射が構成できるわけです。

 

$h$が単射であることを示すためには$h(x_1)=h(x_2)$を仮定して$x_1=x_2$を導けば良いです。また$h$が全射であることを示すには任意の$y\in\beta$について$h(x)=y$となる$x$ が存在することを言えば良いです。$A$や$h$をLean4でうまく定義できれば$h$が単射であること、全射であることは形式的に示すことができそうです。

 

実際の形式証明は全部で100行くらいです。$h$の単射性を示す際に$x_1\in A \lor x_2\in A$の場合とそうでない場合への場合分けをby_caseタクティクで記述しているのですが、これは自分には難易度が高いです。もう1つwlogタクティクを使って対称性のある議論をまとめているのですがこれも結構難易度が高いです。それ以外は集合と関数で知ったやり方でほぼ証明を進めることができます。

 

無事に全てのsorryをタクティクに置き換えることができて、形式証明を完成させることができました!