{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,27]],"date-time":"2026-05-27T06:03:16Z","timestamp":1779861796780,"version":"3.53.1"},"reference-count":11,"publisher":"Walter de Gruyter GmbH","issue":"2","license":[{"start":{"date-parts":[[2019,7,1]],"date-time":"2019-07-01T00:00:00Z","timestamp":1561939200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,7,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats: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.<\/jats:p>\n                  <jats: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.<\/jats:p>","DOI":"10.2478\/forma-2019-0013","type":"journal-article","created":{"date-parts":[[2019,7,22]],"date-time":"2019-07-22T05:30:34Z","timestamp":1563773434000},"page":"117-131","source":"Crossref","is-referenced-by-count":2,"title":["Implicit Function Theorem. Part II"],"prefix":"10.2478","volume":"27","author":[{"given":"Kazuhisa","family":"Nakasho","sequence":"first","affiliation":[{"name":"Yamaguchi University , Yamaguchi , Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yasunari","family":"Shidama","sequence":"additional","affiliation":[{"name":"Shinshu University , Nagano , Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"374","published-online":{"date-parts":[[2019,7,20]]},"reference":[{"key":"2026052705130499008_j_forma-2019-0013_ref_001_w2aab3b7b3b1b6b1ab1ab1Aa","doi-asserted-by":"crossref","unstructured":"[1] Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, and Karol P\u0105k. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9\u201332, 2018. doi:10.1007\/s10817-017-9440-6.10.1007\/s10817-017-9440-6604425130069070","DOI":"10.1007\/s10817-017-9440-6"},{"key":"2026052705130499008_j_forma-2019-0013_ref_002_w2aab3b7b3b1b6b1ab1ab2Aa","unstructured":"[2] Bruce K. Driver. Analysis Tools with Applications. Springer, Berlin, 2003."},{"key":"2026052705130499008_j_forma-2019-0013_ref_003_w2aab3b7b3b1b6b1ab1ab3Aa","doi-asserted-by":"crossref","unstructured":"[3] Adam Grabowski, Artur Korni\u0142owicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191\u2013198, 2015. doi:10.1007\/s10817-015-9345-1.10.1007\/s10817-015-9345-1","DOI":"10.1007\/s10817-015-9345-1"},{"key":"2026052705130499008_j_forma-2019-0013_ref_004_w2aab3b7b3b1b6b1ab1ab4Aa","unstructured":"[4] Hiroshi Imura, Morishige Kimura, and Yasunari Shidama. The differentiable functions on normed linear spaces. Formalized Mathematics, 12(3):321\u2013327, 2004."},{"key":"2026052705130499008_j_forma-2019-0013_ref_005_w2aab3b7b3b1b6b1ab1ab5Aa","doi-asserted-by":"crossref","unstructured":"[5] Kazuhisa Nakasho. Invertible operators on Banach spaces. Formalized Mathematics, 27 (2):107\u2013115, 2019. doi:10.2478\/forma-2019-0012.10.2478\/forma-2019-0012","DOI":"10.2478\/forma-2019-0012"},{"key":"2026052705130499008_j_forma-2019-0013_ref_006_w2aab3b7b3b1b6b1ab1ab6Aa","doi-asserted-by":"crossref","unstructured":"[6] Kazuhisa Nakasho, Yuichi Futa, and Yasunari Shidama. Implicit function theorem. Part I. Formalized Mathematics, 25(4):269\u2013281, 2017. doi:10.1515\/forma-2017-0026.10.1515\/forma-2017-0026","DOI":"10.1515\/forma-2017-0026"},{"key":"2026052705130499008_j_forma-2019-0013_ref_007_w2aab3b7b3b1b6b1ab1ab7Aa","unstructured":"[7] Takaya Nishiyama, Keiji Ohkubo, and Yasunari Shidama. The continuous functions on normed linear spaces. Formalized Mathematics, 12(3):269\u2013275, 2004."},{"key":"2026052705130499008_j_forma-2019-0013_ref_008_w2aab3b7b3b1b6b1ab1ab8Aa","doi-asserted-by":"crossref","unstructured":"[8] Hiroyuki Okazaki, Noboru Endou, and Yasunari Shidama. Cartesian products of family of real linear spaces. Formalized Mathematics, 19(1):51\u201359, 2011. doi:10.2478\/v10037-011-0009-2.10.2478\/v10037-011-0009-2","DOI":"10.2478\/v10037-011-0009-2"},{"key":"2026052705130499008_j_forma-2019-0013_ref_009_w2aab3b7b3b1b6b1ab1ab9Aa","doi-asserted-by":"crossref","unstructured":"[9] Hideki Sakurai, Hiroyuki Okazaki, and Yasunari Shidama. Banach\u2019s continuous inverse theorem and closed graph theorem. Formalized Mathematics, 20(4):271\u2013274, 2012. doi:10.2478\/v10037-012-0032-y.10.2478\/v10037-012-0032-y","DOI":"10.2478\/v10037-012-0032-y"},{"key":"2026052705130499008_j_forma-2019-0013_ref_010_w2aab3b7b3b1b6b1ab1ac10Aa","unstructured":"[10] Laurent Schwartz. Th\u00e9orie des ensembles et topologie, tome 1. Analyse. Hermann, 1997."},{"key":"2026052705130499008_j_forma-2019-0013_ref_011_w2aab3b7b3b1b6b1ab1ac11Aa","unstructured":"[11] Laurent Schwartz. Calcul diff\u00e9rentiel, tome 2. Analyse. Hermann, 1997."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/27\/2\/article-p117.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2019-0013","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,27]],"date-time":"2026-05-27T05:13:15Z","timestamp":1779858795000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2019-0013"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,1]]},"references-count":11,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2019,7,20]]},"published-print":{"date-parts":[[2019,7,1]]}},"alternative-id":["10.2478\/forma-2019-0013"],"URL":"https:\/\/doi.org\/10.2478\/forma-2019-0013","relation":{},"ISSN":["1898-9934","1426-2630"],"issn-type":[{"value":"1898-9934","type":"electronic"},{"value":"1426-2630","type":"print"}],"subject":[],"published":{"date-parts":[[2019,7,1]]}}}