Have a personal or library account? Click to login
Summable Family in a Commutative Group Cover

Summable Family in a Commutative Group

Formalized Mathematics
Volume 23 (2015): Issue 4 (December 2015)
By: Roland Coghetto  
Open Access
|Mar 2016

References

  1. [1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.
    Search in Google Scholar
  2. [2] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.
    Search in Google Scholar
  3. [3] Grzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Formalized Mathematics, 6(1):93–107, 1997.
    Search in Google Scholar
  4. [4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.
    Search in Google Scholar
  5. [5] Grzegorz Bancerek, Noboru Endou, and Yuji Sakai. On the characterizations of compactness. Formalized Mathematics, 9(4):733–738, 2001.
    Search in Google Scholar
  6. [6] 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.10.1007/978-3-319-20615-8
    Search in Google Scholar
  7. [7] 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.
    Search in Google Scholar
  8. [8] Leszek Borys. Paracompact and metrizable spaces. Formalized Mathematics, 2(4):481–485, 1991.
    Search in Google Scholar
  9. [9] Nicolas Bourbaki. Topologie générale: Chapitres 1 à 4. Eléments de mathématique. Springer Science & Business Media, 2007.10.1007/978-3-540-34486-5_1
    Search in Google Scholar
  10. [10] Nicolas Bourbaki. General Topology: Chapters 1–4. Springer Science and Business Media, 2013.
    Search in Google Scholar
  11. [11] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55–65, 1990.
    Search in Google Scholar
  12. [12] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.
    Search in Google Scholar
  13. [13] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357–367, 1990.
    Search in Google Scholar
  14. [14] Czesław Byliński. Introduction to real linear topological spaces. Formalized Mathematics, 13(1):99–107, 2005.
    Search in Google Scholar
  15. [15] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.
    Search in Google Scholar
  16. [16] Roland Coghetto. Convergent filter bases. Formalized Mathematics, 23(3):189–203, 2015. doi:10.1515/forma-2015-0016.10.1515/forma-2015-0016
    Search in Google Scholar
  17. [17] Roland Coghetto. Groups – additive notation. Formalized Mathematics, 23(2):127–160, 2015. doi:10.1515/forma-2015-0013.10.1515/forma-2015-0013
    Search in Google Scholar
  18. [18] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990.
    Search in Google Scholar
  19. [19] Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama. Dimension of real unitary space. Formalized Mathematics, 11(1):23–28, 2003.
    Search in Google Scholar
  20. [20] 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.10.2478/v10037-006-0024-x
    Search in Google Scholar
  21. [21] Adam Grabowski and Robert Milewski. Boolean posets, posets under inclusion and products of relational structures. Formalized Mathematics, 6(1):117–121, 1997.
    Search in Google Scholar
  22. [22] 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.10.1007/978-3-642-39634-2_21
    Search in Google Scholar
  23. [23] Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics, 1(3):607–610, 1990.
    Search in Google Scholar
  24. [24] Artur Korniłowicz. The definition and basic properties of topological groups. Formalized Mathematics, 7(2):217–225, 1998.
    Search in Google Scholar
  25. [25] Artur Korniłowicz. Introduction to meet-continuous topological lattices. Formalized Mathematics, 7(2):279–283, 1998.
    Search in Google Scholar
  26. [26] Michał Muzalewski and Wojciech Skaba. From loops to Abelian multiplicative groups with zero. Formalized Mathematics, 1(5):833–840, 1990.
    Search in Google Scholar
  27. [27] Beata Padlewska. Locally connected spaces. Formalized Mathematics, 2(1):93–96, 1991.
    Search in Google Scholar
  28. [28] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.
    Search in Google Scholar
  29. [29] Jan Popiołek. Real normed space. Formalized Mathematics, 2(1):111–115, 1991.
    Search in Google Scholar
  30. [30] Bartłomiej Skorulski. First-countable, sequential, and Frechet spaces. Formalized Mathematics, 7(1):81–86, 1998.
    Search in Google Scholar
  31. [31] Andrzej Trybulec. Semilattice operations on finite subsets. Formalized Mathematics, 1 (2):369–376, 1990.
    Search in Google Scholar
  32. [32] Andrzej Trybulec and Agata Darmochwał. Boolean domains. Formalized Mathematics, 1 (1):187–190, 1990.
    Search in Google Scholar
  33. [33] Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569–573, 1990.
    Search in Google Scholar
  34. [34] Wojciech A. Trybulec. Binary operations on finite sequences. Formalized Mathematics, 1 (5):979–981, 1990.
    Search in Google Scholar
  35. [35] Wojciech A. Trybulec. Groups. Formalized Mathematics, 1(5):821–827, 1990.
    Search in Google Scholar
  36. [36] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291–296, 1990.
    Search in Google Scholar
  37. [37] Wojciech A. Trybulec and Grzegorz Bancerek. Kuratowski – Zorn lemma. Formalized Mathematics, 1(2):387–393, 1990.
    Search in Google Scholar
  38. [38] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.
    Search in Google Scholar
  39. [39] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73–83, 1990.
    Search in Google Scholar
DOI: https://doi.org/10.1515/forma-2015-0022 | Journal eISSN: 1898-9934 | Journal ISSN: 1426-2630
Journal RSS Feed
Language: English
Page range: 279 - 288
Submitted on: Aug 14, 2015
|
Published on: Mar 25, 2016
Published by: University of Białystok
In partnership with: Paradigm Publishing Services
Publication frequency: 1 issue per year
Keywords:
54A20,
54H11,
22A05,
03B35
Related subjects:
Computer sciences,
Computer sciences, other,
Mathematics,
General mathematics

© 2016 Roland Coghetto, published by University of Białystok
This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Volume 23 (2015): Issue 4 (December 2015)Next article