<abstract xmlns="http://www.w3.org/1999/xhtml">

<p>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.</p>
</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.

Transformation Tools for Real Linear Spaces

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

{"article-title":"Transformation Tools for Real Linear Spaces"}

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...

Transformation Tools for Real Linear Spaces

Published Online: Dec 24, 2022

Page range: 93 - 98

Accepted: Jul 23, 2022

DOI: https://doi.org/10.2478/forma-2022-0008

Keywords
real linear space, real normed space, real Euclidean space, real vector space

© 2022 Kazuhisa Nakasho, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Transformation Tools for Real Linear Spaces

Published Online: Dec 24, 2022

Page range: 93 - 98

Accepted: Jul 23, 2022

DOI: https://doi.org/10.2478/forma-2022-0008

Keywordsreal linear space, real normed space, real Euclidean space, real vector space

© 2022 Kazuhisa Nakasho, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Keywords
real linear space, real normed space, real Euclidean space, real vector space