<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

Pubblicato online: 20 lug 2019

Pagine: 117 - 131

Accettato: 27 mag 2019

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

Parole chiave
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

Pubblicato online: 20 lug 2019

Pagine: 117 - 131

Accettato: 27 mag 2019

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

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

Parole chiave
implicit function theorem, Lipschitz continuity, differentiability, implicit function