<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

Data publikacji: 28 mar 2018

Zakres stron: 269 - 281

Otrzymano: 29 lis 2017

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

Słowa kluczowe
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

Data publikacji: 28 mar 2018

Zakres stron: 269 - 281

Otrzymano: 29 lis 2017

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

Słowa kluczoweimplicit 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.

Słowa kluczowe
implicit function theorem, Banach fixed point theorem, Lipschitz continuity