Double Sequences and Iterated Limits in Regular Space

Roland Coghetto. "Double Sequences and Iterated Limits in Regular Space." Formalized Mathematics 24.3 (2016): 173-186. <http://eudml.org/doc/288074>.

@article{RolandCoghetto2016,
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].},
author = {Roland Coghetto},
journal = {Formalized Mathematics},
keywords = {filter; double limits; Pringsheim convergence; iterated limits; regular space},
language = {eng},
number = {3},
pages = {173-186},
title = {Double Sequences and Iterated Limits in Regular Space},
url = {http://eudml.org/doc/288074},
volume = {24},
year = {2016},
}

TY - JOUR
AU - Roland Coghetto
TI - Double Sequences and Iterated Limits in Regular Space
JO - Formalized Mathematics
PY - 2016
VL - 24
IS - 3
SP - 173
EP - 186
AB - 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].
LA - eng
KW - filter; double limits; Pringsheim convergence; iterated limits; regular space
UR - http://eudml.org/doc/288074
ER -