Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/4901
Tytuł: | Summable Family in a Commutative Group |
Autorzy: | Coghetto, Roland |
Słowa kluczowe: | limits filters topological group summable family convergence series linear topological space |
Data wydania: | 2015 |
Data dodania: | 16-gru-2016 |
Wydawca: | De Gruyter Open |
Źródło: | Formalized Mathematics, Volume 23, Issue 4, 279–288 |
Abstrakt: | Hölzl et al. showed that it was possible to build “a generic theory of limits based on filters” in Isabelle/HOL [22], [7]. In this paper we present our formalization of this theory in Mizar [6].First, we compare the notions of the limit of a family indexed by a directed set, or a sequence, in a metric space [30], a real normed linear space [29] and a linear topological space [14] with the concept of the limit of an image filter [16].Then, following Bourbaki [9], [10] (TG.III, §5.1 Familles sommables dans un groupe commutatif), we conclude by defining the summable families in a commutative group (“additive notation” in [17]), using the notion of filters. |
Afiliacja: | Rue de la Brasserie 5, 7100 La Louvière, Belgium |
URI: | http://hdl.handle.net/11320/4901 |
DOI: | 10.1515/forma-2015-0022 |
ISSN: | 1426-2630 1898-9934 |
Typ Dokumentu: | Article |
Występuje w kolekcji(ach): | Formalized Mathematics, 2015, Volume 23, Issue 4 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma-2015-0022.pdf | 278,19 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL