Double Sequences and Limits

Noboru Endou; Hiroyuki Okazaki; Yasunari Shidama

Formalized Mathematics (2013)

  • Volume: 21, Issue: 3, page 163-170
  • ISSN: 1426-2630

Abstract

top
Double sequences are important extension of the ordinary notion of a sequence. In this article we formalized three types of limits of double sequences and the theory of these limits.

How to cite

top

Noboru Endou, Hiroyuki Okazaki, and Yasunari Shidama. "Double Sequences and Limits." Formalized Mathematics 21.3 (2013): 163-170. <http://eudml.org/doc/266553>.

@article{NoboruEndou2013,
abstract = {Double sequences are important extension of the ordinary notion of a sequence. In this article we formalized three types of limits of double sequences and the theory of these limits.},
author = {Noboru Endou, Hiroyuki Okazaki, Yasunari Shidama},
journal = {Formalized Mathematics},
keywords = {formalization of basic metric space; limits of double sequences},
language = {eng},
number = {3},
pages = {163-170},
title = {Double Sequences and Limits},
url = {http://eudml.org/doc/266553},
volume = {21},
year = {2013},
}

TY - JOUR
AU - Noboru Endou
AU - Hiroyuki Okazaki
AU - Yasunari Shidama
TI - Double Sequences and Limits
JO - Formalized Mathematics
PY - 2013
VL - 21
IS - 3
SP - 163
EP - 170
AB - Double sequences are important extension of the ordinary notion of a sequence. In this article we formalized three types of limits of double sequences and the theory of these limits.
LA - eng
KW - formalization of basic metric space; limits of double sequences
UR - http://eudml.org/doc/266553
ER -

References

top
  1. [1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. Zbl06213858
  2. [2] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990. 
  3. [3] Czesław Bylinski. Binary operations. Formalized Mathematics, 1(1):175-180, 1990. 
  4. [4] Czesław Bylinski. The complex numbers. Formalized Mathematics, 1(3):507-513, 1990. 
  5. [5] Czesław Bylinski. Binary operations applied to finite sequences. Formalized Mathematics, 1(4):643-649, 1990. 
  6. [6] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990. 
  7. [7] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  8. [8] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990. 
  9. [9] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  10. [10] Noboru Endou, Keiko Narita, and Yasunari Shidama. The Lebesgue monotone convergence theorem. Formalized Mathematics, 16(2):167-175, 2008. doi:10.2478/v10037-008-0023-1.[Crossref] Zbl1321.46022
  11. [11] Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5): 841-845, 1990. 
  12. [12] Jarosław Kotowicz. Convergent sequences and the limit of sequences. Formalized Mathematics, 1(2):273-275, 1990. 
  13. [13] Adam Naumowicz. Conjugate sequences, bounded complex sequences and convergent complex sequences. Formalized Mathematics, 6(2):265-268, 1997. 
  14. [14] Jan Popiołek. Some properties of functions modul and signum. Formalized Mathematics, 1(2):263-264, 1990. 
  15. [15] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329-334, 1990. 
  16. [16] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990. 
  17. [17] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  18. [18] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.