Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002
Association of Mizar Users
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
The terminology and notation used in this paper have been
introduced in the following articles
[7]
[3]
[10]
[11]
[2]
[1]
[13]
[12]
[6]
[9]
[5]
[4]

Definitions of Sum and Intersection of Subspaces

Theorems of Sum and Intersecton of Subspaces

Introduction of a Set of Subspaces of Real Unitary Space

Definition of the Direct Sum and Linear Complement of Subspaces

Theorems Concerning the Sum, Linear Complement and Coset of Subspace

Decomposition of a Vector of Real Unitary Space

Introduction of Operations on Set of Subspaces

Theorems of Functions SubJoin, SubMeet

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.
Received October 9, 2002
[
Download a postscript version,
MML identifier index,
Mizar home page]