First, we define in Mizar [5], the Cartesian product of two filters bases and the Cartesian product of two filters. After comparing the product of two Fréchet filters on ℕ (F1) with the Fréchet filter on ℕ × ℕ (F2), we compare limF₁ and limF₂ for all double sequences in a non empty topological space. Endou, Okazaki and Shidama formalized in [14] the “convergence in Pringsheim’s sense” for double sequence of real numbers. We show some basic correspondences between the p-convergence and the filter convergence in a topological space. Then we formalize that the double sequence [...] converges in “Pringsheim’s sense” but not in Frechet filter on ℕ × ℕ sense. In the next section, we generalize some definitions: “is convergent in the first coordinate”, “is convergent in the second coordinate”, “the lim in the first coordinate of”, “the lim in the second coordinate of” according to [14], in Hausdorff space. Finally, we generalize two theorems: (3) and (4) from [14] in the case of double sequences and we formalize the “iterated limit” theorem (“Double limit” [7], p. 81, par. 8.5 “Double limite” [6] (TG I,57)), all in regular space. We were inspired by the exercises (2.11.4), (2.17.5) [17] and the corrections B.10 [18].
@article{bwmeta1.element.doi-10_1515_forma-2016-0014,
author = {Roland Coghetto},
title = {Double Sequences and Iterated Limits in Regular Space},
journal = {Formalized Mathematics},
volume = {24},
year = {2016},
pages = {173-186},
zbl = {1357.54004},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0014}
}
Roland Coghetto. Double Sequences and Iterated Limits in Regular Space. Formalized Mathematics, Tome 24 (2016) pp. 173-186. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0014/