Lean 総合スレッドat MATHLean 総合スレッド - 暇つぶし2ch■コピペモード□スレを通常表示□オプションモード□このｽﾚｯﾄﾞのURL■項目テキスト3:１３２人目の素数さん 24/11/21 17:16:47.95 UM7SSSK3.net Reen 4:１３２人目の素数さん 24/11/21 17:41:23.96 kV2krKdg.net これは良いツールだ 5:１３２人目の素数さん 24/11/21 18:08:04.33 Bx74CtUo.net theorem mp {p q: Prop}: p -> (p -> q) -> q := fun hp: p => fun hpq: p -> q => hpq p 6:１３２人目の素数さん 24/11/21 18:36:09.01 LbV7eOsa.net theorem comm_and {p q: Prop}: (p \and q) -> (q \and p) := fun pq: (p \and q) => \< pq.right, pq.left \> 7:１３２人目の素数さん 24/11/21 18:58:09.88 UA5Mrabs.net 依存型すげー 8:１３２人目の素数さん 24/11/21 19:08:42.56 JRU6FbM9.net でも、証明は自分で考えなきゃいけないんでしょ 9:１３２人目の素数さん 24/11/21 19:57:38.51 cP6jPjOP.net Sはℕの空ではない部分集合とすると、Sには最小元が存在する。 10:１３２人目の素数さん 24/11/21 20:17:28.08 9NACk29m.net 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)が成り立つ。 次ページ最新レス表示レスジャンプ類似スレ一覧スレッドの検索話題のニュースおまかせリストオプションしおりを挟むスレッドに書込スレッドの一覧暇つぶし2ch