<abstract xmlns="http://www.w3.org/1999/xhtml"><p>In this article, we formalize differentiability of implicit function theorem in the Mizar system [3], [1]. In the first half section, properties of Lipschitz continuous linear operators are discussed. Some norm properties of a direct sum decomposition of Lipschitz continuous linear operator are mentioned here.</p><p>In the last half section, differentiability of implicit function in implicit function theorem is formalized. The existence and uniqueness of implicit function in [6] is cited. We referred to [10], [11], and [2] in the formalization.</p></abstract>

In this article, we formalize differentiability of implicit function theorem in the Mizar system [3], [1]. In the first half section, properties of Lipschitz continuous linear operators are discussed. Some norm properties of a direct sum decomposition of Lipschitz continuous linear operator are mentioned here.In the last half section, differentiability of implicit function in implicit function theorem is formalized. The existence and uniqueness of implicit function in [6] is cited. We referred to [10], [11], and [2] in the formalization.

Implicit Function Theorem. Part II

Formalized Mathematics

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

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

In this article, we formalize differentiability of implicit function theorem in the Mizar system [3], [1]. In the first half section, properties of Lipschitz...

Implicit Function Theorem. Part II

Data publikacji: 20 lip 2019

Zakres stron: 117 - 131

Przyjęty: 27 maj 2019

DOI: https://doi.org/10.2478/forma-2019-0013

Słowa kluczowe
implicit function theorem, Lipschitz continuity, differentiability, implicit function

© 2019 Kazuhisa Nakasho et al., published by Sciendo

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Implicit Function Theorem. Part II

Data publikacji: 20 lip 2019

Zakres stron: 117 - 131

Przyjęty: 27 maj 2019

DOI: https://doi.org/10.2478/forma-2019-0013

Słowa kluczoweimplicit function theorem, Lipschitz continuity, differentiability, implicit function

© 2019 Kazuhisa Nakasho et al., published by Sciendo

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Słowa kluczowe
implicit function theorem, Lipschitz continuity, differentiability, implicit function