https://ncatlab.org/nlab/show/coherence+law https://ncatlab.org/nlab/show/coherence+theorem+for+monoidal+categories https://ncatlab.org/nlab/show/coherence+theorem https://ncatlab.org/nlab/show/coherence+theorem#ListOfTheorems https://ncat…

ブログ記事のカテゴリーについては： 半形式証明スクリプト https://m-hiyama-memo.hatenablog.jp/archive/category/%E5%8D%8A%E5%BD%A2%E5%BC%8F%E8%A8%BC%E6%98%8E%E3%82%B9%E3%82%AF%E3%83%AA%E3%83%97%E3%83%88 言葉遣い： 公理は要請〈demand〉する。 …

KさんがLeanで証明を書く練習をしているので、それに関してのメモ。このメモ自体は檜山による。関数(引数) = 関数'(引数') という命題を示す根拠として、 A = B がassumeされていて、f(A) = f(B) を示したいなら、congr_arg 規則を使う。 f = g がassumeされ…

「数学の常識・非常識—由緒正しい TEX 入力法」 http://www.math.tohoku.ac.jp/tmj/oda_tex.pdf から注意すべき点を抜粋。 次元のdimは全体をローマン。 線形群の名前はイタリックでよい。 など。 外微分のdは、数学ではイタリック、物理ではローマン。 定理…