Operations on Subspaces in Real Unitary Space

Noboru Endou

Gifu National College of Technology

Takashi Mitsuishi

Miyagi University

Yasunari Shidama

Shinshu University, Nagano

Summary.

In this article, we extend an operation of real linear space to real unitary space. We show theorems proved in [8] on real unitary space.

MML Identifier: RUSUB_2

Contents (PDF format)

1. Definitions of Sum and Intersection of Subspaces
2. Theorems of Sum and Intersecton of Subspaces
3. Introduction of a Set of Subspaces of Real Unitary Space
4. Definition of the Direct Sum and Linear Complement of Subspaces
5. Theorems Concerning the Sum, Linear Complement and Coset of Subspace
6. Decomposition of a Vector of Real Unitary Space
7. Introduction of Operations on Set of Subspaces
8. Theorems of Functions SubJoin, SubMeet
9. Auxiliary Theorems in Real Unitary Space

Bibliography

[1] Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.

[2] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[3] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.

[4] Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama. Subspaces and cosets of subspace of real unitary space. Journal of Formalized Mathematics, 14, 2002.

[5] Jan Popiolek. Introduction to Banach and Hilbert spaces --- part I. Journal of Formalized Mathematics, 3, 1991.

[6] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.

[7] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[8] Wojciech A. Trybulec. Operations on subspaces in real linear space. Journal of Formalized Mathematics, 1, 1989.

[9] Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.

[10] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[11] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[12] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.

[13] Stanislaw Zukowski. Introduction to lattice theory. Journal of Formalized Mathematics, 1, 1989.