<abstract xmlns="http://www.w3.org/1999/xhtml">
<p><bold>Summary</bold>. 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 <monospace>TOP-REAL(n)</monospace>, <monospace>REAL-NS(n)</monospace>, and <monospace>n-VectSp over F Real</monospace>. We referred to [4], [9], and [8] in the formalization.</p>
</abstract>

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

Real Vector Space and Related Notions

Formalized Mathematics

{"article-title":"Real Vector Space and Related Notions"}

Summary. In this paper, we discuss the properties that hold in finite dimensional vector spaces and related spaces. In the Mizar language [1], [2], variables...

Real Vector Space and Related Notions

Article Category: Artikel

Published Online: Dec 30, 2021

Page range: 117 - 127

Accepted: Jun 30, 2021

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

Keywords
real vector space, topological space, normed spaces

© 2021 University of Białystok, published by Sciendo

CC-BY-SA License ver. 3.0 or later

Real Vector Space and Related Notions

Article Category: Artikel

Published Online: Dec 30, 2021

Page range: 117 - 127

Accepted: Jun 30, 2021

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

Keywordsreal vector space, topological space, normed spaces

© 2021 University of Białystok, published by Sciendo

CC-BY-SA License ver. 3.0 or later

Keywords
real vector space, topological space, normed spaces