Appendix B
Mizar ライブラリ定理集
ここには、Mizarライブラリの中で頻繁に引用されるarticleの定理、定義をコンパクトに編集したものを掲載してあります。適宜、もとの abstract file を参照してください。
掲載 article 一覧表
1. A. Trybulec, Tarski Grothendieck Set Theory.(TARSKI).
2. A. Trybulec, Built-in Concepts.(AXIOMS).
3. Z. Trybulec, H.Swieczkowska,Boolean Properties of Sets.(BOOLE).
4. K. Hryniewiecki, Basic Properties of Real Numbers.(REAL_1).
5. B. Bancerek, The Fundamental Properties of Natural Numbers.(NAT_1).
6. Cz. Bylinski, Functions and Their Basic Properties.(FUNCT_).
7. Z. Trybulec, Properties of Subsets.(SUBSET_1).
8. G. Bancerek, K.Hryniewiecki, Segments of Natural Numbers and
Finite Sequences.(FINSEQ_1).
9. Cz. Bylinski, Functions from a Set to a Set.(FUNCT_2(主要定理のみ掲載)).
10. J. Popiolek, Some Properties of Functions Modul and Signum.(ANAL_1).
11. A. Trybulec, Cz. Bylinski, Some Properties of Real Numbers.
Operations: min, max, square, and square root.(SQUARE_1).
12. A. Kondracki, Equalities and Inequalities in Real Numbers.
Continuation of Real_1(REAL_2(主要定理のみ掲載)).