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

<p>In this article, we formalize in Mizar [1], [2] the topological properties of finite-dimensional real normed spaces. In the first section, we formalize the Bolzano-Weierstrass theorem, which states that a bounded sequence of points in an n-dimensional Euclidean space has a certain subsequence that converges to a point. As a corollary, it is also shown the equivalence between a subset of an n-dimensional Euclidean space being compact and being closed and bounded.</p>
<p>In the next section, we formalize the definitions of L1-norm (Manhattan Norm) and maximum norm and show their topological equivalence in n-dimensional Euclidean spaces and finite-dimensional real linear spaces. In the last section, we formalize the linear isometries and their topological properties. Namely, it is shown that a linear isometry between real normed spaces preserves properties such as continuity, the convergence of a sequence, openness, closeness, and compactness of subsets. Finally, it is shown that finite-dimensional real normed spaces are proper metric spaces. We referred to [5], [9], and [7] in the formalization.</p>
</abstract>

In this article, we formalize in Mizar [1], [2] the topological properties of finite-dimensional real normed spaces. In the first section, we formalize the Bolzano-Weierstrass theorem, which states that a bounded sequence of points in an n-dimensional Euclidean space has a certain subsequence that converges to a point. As a corollary, it is also shown the equivalence between a subset of an n-dimensional Euclidean space being compact and being closed and bounded.
In the next section, we formalize the definitions of L1-norm (Manhattan Norm) and maximum norm and show their topological equivalence in n-dimensional Euclidean spaces and finite-dimensional real linear spaces. In the last section, we formalize the linear isometries and their topological properties. Namely, it is shown that a linear isometry between real normed spaces preserves properties such as continuity, the convergence of a sequence, openness, closeness, and compactness of subsets. Finally, it is shown that finite-dimensional real normed spaces are proper metric spaces. We referred to [5], [9], and [7] in the formalization.

Finite Dimensional Real Normed Spaces are Proper Metric Spaces

Formalized Mathematics

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

{"article-title":"Finite Dimensional Real Normed Spaces are Proper Metric Spaces"}

In this article, we formalize in Mizar [1], [2] the topological properties of finite-dimensional real normed spaces. In the first section, we formalize the...

Finite Dimensional Real Normed Spaces are Proper Metric Spaces

Publié en ligne: 09 juil. 2022

Pages: 175 - 184

Accepté: 30 sept. 2021

DOI: https://doi.org/10.2478/forma-2021-0017

Mots clés
real vector space, topological space, normed spaces, L1-norm, maximum norm, linear isometry, proper metric space

© 2022 Kazuhisa Nakasho et al., published by Sciendo

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

Finite Dimensional Real Normed Spaces are Proper Metric Spaces

Publié en ligne: 09 juil. 2022

Pages: 175 - 184

Accepté: 30 sept. 2021

DOI: https://doi.org/10.2478/forma-2021-0017

Mots clésreal vector space, topological space, normed spaces, L1-norm, maximum norm, linear isometry, proper metric space

© 2022 Kazuhisa Nakasho et al., published by Sciendo

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

Mots clés
real vector space, topological space, normed spaces, L1-norm, maximum norm, linear isometry, proper metric space