Lean 総合スレッド (17ﾚｽ)
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
12: １３２人目の素数さん [] 2024/11/22(金) 12:56:29.20 ID:0Nx2foHP なんか役にたつの？ http://rio2016.5ch.net/test/read.cgi/math/1732174248/12
13: １３２人目の素数さん [] 2024/11/22(金) 14:46:13.04 ID:5LNKUSu3 証明が正しいことを検証できる http://rio2016.5ch.net/test/read.cgi/math/1732174248/13
14: １３２人目の素数さん [] 2024/11/22(金) 17:21:30.64 ID:t/qYZ5zF >>13 IUTを検証するつもりか？ http://rio2016.5ch.net/test/read.cgi/math/1732174248/14
15: １３２人目の素数さん [sage] 2024/11/22(金) 19:50:59.34 ID:QPgxUom8 アイルランド語 語源 古アイルランド語 lenaid < ケルト祖語 *linati < 印欧祖語 *(s)ley- 発音 (マンスター) IPA(?): /lʲan̪ˠ/ (コノート, アルスター) IPA: /l̠ʲanˠ/, /l̠ʲan̪ˠ/ 動詞 lean (現在 leanann, 未来 leanfaidh, 動名詞 leanúint, 過去分詞 leanta) 付ついて行いく。従したがう。 http://rio2016.5ch.net/test/read.cgi/math/1732174248/15
16: １３２人目の素数さん [] 2024/11/22(金) 23:54:29.10 ID:7D6cqAMi 痩せ細ってるって意味だぞ http://rio2016.5ch.net/test/read.cgi/math/1732174248/16
17: １３２人目の素数さん [] 2024/11/23(土) 07:20:51.82 ID:VRgZy8E5 >>14 お前がやれ http://rio2016.5ch.net/test/read.cgi/math/1732174248/17
上
下
前
次
1-
新
書
関
写
板
覧
索
設
栞
歴
ｽﾚ情報
赤ﾚｽ抽出
画像ﾚｽ抽出
歴の未読ｽﾚ
AAｻﾑﾈｲﾙ
Google検索
Wikipedia
ぬこの手
ぬこTOP
0.169s*