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.

MML Identifier: COMSEQ_2

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]

Contents (PDF format)

  1. Preliminaries
  2. Conjugate sequences
  3. Bounded complex sequences
  4. Convergent complex sequences
  5. 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]