Cartesian Products of Family of Real Linear Spaces

Hiroyuki Okazaki, Noboru Endou, Yasunari Shidama

Formalized Mathematics · 2011 · 16 citations · 10 references

DOIFull text

Open access

Concepts

Abstract

Cartesian Products of Family of Real Linear SpacesIn this article we introduced the isomorphism mapping between cartesian products of family of linear spaces [4]. Those products had been formalized by two different ways, i.e., the way using the functor [:X, Y:] and ones using the functor "product". By the same way, the isomorphism mapping was defined between Cartesian products of family of linear normed spaces also.

References

10