{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,28]],"date-time":"2026-05-28T01:05:45Z","timestamp":1779930345013,"version":"3.53.1"},"reference-count":0,"publisher":"Walter de Gruyter GmbH","issue":"3","license":[{"start":{"date-parts":[[2014,3,31]],"date-time":"2014-03-31T00:00:00Z","timestamp":1396224000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,9,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats:p>In this article, we formalize topological properties of real normed spaces. In the first part, open and closed, density, separability and sequence and its convergence are discussed. Then we argue properties of real normed subspace. Then we discuss linear functions between real normed speces. Several kinds of subspaces induced by linear functions such as kernel, image and inverse image are considered here. The fact that Lipschitz continuity operators preserve convergence of sequences is also refered here. Then we argue the condition when real normed subspaces become Banach\u2019s spaces. We also formalize quotient vector space. In the last session, we argue the properties of the closure of real normed space. These formalizations are based on [19](p.3-41), [2] and [34](p.3-67).<\/jats:p>","DOI":"10.2478\/forma-2014-0024","type":"journal-article","created":{"date-parts":[[2015,5,4]],"date-time":"2015-05-04T13:03:37Z","timestamp":1430744617000},"page":"209-223","source":"Crossref","is-referenced-by-count":1,"title":["Topological Properties of Real Normed Space"],"prefix":"10.2478","volume":"22","author":[{"given":"Kazuhisa","family":"Nakasho","sequence":"first","affiliation":[{"name":"Shinshu University Nagano, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yuichi","family":"Futa","sequence":"additional","affiliation":[{"name":"Japan Advanced Institute of Science and Technology Ishikawa, 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":[[2014,3,31]]},"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/22\/3\/article-p209.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2014-0024","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,28]],"date-time":"2026-05-28T00:24:37Z","timestamp":1779927877000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2014-0024"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3,31]]},"references-count":0,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2014,3,31]]},"published-print":{"date-parts":[[2014,9,1]]}},"alternative-id":["10.2478\/forma-2014-0024"],"URL":"https:\/\/doi.org\/10.2478\/forma-2014-0024","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,3,31]]}}}