Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991
Association of Mizar Users
Introduction to Banach and Hilbert Spaces  Part II

Jan Popiolek

Warsaw University, Bialystok
Summary.

A continuation of [6].
It contains the definitions of the convergent sequence
and limit of the sequence. The convergence with respect to the norm
and the distance is also introduced.
Last part of this article is devoted to the following
concepts: ball, closed ball and sphere.
MML Identifier:
BHSP_2
The terminology and notation used in this paper have been
introduced in the following articles
[7]
[1]
[8]
[2]
[4]
[3]
[10]
[9]
[6]
[5]
Contents (PDF format)
Bibliography
 [1]
Grzegorz Bancerek.
The ordinal numbers.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Krzysztof Hryniewiecki.
Basic properties of real numbers.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Jaroslaw Kotowicz.
Convergent sequences and the limit of sequences.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Jaroslaw Kotowicz.
Real sequences and basic operations on them.
Journal of Formalized Mathematics,
1, 1989.
 [5]
Jan Popiolek.
Real normed space.
Journal of Formalized Mathematics,
2, 1990.
 [6]
Jan Popiolek.
Introduction to Banach and Hilbert spaces  part I.
Journal of Formalized Mathematics,
3, 1991.
 [7]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [8]
Andrzej Trybulec.
Subsets of real numbers.
Journal of Formalized Mathematics,
Addenda, 2003.
 [9]
Wojciech A. Trybulec.
Vectors in real linear space.
Journal of Formalized Mathematics,
1, 1989.
 [10]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
Received July 19, 1991
[
Download a postscript version,
MML identifier index,
Mizar home page]