Transformation Tools for Real Linear Spaces

Pole DC	Wartość	Język
dc.contributor.author	Nakasho, Kazuhisa	-
dc.date.accessioned	2022-12-30T11:06:12Z	-
dc.date.available	2022-12-30T11:06:12Z	-
dc.date.issued	2022	-
dc.identifier.citation	Formalized Mathematics, Volume 30, Issue 2, Pages 93-98	pl
dc.identifier.issn	1426-2630	-
dc.identifier.uri	http://hdl.handle.net/11320/14265	-
dc.description.abstract	This paper, using the Mizar system [1], [2], provides useful tools for working with real linear spaces and real normed spaces. These include the identification of a real number set with a one-dimensional real normed space, the relationships between real linear spaces and real Euclidean spaces, the transformation from a real linear space to a real vector space, and the properties of basis and dimensions of real linear spaces. We referred to [6], [10], [8], [9] in this formalization.	pl
dc.language.iso	en	pl
dc.publisher	DeGruyter Open	pl
dc.rights	Attribution-ShareAlike 3.0 Unported (CC BY-SA 3.0)	pl
dc.rights.uri	https://creativecommons.org/licenses/by-sa/3.0/	pl
dc.subject	real linear space	pl
dc.subject	real normed space	pl
dc.subject	real Euclidean space	pl
dc.subject	real vector space	pl
dc.title	Transformation Tools for Real Linear Spaces	pl
dc.type	Article	pl
dc.rights.holder	© 2022 The Author(s)	pl
dc.rights.holder	CC BY-SA 3.0 license	pl
dc.identifier.doi	10.2478/forma-2022-0008	-
dc.description.Affiliation	Yamaguchi University, Yamaguchi, Japan	pl
dc.description.references	Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.	pl
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.	pl
dc.description.references	Noboru Endou and Yasunari Shidama. Completeness of the real Euclidean space. Formalized Mathematics, 13(4):577–580, 2005.	pl
dc.description.references	Noboru Endou, Yasunari Shidama, and Keiichi Miyajima. The product space of real normed spaces and its properties. Formalized Mathematics, 15(3):81–85, 2007. doi:10.2478/v10037-007-0010-y.	pl
dc.description.references	Takao Inoué, Adam Naumowicz, Noboru Endou, and Yasunari Shidama. Partial differentiation, differentiation and continuity on n-dimensional real normed linear spaces. Formalized Mathematics, 19(2):65–68, 2011. doi:10.2478/v10037-011-0011-8.	pl
dc.description.references	Miyadera Isao. Functional Analysis. Riko-Gaku-Sya, 1972.	pl
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.	pl
dc.description.references	Laurent Schwartz. Théorie des ensembles et topologie, tome 1. Analyse. Hermann, 1997.	pl
dc.description.references	Laurent Schwartz. Calcul différentiel, tome 2. Analyse. Hermann, 1997.	pl
dc.description.references	Kosaku Yosida. Functional Analysis. Springer, 1980.	pl
dc.identifier.eissn	1898-9934	-
dc.description.volume	30	pl
dc.description.issue	2	pl
dc.description.firstpage	93	pl
dc.description.lastpage	98	pl
dc.identifier.citation2	Formalized Mathematics	pl
dc.identifier.orcid	0000-0003-1110-4342	-
Występuje w kolekcji(ach):	Formalized Mathematics, 2022, Volume 30, Issue 2

Pliki w tej pozycji:

Plik	Opis	Rozmiar	Format
10.2478_forma-2022-0008.pdf		253,87 kB	Adobe PDF	Otwórz

Pokaż uproszczony widok rekordu Zobacz statystyki

Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL