theorem mp {p q: Prop}: p -> (p -> q) -> q :=
fun hp: p =>
fun hpq: p -> q => hpq p
theorem comm_and {p q: Prop}: (p \and q) -> (q \and p) :=
fun pq: (p \and q) => \< pq.right, pq.left \>
Sはℕの空ではない部分集合とすると、Sには最小元が存在する。
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)が成り立つ。
アイルランド語
語源
古アイルランド語 lenaid < ケルト祖語 *linati < 印欧祖語 *(s)ley-
発音
(マンスター) IPA(?): /lʲan̪ˠ/
(コノート, アルスター) IPA: /l̠ʲanˠ/, /l̠ʲan̪ˠ/
動詞
lean (現在 leanann, 未来 leanfaidh, 動名詞 leanúint, 過去分詞 leanta)
付ついて行いく。従したがう。
Mathematics in Lean、サンプルコードがLean4でコンパイルできん
これ、読むだけにするか
>証明が正しいことを検証できる
その検証が正しいことは確かなの?
検証の検証が必要なのでは?
できるだけ小さくてバグのでる余地のない検証器のカーネルを実装するってのが常套だよ