Cite

In this article, we formalize in Mizar [1], [3] the existence and uniqueness part of the implicit function theorem. In the first section, some composition properties of Lipschitz continuous linear function are discussed. In the second section, a definition of closed ball and theorems of several properties of open and closed sets in Banach space are described. In the last section, we formalized the existence and uniqueness of continuous implicit function in Banach space using Banach fixed point theorem. We referred to [7], [8], and [2] in this formalization.

eISSN:
1898-9934
ISSN:
1426-2630
Idioma:
Inglés
Calendario de la edición:
4 veces al año
Temas de la revista:
Computer Sciences, other, Mathematics, General Mathematics