The 3-Fold Product Space of Real Normed Spaces and its Properties

Pole DC	Wartość	Język
dc.contributor.author	Okazaki, Hiroyuki	-
dc.contributor.author	Nakasho, Kazuhisa	-
dc.date.accessioned	2022-07-25T07:12:02Z	-
dc.date.available	2022-07-25T07:12:02Z	-
dc.date.issued	2021	-
dc.identifier.citation	Formalized Mathematics, Volume 29, Issue 4, Pages 241-248	pl
dc.identifier.issn	1426-2630	-
dc.identifier.uri	http://hdl.handle.net/11320/13668	-
dc.description.abstract	In this article, we formalize in Mizar [1], [2] the 3-fold product space of real normed spaces for usefulness in application fields such as engineering, although the formalization of the 2-fold product space of real normed spaces has been stored in the Mizar Mathematical Library [3]. First, we prove some theorems about the 3-variable function and 3-fold Cartesian product for preparation. Then we formalize the definition of 3-fold product space of real linear spaces. Finally, we formulate the definition of 3-fold product space of real normed spaces. We referred to [7] and [6] in the 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	3-fold product spaces	pl
dc.subject	linear spaces	pl
dc.subject	normed spaces	pl
dc.title	The 3-Fold Product Space of Real Normed Spaces and its Properties	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-0022	-
dc.description.Affiliation	Hiroyuki Okazaki - Shinshu University, Nagano, Japan	pl
dc.description.Affiliation	Kazuhisa Nakasho, 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-817.	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, 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	Artur Korniłowicz. Compactness of the bounded closed subsets of Ε²т. Formalized Mathematics, 8(1):61–68, 1999.	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	Michael Read and Barry Simon. Functional Analysis (Methods of Modern Mathematical Physics). Academic Press, 1980.	pl
dc.description.references	Kosaku Yosida. Functional Analysis. Springer, 1980.	pl
dc.identifier.eissn	1898-9934	-
dc.description.volume	29	pl
dc.description.issue	4	pl
dc.description.firstpage	241	pl
dc.description.lastpage	248	pl
dc.identifier.citation2	Formalized Mathematics	pl
dc.identifier.orcid	brakORCID	-
dc.identifier.orcid	0000-0003-1110-4342	-
Występuje w kolekcji(ach):	Formalized Mathematics, 2021, Volume 29, Issue 4

Pliki w tej pozycji:

Plik	Opis	Rozmiar	Format
10.2478_forma-2021-0022.pdf		254,14 kB	Adobe PDF	Otwórz

Pokaż uproszczony widok rekordu Zobacz statystyki

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