Summable Family in a Commutative Group

Pole DC	Wartość	Język
dc.contributor.author	Coghetto, Roland	pl
dc.date.accessioned	2016-12-16T10:30:39Z	-
dc.date.available	2016-12-16T10:30:39Z	-
dc.date.issued	2015	pl
dc.identifier.citation	Formalized Mathematics, Volume 23, Issue 4, 279–288	pl
dc.identifier.issn	1426-2630	pl
dc.identifier.issn	1898-9934	pl
dc.identifier.uri	http://hdl.handle.net/11320/4901	-
dc.description.abstract	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.	pl
dc.language.iso	en	pl
dc.publisher	De Gruyter Open	pl
dc.subject	limits	pl
dc.subject	filters	pl
dc.subject	topological group	pl
dc.subject	summable family	pl
dc.subject	convergence series	pl
dc.subject	linear topological space	pl
dc.title	Summable Family in a Commutative Group	pl
dc.type	Article	pl
dc.identifier.doi	10.1515/forma-2015-0022	pl
dc.description.Affiliation	Rue de la Brasserie 5, 7100 La Louvière, Belgium	pl
dc.description.references	Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.	pl
dc.description.references	Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.	pl
dc.description.references	Grzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Formalized Mathematics, 6(1):93–107, 1997.	pl
dc.description.references	Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.	pl
dc.description.references	Grzegorz Bancerek, Noboru Endou, and Yuji Sakai. On the characterizations of compactness. Formalized Mathematics, 9(4):733–738, 2001.	pl
dc.description.references	Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8 17.	pl
dc.description.references	Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Formalization of real analysis: A survey of proof assistants and libraries. Mathematical Structures in Computer Science, pages 1–38, 2014.	pl
dc.description.references	Leszek Borys. Paracompact and metrizable spaces. Formalized Mathematics, 2(4):481–485, 1991.	pl
dc.description.references	Nicolas Bourbaki. Topologie générale: Chapitres 1 à 4. Eléments de mathématique. Springer Science & Business Media, 2007.	pl
dc.description.references	Nicolas Bourbaki. General Topology: Chapters 1–4. Springer Science and Business Media, 2013.	pl
dc.description.references	Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55–65, 1990.	pl
dc.description.references	Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.	pl
dc.description.references	Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357–367, 1990.	pl
dc.description.references	Czesław Byliński. Introduction to real linear topological spaces. Formalized Mathematics, 13(1):99–107, 2005.	pl
dc.description.references	Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.	pl
dc.description.references	Roland Coghetto. Convergent filter bases. Formalized Mathematics, 23(3):189–203, 2015. doi:10.1515/forma-2015-0016. [Crossref]	pl
dc.description.references	Roland Coghetto. Groups – additive notation. Formalized Mathematics, 23(2):127–160, 2015. doi:10.1515/forma-2015-0013. [Crossref]	pl
dc.description.references	Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990.	pl
dc.description.references	Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama. Dimension of real unitary space. Formalized Mathematics, 11(1):23–28, 2003.	pl
dc.description.references	Noboru Endou, Yasunari Shidama, and Katsumasa Okamura. Baire’s category theorem and some spaces generated from real normed space. Formalized Mathematics, 14(4): 213–219, 2006. doi:10.2478/v10037-006-0024-x. [Crossref]	pl
dc.description.references	Adam Grabowski and Robert Milewski. Boolean posets, posets under inclusion and products of relational structures. Formalized Mathematics, 6(1):117–121, 1997.	pl
dc.description.references	Johannes Hölzl, Fabian Immler, and Brian Huffman. Type classes and filters for mathematical analysis in Isabelle/HOL. In Interactive Theorem Proving, pages 279–294. Springer, 2013.	pl
dc.description.references	Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics, 1(3):607–610, 1990.	pl
dc.description.references	Artur Korniłowicz. The definition and basic properties of topological groups. Formalized Mathematics, 7(2):217–225, 1998.	pl
dc.description.references	Artur Korniłowicz. Introduction to meet-continuous topological lattices. Formalized Mathematics, 7(2):279–283, 1998.	pl
dc.description.references	Michał Muzalewski and Wojciech Skaba. From loops to Abelian multiplicative groups with zero. Formalized Mathematics, 1(5):833–840, 1990.	pl
dc.description.references	Beata Padlewska. Locally connected spaces. Formalized Mathematics, 2(1):93–96, 1991.	pl
dc.description.references	Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.	pl
dc.description.references	Jan Popiołek. Real normed space. Formalized Mathematics, 2(1):111–115, 1991.	pl
dc.description.references	Bartłomiej Skorulski. First-countable, sequential, and Frechet spaces. Formalized Mathematics, 7(1):81–86, 1998.	pl
dc.description.references	Andrzej Trybulec. Semilattice operations on finite subsets. Formalized Mathematics, 1 (2):369–376, 1990.	pl
dc.description.references	Andrzej Trybulec and Agata Darmochwał. Boolean domains. Formalized Mathematics, 1 (1):187–190, 1990.	pl
dc.description.references	Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569–573, 1990.	pl
dc.description.references	Wojciech A. Trybulec. Binary operations on finite sequences. Formalized Mathematics, 1 (5):979–981, 1990.	pl
dc.description.references	Wojciech A. Trybulec. Groups. Formalized Mathematics, 1(5):821–827, 1990.	pl
dc.description.references	Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291–296, 1990.	pl
dc.description.references	Wojciech A. Trybulec and Grzegorz Bancerek. Kuratowski – Zorn lemma. Formalized Mathematics, 1(2):387–393, 1990.	pl
dc.description.references	Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.	pl
dc.description.references	Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73–83, 1990.	pl
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

Pokaż uproszczony widok rekordu Zobacz statystyki

Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL