Topology from Neighbourhoods

Roland Coghetto

Formalized Mathematics (2015)

  • Volume: 23, Issue: 4, page 289-296
  • ISSN: 1426-2630

Abstract

top
Using Mizar [9], and the formal topological space structure (FMT_Space_Str) [19], we introduce the three U-FMT conditions (U-FMT filter, U-FMT with point and U-FMT local) similar to those VI, VII, VIII and VIV of the proposition 2 in [10]: If to each element x of a set X there corresponds a set B(x) of subsets of X such that the properties VI, VII, VIII and VIV are satisfied, then there is a unique topological structure on X such that, for each x ∈ X, B(x) is the set of neighborhoods of x in this topology. We present a correspondence between a topological space and a space defined with the formal topological space structure with the three U-FMT conditions called the topology from neighbourhoods. For the formalization, we were inspired by the works of Bourbaki [11] and Claude Wagschal [31].

How to cite

top

Roland Coghetto. "Topology from Neighbourhoods." Formalized Mathematics 23.4 (2015): 289-296. <http://eudml.org/doc/276876>.

@article{RolandCoghetto2015,
abstract = {Using Mizar [9], and the formal topological space structure (FMT\_Space\_Str) [19], we introduce the three U-FMT conditions (U-FMT filter, U-FMT with point and U-FMT local) similar to those VI, VII, VIII and VIV of the proposition 2 in [10]: If to each element x of a set X there corresponds a set B(x) of subsets of X such that the properties VI, VII, VIII and VIV are satisfied, then there is a unique topological structure on X such that, for each x ∈ X, B(x) is the set of neighborhoods of x in this topology. We present a correspondence between a topological space and a space defined with the formal topological space structure with the three U-FMT conditions called the topology from neighbourhoods. For the formalization, we were inspired by the works of Bourbaki [11] and Claude Wagschal [31].},
author = {Roland Coghetto},
journal = {Formalized Mathematics},
keywords = {filter; topological space; neighbourhoods system},
language = {eng},
number = {4},
pages = {289-296},
title = {Topology from Neighbourhoods},
url = {http://eudml.org/doc/276876},
volume = {23},
year = {2015},
}

TY - JOUR
AU - Roland Coghetto
TI - Topology from Neighbourhoods
JO - Formalized Mathematics
PY - 2015
VL - 23
IS - 4
SP - 289
EP - 296
AB - Using Mizar [9], and the formal topological space structure (FMT_Space_Str) [19], we introduce the three U-FMT conditions (U-FMT filter, U-FMT with point and U-FMT local) similar to those VI, VII, VIII and VIV of the proposition 2 in [10]: If to each element x of a set X there corresponds a set B(x) of subsets of X such that the properties VI, VII, VIII and VIV are satisfied, then there is a unique topological structure on X such that, for each x ∈ X, B(x) is the set of neighborhoods of x in this topology. We present a correspondence between a topological space and a space defined with the formal topological space structure with the three U-FMT conditions called the topology from neighbourhoods. For the formalization, we were inspired by the works of Bourbaki [11] and Claude Wagschal [31].
LA - eng
KW - filter; topological space; neighbourhoods system
UR - http://eudml.org/doc/276876
ER -

References

top
  1. [1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990. 
  2. [2] Grzegorz Bancerek. Complete lattices. Formalized Mathematics, 2(5):719–725, 1991. 
  3. [3] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990. Zbl06213858
  4. [4] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990. 
  5. [5] Grzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Formalized Mathematics, 6(1):93–107, 1997. 
  6. [6] Grzegorz Bancerek. Prime ideals and filters. Formalized Mathematics, 6(2):241–247, 1997. 
  7. [7] Grzegorz Bancerek. Bases and refinements of topologies. Formalized Mathematics, 7(1): 35–43, 1998. 
  8. [8] Grzegorz Bancerek, Noboru Endou, and Yuji Sakai. On the characterizations of compactness. Formalized Mathematics, 9(4):733–738, 2001. 
  9. [9] 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.[Crossref] Zbl06512423
  10. [10] Nicolas Bourbaki. General Topology: Chapters 1–4. Springer Science and Business Media, 2013. Zbl1107.54001
  11. [11] Nicolas Bourbaki. Topologie générale: Chapitres 1 à 4. Eléments de mathématique. Springer Science & Business Media, 2007. 
  12. [12] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55–65, 1990. 
  13. [13] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990. 
  14. [14] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357–367, 1990. 
  15. [15] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990. 
  16. [16] Roland Coghetto. Convergent filter bases. Formalized Mathematics, 23(3):189–203, 2015. doi:10.1515/forma-2015-0016.[Crossref] Zbl1321.54006
  17. [17] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990. 
  18. [18] Adam Grabowski and Robert Milewski. Boolean posets, posets under inclusion and products of relational structures. Formalized Mathematics, 6(1):117–121, 1997. 
  19. [19] Gang Liu, Yasushi Fuwa, and Masayoshi Eguchi. Formal topological spaces. Formalized Mathematics, 9(3):537–543, 2001. 
  20. [20] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, I. Formalized Mathematics, 5(2):167–172, 1996. 
  21. [21] Beata Padlewska. Locally connected spaces. Formalized Mathematics, 2(1):93–96, 1991. 
  22. [22] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147–152, 1990. 
  23. [23] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990. 
  24. [24] Alexander Yu. Shibakov and Andrzej Trybulec. The Cantor set. Formalized Mathematics, 5(2):233–236, 1996. 
  25. [25] Andrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics, 11(4): 341–347, 2003. 
  26. [26] Andrzej Trybulec. Moore-Smith convergence. Formalized Mathematics, 6(2):213–225, 1997. 
  27. [27] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501–505, 1990. 
  28. [28] Wojciech A. Trybulec and Grzegorz Bancerek. Kuratowski – Zorn lemma. Formalized Mathematics, 1(2):387–393, 1990. 
  29. [29] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990. 
  30. [30] Josef Urban. Basic facts about inaccessible and measurable cardinals. Formalized Mathematics, 9(2):323–329, 2001. 
  31. [31] Claude Wagschal. Topologie et analyse fonctionnelle. Hermann, 1995. 
  32. [32] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73–83, 1990. 
  33. [33] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990. 
  34. [34] Stanisław Żukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215–222, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.