Lean 総合スレッド (11ﾚｽ)
Lean 総合スレッド http://rio2016.5ch.net/test/read.cgi/math/1732174248/
上
下
前
次
1-
新
通常表示
512ﾊﾞｲﾄ分割
ﾚｽ栞
1: １３２人目の素数さん [] 2024/11/21(木) 16:30:48.75 ID:f0B7SpBa Lean 総合スレッド http://rio2016.5ch.net/test/read.cgi/math/1732174248/1
2: １３２人目の素数さん [sage] 2024/11/21(木) 17:16:22.87 ID:UM7SSSK3 Leen http://rio2016.5ch.net/test/read.cgi/math/1732174248/2
3: １３２人目の素数さん [sage] 2024/11/21(木) 17:16:47.95 ID:UM7SSSK3 Reen http://rio2016.5ch.net/test/read.cgi/math/1732174248/3
4: １３２人目の素数さん [] 2024/11/21(木) 17:41:23.96 ID:kV2krKdg これは良いツールだ http://rio2016.5ch.net/test/read.cgi/math/1732174248/4
5: １３２人目の素数さん [] 2024/11/21(木) 18:08:04.33 ID:Bx74CtUo theorem mp {p q: Prop}: p -> (p -> q) -> q := fun hp: p => fun hpq: p -> q => hpq p http://rio2016.5ch.net/test/read.cgi/math/1732174248/5
6: １３２人目の素数さん [] 2024/11/21(木) 18:36:09.01 ID:LbV7eOsa theorem comm_and {p q: Prop}: (p \and q) -> (q \and p) := fun pq: (p \and q) => \< pq.right, pq.left \> http://rio2016.5ch.net/test/read.cgi/math/1732174248/6
7: １３２人目の素数さん [] 2024/11/21(木) 18:58:09.88 ID:UA5Mrabs 依存型すげー http://rio2016.5ch.net/test/read.cgi/math/1732174248/7
8: １３２人目の素数さん [] 2024/11/21(木) 19:08:42.56 ID:JRU6FbM9 でも、証明は自分で考えなきゃいけないんでしょ http://rio2016.5ch.net/test/read.cgi/math/1732174248/8
9: １３２人目の素数さん [] 2024/11/21(木) 19:57:38.51 ID:cP6jPjOP Sはℕの空ではない部分集合とすると、Sには最小元が存在する。 http://rio2016.5ch.net/test/read.cgi/math/1732174248/9
10: １３２人目の素数さん [] 2024/11/21(木) 20:17:28.08 ID:9NACk29m 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)が成り立つ。 http://rio2016.5ch.net/test/read.cgi/math/1732174248/10
11: １３２人目の素数さん [sage] 2024/11/21(木) 20:36:20.97 ID:UM7SSSK3 learn http://rio2016.5ch.net/test/read.cgi/math/1732174248/11
上
下
前
次
1-
新
書
関
写
板
覧
索
設
栞
歴
ｽﾚ情報
赤ﾚｽ抽出
画像ﾚｽ抽出
歴の未読ｽﾚ
AAｻﾑﾈｲﾙ
Google検索
Wikipedia
ぬこの手
ぬこTOP
0.003s