2026.03.15
https://gyazo.com/60449eadc4739ad81bd65bdbfe9a683c
前：
2026.03.14
後：
2026.03.16
#日報
見ている
ハイスコアガール
おもしろいなーー
メモ
例えば
$ A \implies \exists n. \mathcal{P}_A(n)
と
$ \lnot A \implies \exists n. \mathcal{P}_{\lnot A}(n)
というプロシージャがあることがわかっていたとき
$ (A \lor \lnot A)
から
$ A
または
$ \lnot A
は出せるか？
Harropの補題
っぽいことを
Lean
で形式化出来るか？