Have a personal or library account? Click to login
The Real Vector Spaces of Finite Sequences are Finite Dimensional Cover

The Real Vector Spaces of Finite Sequences are Finite Dimensional

Formalized Mathematics
Volume 17 (2009): Issue 1 (March 2009)
By: Yatsuka Nakamura,  Artur Korniłowicz,  Nagato Oya and  Yasunari Shidama  
Open Access
|Mar 2009

References

  1. [1] Kanchun and Yatsuka Nakamura. The inner product of finite sequences and of points of n-dimensional topological space. Formalized Mathematics, 11(2):179-183, 2003.
    Search in Google Scholar
  2. [2] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.
    Search in Google Scholar
  3. [3] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990.
    Search in Google Scholar
  4. [4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990.
    Search in Google Scholar
  5. [5] Czesław Byliński. Basic functions and operations on functions. Formalized Mathematics, 1(1):245-254, 1990.
    Search in Google Scholar
  6. [6] Czesław Byliński. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529-536, 1990.
    Search in Google Scholar
  7. [7] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990.
    Search in Google Scholar
  8. [8] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.
    Search in Google Scholar
  9. [9] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357-367, 1990.
    Search in Google Scholar
  10. [10] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
    Search in Google Scholar
  11. [11] Czesław Byliński. The sum and product of finite sequences of real numbers. Formalized Mathematics, 1(4):661-668, 1990.
    Search in Google Scholar
  12. [12] Jing-Chao Chen. The Steinitz theorem and the dimension of a real linear space. Formalized Mathematics, 6(3):411-415, 1997.
    Search in Google Scholar
  13. [13] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990.
    Search in Google Scholar
  14. [14] Agata Darmochwał. The Euclidean space. Formalized Mathematics, 2(4):599-603, 1991.
    Search in Google Scholar
  15. [15] Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama. Dimension of real unitary space. Formalized Mathematics, 11(1):23-28, 2003.
    Search in Google Scholar
  16. [16] Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama. Linear combinations in real unitary space. Formalized Mathematics, 11(1):17-22, 2003.
    Search in Google Scholar
  17. [17] Noboru Endou and Yasunari Shidama. Completeness of the real Euclidean space. Formalized Mathematics, 13(4):577-580, 2005.
    Search in Google Scholar
  18. [18] Jarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269-272, 1990.
    Search in Google Scholar
  19. [19] Yatsuka Nakamura. Sorting operators for finite sequences. Formalized Mathematics, 12(1):1-4, 2004.
    Search in Google Scholar
  20. [20] Henryk Oryszczyszyn and Krzysztof Prażmowski. Real functions spaces. Formalized Mathematics, 1(3):555-561, 1990.
    Search in Google Scholar
  21. [21] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147-152, 1990.
    Search in Google Scholar
  22. [22] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223-230, 1990.
    Search in Google Scholar
  23. [23] Nobuyuki Tamura and Yatsuka Nakamura. Determinant and inverse of matrices of real elements. Formalized Mathematics, 15(3):127-136, 2007, doi:10.2478/v10037-007-00014-7.
    Search in Google Scholar
  24. [24] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1(2):329-334, 1990.
    Search in Google Scholar
  25. [25] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115-122, 1990.
    Search in Google Scholar
  26. [26] Wojciech A. Trybulec. Basis of real linear space. Formalized Mathematics, 1(5):847-850, 1990.
    Search in Google Scholar
  27. [27] Wojciech A. Trybulec. Binary operations on finite sequences. Formalized Mathematics, 1(5):979-981, 1990.
    Search in Google Scholar
  28. [28] Wojciech A. Trybulec. Linear combinations in real linear space. Formalized Mathematics, 1(3):581-588, 1990.
    Search in Google Scholar
  29. [29] Wojciech A. Trybulec. Subspaces and cosets of subspaces in real linear space. Formalized Mathematics, 1(2):297-301, 1990.
    Search in Google Scholar
  30. [30] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990.
    Search in Google Scholar
  31. [31] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
    Search in Google Scholar
  32. [32] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990.
    Search in Google Scholar
  33. [33] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990.
    Search in Google Scholar
  34. [34] Hiroshi Yamazaki, Yoshinori Fujisawa, and Yatsuka Nakamura. On replace function and swap function for finite sequences. Formalized Mathematics, 9(3):471-474, 2001.
    Search in Google Scholar
DOI: https://doi.org/10.2478/v10037-009-0001-2 | Journal eISSN: 1898-9934 | Journal ISSN: 1426-2630
Journal RSS Feed
Language: English
Page range: 1 - 9
Published on: Mar 20, 2009
Published by: University of Białystok
In partnership with: Paradigm Publishing Services
Publication frequency: 1 issue per year
Related subjects:
Mathematics,
General mathematics,
Computer sciences,
Computer sciences, other

© 2009 Yatsuka Nakamura, Artur Korniłowicz, Nagato Oya, Yasunari Shidama, published by University of Białystok
This work is licensed under the Creative Commons License.

Volume 17 (2009): Issue 1 (March 2009)