[12] Hiroshi Imura, Morishige Kimura, and Yasunari Shidama. The differentiable functions on normed linear spaces. Formalized Mathematics, 12(3):321-327, 2004.
[13] Jarosław Kotowicz. Partial functions from a domain to a domain. Formalized Mathematics, 1(4):697-702, 1990.
[14] Jarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269-272, 1990.
[15] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223-230, 1990.
[16] Jan Popiołek. Real normed space. Formalized Mathematics, 2(1):111-115, 1991.
[17] Konrad Raczkowski and Paweł Sadowski. Real function differentiability. Formalized Mathematics, 1(4):797-801, 1990.
[18] Laurent Schwartz. Cours d'analyse. Hermann, 1981.[WoS]
[19] Yasunari Shidama. Banach space of bounded linear operators. Formalized Mathematics, 12(1):39-48, 2004.
[20] Andrzej Trybulec. Subsets of complex numbers. To appear in Formalized Mathematics.
[21] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9-11, 1990.
[22] Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575-579, 1990.
[23] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990.
[24] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
[25] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990.
[26] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990.
[27] Hiroshi Yamazaki, Yoshinori Fujisawa, and Yatsuka Nakamura. On replace function and swap function for finite sequences. Formalized Mathematics, 9(3):471-474, 2001.
[28] Hiroshi Yamazaki and Yasunari Shidama. Algebra of vector functions. Formalized Mathematics, 3(2):171-175, 1992.
[6] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.