<abstract xmlns="http://www.w3.org/1999/xhtml"><p> 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.</p></abstract>

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.

Implicit Function Theorem. Part I

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) License.

{"article-title":"Implicit Function Theorem. Part I"}

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...

Implicit Function Theorem. Part I

Publicado en línea: 28 mar 2018

Páginas: 269 - 281

Recibido: 29 nov 2017

DOI: https://doi.org/10.1515/forma-2017-0026

Palabras clave
implicit function theorem, Banach fixed point theorem, Lipschitz continuity

© by Kazuhisa Nakasho

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) License.

Implicit Function Theorem. Part I

Publicado en línea: 28 mar 2018

Páginas: 269 - 281

Recibido: 29 nov 2017

DOI: https://doi.org/10.1515/forma-2017-0026

Palabras claveimplicit function theorem, Banach fixed point theorem, Lipschitz continuity

© by Kazuhisa Nakasho

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) License.

Palabras clave
implicit function theorem, Banach fixed point theorem, Lipschitz continuity