https://twitter.com/kinaba のログ (twilog の方が便利です。)
| The Averaging Trick and the Černý Conjecture http://dx.doi.org/10.1007/978-3-642-14455-4_38 こんなシンプルな未解決問題があるのか。そして引用28本中25本が一つの[～]に入ってるすごい… | |
| SpringerのLNCSの最新刊ページ見てたら MFCS&CSL http://mfcsl2010.fi.muni.cz/ もこの時期だということに気づいた。ひー読みたい論文が多すぎる。 | |
| Increase2 解いたけど、実は http://twitter.com/kikx/status/21212649080 http://twitter.com/ksknac/status/21448577890 この辺りの意味がまったくわかってない…完全に別問題の感覚でいました | |
| B を消さない apply A in B と、A を消す generalize A と、rewrite H が失敗したら勝手にrewrite <-H するのが欲しいことがわかった。あと apply False_ind. → 怒られる → contradict H. intro. | |
| @kikx Increasing Sequence の方は定理のステートメントにexistsが無いので、証明中に使う存在命題を全部 { _ } で書くだけであとは力押しだー、とやっちゃったんですが、これexistsが出るライブラリ定理とか使うと綺麗に書けたりするんですかね…mmm |