The Function Differential, Partial Differentiation, Grads, Divergence, And Curl In Mizar

The Mizar system is a computer language system, which is a formalization of mathematical knowledge and information, with the function of proving, verifying and typesetting, possessing of Mizar Mathematical Library.This dissertation introduces mathematics mechanization, describes the history of Mizar system and how to write articles in Mizar language. The article discusses the theory of partial differentiation and higher-order partial derivatives, dissertates the correlative properties as well as grads, divergence, curl in Mizar system, also provides the corresponding proof and calculation methods. The automatic reasoning and proving process, which are related to the above aspects, have been embodied in Mizar Mathematical Library. At the same time, the dissertation has been published in《Formalized Mathematics》(Poland). The main contents are summarized as follows:1. In Mizar language project, the differential coefficient of multivariable function is realized, by dint of this the partial differentiation of real binary functions is defined, their operation together with the relation between differential coefficient and continuity are discussed.2. For the first time the second-order partial differentiation is formalized concisely in Mizar system , the interrelated operation formulas and theorems are also given.3. The correlative theorems are extended in 3-dimensional euclidian space, the definition of grads, divergence, curl as well as theorems and formulas are formalized in Mizar system for the first time.