Real Vector Space and Related Notions

Pole DC	Wartość	Język
dc.contributor.author	Nakasho, Kazuhisa	-
dc.contributor.author	Okazaki, Hiroyuki	-
dc.contributor.author	Shidama, Yasunari	-
dc.date.accessioned	2022-01-04T06:38:42Z	-
dc.date.available	2022-01-04T06:38:42Z	-
dc.date.issued	2021	-
dc.identifier.citation	Formalized Mathematics, Volume 29, Issue 3, Pages 117-127	pl
dc.identifier.issn	1426–2630	-
dc.identifier.uri	http://hdl.handle.net/11320/12388	-
dc.description	This study was supported in part by JSPS KAKENHI Grant Numbers 17K00182 and 20K19863.	pl
dc.description.abstract	In this paper, we discuss the properties that hold in finite dimensional vector spaces and related spaces. In the Mizar language [1], [2], variables are strictly typed, and their type conversion requires a complicated process. Our purpose is to formalize that some properties of finite dimensional vector spaces are preserved in type transformations, and to contain the complexity of type transformations into this paper. Specifically, we show that properties such as algebraic structure, subsets, finite sequences and their sums, linear combination, linear independence, and affine independence are preserved in type conversions among TOP-REAL(n), REAL-NS(n), and n-VectSp over F Real. We referred to [4], [9], and [8] in the formalization.	pl
dc.language.iso	en	pl
dc.publisher	DeGruyter Open	pl
dc.subject	real vector space	pl
dc.subject	topological space	pl
dc.subject	normed spaces	pl
dc.title	Real Vector Space and Related Notions	pl
dc.type	Article	pl
dc.rights.holder	© 2021 University of Białymstoku	pl
dc.rights.holder	CC-BY-SA License ver. 3.0 or later	pl
dc.identifier.doi	10.2478/forma-2021-0012	-
dc.description.Affiliation	Kazuhisa Nakasho - Yamaguchi University, Yamaguchi, Japan	pl
dc.description.Affiliation	Hiroyuki Okazaki - Shinshu University, Nagano, Japan	pl
dc.description.Affiliation	Yasunari Shidama - Shinshu University, Nagano, 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	Miyadera Isao. Functional Analysis. Riko-Gaku-Sya, 1972.	pl
dc.description.references	Robert Milewski. Associated matrix of linear map. Formalized Mathematics, 5(3):339–345, 1996.	pl
dc.description.references	Karol Pąk. Basic properties of the rank of matrices over a field. Formalized Mathematics, 15(4):199–211, 2007. doi:10.2478/v10037-007-0024-5.	pl
dc.description.references	Karol Pąk. Linear map of matrices. Formalized Mathematics, 16(3):269–275, 2008. doi:10.2478/v10037-008-0032-0.	pl
dc.description.references	Laurent Schwartz. Theorie des ensembles et topologie, tome 1. Analyse. Hermann, 1997.	pl
dc.description.references	Kosaku Yosida. Functional Analysis. Springer, 1980.	pl
dc.identifier.eissn	1898-9934	-
dc.description.volume	29	pl
dc.description.issue	3	pl
dc.description.firstpage	117	pl
dc.description.lastpage	127	pl
dc.identifier.citation2	Formalized Mathematics	pl
Występuje w kolekcji(ach):	Formalized Mathematics, 2021, Volume 29, Issue 3

Pliki w tej pozycji:

Plik	Opis	Rozmiar	Format
10.2478_forma-2021-0012.pdf		284,25 kB	Adobe PDF	Otwórz

Pokaż uproszczony widok rekordu Zobacz statystyki