<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

Published Online: Mar 28, 2018

Page range: 269 - 281

Received: Nov 29, 2017

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

Keywords
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

Published Online: Mar 28, 2018

Page range: 269 - 281

Received: Nov 29, 2017

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

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

Keywords
implicit function theorem, Banach fixed point theorem, Lipschitz continuity