Lean 総合スレッド (13ﾚｽ)
上下前次1-新

---

1: 11/21(木)16:30 ID:f0B7SpBa(1) AAS
Lean 総合スレッド

---

2: 11/21(木)17:16 ID:UM7SSSK3(1/3) AAS
Leen

---

3: 11/21(木)17:16 ID:UM7SSSK3(2/3) AAS
Reen

---

4: 11/21(木)17:41 ID:kV2krKdg(1) AAS
これは良いツールだ

---

5: 11/21(木)18:08 ID:Bx74CtUo(1) AAS
theorem mp {p q: Prop}: p -> (p -> q) -> q :=
　fun hp: p =>
　　fun hpq: p -> q => hpq p

---

6: 11/21(木)18:36 ID:LbV7eOsa(1) AAS
theorem comm_and {p q: Prop}: (p \and q) -> (q \and p) :=
　fun pq: (p \and q) => \< pq.right, pq.left \>

---

7: 11/21(木)18:58 ID:UA5Mrabs(1) AAS
依存型すげー

---

8: 11/21(木)19:08 ID:JRU6FbM9(1) AAS
でも、証明は自分で考えなきゃいけないんでしょ

---

9: 11/21(木)19:57 ID:cP6jPjOP(1) AAS
Sはℕの空ではない部分集合とすると、Sには最小元が存在する。

---

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)が成り立つ。

---

11: 11/21(木)20:36 ID:UM7SSSK3(3/3) AAS
learn

---

12: 11/22(金)12:56 ID:0Nx2foHP(1) AAS
なんか役にたつの？

---

13: 11/22(金)14:46 ID:5LNKUSu3(1) AAS
証明が正しいことを検証できる

---

上下前次1-新書関写板覧索設栞歴

---

ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ

---

ぬこの手 ぬこTOP 0.166s*