Appendix B

A Compilation of Mizar Library Theorems


In this chapter, article theorems and definitions that are frequently phrased in the Mizar library are compactly edited and listed. Please look at the original abstract file if necessary.


Table of Listed Articles

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(only the main theorems are listed.).

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(only the main theorems are listed)).