<abstract xmlns="http://www.w3.org/1999/xhtml"> 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 <inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/2016.24.3.173.jpg"></inline-graphic> 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].</abstract>

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].

Double Sequences and Iterated Limits in Regular Space

Formalized Mathematics

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License

{"article-title":"Double Sequences and Iterated Limits in Regular Space"}

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...

Double Sequences and Iterated Limits in Regular Space

Data publikacji: 21 lut 2017

Zakres stron: 173 - 186

Otrzymano: 30 cze 2016

DOI: https://doi.org/10.1515/forma-2016-0014

Słowa kluczowe
filter, double limits, Pringsheim convergence, iterated limits, regular space

© by Roland Coghetto

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License

Double Sequences and Iterated Limits in Regular Space

Data publikacji: 21 lut 2017

Zakres stron: 173 - 186

Otrzymano: 30 cze 2016

DOI: https://doi.org/10.1515/forma-2016-0014

Słowa kluczowefilter, double limits, Pringsheim convergence, iterated limits, regular space

© by Roland Coghetto

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License

Słowa kluczowe
filter, double limits, Pringsheim convergence, iterated limits, regular space