Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
Pełny rekord metadanych
Pole DCWartośćJęzyk
dc.contributor.authorCoghetto, Rolandpl
dc.identifier.citationFormalized Mathematics, Volume 23, Issue 4, 289–296pl
dc.description.abstractUsing 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].pl
dc.publisherDe Gruyter Openpl
dc.subjecttopological spacepl
dc.subjectneighbourhoods systempl
dc.titleTopology from Neighbourhoodspl
dc.description.AffiliationRue de la Brasserie 5, 7100 La Louvière, Belgiumpl
dc.description.referencesGrzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382,
dc.description.referencesGrzegorz Bancerek. Complete lattices. Formalized Mathematics, 2(5):719–725,
dc.description.referencesGrzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46,
dc.description.referencesGrzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96,
dc.description.referencesGrzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Formalized Mathematics, 6(1):93–107,
dc.description.referencesGrzegorz Bancerek. Prime ideals and filters. Formalized Mathematics, 6(2):241–247,
dc.description.referencesGrzegorz Bancerek. Bases and refinements of topologies. Formalized Mathematics, 7(1): 35–43,
dc.description.referencesGrzegorz Bancerek, Noboru Endou, and Yuji Sakai. On the characterizations of compactness. Formalized Mathematics, 9(4):733–738,
dc.description.referencesGrzegorz 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]pl
dc.description.referencesNicolas Bourbaki. General Topology: Chapters 1–4. Springer Science and Business Media,
dc.description.referencesNicolas Bourbaki. Topologie générale: Chapitres 1 à 4. Eléments de mathématique. Springer Science & Business Media,
dc.description.referencesCzesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55–65,
dc.description.referencesCzesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164,
dc.description.referencesCzesław Byliński. Partial functions. Formalized Mathematics, 1(2):357–367,
dc.description.referencesCzesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53,
dc.description.referencesRoland Coghetto. Convergent filter bases. Formalized Mathematics, 23(3):189–203, 2015. doi:10.1515/forma-2015-0016. [Crossref]pl
dc.description.referencesAgata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167,
dc.description.referencesAdam Grabowski and Robert Milewski. Boolean posets, posets under inclusion and products of relational structures. Formalized Mathematics, 6(1):117–121,
dc.description.referencesGang Liu, Yasushi Fuwa, and Masayoshi Eguchi. Formal topological spaces. Formalized Mathematics, 9(3):537–543,
dc.description.referencesYatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, I. Formalized Mathematics, 5(2):167–172,
dc.description.referencesBeata Padlewska. Locally connected spaces. Formalized Mathematics, 2(1):93–96,
dc.description.referencesBeata Padlewska. Families of sets. Formalized Mathematics, 1(1):147–152,
dc.description.referencesBeata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230,
dc.description.referencesAlexander Yu. Shibakov and Andrzej Trybulec. The Cantor set. Formalized Mathematics, 5(2):233–236,
dc.description.referencesAndrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics, 11(4): 341–347,
dc.description.referencesAndrzej Trybulec. Moore-Smith convergence. Formalized Mathematics, 6(2):213–225,
dc.description.referencesMichał J. Trybulec. Integers. Formalized Mathematics, 1(3):501–505,
dc.description.referencesWojciech A. Trybulec and Grzegorz Bancerek. Kuratowski – Zorn lemma. Formalized Mathematics, 1(2):387–393,
dc.description.referencesZinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71,
dc.description.referencesJosef Urban. Basic facts about inaccessible and measurable cardinals. Formalized Mathematics, 9(2):323–329,
dc.description.referencesClaude Wagschal. Topologie et analyse fonctionnelle. Hermann,
dc.description.referencesEdmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73–83,
dc.description.referencesEdmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186,
dc.description.referencesStanisław Żukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215–222,
Występuje w kolekcji(ach):Formalized Mathematics, 2015, Volume 23, Issue 4

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma-2015-0023.pdf267,36 kBAdobe PDFOtwórz
Pokaż uproszczony widok rekordu Zobacz statystyki

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