Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/5552
Tytuł: | Double Sequences and Iterated Limits in Regular Space |
Autorzy: | Coghetto, Roland |
Słowa kluczowe: | filter double limits Pringsheim convergence iterated limits regular space |
Data wydania: | 2016 |
Data dodania: | 2-cze-2017 |
Wydawca: | De Gruyter Open |
Źródło: | Formalized Mathematics, Volume 24, Issue 3, pp. 173-186 |
Abstrakt: | 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]. |
Afiliacja: | Coghetto Roland - Rue de la Brasserie 5 7100 La Louvière, Belgium |
URI: | http://hdl.handle.net/11320/5552 |
DOI: | 10.1515/forma-2016-0014 |
ISSN: | 1426-2630 1898-9934 |
Typ Dokumentu: | Article |
Występuje w kolekcji(ach): | Formalized Mathematics, 2016, Volume 24, Issue 3 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma-2016-0014.pdf | 301,98 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL