パターンがあるものは、3分間・URIテンプレート - 檜山正幸のキマイラ飼育記 で示す。 http://webmizar.cs.shinshu-u.ac.jp/mmlfe/current/ http://mizar.org/version/current/html/{小文字ID}.html http://mizar.org/JFM/pdf/{小文字ID}.pdf http://fm.miza…

http://mizar.org/version/current/html/ hidden tarski_0 tarski xboole_0 xboole_1 enumset1 xfamily xregular xtuple_0 zfmisc_1 subset_1 setfam_1 relat_1 fanct_1 ordinal1 ordinal2 ordinal3 relat_2 wellord1 wellord2 funct_2 funct_3 funct_4 grun…

適当な訳語がない。等力かな。集合が等力とは、1:1対応があること、基数が等しいこと。

$MIZFILE/mml.larにすべてのアーティクルの名前（list of articlesだろう）。mml.vctにすべてのシンボル。

environは地獄だ。environはノービスには書けない。エキスパートが書いてあげるのが前提みたいだ。スライド http://mizar.org/cicm_tutorial/mizar.pdf "Mizar Hands-on Tutorial" by Adam Naumowicz, Artur Korni lowicz, Adam Grabowski (July 29, 2016) …