<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

Online veröffentlicht: 28. März 2018

Seitenbereich: 269 - 281

Eingereicht: 29. Nov. 2017

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

Schlüsselwörter
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

Online veröffentlicht: 28. März 2018

Seitenbereich: 269 - 281

Eingereicht: 29. Nov. 2017

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

Schlüsselwörterimplicit 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.

Schlüsselwörter
implicit function theorem, Banach fixed point theorem, Lipschitz continuity