Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996
Association of Mizar Users
Conjugate Sequences, Bounded Complex Sequences and
Convergent Complex Sequences

Adam Naumowicz

Warsaw University, Bialystok
Summary.

This article is a continuation of [1]. It is divided into five
sections. The first one contains a few useful lemmas. In the second part there
is a definition of conjugate sequences and proofs of some basic properties of
such sequences. The third segment treats of bounded complex sequences,next one
contains description of convergent complex sequences. The last and the biggest
part of the article contains proofs of main theorems concerning the theory of
bounded and convergent complex sequences.
The terminology and notation used in this paper have been
introduced in the following articles
[10]
[2]
[8]
[6]
[3]
[11]
[4]
[7]
[9]
[5]
[1]

Preliminaries

Conjugate sequences

Bounded complex sequences

Convergent complex sequences

Main theorems
Bibliography
 [1]
Agnieszka Banachowicz and Anna Winnicka.
Complex sequences.
Journal of Formalized Mathematics,
5, 1993.
 [2]
Grzegorz Bancerek.
The ordinal numbers.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Czeslaw Bylinski.
Functions from a set to a set.
Journal of Formalized Mathematics,
1, 1989.
 [5]
Czeslaw Bylinski.
The complex numbers.
Journal of Formalized Mathematics,
2, 1990.
 [6]
Krzysztof Hryniewiecki.
Basic properties of real numbers.
Journal of Formalized Mathematics,
1, 1989.
 [7]
Jaroslaw Kotowicz.
Convergent sequences and the limit of sequences.
Journal of Formalized Mathematics,
1, 1989.
 [8]
Andrzej Trybulec.
Subsets of real numbers.
Journal of Formalized Mathematics,
Addenda, 2003.
 [9]
Wojciech A. Trybulec.
Pigeon hole principle.
Journal of Formalized Mathematics,
2, 1990.
 [10]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
 [11]
Edmund Woronowicz.
Relations defined on sets.
Journal of Formalized Mathematics,
1, 1989.
Received December 20, 1996
[
Download a postscript version,
MML identifier index,
Mizar home page]