このテキストは,集合論を題材に,mizarを使った, 数学定理の記述が,実際にどのようになされているか を説明します。
mizarでは,その数学記述言語によって書かれたテキストをarticleと称します。 mizarシステムやそれで使われる数学記述言語の文法については, 中村八束教授著のmizar講義録第3版
http://markun.cs.shinshu-u.ac.jp/kiso/projects2/proofchecker/mizar/Mizar-J/Miz-tit.htm
に説明されています。 また,PC用のmizarシステムのダウンロード,WEB上で使用できる mizarシステムは
http://markun.cs.shinshu-u.ac.jp/kiso/projects2/proofchecker/mizar/index-j.htmlにあります。
このテキストでは,mizarで記述された数学定理のデータベースである
ライブラリ中の集合論についての,基礎的なarticle