In this article we formalized the Fréchet differentiation. It is defined as a generalization of the differentiation of a real-valued function of a single real variable to more general functions whose domain and range are subsets of normed spaces [14].
[11] Hiroshi Imura, Morishige Kimura, and Yasunari Shidama. The differentiable functions on normed linear spaces. Formalized Mathematics, 12(3):321-327, 2004.
[12] Takaya Nishiyama, Keiji Ohkubo, and Yasunari Shidama. The continuous functions on normed linear spaces. Formalized Mathematics, 12(3):269-275, 2004.
[13] Jan Popiołek. Real normed space. Formalized Mathematics, 2(1):111-115, 1991.
[14] Laurent Schwartz. Cours d’analyse. Hermann, 1981.[WoS]
[15] Yasunari Shidama. Banach space of bounded linear operators. Formalized Mathematics, 12(1):39-48, 2004.
[16] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990.
[17] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990.
[18] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
[19] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990.
[20] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990.
[21] Hiroshi Yamazaki and Yasunari Shidama. Algebra of vector functions. Formalized Mathematics, 3(2):171-175, 1992.