{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T11:04:39Z","timestamp":1774868679006,"version":"3.50.1"},"reference-count":10,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2025,9,1]],"date-time":"2025-09-01T00:00:00Z","timestamp":1756684800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,9,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats:p>This article formalizes higher-order partial differentiable functions in Mizar: it introduces the concept of partial differentiation for functions between real normed spaces and develops the theory of partial derivatives of arbitrary order. Key results include properties of partial derivatives, their relationship with total derivatives, and criteria for the continuity of higher-order partial derivatives.<\/jats:p>","DOI":"10.2478\/forma-2025-0009","type":"journal-article","created":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T05:00:19Z","timestamp":1767762019000},"page":"103-115","source":"Crossref","is-referenced-by-count":0,"title":["Higher Order Partial Differentiable Functions"],"prefix":"10.2478","volume":"33","author":[{"given":"Kazuhisa","family":"Nakasho","sequence":"first","affiliation":[{"name":"Yamaguchi University Yamaguchi , Japan"}]},{"given":"Yasunari","family":"Shidama","sequence":"additional","affiliation":[{"name":"Karuizawa Hotch 244-1 Nagano , Japan"}]}],"member":"374","published-online":{"date-parts":[[2025,12,31]]},"reference":[{"key":"2026033010152392412_j_forma-2025-0009_ref_001","unstructured":"Nelson Dunford and Jacob T. Schwartz. Linear operators I. Interscience Publ., 1958."},{"key":"2026033010152392412_j_forma-2025-0009_ref_002","doi-asserted-by":"crossref","unstructured":"Noboru Endou and Yasunari Shidama. Differentiation in normed spaces. Formalized Mathematics, 21(2):95\u2013102, 2013. doi:10.2478\/forma-2013-0011.","DOI":"10.2478\/forma-2013-0011"},{"key":"2026033010152392412_j_forma-2025-0009_ref_003","unstructured":"Adam Grabowski, Artur Korni\u0142owicz, and Adam Naumowicz. Mizar in a nutshell. Journal of Formalized Reasoning, 3(2):153\u2013245, 2010."},{"key":"2026033010152392412_j_forma-2025-0009_ref_004","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/s10817-015-9345-1"},{"key":"2026033010152392412_j_forma-2025-0009_ref_005","unstructured":"Isao Miyadera. Functional Analysis. Riko-Gaku-Sya, 1972."},{"key":"2026033010152392412_j_forma-2025-0009_ref_006","doi-asserted-by":"crossref","unstructured":"Kazuhisa Nakasho and Yasunari Shidama. Higher-order differentiation and inverse function theorem in real normed spaces. Formalized Mathematics, 32(1):247\u2013269, 2024. doi:10.2478\/forma-2024-0021.","DOI":"10.2478\/forma-2024-0021"},{"key":"2026033010152392412_j_forma-2025-0009_ref_007","unstructured":"Laurent Schwartz. Th\u00e9orie des ensembles et topologie, tome 1. Analyse. Hermann, 1997."},{"key":"2026033010152392412_j_forma-2025-0009_ref_008","unstructured":"Laurent Schwartz. Calcul diff\u00e9rentiel, tome 2. Analyse. Hermann, 1997."},{"key":"2026033010152392412_j_forma-2025-0009_ref_009","doi-asserted-by":"crossref","unstructured":"Yasunari Shidama. Differentiable functions on normed linear spaces. Formalized Mathematics, 20(1):31\u201340, 2012. doi:10.2478\/v10037-012-0005-1.","DOI":"10.2478\/v10037-012-0005-1"},{"key":"2026033010152392412_j_forma-2025-0009_ref_010","unstructured":"K\u00f4saku Yosida. Functional Analysis. Springer, 1980."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.sciendo.com\/pdf\/10.2478\/forma-2025-0009","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T10:15:30Z","timestamp":1774865730000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.2478\/forma-2025-0009"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,1]]},"references-count":10,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2025,12,31]]},"published-print":{"date-parts":[[2025,9,1]]}},"alternative-id":["10.2478\/forma-2025-0009"],"URL":"https:\/\/doi.org\/10.2478\/forma-2025-0009","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,1]]}}}