Lean 総合スレッド (11ﾚｽ)
上下前次1-新
抽出解除 必死ﾁｪｯｶｰ(本家) (べ) ﾚｽ栞 あぼーん
10: 11/21(木)20:17 ID:9NACk29m(1) AAS
Sをℕの部分集合とする。自然数nに対して、命題P_S(n)を以下のように定める:
Sがnを含むならば、Sは最小元を持つ。
すべての自然数nに対してP_S(n)が成り立つことを、数学的帰納法で証明する。
まず、P_S(0)は正しい。なぜならば、Sの要素は自然数であるので、0以上であるからである。
0以上n以下の自然数kについてP_S(k)が成り立つと仮定し、P_S(k+1)を示す。
Sがn+1を含むとする。
Sがn以下の自然数を含むならば、仮定よりSは最小元をもつ。
そうでなければ、n+1がSの最小元である。
よって、P_S(k+1)が成り立つ。
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.160s*