<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

Online veröffentlicht: 20. Juli 2019

Seitenbereich: 117 - 131

Akzeptiert: 27. Mai 2019

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

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

Online veröffentlicht: 20. Juli 2019

Seitenbereich: 117 - 131

Akzeptiert: 27. Mai 2019

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

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

Schlüsselwörter
implicit function theorem, Lipschitz continuity, differentiability, implicit function