Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/8131
Pełny rekord metadanych
Pole DC | Wartość | Język |
---|---|---|
dc.contributor.author | Nakasho, Kazuhisa | - |
dc.contributor.author | Shidama, Yasunari | - |
dc.date.accessioned | 2019-07-29T08:28:48Z | - |
dc.date.available | 2019-07-29T08:28:48Z | - |
dc.date.issued | 2019 | - |
dc.identifier.citation | Formalized Mathematics, Volume 27, Issue 2, Pages 117 - 131 | - |
dc.identifier.issn | 1426-2630 | - |
dc.identifier.uri | http://hdl.handle.net/11320/8131 | - |
dc.description.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. | - |
dc.language.iso | en | - |
dc.publisher | DeGruyter Open | - |
dc.subject | implicit function theorem | - |
dc.subject | Lipschitz continuity | - |
dc.subject | differentiability | - |
dc.subject | implicit function | - |
dc.subject | 26B10 | - |
dc.subject | 47A05 | - |
dc.subject | 47J07 | - |
dc.subject | 53A07 | - |
dc.subject | 03B35 | - |
dc.title | Implicit Function Theorem. Part II | - |
dc.type | Article | - |
dc.identifier.doi | 10.2478/forma-2019-0013 | - |
dc.description.Affiliation | Kazuhisa Nakasho - Yamaguchi University, Yamaguchi, Japan | - |
dc.description.Affiliation | Yasunari Shidama - Shinshu University, Nagano, Japan | - |
dc.description.references | Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6. | - |
dc.description.references | Bruce K. Driver. Analysis Tools with Applications. Springer, Berlin, 2003. | - |
dc.description.references | Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1. | - |
dc.description.references | Hiroshi Imura, Morishige Kimura, and Yasunari Shidama. The differentiable functions on normed linear spaces. Formalized Mathematics, 12(3):321–327, 2004. | - |
dc.description.references | Kazuhisa Nakasho. Invertible operators on Banach spaces. Formalized Mathematics, 27 (2):107–115, 2019. doi:10.2478/forma-2019-0012. | - |
dc.description.references | Kazuhisa Nakasho, Yuichi Futa, and Yasunari Shidama. Implicit function theorem. Part I. Formalized Mathematics, 25(4):269–281, 2017. doi:10.1515/forma-2017-0026. | - |
dc.description.references | Takaya Nishiyama, Keiji Ohkubo, and Yasunari Shidama. The continuous functions on normed linear spaces. Formalized Mathematics, 12(3):269–275, 2004. | - |
dc.description.references | Hiroyuki Okazaki, Noboru Endou, and Yasunari Shidama. Cartesian products of family of real linear spaces. Formalized Mathematics, 19(1):51–59, 2011. doi:10.2478/v10037-011-0009-2. | - |
dc.description.references | Hideki Sakurai, Hiroyuki Okazaki, and Yasunari Shidama. Banach’s continuous inverse theorem and closed graph theorem. Formalized Mathematics, 20(4):271–274, 2012. doi:10.2478/v10037-012-0032-y. | - |
dc.description.references | Laurent Schwartz. Théorie des ensembles et topologie, tome 1. Analyse. Hermann, 1997. | - |
dc.description.references | Laurent Schwartz. Calcul différentiel, tome 2. Analyse. Hermann, 1997. | - |
dc.identifier.eissn | 1898-9934 | - |
dc.description.volume | 27 | - |
dc.description.issue | 2 | - |
dc.description.firstpage | 117 | - |
dc.description.lastpage | 131 | - |
dc.identifier.citation2 | Formalized Mathematics | - |
dc.identifier.orcid | 0000-0003-1110-4342 | - |
Występuje w kolekcji(ach): | Formalized Mathematics, 2019, Volume 27, Issue 2 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma_2019_27_2_004.pdf | 272,89 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL